Dependent Types not fully evaluating?

DepZipTestIdris2.idr

%default total 
data Term : Type -> Type where
  Const : {a : Type} -> a -> Term a
  Pair : {a : Type} -> {b : Type} -> Term a -> Term b -> Term (a, b)
  App : {a : Type} -> {b : Type} -> Term (a -> b) -> Term a -> Term b

GoLeft : {a : Type} -> Term a -> Maybe Type
GoLeft (Const x) = Nothing
GoLeft (Pair {a} x y) = Just a
GoLeft (App {a} {b} f x) = Just (a -> b)

GoRight : {a : Type} -> Term a -> Maybe Type
GoRight (Const x) = Nothing
GoRight (Pair x {b} y) = Just b
GoRight (App {a} f x) = Just a


data Context : Maybe Type -> Type where
  Root : {a : Type} -> Context (Just a)
  L : {a : Type} -> (x : Term a) -> Context (Just a) -> Context (GoLeft x)
  R : {a : Type} -> (x : Term a) -> Context (Just a) -> Context (GoRight x)

data Zipper : Type -> Type where
  Zip : {a : Type} -> Term a -> Context (Just a) -> Zipper a
  Fail : Zipper Void


left : (a : Type ** Zipper a) -> (b : Type ** Zipper b)
left (ty ** (Zip (Const x) ctx)) = (Void ** Fail)
left ((a, b) ** (Zip (Pair x y) ctx)) = (a ** Zip x (L (Pair x y) ctx))
left (b ** (Zip (App {a} f x) ctx)) = (a -> b ** Zip f (L (App f x) ctx))
left (Void ** Fail) = (Void ** Fail)

right : (a : Type ** Zipper a) -> (b : Type ** Zipper b)
right (ty ** (Zip (Const x) ctx)) = (Void ** Fail)
right ((a, b) ** (Zip (Pair x y) ctx)) = (b ** Zip y (R (Pair x y) ctx))
right (_ ** (Zip (App {a} f x) ctx)) = (a ** Zip x (R (App f x) ctx))
right (Void ** Fail) = (Void ** Fail)

{-
Can't solve constraint between:
	GoLeft (App f x)
and
	Just (a -> b)
at:
31	left (b ** (Zip (App {a} f x) ctx)) = (a -> b ** Zip f (R (App f x) ctx))

Can't solve constraint between:
	GoRight (App f x)
and
	Just a
at:
37	right (_ ** (Zip (App {a} f x) ctx)) = (a ** Zip x (R (App f x) ctx))
-}