dependent match elimination failed, inaccessible pattern

Stream: new members

[pandaman]

Hi. A friend of mine is trying to define an AVL tree with dependent types as follows, but faced a strange error when writing a dependent pattern matching. For some reason, the match succeeded when we explicitly listed the constructor arguments. Can someone explain why the original version failed with pattern matching?

inductive Balance: Nat -> Nat -> Nat -> Type where
  | lefty : Balance n.succ n.succ.succ n
  | mid   : Balance n      n.succ      n
  | righty: Balance n      n.succ.succ n.succ

inductive Tree (a: Type u): Nat -> Type u where
  | leaf: Tree a 0
  | node: Balance l n r -> Tree a l -> a -> Tree a r-> Tree a n

/-
Fails with:

dependent match elimination failed, inaccessible pattern found
  .(n✝)
constructor expected
-/
def rotateL (l: Tree a n) (v: a) (r: Tree a n.succ.succ): (Tree a n.succ.succ) ⊕ (Tree a n.succ.succ.succ) :=
  match r with
  | .node .lefty  (.node .lefty  rll rlv rlr) rv rr => sorry
  | .node .lefty  (.node .mid    rll rlv rlr) rv rr => sorry
  | .node .lefty  (.node .righty rll rlv rlr) rv rr => sorry
  | .node .mid    rl rv rr => sorry
  | .node .righty rl rv rr => sorry

def rotateL' (l: Tree a n) (v: a) (r: Tree a n.succ.succ): (Tree a n.succ.succ) ⊕ (Tree a n.succ.succ.succ) :=
  match r with
  | .node (l := _) (n := _) (r := _) .lefty  (.node (l := _) (n := _) (r := _) .lefty  rll rlv rlr) rv rr => sorry
  | .node (l := _) (n := _) (r := _) .lefty  (.node (l := _) (n := _) (r := _) .mid    rll rlv rlr) rv rr => sorry
  | .node (l := _) (n := _) (r := _) .lefty  (.node (l := _) (n := _) (r := _) .righty rll rlv rlr) rv rr => sorry
  | .node (l := _) (n := _) (r := _) .mid    rl rv rr => sorry
  | .node (l := _) (n := _) (r := _) .righty rl rv rr => sorry