Idris实现自定义Vect拼接时重写未生效及类型报错问题

• 类型约束推导
  第二个分支匹配时，长度参数r被绑定为S rr，因此函数签名要求的预期返回类型为Vect (r' + S rr) Nat。
  手动构造的右值x :: (xs ++: y)中，xs是长度为rr的Vect，因此xs ++: y的类型为Vect (r' + rr) Nat，套上x ::后整体表达式的实际类型为Vect (S (r' + rr)) Nat。编译器需要对齐的核心等式约束为S (r' + rr) = r' + S rr。
• 重写方向匹配错误
  Idris的rewrite语法规则为：若证明p的类型为A = B，则rewrite p in e会将**目标类型（即表达式需要符合的预期类型）**中所有出现的A替换为B，再与e的实际类型做匹配。
  你编写的第一个分支是正确的：plusZeroRightNeutral r'的类型为r' + 0 = r'，其左侧项r' + 0刚好存在于预期目标类型Vect (r' + 0) Nat中，重写后目标类型变为Vect r' Nat，与参数y的实际类型完全匹配。
  但第二个分支使用的plusSuccRightSucc r' rr的类型为S (r' + rr) = r' + S rr，即A为S (r' + rr)，B为r' + S rr。当前预期目标类型为Vect (r' + S rr) Nat，其中根本不存在可替换的A项，因此重写操作没有任何效果，触发“重写未改变类型”的报错。
  移除重写时，编译器不会自动应用等式证明，只会识别到两个结构不同的长度表达式，因此报约束不匹配错误。

需要将证明的方向反转，生成类型为r' + S rr = S (r' + rr)的等价证明，也就是用sym反转原有等式的方向。重写时即可将目标类型中的r' + S rr替换为S (r' + rr)，与构造的表达式实际类型对齐。
修复后的完整代码如下：

import Data.Vect
import Data.Nat

infixl 9 ++:

public export
(++:) : {0 r, r' : Nat} -> Vect r Nat -> Vect r' Nat -> Vect (r' + r) Nat
(++:) [] y = rewrite plusZeroRightNeutral r' in y
(++:) {r = S rr} (x :: xs) y = rewrite sym (plusSuccRightSucc r' rr) in x :: (xs ++: y)

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