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有所抱怨，令我惊讶的是（令我惊讶的是，我看到它将它们标记为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')

with：

a' ~ Lit Float
b' ~ Lit n

（（实例定义中的约束在匹配过程中不起作用，因此与该实例匹配没有问题。）这会导致附加约束：

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

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

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

但是，加上上面的（*），GHC可以得出n ~ Float。

所以，最后的输入是：

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

并且没有歧义。