segfault with broken code (accessing H.0 if H : comm_ring R)

[kbuzzard]

Prerequisites

• [X ] Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
    • Specifically, check out the wishlist, open RFCs,
      or feature requests.
  • Reduced the issue to a self-contained, reproducible test case.

Description

Lean segfaults when trying to make sense of some meaningless code.

Steps to Reproduce

Running Lean on a file which just has one line:

def X (R : Type) [H : comm_ring R] := H.0

reliably produces a segfault for me.

buzzard@ebony:~$ cat > test.lean
def X (R : Type) [H : comm_ring R] := H.0
buzzard@ebony:~$ lean test.lean
Segmentation fault (core dumped)

Expected behavior: [What you expect to happen]

Some error

Actual behavior: [What actually happens]

SIGSEGV

Reproduces how often: [What percentage of the time does it reproduce?]

100 percent

Versions

buzzard@ebony:~$ lean --version
Lean (version 3.3.1, commit 6e02ce9b345b, Release)
buzzard@ebony:~$ lean --githash
6e02ce9b345bc9263272668ead709d3d24c2a1fa
buzzard@ebony:~$ uname -a
Linux ebony 4.10.0-42-generic #46~16.04.1-Ubuntu SMP Mon Dec 4 15:57:59 UTC 2017 x86_64 x86_64 x86_64 GNU/Linux
buzzard@ebony:~$ more /etc/lsb-release 
DISTRIB_ID=Ubuntu
DISTRIB_RELEASE=16.04
DISTRIB_CODENAME=xenial
DISTRIB_DESCRIPTION="Ubuntu 16.04.3 LTS"
buzzard@ebony:~$ 

Additional Information

Reports on gitter that the issue is also there on Windows and Mac