segfault on inductive type with binder starting with `_`

[rwbarton]

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

If you create an inductive type with one constructor containing a field starting with an underscore, and then later use . notation, Lean will segfault.

Steps to Reproduce

inductive S
| mk : Π (_foo : nat → int), S

namespace S
def bar (s : S) : nat := 0

variable s : S
#check s.bar

end S

Expected behavior: s.bar : ℕ

Actual behavior: Lean segfaults

Reproduces how often: 100%

Essential features:

• the field _foo has a name starting with an underscore
• the inductive type has exactly one constructor
• the type of _foo is a Pi-type

Lean thinks that S is a structure and _foo is a field containing a parent structure ("subobject") foo.

Versions

Lean (version 3.18.4, commit f539be1e867c, Release) linux

[rwbarton]

The crash is in is_subobject_field of src/frontends/lean/structure_cmd.cpp. Lean apparently thinks S is a structure which extends foo and then gets confused.

[rwbarton]

By the way, Lean won't let you name a structure field with something starting with an underscore, but using inductive as above bypasses this check.