segfault in badly typed pattern match

[robertylewis]

This was found in class today by Joseph Rotella:

def f : ∀ (α : Type), list α → unit
| α [] := ()
| α ((y::ys)::xs) := ()

crashes the server. I don't have a debug version of Lean handy to see if/where there are assertion violations.

Prerequisites

• [ ] 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

[Description of the issue]

Steps to Reproduce

1. [First Step]
2. [Second Step]
3. [and so on...]

Expected behavior: [What you expect to happen]

Actual behavior: [What actually happens]

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

Versions

Replicated in 3.30 and 3.33.

Additional Information

Any additional information, configuration or data that might be necessary to reproduce the issue.