Deriving curiosty

Stream: lean4

[Mac]

Why is it possible to derive BEq and Repr for this type:

structure Foo (t) where
  f1 : t
  f2 : Array t
  deriving BEq, Repr

But not possible for this one:

structure Bar (t) where
  f1 : t
  deriving BEq, Repr
/-
failed to synthesize instance
  BEq t✝
failed to synthesize instance
  Repr t✝
-/

[Kevin Buzzard]

Is it to do with the fact that Array prevents t : Prop (and BEq expects t : Type _)?

structure Foo (t : Type _) where
  f1 : t
  deriving BEq, Repr -- works