跟踪约束的技巧
以下是这种情况：我写了一些带有类型签名的代码，GHC抱怨无法为x和y推出x〜y。 您通常可以将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) 。 我基本上碰到了正确的约束。 我仍然没有系统的方法来找到它们。
我的问题是：
Internal a ~ Internal b a〜 Internal a ~ Internal b ，那么GHC从哪里来拉？ 首先，你的函数有错误的类型; 我很确定它应该是（没有上下文） 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的调试标志，特别是-ddump-tc-trace ，然后通过结果日志读取Internal (a -> b) ~ t -ddump-tc-trace和(Internal a -> Internal a) ~ t被添加到Wanted集中，但这将是相当长的一段时间。