(kernel) invalid projection

Stream: lean4

[Adrien Champion]

I've got this error and I'm not sure what to do. Basically, the problem happens when I rewrite a structure-type using a type-level equality and try to access a field

class Flags (α : Type) where
  toType : α → Type
  consume : (a : α) → (toType a → Unit) → Unit

structure Person where
  name : String
  email : String

class Person.FlagsEq (α : Type) [I : Flags α] where
  flag : α
  flag_spec : I.toType flag = Person

--  vvvvv~~~~~ (kernel) invalid projection `p.1`
def test₂
  [I : Flags α]
  [IEq : Person.FlagsEq α]
:=
  I.consume IEq.flag fun p =>
    let p : Person := IEq.flag_spec ▸ p
    let name := p.name
    ()

[Adrien Champion]

Removing the p.name line yields no error (just the unused var warning)

class Flags (α : Type) where
  toType : α → Type
  consume : (a : α) → (toType a → Unit) → Unit

structure Person where
  name : String
  email : String

class Person.FlagsEq (α : Type) [I : Flags α] where
  flag : α
  flag_spec : I.toType flag = Person

def test₂
  [I : Flags α]
  [IEq : Person.FlagsEq α]
:=
  I.consume IEq.flag fun p =>
    let p : Person := IEq.flag_spec ▸ p
    -- let name := p.name
    ()

[Max Nowak 🐉]

Removing p.name probably yields no error since p is unused and gets removed entirely (is my guess, don't quote me on that, I had similar things happen).

[Kyle Miller]

I checked that it's got nothing to do with name shadowing. This causes the same error too:

def test₂
  [I : Flags α]
  [IEq : Person.FlagsEq α]
:=
  I.consume IEq.flag fun p =>
    let q : Person := IEq.flag_spec ▸ p
    let name := q.name
    ()

[Kyle Miller]

It seems possible that there is a kernel bug with how projections are reduced? This sidesteps the issue:

def Person_name (p : Person) : String := p.name

--  vvvvv~~~~~ (kernel) invalid projection `p.1`
def test₂
  [I : Flags α]
  [IEq : Person.FlagsEq α]
:=
  I.consume IEq.flag fun p =>
    let q : Person := IEq.flag_spec ▸ p
    let name := Person_name q
    ()

[Kyle Miller]

Even with renaming p -> q, you get (kernel) invalid projection p.1 (with p, not q). If you mouse over p, you see it thinks it has type Flags.toType Person.FlagsEq.flag, which explains why it thinks its an invalid projection at this point.

[Adrien Champion]

I did notice that as well, it seems the rewrite makes type-checking go through but after that the kernel somehow still works with the pre-rewrite datatype

[Kyle Miller]

If I were to guess, it looks like the kernel is reducing IEq.flag_spec ▸ p to p (or in that last example, IEq.flag_spec ▸ q to p) before trying to take the projection