segfault on inductive type with binder starting with `_`

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

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

Run the self-contained Lean reproducer from the issue and confirm that #check s.bar segfaults. Trace the handling of inductive types with a single constructor, underscore-prefixed fields, Pi-types, and dot notation; done means the check reports s.bar : ℕ without crashing.