bug with default structure values?

Stream: lean4

[Scott Kovach]

structure Foo where
  t : Type
  fn : t → t

structure Bar extends Foo where
  fn := fun x => x
  --fn := id -- using this line, example below works

example : Bar where -- fields missing: 'fn'
  t := Unit

this seems to only happen when the default field involves a type t that is a field of Foo.
I tested on 4.5 and 4.6

[Kyle Miller]

I haven't confirmed this yet, but it's possible that the issue is that docs#Lean.Elab.Term.StructInst.DefaultFields.reduce doesn't look at the types of the arguments to a fun when processing.

A workaround is to define the default value as a separate declaration:

structure Foo where
  t : Type
  fn : t → t

abbrev defFun (t : Type) := fun (x : t) => x

structure Bar extends Foo where
  fn := defFun t