How do I trace inferred inaccessible pattern?

Stream: general

[nrs]

Am trying to figure out what pattern was inferred at the .(_) in the very last line of the code block below. Is there any way I can trace what was inferred?

structure Container where
  shape : Type _
  positions : shape -> Type _

inductive ExtensionOf : Container -> Type _ -> Type _
  | apply : (c : Container) -> (α : Type _) -> (s : c.shape) -> (c.positions s -> α) -> ExtensionOf c α

inductive WType (c : Container)
  | sup : ExtensionOf c (WType c) -> WType c

def FAlg (c : Container) (α : Type) := ExtensionOf c α -> α

def cata (alg : FAlg c α) : WType c -> α
  | .sup ext => match ext with
    | .apply .(c) .(_) s f => alg _

[Mario Carneiro]

you can actually see it in the result of #print:

def cata.{u_1, u_2} : {c : Container} → {α : Type} → FAlg c α → WType c → α :=
fun {c} {α} alg x ↦
  match x with
  | WType.sup ext =>
    match ext with
    | ExtensionOf.apply .(c) .(WType c) s f => alg (sorryAx (ExtensionOf c α))

[nrs]

ah very cool! thanks a lot for the help!!