GHC infers my ambiguous type to make constraint succeed

user_5421435 0
Viewed 105

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?

typeclass type-inference haskell
1 Answers

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.

user_72030160
Related