why can't lean infer this vector's length?

Stream: new members

[Alok Singh]

structure DenseStorage (α : Type u) where
  coeffs {degree : Nat} : Vector α (degree + 1)

/- don't know how to synthesize implicit argument 'degree'
  @coeffs α s (?m.729 s)
context:

α : Type u_1
s : DenseStorage α
⊢ Nat
-/
def DenseStorage.degree (s : DenseStorage α) : Nat :=
  let deg := s.coeffs.size - 1
  deg

The error message I get is confusing, and even casting toArray doesn't help. isn't the length of the vector known, so once i have an instance of DenseStorage, I should have a vector I can find the length of?

[suhr]

DenseStorage.coeffs is a function that takes Nat as an implicit argument. Maybe you need something like this instead?

structure DenseStorage (α : Type u) where
  degree : Nat
  coeffs : Vector α (degree + 1)