这是一个场景:我写了一些带有类型签名的代码，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.
