Type unification with multi-parameter type classes

Question

{-# LANGUAGE MultiParamTypeClasses #-}
class Coerce a b where coerce :: a -> b
instance Coerce a a where coerce a = a

Now, this won't work: coerce 0 :: Int But if the instance is replace with this, the expression works:

instance a ~ b => Coerce a b where coerce x = x

Why?

Answer 1

I can tell you why the first one doesn't work.

Coerce could potentially be defined for any possible pair of types. coerce 0 :: Int is parsed as (coerce 0) :: Int. So you've fixed the b in coerce :: a -> b with the type annotation, but not the the a.

Numeric literals are polymorphic, so 0 has type Num a => a. That won't work; there's no instance matching Coerce a Int. There could be Coerce Double Int, Coerce Complex Int, etc, so knowing that b is Int isn't enough to infer that that 0 is an Int. We'd need to say coerce (0 :: Int) :: Int to fix both type parameters.

I believe the second one works because constraints on the instance declaration aren't used to help resolve type classes. instance a ~ b => Coerce a b is matched exactly as if you'd written instance Coerce a b. I.e. this is the most general instance possible (for the purpose of type class resolution), which well match any possible call to coerce (and so you can't write any other non-overlapping instances). The a ~ b constraint is only applied after the instance is chosen.

Since you have one instance that matches anything, there's no problem selecting an instance for coerce 0 :: Int, even though we still have the same problem of not knowing what type the 0 is. But then after instance selection, we now have the additional constraint a ~ Int, which allows unambiguous types to be assigned to everything.