instance binders in structure

Stream: lean4

[Jovan Gerbscheid]

While working on lean#10178, I noticed that structure doesn't verify that instance implicit binders are indeed binding a class, which I think is a bug:

structure A (n : Nat) where
  x : Nat
structure B (n : Nat) where
  y : Nat

structure C (n : Nat) where
  [toA : A n]
  [toB : B n]

#check C.mk -- C.mk {n : Nat} [toA : A n] [toB : B n] : C n