Idris判定Force、Delay插入位置的具体规则是什么

Idris中Lazy a和a之间的隐式转换完全由类型检查阶段的类型匹配规则驱动，具体插入Delay（转惰性）和Force（转求值）的规则如下：

• 自动插入Delay（a → Lazy a）的场景
  当实际传入值的类型为a，但上下文期望的类型是Lazy a时触发，常见场景包括：
  • 调用函数时，参数声明类型为Lazy a，传入的实参为a类型。比如逻辑与运算符(&&)的签名为Bool -> Lazy Bool -> Bool，因此b1 && b2会自动转换为b1 && Delay b2，和示例描述一致。
  • 将a类型的值赋值/绑定到显式声明为Lazy a类型的变量时。
• 自动插入Force（Lazy a → a）的场景
  当实际传入值的类型为Lazy a，但上下文期望的类型是a时触发，常见场景包括：
  • 将Lazy a类型的值传入参数要求为a的普通函数
  • Lazy a类型的值直接参与需要非惰性值的运算（比如数值计算、模式匹配普通构造器），例如存在x : Lazy Nat时，表达式x + 2会自动转换为Force x + 2
• 限制规则
  隐式转换仅支持单层Lazy包装的匹配：如果上下文期望Lazy (Lazy a)，传入a类型值时仅会自动插入一层Delay得到Lazy a，不会自动嵌套插入两层，这种情况需要手动处理多层惰性包装。
  转换仅在Lazy a和a的类型完全匹配时触发，不会和其他类型的隐式转换产生歧义。

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