Idris - Can I express that two type parameters are equal in a pattern match?

Question

Lets say I have the following

data Expr : Type -> Type where
  Lift : a -> Expr a
  Add  : Num a => Expr a -> Expr a -> Expr a
  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 ()

I would like to write a function to rebuild a Zipper if I'm going up one level in the expression tree. Something like:

total
ZipUp : Zipper focus parent -> Type
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 ()

the problem comes when I want to write the function to return a ZipUp

up : (x : Zipper focus parent) -> ZipUp x
up (Z e (R (Cnst l r) c x y)) = Z (Cnst l e) c
up (Z e (L (Cnst l r) c x y)) = Z (Cnst e r) c
up (Z e (R (Add l r) c x y))  = Z (Add l e) c
up (Z e (L (Add 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 fails to typecheck on the Add case, because it can't infer that focus (type of e) matches with parent (expected type)

So my question has two parts then.

What can I do to express this relationship? (that if the Zipper is an R constructed, e has the same type as r, or that e has the same type as l in the L constructed case. I've tried using {e = l} and other variants of this, but to no avail.)

The the code typechecks and runs if I comment out the last for lines of up to finish with:

up : (x : Zipper focus parent) -> ZipUp x
up (Z e (R (Cnst l r) c x y)) = Z (Cnst l e) c
up (Z e (L (Cnst l r) c x y)) = Z (Cnst e r) c

but the actual manipulation of the types should be the same in the Add case, yet this fails to typecheck, why is that?

Thanks for taking the time to read and/or answer!

Answer 1

This fails to typecheck on the Add case, because it can't infer that focus (type of e) matches with parent (expected type)

Because this is not always the case, e.g.

*main> :t Z (Lift "a") (R (Add (Lift 1) (Lift 2)) Root (Lift 4) (Lift 8))
Z (Lift "a") (R (Add (Lift 1) (Lift 2)) Root (Lift 4) (Lift 8)) : Zipper String Integer

And Add (Lift 1) (Lift "a") doesn't work because of the Num a constraint.

What can I do to express this relationship?

If you want to express the relationship within up: You have e : Expr f and can say that the same f should be used in the Add case:

up (Z {f} e (R (Add l r {a=f}) c x y)) = Z (Add l e) c
up (Z {f} e (L (Add l r {a=f}) c x y)) = Z (Add e r) c
up (Z e (R (Add l r) c x y)) = ?whattodo_1
up (Z e (L (Add l r) c x y)) = ?whattodo_2

Now you have a non total function because of the cases where a != f. I don't quite what you want to do, so I can't offer an option. :-)

If you want to express the relationship in Zipper you could do (very roughly) something like:

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

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

Now you construct a proof when building up a zipper that f = g in a R-Context. Again, I cannot be specific, but I hope it helps in some way.