GHC infers my ambiguous type to make constraint succeed

Question

At my very early stages of implementing a type-level encoded tree, I came across GHC's peculiar behavior in its type inference when faced with ambiguous types when it involves type constraints. I wrote two AST nodes as below both of which can have their types checked via their implemented Typed type class instance:

{-# 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

I then wrote the not type-checked badPlus function which performs no Typed instance check on the function arguments:

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)

As can be seen GHC inferred both un-annotated (Lit 1)s as (Lit Integer)s which were no surprise. Now to my goodPlus where I add the Typed constraint on the signature:

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)

I was still expecting GHC to infer the two un-annotated types as Integer but, complain on Couldn't match type 'Float' with 'Integer yet, to my surprise (& delight) I saw that it marked them as Floats to make the constraint succeed. My question is: Does GHC bend its type inference rules when constraints are involved? What is its defined procedure & priorities for type inference involving various type-signature constructs?

Possibly relevant: warning: [-Wsimplifiable-class-constraints] • The constraint ‘Typed (Plus a b)’ matches instance (T a ~ T b) => Typed (Plus a b) This makes type inference for inner bindings fragile; either use MonoLocalBinds, or simplify it using the instance • In the type signature: goodPlus :: Typed (Plus a b) => a -> b -> Plus a b — Joseph Sible-Reinstate Monica
Note that (1::Integer) + 2 and (1.5 :: Double) + 2 both type check. In the first case, 2 is inferred to be an Integer. In the second case, we do not get the same type for 2 and a type error, but instead Haskell makes 2 :: Double. Essentially, the type of numeric literals is chosen to match the context. If the context poses no constraints, at the very end of the type inference process, a few default types are taken: that's why you get 1 :: Integer in badExample -- that was picked as a default. — chi

K. A. Buhr K. A. Buhr · Accepted Answer · 2020-03-12T03:10:01

Here's what's going on here. When GHC tries to typecheck the expression:

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

against the signature:

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

this results in the type equalities / constraints:

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

To solve this Typed constraint, GHC matches it against:

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

with:

a' ~ Lit Float
b' ~ Lit n

(Recall that constraints in instance definitions play no role in the matching process, so there's no problem matching to this instance.) This results in an additional constraint:

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

However, T is an associated type family, and the instance for Typed (Lit a'') specialized to Typed (Lit Float) and Typed (Lit n) allow GHC to resolve these type functions:

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

But, this together with (*) above allow GHC to conclude Float ~ n.

So, the final typing is:

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

and there's no ambiguity.

GHC infers my ambiguous type to make constraint succeed

1 Answers