Idris中如何触发内部bug崩溃同时保证模式匹配穷尽性

Idris要求Ord接口的compare方法必须是覆盖函数（即对所有合法输入都有明确定义的返回值）。你用到的Builtin.idris_crash本身是非覆盖函数（调用后会直接终止程序，不会返回正常值），因此编译器认为你的compare函数没有覆盖所有分支，抛出该错误。

有两种常用方案都可以满足你「非法返回值直接崩溃、模式匹配被认定为穷尽」的需求：

方案1：用assert_total标记不可达分支 #

直接在idris_crash外层套assert_total，向编译器保证这个默认分支理论上永远不会被执行，函数整体是覆盖的：

prim__compare : Scalar -> Scalar -> Int

Ord Scalar where
  compare x y = case prim__compare x y of
                  -1 => LT
                  0 => EQ
                  1 => GT
                  _ => assert_total $ idris_crash "Illegal compare result from C FFI, this should never happen"

这种方案改动最小，运行时行为和你最初的写法完全一致，遇到非法值会直接崩溃。

方案2：封装合法返回值类型（更易维护） #

先定义仅包含三种合法比较结果的自定义类型，把FFI返回值的校验和崩溃逻辑封装到类型转换函数里，之后的模式匹配天然就是穷尽的：

-- 定义仅包含三种合法比较结果的类型
data CmpRes = CmpLT | CmpEQ | CmpGT

-- Int转CmpRes，非法值直接崩溃
fromInt : Int -> CmpRes
fromInt (-1) = CmpLT
fromInt 0 = CmpEQ
fromInt 1 = CmpGT
fromInt _ = assert_total $ idris_crash "Illegal compare result from C FFI"

prim__compare : Scalar -> Scalar -> Int

Ord Scalar where
  compare x y = case fromInt (prim__compare x y) of
                  CmpLT => LT
                  CmpEQ => EQ
                  CmpGT => GT

这种方案下compare里的模式匹配不需要默认分支，编译器会自动判定为穷尽，后续如果要修改比较逻辑也更清晰。

注意：两种方案都需要你自行保证FFI调用的C函数实际返回值只有-1、0、1三种，否则运行时会触发崩溃。

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