跟踪约束的技术

这是一个场景:我写了一些带有类型签名的代码，GHC抱怨不能对某些x和y推断x ~ y。你通常可以扔GHC一根骨头，简单地将同构添加到函数约束中，但这是一个坏主意，原因如下:

它不强调理解代码。您最终可以得到5个约束，其中一个约束就足够了(例如，如果这5个约束是由一个更具体的约束暗示的) 如果你做错了什么，或者GHC没有帮助，你就会得到虚假的约束

我刚花了几个小时处理三号病例。我正在使用syntax -2.0，并试图定义一个与域无关的共享版本，类似于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不能推导(内部a) ~(内部b)，这当然不是我想要的。所以，要么是我写了一些我不打算写的代码(这需要约束)，要么是GHC因为我写的其他一些约束而想要那个约束。

原来我需要添加(句法a，句法b，句法(a->b))到约束列表，其中没有一个暗示(内部a) ~(内部b)。我基本上偶然发现了正确的约束;我仍然没有一个系统的方法来找到它们。

我的问题是:

Why did GHC propose that constraint? Nowhere in syntactic is there a constraint Internal a ~ Internal b, so where did GHC pull that from? In general, what techniques can be used to trace the origin of a constraint which GHC believes it needs? Even for constraints that I can discover myself, my approach is essentially brute forcing the offending path by physically writing down recursive constraints. This approach is basically going down an infinite rabbit hole of constraints and is about the least efficient method I can imagine.

首先，你的函数有错误的类型;我很确定它应该是(没有上下文)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)) After adding the above, we get Could not deduce (sup ~ Domain (a -> b)) After adding that, we get Could not deduce (Syntactic a), Could not deduce (Syntactic b) and Could not deduce (Syntactic (a -> b)) After adding these three, it finally typechecks; so we end up with 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，然后读取结果日志，看看内部(a -> b) ~ t和(Internal a -> Internal a) ~ t被添加到Wanted集，但这将是一个相当长的读取。

2016-01-15 06:11:29

你在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

关键是在约束中使用类型hole: _ =>您的困难类型

2020-05-16 16:29:08

跟踪约束的技术

推荐文章

最新文章

标签