haskell - 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) 推断为 (Lit Integer)，这并不奇怪。现在到我的 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 yet, to令我惊讶(和高兴)的是，我看到它将它们标记为 Float 以使约束成功。我的问题是:当涉及约束时，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)

而且没有歧义。