为何Idris2的Prelude.mod被标记为全函数？参数为0时实则未定义

Idris2的Prelude.mod被官方标记为全函数，执行REPL命令:total mod会得到反馈：

Prelude.Num.mod is total

但实际调用时，若第二个参数（除数）为0，该函数并未定义，会直接触发运行时错误，这与Idris对全函数"对所有输入都有合法定义"的保证相矛盾。

问题原因 #

这是因为mod是Num类型类中的方法，类型层面并未强制要求实现必须处理除数为0的场景。Idris的全函数检查仅基于类型签名和函数定义的结构分析，无法静态验证这类依赖具体数值的边界情况，因此误将其标记为全函数。

解决方案 #

可以通过以下方式规避这个问题：

• 静态安全版本：利用So类型添加除数非0的编译期约束，确保只有合法输入能通过类型检查：

safeMod : (x : Integer) -> (y : Integer) -> {auto ok : So (y /= 0)} -> Integer
safeMod x y = mod x y

• 显式错误处理版本：返回Maybe类型，明确处理除数为0的情况：

maybeMod : Integer -> Integer -> Maybe Integer
maybeMod x 0 = Nothing
maybeMod x y = Just (mod x y)

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