Segfault during type checking

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

Lean segfaults when type checking rather than giving a proper error.

Steps to Reproduce

inductive convex_hull : set α
| intrv (v₁ ∈ convex_hull) : convex_hull v₁

Expected behavior: A proper error about neither α nor set being known identifiers, or if they're in the context, acceptance.

Actual behavior: Lean segfaults with no output. For some people, a very similar example was producing many "unreachable code" errors, but I wasn't getting them on my particular setup.

The alternative version:

inductive convex_hull (s : set α) : set α
| of_set : ∀ v ∈ s, convex_hull v
| intrv (v₁ v₂ ∈ convex_hull) : convex_hull v₁

Reproduces how often: 100% (for me)

Versions

Lean (version 3.18.4, commit f539be1e867c, Release)
Windows 10

Additional Information

A segfault with no output occurs with both of the examples given on my machine, but some people who tried it in the zulip had unreachable code errors. One member had Lean continue working fine for the second example despite still giving unreachable code errors, though I couldn't reproduce.

Reproduce both inductive examples with Lean 3.18.4 on the reported setup, starting from the type-checking path mentioned in the issue. Done means neither example segfaults or emits unreachable-code failures, and invalid identifiers produce proper errors while valid contextual identifiers are accepted.