跟踪约束的技术答案

【问题标题】：Techniques for Tracing Constraints跟踪约束的技术
【发布时间】：2014-06-20 07:39:33
【问题描述】：

情况如下：我编写了一些带有类型签名的代码，GHC 抱怨无法推断出某些x 和y 的x ~ y。您通常可以将 GHC 扔掉，然后简单地将同构添加到函数约束中，但这是一个坏主意，原因如下：

不强调理解代码。
您最终可以得到 5 个约束条件，其中一个就足够了（例如，如果 5 个约束条件隐含在一个更具体的约束条件中）
如果您做错了什么或 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 could not deduce (Internal a) ~ (Internal b)，这当然不是我想要的。所以要么我写了一些我不打算写的代码（这需要约束），要么 GHC 想要那个约束，因为我写了一些其他的约束。

事实证明，我需要将(Syntactic a, Syntactic b, Syntactic (a->b)) 添加到约束列表中，这些都没有暗示(Internal a) ~ (Internal b)。我基本上偶然发现了正确的约束；我仍然没有系统的方法来找到它们。

我的问题是：

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

【问题讨论】：

有一些关于类型级调试器的讨论，但普遍的共识似乎表明类型检查器的内部逻辑无济于事：/ 截至目前，Haskell 的约束求解器很糟糕不透明的逻辑语言:)
@jozefg 你有那个讨论的链接吗？
通常完全删除类型签名并让 ghci 告诉你它认为签名应该是什么会有所帮助。
不知何故 a 和 b 被绑定 - 查看上下文之外的类型签名 - a -> (a -> b) -> a，而不是 a -> (a -> b) -> b。也许就是这样？使用约束求解器，它们可以影响传递等式任何地方，但错误通常显示位置“靠近”引发约束的位置。尽管@jozefg 那会很酷 - 也许用标签或其他东西注释约束，以显示它们来自哪里？ :s

标签： haskell constraints ghc

【解决方案1】：

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

Could not deduce (Internal (a -> b) ~ (Internal a -> Internal b))
加上上面的，我们得到Could not deduce (sup ~ Domain (a -> b))
添加之后，我们得到Could not deduce (Syntactic a)、Could not deduce (Syntactic b)和Could not deduce (Syntactic (a -> b))

加上这三个后，最后进行类型检查；所以我们最终得到了

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 -> Internal a) ~ t到Wanted 集，但这将是相当长的阅读。

【讨论】：

【解决方案2】：

您是否在 GHC 8.8+ 中尝试过这个？

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

关键是在约束中使用类型空洞：_ => your difficult type

【讨论】：