Idris2中mult函数totality检查失败，递归参数为何未被判定为更小？

问题核心在于：Idris的totality检查器无法自动识别weaken a比(FS a)更小——它只认可直接的结构子项或能通过类型系统自动推导的大小递减关系，而weaken a是函数应用后的结果，不在检查器的默认识别范围内。

具体拆解：

• 当匹配mult (FS a) b时，a的类型是Fin m，此时函数的k参数实际是S m（因为FS a属于Fin (S m)类型）。
• weaken a会把a转换成Fin (S m)（也就是Fin k），它的结构复杂度和a完全一致（比如a是FS x，weaken a就是FS (weaken x)）。
• 检查器看到递归调用的参数是weaken a，它的类型和原参数(FS a)相同，但不是原参数的直接子项（原参数的直接子项是a，但a的类型是Fin m，无法直接传给需要Fin k的mult），因此无法推导递归会终止。

可行的解决方法 #

1. 用%assert_total跳过检查（简单但不严谨） #

如果你确定函数是终止的，可以直接告诉检查器跳过totality验证：

import Data.Fin

%default total

negate : {k:_} -> Fin k -> Fin k
subt : {k:_} -> Fin k -> Fin k -> Fin k
add : {k:_} -> Fin k -> Fin k -> Fin k

mult : {k:_} -> Fin k -> Fin k -> Fin k
mult FZ b = FZ
%assert_total
mult (FS a) b = add b $ mult (weaken a) b

2. 显式用大小类型标注递减关系 #

通过Size类型让检查器明确看到递归时的大小递减：

import Data.Fin

%default total

negate : {k:_} -> Fin k -> Fin k
subt : {k:_} -> Fin k -> Fin k -> Fin k
add : {k:_} -> Fin k -> Fin k -> Fin k

mult : {s : Size} -> Fin (s) -> Fin (s) -> Fin (s)
mult FZ b = FZ
mult (FS a) b = add b $ mult (weaken a) b

3. 调整递归逻辑，使用直接子项 #

重新设计实现，让递归调用直接使用原参数的子项（需要配合正确的add实现）：

import Data.Fin

%default total

add : {k : Nat} -> Fin k -> Fin k -> Fin k
add FZ b = b
add (FS a) b = FS (add a b)

mult : {k : Nat} -> Fin k -> Fin k -> Fin k
mult FZ _ = FZ
mult (FS a) b = add b (mult a b)

（注：这里的mult实现依赖add正确处理Fin的加法，确保结果不会溢出Fin k的范围，若需要严格的无溢出加法，需调整add的实现）

内容的提问来源于stack exchange，提问作者haskell looks great