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

It's almost like the 2nd call to right happens -before- the ZipRight type-level function gets evaluated. If this is what's happening, does anyone out there know a way of fixing it? — Donovan
Ugh, so it does! Would you like to make it an answer so I can accept it? — Donovan
I'd rather someone else come tell us both why the original error occurs. Glad that helped though! — Thomas M. DuBuisson
I don't know what's going on exactly, but I suspect that the problem may be that the typechecker is shy about evaluating programs which have not been checked total. — pigworker

Donovan Donovan · Accepted Answer · 2018-01-27T23:07:04

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

Idris - Type errors in dependently typed functions

1 Answers