Idris2编译器意外尝试统一类型值的异常报错问题咨询

算力阿峰

2026-10-6

Idris2 Hoare状态Monad编译异常排查

复现代码

在试验Hoare状态Monad时遇到了无法解释的Idris2编译错误，相关复现代码如下：

data PostS : (valType : Type) -> (stateType : Type) -> (valType -> stateType -> Type) -> Type where
  MkPostS
    :  (val : valType)
    -> (outState : stateType)
    -> {auto 0 prf : prop val outState}
    -> PostS valType stateType prop


mkPost : Nat -> PostS Nat Nat Equal
mkPost s2 = MkPostS s2 s2

f : (s1 : Nat) -> {auto 0 prf : Equal 0 s1} -> PostS Nat Nat (Equal)
f inState {prf} = MkPostS 7 7

异常现象与疑问

编译器报错提示f的右侧无法统一inState和7，二者确实不匹配，但目前不理解编译器为何会触发该统一操作。
更反常的是，将f的右侧替换为mkPost 7即可无错误编译，使用类似lambda函数的实现也能正常编译，暂时无法定位问题成因。

补充实验结果

后续补充测试得到以下结论：

无入参版本的同逻辑定义同样编译失败，编译器会尝试统一7和0：
```
f : PostS Nat Nat (Equal)
f = MkPostS 7 7
```
提前定义seven : Nat = 7再代入使用也会触发相同错误，但如下的f'定义可以正常工作：
```
f' : (s1 : Nat) -> PostS Nat Nat (\n => Equal (s1 + n))
f' s1 = MkPostS 7 (s1+7)
```
最初猜测问题源于数值7的类型歧义，后续测试推翻了该猜想：
```
data Foo = Bar | Baz

f'' : PostS Foo Foo (Equal)
f'' = MkPostS Baz Baz
```
上述代码可以正常编译，Baz与Baz的统一符合预期，尝试统一Bar和Baz的报错也符合预期，但MkPostS Bar Bar会抛出「Baz和Bar不匹配」的错误，手动指定{prf=Refl}后该错误就会消失。