Ways to (refine? is it?) type variables to concrete types in Idris? For a dependently typed HOAS Zipper

Question

I have the following:

data Expr : Type -> Type where
  Lift : a -> Expr a
  Add  : Num a => Expr a -> Expr a -> Expr a
  And  : Expr Bool -> Expr Bool -> Expr Bool
  Cnst : Expr a -> Expr b -> Expr a

data Context : Type -> Type where
  Root : Context ()
  L    : Expr w -> Context x -> Expr y -> Expr z -> Context w
  R    : Expr w -> Context x -> Expr y -> Expr z -> Context w 
  M    : Expr w -> Context x -> Expr y -> Expr z -> Context w 

data Zipper : Type -> Type -> Type where
  Z : Expr f -> Context g -> Zipper f g
  E : String -> Context g -> Zipper String ()



total
ZipUp : Zipper focus parent -> Type
ZipUp (Z e (R (And e1 e2) {x} c t u))      = Zipper Bool x
ZipUp (Z e (L (And e1 e2) {x} c t u))      = Zipper Bool x
ZipUp (Z e (R (Cnst {a} e1 e2) {x} c t u)) = Zipper a x
ZipUp (Z {f} e (L (Cnst l r) {x} c t u))   = Zipper f x
ZipUp (Z e (R (Add {a} e1 e2) {x} c t u))  = Zipper a x
ZipUp (Z {f} e (L (Add e1 e2) {x} c t u))  = Zipper f x
ZipUp _                                    = Zipper String ()

up : (x : Zipper focus parent) -> ZipUp x
up (Z e (R (And l r) c x y))  = Z (And l e) c
up (Z e (R (And l r) c x y))  = Z (And e r) c
up (Z {f = b} e (R (Cnst l {b} r) c x y)) = Z (Cnst l e) c
up (Z {f = a} e (L (Cnst l {a} r) c x y)) = Z (Cnst e r) c
up (Z {f = a} e (R (Add {a} l r) c x y))  = Z (Add l e) c
up (Z {f = a} e (L (Add {a} l r) c x y))  = Z (Add e r) c
up (Z e (R (Lift x) c l r))   = E "Some error" c
up (Z e (L (Lift x) c l r))   = E "Some error" c
up (E s c)                    = E s c

This does not type check for the And cases of up because Idris cannot match Zipper f g with Zipper Bool g My question is, how can I get this to work so that i can rebuild up one level in the tree when my expressions have children of concrete types? I think I need to refine the types in some way, but I can't really see how making a new dependent-type (or GADT) would help with this (and I don't know any other way to refine types!)

I've looked into views and proofs, but after trying my best for a few weeks now, I can't seem to find a way to write the problem to say the following The focus of the zipper has the same type as the right child of the context's parent expression, if the context was constructed with R. The same is true for the focus and the context's left child, if the context was constructed with L.

I've tried increasing the type parameters, so that each expression carries the types of its children Expr a l m r but I end up with the same error, even though I can write a new version of R : Expr r t u v -> Expr a l m r -> Expr m h i j -> Expr r x y z -> Context -> Context to capture this relationship. In the end I need a way to tell Idris that some parametric a is really Bool under a certain pattern match!

I'm extremely stuck, so any advice would be very much appreciated!

Kind regards, Donovan

gallais gallais · Accepted Answer · 2018-02-09T16:21:14

Surely these constructors' types are not precise enough: there is no link between w, x, y, and z.

L    : Expr w -> Context x -> Expr y -> Expr z -> Context w
R    : Expr w -> Context x -> Expr y -> Expr z -> Context w 
M    : Expr w -> Context x -> Expr y -> Expr z -> Context w

Ways to (refine? is it?) type variables to concrete types in Idris? For a dependently typed HOAS Zipper

1 Answers