GH C выводит мой неоднозначный тип, чтобы сделать ограничение успешным

Question

На самых ранних этапах реализации кодированного дерева на уровне типов я сталкивался со своеобразным поведением GH C в выводе его типов, когда сталкивался с неоднозначными типами, когда оно включает ограничения типов. Я написал два узла 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)

Как можно видеть, GH C выводит оба аннотированных (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)

Я все еще ожидал, что GH C выведет два неаннотированных типа как Integer, но жалуются в Couldn't match type 'Float' with 'Integer пока, к моему удивлению (& восхищению), я увидел, что он пометил их как Float s, чтобы ограничение сработало. Мой вопрос: изгибает ли GH C свои правила вывода типов при наличии ограничений? Какова его определенная процедура и приоритеты для вывода типа, включающего различные конструкции сигнатуры типа?

Answer 1

Вот что здесь происходит. Когда GH C пытается проверить тип выражения:

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, GH C сопоставляет его с:

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) позволяют GH C разрешать следующие функции типа:

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

Но это вместе с (*) выше позволяет GH C сделать заключение Float ~ n.

Итак, окончательный набор:

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

и нет никакой двусмысленности.