Weird totality errors with dependent pairs on proofs of functions?

CantGoLeft.idr

module CantGoLeft

%default total

data Expr : Type -> Type where
  Val : {a : Type} -> a -> Expr a
  Add : {a : Type} -> Num a => Expr a -> Expr a -> Expr a
  App : {a, b : Type} -> Expr (a -> b) -> Expr a -> Expr b
  Lam : {a, b : Type} -> (a -> Expr b) -> Expr (a -> b)

GoRight : Expr a -> Maybe Type
GoRight (Val {a} x) = Nothing
GoRight (Add {a} x y) = Just a
GoRight (App {a} f x) = Just a
GoRight (Lam {a, b} f) = Nothing

GoLeft : Expr a -> Maybe Type
GoLeft (Val {a} x) = Nothing
GoLeft (Add {a} x y) = Just a
GoLeft (App {a, b} f x) = Just (a -> b)
GoLeft (Lam {a, b} f) = Nothing

GoDown : Expr a -> Maybe Type
GoDown (Val {a} x) = Nothing
GoDown (Add {a} x y) = Nothing
GoDown (App {a, b} f x) = Nothing
GoDown (Lam {a, b} f) = Nothing

data TreeContext : Maybe Type -> Type where
  Root : TreeContext a
  L : {a : Type} -> (x : Expr a) -> TreeContext (Just a) -> TreeContext (GoLeft x)
  R : {a : Type} -> (x : Expr a) -> TreeContext (Just a) -> TreeContext (GoRight x)
  D : {a : Type} -> (x : Expr a) -> TreeContext (Just a) -> TreeContext (GoDown x)

data Focus : Type -> Type where
  MkFocus : {a : Type} -> Expr a -> TreeContext (Just a) -> Focus a

 
-- Why is this not covering, is it the implicit `{ty = Type}`?
-- Am I mixing up Type as a Type and Type as a Term?
{-
left : (a : Type ** Focus a) -> (b : Type ** Focus b)
left (ty ** focus) = 
  case focus of
    (MkFocus (Val x) ctx) => ?t1
    (MkFocus (Add x y) ctx) => ?t2
    (MkFocus (App x y) ctx) => ?t3
    (MkFocus (Lam f) ctx) => ?t4
-}


-- Why is this pattern match not working?
-- We have holes for 'a' and 'b' in the 'Lam' case but
-- attempting to assign them is not helping.
{-
left : (a : Type ** Focus a) -> (b : Type ** Focus b)
left (ty ** (MkFocus (Val x) ctx)) = ?look_1
left (ty ** (MkFocus (Add x y) ctx)) = ?look_2
left (ty ** (MkFocus (App x y) ctx)) = ?look_3
left (ty ** (MkFocus (Lam f) ctx)) = ?look_4
-}