追踪约束的技术

Question

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

1. 它不强调理解代码。
2. 你可能最终会有5个约束，而一个约束就足够了(例如，如果这5个约束是由一个更具体的约束所暗示的)
3. 如果你做错了什么事，或者GHC没有提供帮助，你可能最终会得到假的约束条件

我刚刚花了好几个小时和第三种情况作斗争。我在玩 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). 我基本上是偶然发现了正确的约束条件，我还是没有系统的方法去找到它们。

我的问题是：

1. 为什么GHC要提出这个约束条件? 句法中没有任何一个地方有约束条件。Internal a ~ Internal b那么，GHC是从哪里得到的呢？
2. 一般来说，有什么技术可以用来追踪一个GHC认为它需要的约束的来源？即使是对于那些我 可以 发现自己，我的方法基本上是通过物理写下递归约束的方式，蛮横地强行找到违规路径。这种方法基本上是在走一个无限的约束条件的兔子洞，是我能想到的效率最低的方法。

Answer 1

首先，你的函数有错误的类型；我很确定它应该是（没有上下文）。a -> (a -> b) -> b. GHC 7.10在指出这一点上更有帮助，因为在你的原始代码中，它抱怨缺少了一个约束条件。Internal (a -> b) ~ (Internal a -> Internal a) 固定后 share'的类型，GHC7.10仍然对我们有指导意义。

1. Could not deduce (Internal (a -> b) ~ (Internal a -> Internal b))

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

3. 添加后，我们得到 Could not deduce (Syntactic a), Could not deduce (Syntactic b) 和 Could not deduce (Syntactic (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的调试标志特别是： -ddump-tc-trace，然后阅读所产生的日志，看看哪里有 Internal (a -> b) ~ t 和 (Internal a -> Internal a) ~ t 加到 Wanted 集，但这将是一个相当长的阅读。

Answer 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