GHC 推断我的歧义类型使约束成功

Question

在我实现类型级编码树的早期阶段，当涉及类型约束时遇到不明确的类型时，我遇到了 GHC 在其类型推断中的特殊行为。我写了两个 AST 节点，如下所示，它们都可以通过它们实现的Typed类型类实例检查它们的类型：

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleContexts #-}

class Typed t where
  type T t

-- | A Literal node
newtype Lit a =
  Lit a

instance Typed (Lit a) where
  type T (Lit a) = a

-- | A Plus Node
data Plus a b =
  Plus a b

instance T a ~ T b => Typed (Plus a b) where
  type T (Plus a b) = T a 

然后我编写了未类型检查的badPlus函数，它不对Typed函数参数执行实例检查：

badPlus :: a -> b -> Plus a b
badPlus = Plus

badExample = Lit (1 :: Float) `badPlus` Lit 1 `badPlus` Lit 1 

>:i badExample
badExample :: Plus (Plus (Lit Float) (Lit Integer)) (Lit Integer)

可以看出，GHC 将两个未注释的(Lit 1)s推断为 ( Lit Integer)s，这并不奇怪。现在到我goodPlus在Typed签名上添加约束的地方：

goodPlus :: Typed (Plus a b) => a -> b -> Plus a b
goodPlus = Plus

goodExample = Lit (1 :: Float) `goodPlus` Lit 1 `goodPlus` Lit 1 

>:i goodExample
goodExample :: Plus (Plus (Lit Float) (Lit Float)) (Lit Float)

我仍然期待 GHC 推断出这两种未注释的类型，Integer但是，Couldn't match type 'Float' with 'Integer仍然抱怨，令我惊讶（和高兴）我看到它将它们标记为Floats 以使约束成功。我的问题是：当涉及约束时，GHC 是否会改变其类型推断规则？涉及各种类型签名结构的类型推断的定义程序和优先级是什么？

Answer 1

这就是这里发生的事情。当 GHC 尝试对表达式进行类型检查时：

goodPlus (Lit (1 :: Float)) (Lit 1)

反对签名：

goodPlus :: Typed (Plus a b) => a -> b -> Plus a b

这导致类型相等/约束：

a ~ Lit Float
b ~ Lit n
Num n
Typed (Plus (Lit Float) (Lit n))

为了解决这个Typed约束，GHC 将它与：

instance T a' ~ T b' => Typed (Plus a' b')

和：

a' ~ Lit Float
b' ~ Lit n

（回想一下，实例定义中的约束在匹配过程中不起作用，所以匹配到这个实例没有问题。）这导致了一个额外的约束：

T (Lit Float) ~ T (Lit n)                 -- (*)

然而，T是一个关联的类型族，并且Typed (Lit a'')专门用于Typed (Lit Float)并Typed (Lit n)允许 GHC 解析这些类型函数的实例：

T (Lit Float) ~ Float
T (Lit n) ~ n

但是，这与上面的 (*) 一起允许 GHC 得出结论Float ~ n。

所以，最后的打字是：

goodPlus (Lit (1 :: Float)) (Lit 1) :: Plus (Lit Float) (Lit Float)

并且没有歧义。