追踪约束的技巧

Question

这是场景:我已经编写了一些带有类型签名的代码,并且GHC抱怨无法推断x~y某些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想要这个约束,因为我写了一些其他的约束.

事实证明我需要添加(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修好后,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. 加上这三个后,它终于出现了问题; 所以我们最终得到了

   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集合中,但这将是相当长的阅读.