Univerally quantified type class expression

Stream: lean4

[Alex Keizer]

I'm working with vectors of things, implemented as maps from a finite index typed, i.e.,

/-- An alternate definition of `fin n` defined as an inductive type instead of a subtype of `Nat`. -/
inductive Fin2 : Nat → Type
  | /-- `0` as a member of `fin (succ n)` (`fin 0` is empty) -/
  fz {n : Nat} : Fin2 (n.succ)
  | /-- `n` as a member of `fin (succ n)` -/
  fs {n : Nat} : Fin2 n → Fin2 (n.succ)
  deriving DecidableEq

abbrev TypeVec (n : Nat) := Fin2 n → (Type _)

Now I want to require that all elements of such a vector implement a typeclass, say Inhabited for a vector of types. Since there are finitely many element in any vector, I want this assumption to be inferred.

-- The compiler accepts a quantified type class
example (v : TypeVec n) [∀i, Inhabited (v i)] :
  True := by sorry

However, I cannot seem to provide instances for such a quantified statement.
The instances are accepted just fine, but inference does not find them

section
  abbrev VecClass' (v : TypeVec n) :=
  ∀ i, Inhabited (v i)

  instance VecInhabited_nil' (v : TypeVec 0) : ∀ i, Inhabited (v i)
    := by intro i; cases i

  instance VecClass_succ'  (v : TypeVec (.succ n))
                              [zero : Inhabited (v .fz)]
                              [succ : VecClass' (fun i => v (.fs i))] :
                          ∀ i, Inhabited (v i) :=
  by intro i;
      cases i;
      exact zero;
      apply succ
end

/-- The vector `![Nat, Int]` -/
abbrev v₂ : TypeVec 2
  | .fz     => Nat
  | .fs .fz => Int

-- This fails
example : VecClass' v₂ :=
  by infer_instance

If I take the same idea, but instead box ∀ i, Inhabited (v i) in a new type class, everything works as expected.

section
  /-- A custom type class to express that all elements of `v` implement `Inhabited` -/
  class VecClass (v : TypeVec n) where
    prop : ∀ i, Inhabited (v i)


  instance VecClass_nil (v : TypeVec 0) : VecClass v
    := ⟨by intro i; cases i⟩

  instance VecClass_succ  (v : TypeVec (.succ n))
                              [zero : Inhabited (v .fz)]
                              [succ : VecClass (fun i => v i.fs)] :
                          VecClass v :=
  ⟨by intro i;
      cases i;
      exact zero;
      apply succ.prop
    ⟩
end

-- succeeds
example : VecClass v₂ :=
  by infer_instance

Oddly enough, I can provide an instance for the abbrev version if I defer directly to the boxed version.

section
  instance instUnbox [box : VecClass v] : VecClass' v
   := box.prop

  -- Now it works for the abbreviation as well
  example : VecClass' v₂ :=
    by infer_instance
end

So my direct issue is solved, but I am quite surprised that I need the boxed version. Does anybody have an idea as to what is going on?