为什么该Idris的merge2函数无法通过总性检查，如何修改使其通过校验

问题原因 #

Idris 的总性检查器不会跨分支推导变量约束：你前两个分支虽然已经过滤了left或right为空的场景，但第三个分支中使用let语句做的列表非空匹配属于局部不完全匹配，检查器不会关联前面的分支条件，因此判定存在缺失分支。同时递归调用的终止性也需要依赖明确的参数结构才能被验证。

修复方案 #

直接将第三个分支的参数写为两个非空列表的模式匹配，替代let块内的解构操作，总性检查器可以直接识别该分支的输入约束，不需要额外跨分支推导。

修复后的代码如下：

module Main

record Mergeable where
    constructor MkMergeable
    left : List Nat
    right : List Nat

merge2 : Mergeable -> List Nat
merge2 (MkMergeable [] right) = right
merge2 (MkMergeable left []) = left
merge2 (MkMergeable (a1 :: a2) (b1 :: b2)) =
    if a1 < b1 
        then a1 :: merge2 (MkMergeable a2 (b1 :: b2))
        else b1 :: merge2 (MkMergeable (a1 :: a2) b2)

改写后所有分支的模式匹配都是完全覆盖的，且每次递归调用时两个列表的总长度严格递减，总性检查器可以直接验证函数的总性。

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