functional-programming - Idrisの具体的な型に変数を入力する方法は? 依存型の HOAS Zipper の場合

Question

私は次のものを持っています：

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 

Idris が一致できないため、これは型チェックを行いません私の質問は、式に具象型の子がある場合に、ツリー内の 1 レベルを再構築できるようにするにはどうすればよいですかAnd? なんらかの方法で型を改良する必要があると思いますが、新しい従属型 (または GADT) を作成することがこれにどのように役立つか実際にはわかりません (そして、型を改良する他の方法を知りません!)upZipper f gZipper Bool g

私は意見と証明を調べましたが、数週間最善を尽くした後、問題を次のように書く方法を見つけることができないようです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.

各式がその子の型を保持するように型パラメーターを増やしてみましたが、この関係をキャプチャするExpr a l m rために新しいバージョンを作成できても、同じエラーが発生します。最後に、いくつかのパラメトリックが実際に特定のパターン マッチの下にあるR : Expr r t u v -> Expr a l m r -> Expr m h i j -> Expr r x y z -> Context -> Contextことを Idris に伝える方法が必要です!aBool

私は非常に立ち往生しているので、アドバイスをいただければ幸いです！

よろしく、ドノバン