跟踪约束的技巧

这里是这样的情景：我写了一些代码和一个types签名，GHC抱怨不能推导出一些x和y 。 您通常可以将GHC扔到骨头上，并简单地将同构添加到函数约束中，但出于以下几个原因，这是一个糟糕的主意：

1. 它不强调理解代码。
2. 你可以在5个约束条件下得到足够的结果（例如，如果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 could not deduce (Internal a) ~ (Internal b) ，这当然不是我想要的。 所以要么我写了一些我不想要的代码（需要这个约束），要么由于我写的其他约束条件，GHC想要这个约束。

事实certificate，我需要在约束列表中添加(Syntactic a, Syntactic b, Syntactic (a->b)) ，其中没有一个暗示(Internal a) ~ (Internal b) 。 我基本上碰到了正确的约束。 我还没有系统的方法来find它们。

我的问题是：

1. GHC为什么提出这个约束？ 在句法上没有任何限制Internal a ~ Internal b a〜 Internal a ~ Internal b ，那么GHC从哪里来呢？
2. 一般而言，可以使用哪些技术来追溯GHC认为需要的约束的起源？ 即使是我可以发现自己的限制，我的方法本质上是通过物理写下recursion约束来强制违规path。 这种方法基本上是在一个无限的兔子的限制之下，是我能想象到的效率最低的方法。

Answer 1

首先，你的function有错误的types; 我很确定它应该是（没有上下文） a -> (a -> b) -> b 。 GHC 7.10在指出这一点时更有帮助，因为用你最初的代码，它会抱怨一个缺失的约束Internal (a -> b) ~ (Internal a -> Internal a) 。 确定sharetypes后，GHC 7.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. join这三个后，终于搞到了; 所以我们结束了

    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的debugging标志 ，特别是-ddump-tc-trace ，然后读取结果日志以查看Internal (a -> b) ~ t -ddump-tc-trace和(Internal a -> Internal a) ~ t被添加到Wanted集，但这将是一个相当长的阅读。