Idris：模式匹配中如何表达类型参数相等及Add案例报错原因

让我们一步步拆解你的问题，先解决核心的类型关系表达，再解释Cnst和Add案例的差异。

1. 如何表达Context与子节点的类型关系？ #

你的Context构造函数目前没有明确关联当前focus的类型和父节点中对应子位置的类型，这是Idris无法推断Add案例类型匹配的根本原因。我们可以通过两种方式修复这个问题：

方式一：为不同父节点操作定义专用Context构造器 #

最直接的方式是针对Add和Cnst分别定义Context的左/右子节点构造器，把类型约束直接嵌入构造器中：

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

-- 重新定义Context，明确每个构造器对应的父节点操作和类型约束
data Context : Type -> Type where
  Root : Context ()
  -- 当前在Add的左子节点：保存右子节点（Expr a）和上层上下文，focus类型为a
  LAdd : Num a => Expr a -> Context x -> Context a
  -- 当前在Add的右子节点：保存左子节点（Expr a）和上层上下文，focus类型为a
  RAdd : Num a => Expr a -> Context x -> Context a
  -- 当前在Cnst的左子节点：保存右子节点（Expr b）和上层上下文，focus类型为a
  LCnst : Expr b -> Context x -> Context a
  -- 当前在Cnst的右子节点：保存左子节点（Expr a）和上层上下文，focus类型为b
  RCnst : Expr a -> Context x -> Context b
  -- 保留原M构造器（根据你的需求调整）
  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 ()

-- 简化ZipUp类型族，直接根据Context构造器推断返回类型
total ZipUp : Zipper focus parent -> Type
ZipUp (Z e (RAdd _ c)) = Zipper _ (typeof c)
ZipUp (Z e (LAdd _ c)) = Zipper _ (typeof c)
ZipUp (Z e (RCnst _ c)) = Zipper _ (typeof c)
ZipUp (Z e (LCnst _ c)) = Zipper _ (typeof c)
ZipUp _ = Zipper String ()

-- 辅助函数：提取Context的类型参数
typeof : Context a -> Type
typeof {a} _ = a

up : (x : Zipper focus parent) -> ZipUp x
up (Z e (RAdd left c)) = Z (Add left e) c  -- left和e都是Expr a，符合Add的约束
up (Z e (LAdd right c)) = Z (Add e right) c
up (Z e (RCnst left c)) = Z (Cnst left e) c  -- left是Expr a，e是Expr b，符合Cnst的约束
up (Z e (LCnst right c)) = Z (Cnst e right) 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可以直接推断出所有类型匹配，不需要额外的证明。

方式二：使用依赖类型证明统一构造器 #

如果你想保留通用的L/R构造器，可以通过类型族和证明来关联focus类型与父节点子位置的类型：

-- 定义子节点位置
data ChildPos = LeftChild | RightChild

-- 类型族：给定Expr和子节点位置，返回该子节点的类型
ChildType : Expr p -> ChildPos -> Type
ChildType (Add {a} _ _) LeftChild = a
ChildType (Add {a} _ _) RightChild = a
ChildType (Cnst {a} {b} _ _) LeftChild = a
ChildType (Cnst {a} {b} _ _) RightChild = b
ChildType (Lift _) _ = Void  -- Lift没有子节点，用Void标记无效位置

data Context : Type -> Type where
  Root : Context ()
  -- 通用子节点构造器：携带位置、父节点、focus类型与子位置类型相等的证明
  Child : (pos : ChildPos) -> (op : Expr p) -> (prf : f = ChildType op pos) -> Context x -> Context f

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

-- 更新ZipUp，根据证明推断返回类型
total ZipUp : Zipper focus parent -> Type
ZipUp (Z e (Child pos op prf c)) = Zipper (typeof op) (typeof c)
ZipUp _ = Zipper String ()

up : (x : Zipper focus parent) -> ZipUp x
up (Z e (Child RightChild (Add l _) Refl c)) = Z (Add l e) c
up (Z e (Child LeftChild (Add _ r) Refl c)) = Z (Add e r) c
up (Z e (Child RightChild (Cnst l _) Refl c)) = Z (Cnst l e) c
up (Z e (Child LeftChild (Cnst _ r) Refl c)) = Z (Cnst e r) c
up (Z e (Child _ (Lift x) _ c)) = E "Cannot up from Lift" c
up (E s c) = E s c

这里Refl是类型相等的证明，Idris会自动验证focus类型与父节点子位置类型一致，确保up函数的类型安全。

2. 为什么Cnst案例能通过，Add案例不行？ #

这完全是由两个构造器的类型签名差异导致的：

• Cnst的类型签名：Cnst : Expr a -> Expr b -> Expr a
  它允许左右子节点的类型不同（左是a，右是b），父节点的类型是a。当你在up中构造Cnst l e时，Idris只需要e的类型是b（与原右子节点类型一致），而这个约束可以从Cnst的类型签名直接推断出来——因为l的类型是a，所以第二个参数必须是Expr b。即使你的Context没有明确关联类型，Idris也能自动推导e的类型匹配。

• Add的类型签名：Add : Num a => Expr a -> Expr a -> Expr a
  它要求左右子节点的类型必须相同（都是a），父节点的类型也是a。当你构造Add l e时，Idris需要e的类型等于l的类型a，但你的原Context构造器没有任何约束表明当前focus的类型是a，所以Idris无法完成这个推断，导致类型检查失败。

内容的提问来源于stack exchange，提问作者Donovan