Idris - Type errors in dependently typed functions

Question

I'm having a problem with unexpected type errors in Idris when I try to use my dependently-typed functions in the REPL. Here's what I have:

data Expr : Type -> Type where
  Null     : Expr ()
  Lift     : Show a => a -> Expr a
  Add      : Num a => Expr a -> Expr a -> Expr a
  Mul      : Num a => Expr a -> Expr a -> Expr a

data Context : Type where
  Root  : Context
  Error : String -> Context
  L     : Expr a -> Context -> Expr b -> Expr c -> Context
  R     : Expr a -> Context -> Expr b -> Expr c -> Context
  M     : Expr a -> Context -> Expr b -> Expr c -> Context

data Zipper : Type -> Type where
  Z : Expr a -> Context -> Zipper a
  E : String -> Context -> Zipper String

UnZip : Zipper b -> Type
UnZip (Z {a} e c) = Expr a
UnZip (E x c)     = String

unZip : (x : Zipper a) -> UnZip x
unZip (Z e c) = e
unZip (E x c) = x

total
ZipRight : Zipper a -> Type
ZipRight (Z (Add {a} l r) c)            = Zipper a
ZipRight (Z (Mul {a} l r) c)            = Zipper a
ZipRight _                              = Zipper String

err : String
err = "Some Error"

total
right : (x : Zipper a) -> ZipRight x
right (Z Null c)                     = E err c
right (Z (Lift _) c)                 = E err c
right (Z (Add l r) c)                = Z r (R (Add l r) c Null l)
right (Z (Mul l r) c)                = Z r (R (Mul l r) c Null l)

when I go to run the following in the REPL unZip $ right $ Z (Add (Lift 2) (Mul (Lift 3) (Lift 4))) Root I get the expected Expr Integer.

when I add an additional right to the line in unZip $ right $ right $ Z (Add (Lift 2) (Mul (Lift 3) (Lift 4))) Root I get a type error between ZipRight (right (Z (Add (Lift 2) (Sub (Lift 4) (Lift 5))) Root)) (Type of right (right (Z (Add (Lift 2) (Sub (Lift 4) (Lift 5))) Root))) and Zipper a (Expected Type)

however running right $ right $ Z (Add (Lift 2) (Mul (Lift 3) (Lift 4))) Root shows the expected Zipper Integer.

What I would like to know is. Why am I getting a type error with the 2nd call to right and is there a way I can fix my code so that either, the error will no longer occur, or that I can refactor in such a way that the problem is circumvented?

Kind regards,

Donovan

Answer 1

Making the function total fixes the problem. As to why the problem occurs in the first place, I'm still in the dark!