Typeclass parameters are not instantiated by match

Stream: new members

[Moritz R]

In my (reduced) example, i would expect the p in pvalid to be instantiated as .child ...
Why is this not happening?

inductive Position : Type where
  | full : Position
  | child (i : ℕ) (p : Position) : Position

def valid : Position → Nat → Prop
| _, _ => True

class Valid (p : Position) (t : Nat) where
  isValid : valid p t

def subtermAt (t : Nat) (p : Position) [pvalid : Valid p t] : Nat :=
  match p, t with
  | .full, t => t
  | .child i p', x => by -- here no instantiation happens

If instead of [pvalid : Valid p t] i use (pvalid : Position.valid p t) it gets instantiated as expected.
Same for the first case in the match, but with .full

[Aaron Liu]

try adding pvalid as an explicit match discriminant

[Aaron Liu]

don't know why this happens (does it have to do with the binderinfo?) but there is a workaround