Idris中Bits8转Subset Nat (`LT` 256)的编译错误修复及优化问询

报错根因 #

• 整数字面量在Idris中会隐式调用Num接口的fromInteger方法转换为目标类型，你需要返回的Subset Nat (\n => LT n 256)类型未实现Num接口，因此编译器报错找不到对应实例。你单独执行the Nat 0正常是因为Nat类型本身有Num接口实现，和当前问题的目标类型完全不同。
• 枚举所有256个Bits8取值分支的写法会强制编译器逐一校验256个分支的类型约束，直接导致编译时长爆炸，属于完全不必要的实现方式。

最优修改方案 #

直接利用Idris标准库内置的Bits8边界特性实现，无需枚举任何分支，编译可以在数秒内完成：

1. 首先导入依赖模块：

import Data.Bits
import Data.Fin
import Data.Subset

2. 函数实现：

bits8ToNat256 : Bits8 -> Subset Nat (`LT` 256)
bits8ToNat256 b = let valFin = bits8ToFin b in Element (finToNat valFin) (natLt {n=valFin})

实现说明 #

• 标准库bits8ToFin方法可以直接将Bits8类型转换为Fin 256类型，Fin n类型的所有值天然满足对应的自然数小于n的约束
• natLt方法可以直接提取Fin值对应的自然数小于其边界的证明，无需手动编写约束证明

原枚举写法的修复方式（不推荐） #

如果你坚持要使用枚举256个分支的写法，只需要将每个分支的返回值显式构造为Subset类型即可，避免触发Num接口查找：

case b of
  0x0 => Element 0 %search
  0x1 => Element 1 %search
  -- 其余254个分支按照相同格式修改即可

该写法虽然可以解决编译报错问题，但仍然需要编译器处理数百个分支的类型校验，编译时长会远高于最优方案。

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