为什么 Idris 2 无法解决这个简单示例中函数组合的约束？

Question

我尝试在 Idris 2 中编写的一些代码遇到了问题。我想解决这个问题，但更重要的是，我希望更深入地理解它并培养一些诊断此类问题的技能。

我将问题提炼为以下相对简单的示例：

data D : Nat -> Type where
  V : (n : Nat) -> D n

d : (n : Nat) -> D n
d n = V n

f : D n -> String
f (V n) = show n

t : Nat -> String
t = f . d

t 的定义失败了类型检查，输出如下：

Error: While processing right hand side of t. Can't solve constraint between: ?n [no locals in scope] and n.

Test:11:9--11:10
 07 | f : D n -> String
 08 | f (V n) = show n
 09 | 
 10 | t : Nat -> String
 11 | t = f . d

一些实验表明 t 的以下替代定义也类型检查失败：

t : Nat -> String
t n = (f . d) n

t : Nat -> String
t = \n => (f . d) n

虽然这些替代方案类型检查成功：

t : Nat -> String
t n = f (d n)

t : Nat -> String
t = \n => f (d n)

我正在努力学习 Idris（第二次），因此虽然我可以继续不涉及函数组合的定义，但我想提高我的理解。

在我看来，通过类型检查的定义只是具有相同语义和行为的语法替代方案，并且我不明白为什么函数组合定义无法通过类型检查。我还想了解类型检查器报告的特定错误消息，以便我可以加深理解并解决将来类似的类型检查错误。

我有几个广泛的问题：

• 我应该如何解释此示例中类型检查器报告的错误，以及如何收集有关 的更多信息？提到了 和 n 类型？我特别欢迎任何有关如何理解和解决此类错误的建议或提示（俗话说授人以渔）。
• 为什么涉及函数组合的定义无法通过类型检查？
• 此示例的最佳解决方案是什么？ 我应该使用不涉及函数组合的定义吗？有更好的选择吗？

Answer 1

我们看看涉及到的类型

Prelude.. : (b   -> c     ) -> (a        -> b   ) -> a -> c
f :          D n -> String
d :                             (n : Nat) -> D n

问题是：

(a        -> b   )
(n : Nat) -> D n

无法统一，因为(a -> b)不允许通过参数的值来决定返回值的类型。