haskell - 跟踪约束的技术

Question

场景如下:我编写了一些带有类型签名的代码，GHC 提示无法推断出某些 x 和 y 的 x ~ y。通常，您可以扔掉 GHC 并简单地将同构添加到函数约束中，但由于以下几个原因，这是一个坏主意:

1. 它并不强调理解代码。
2. 最终可能会出现 5 个约束，其中 1 个约束就足够了(例如，如果一个更具体的约束隐含了 5 个约束)
3. 如果您做错了什么或者 GHC 没有帮助，您最终可能会遇到虚假约束

我刚刚花了几个小时与案例 3 作斗争。我正在玩 syntactic-2.0 ，我试图定义一个与域无关的 share 版本，类似于 NanoFeldspar.hs 中定义的版本。 .

我有这个:

{-# LANGUAGE GADTs, FlexibleContexts, TypeOperators #-}
import Data.Syntactic

-- Based on NanoFeldspar.hs
data Let a where
    Let :: Let (a :-> (a -> b) :-> Full b)

share :: (Let :<: sup,
          Domain a ~ sup,
          Domain b ~ sup,
          SyntacticN (a -> (a -> b) -> b) fi) 
      => a -> (a -> b) -> a
share = sugarSym Let

并且 GHC 无法推导出 (Internal a) ~ (Internal b)，这当然不是我想要的。因此，要么我编写了一些我不打算编写的代码(需要约束)，要么 GHC 由于我编写的其他一些约束而需要该约束。

原来我需要将 (Syntropic a, Syntropic b, Syntropic (a->b)) 添加到约束列表中，其中没有一个暗示 (Internal a) ~ (内部b)。我基本上偶然发现了正确的约束；我仍然没有系统的方法来找到它们。

我的问题是:

1. 为什么 GHC 提出这个限制？句法中没有任何地方存在约束Internal a ~ Internal b，那么 GHC 从哪里得出这个约束呢？
2. 一般来说，可以使用哪些技术来追踪 GHC 认为其需要的约束的起源？即使对于我自己可以发现的约束，我的方法本质上也是通过物理地写下递归约束来暴力破解有问题的路径。这种方法基本上陷入了无限的约束兔子洞，并且是我能想象到的效率最低的方法。

Answer 1

首先，你的函数类型错误；我很确定它应该是(没有上下文)a -> (a -> b) -> b。 GHC 7.10 在指出这一点方面更有帮助，因为使用您的原始代码，它会提示缺少约束内部(a -> b)~(内部a -> 内部a)。修复 share 的类型后，GHC 7.10 仍然对指导我们很有帮助:

1. 无法推论(内部(a -> b)~(内部 a -> 内部 b))

2. 添加上述内容后，我们得到Could not deduc (sup ~ Domain (a -> b))

3. 添加后，我们得到无法推导(语法a)，无法推导(语法b)和无法推导(语法) (a -> b))

4. 添加这三个之后，最后进行类型检查；所以我们最终得到

   share :: (Let :<: sup,
             Domain a ~ sup,
             Domain b ~ sup,
             Domain (a -> b) ~ sup,
             Internal (a -> b) ~ (Internal a -> Internal b),
             Syntactic a, Syntactic b, Syntactic (a -> b),
             SyntacticN (a -> (a -> b) -> b) fi)
         => a -> (a -> b) -> b
   share = sugarSym Let
   

所以我想说 GHC 在领导我们方面并非毫无用处。

至于您关于跟踪 GHC 从哪里获取约束要求的问题，您可以尝试 GHC's debugging flags ，特别是 -ddump-tc-trace，然后通读生成的日志以查看 Internal (a -> b) ~ t 和 (Internal a -> 内部 a) ~ t 已添加到 Wanted 集合中，但这将是相当长的阅读时间。