为何Idris代码中hole的上下文未正常归一化？

你遇到的是Idris类型检查器未自动归一化natToFin Z 256的问题，导致孔的上下文里显示natToFin _ 256而非预期的natToFin Z 256（后者本应直接归一化为Just FZ）。我们先梳理问题场景，再给出具体的解决思路。

问题复现 #

先看你的完整代码：

module Bytes

import Data.Fin

%default total

Byte : Type
Byte = Fin 256

fromNat : Nat -> Byte
fromNat n = maybe FZ (\x=>x) (natToFin n 256)

toNat : Byte -> Nat
toNat FZ     = Z
toNat (FS b) = S (toNat b)

prop : (b : Byte) -> fromNat (toNat b) = b
prop FZ     = ?prop_rhs_1
prop (FS x) = ?prop_rhs_2

查看?prop_rhs_1的上下文时，Idris显示：

---

prop_rhs_1 : maybe (Delay FZ) (Delay (\x => x)) (natToFin _ 256) = FZ

这里的下划线_表示Idris尚未推断出该参数为Z，加上maybe函数的参数是延迟求值的（为了保证 totality），导致后续无法自动归一化natToFin Z 256为Just FZ，进而不能直接用Refl填充孔。

解决方法 #

我们可以手动引导Idris完成归一化，具体有两种思路：

方法1：直接填入Refl

对于prop FZ的情况，toNat FZ的归一化结果是Z，而natToFin Z 256会被解析为Just FZ，最终maybe FZ id (Just FZ)等于FZ，等式变为FZ = FZ，直接用Refl即可证明：

prop FZ     = Refl

方法2：利用归纳法处理归纳步骤

对于prop (FS x)，我们可以借助归纳假设和cong函数（构造函数的同余性质）来完成证明：

prop (FS x) = cong FS (prop x)

原理是：toNat (FS x)等于S (toNat x)，而fromNat对S n的处理会返回FS (fromNat n)，结合归纳假设prop x（即fromNat (toNat x) = x），就能推导出fromNat (toNat (FS x)) = FS x。

完整修正代码 #

module Bytes

import Data.Fin

%default total

Byte : Type
Byte = Fin 256

fromNat : Nat -> Byte
fromNat n = maybe FZ (\x=>x) (natToFin n 256)

toNat : Byte -> Nat
toNat FZ     = Z
toNat (FS b) = S (toNat b)

prop : (b : Byte) -> fromNat (toNat b) = b
prop FZ     = Refl
prop (FS x) = cong FS (prop x)

这段代码能顺利通过Idris的类型检查，因为FZ分支的归一化被显式触发，归纳分支则利用同余性质传递了归纳假设。

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