Compilation error with a class constraint on a phantom type in a default method

Question

This (somewhat nonsensical) module compiles:

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ExplicitForAll #-}

module Foo where

class A t where
  f :: forall x m. Monoid x => t m -> m
  f = undefined

instance A [] where
  f = undefined

If I remove the instance's definition of f, I would expect it to inherit the method default and amount to the same thing.

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ExplicitForAll #-}

module Foo where

class A t where
  f :: forall x m. Monoid x => t m -> m
  f = undefined

instance A [] where

This does not work, however. GHC 8.0.2 gives this error:

• Could not deduce (Monoid x0)
    arising from a use of ‘Foo.$dmf’
  from the context: Monoid x
    bound by the type signature for:
               f :: Monoid x => [m] -> m
    at src/Foo.hs:10:10-13
  The type variable ‘x0’ is ambiguous
  These potential instances exist:
    instance Monoid a => Monoid (IO a) -- Defined in ‘GHC.Base’
    instance Monoid Ordering -- Defined in ‘GHC.Base’
    instance Monoid a => Monoid (Maybe a) -- Defined in ‘GHC.Base’
    ...plus 7 others
    (use -fprint-potential-instances to see them all)
• In the expression: Foo.$dmf @[]
  In an equation for ‘f’: f = Foo.$dmf @[]
  In the instance declaration for ‘A []’

I'm not sure how to read this error, because I don't know where the imaginary x0 is being inserted. Why doesn't the second example compile?

Answer 1

GHC is basically converting your code to this:

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ExplicitForAll #-}

module Foo where

defaultF :: forall t x m. (A t, Monoid x) => t m -> m
defaultF = undefined

class A t where
  f :: forall x m. Monoid x => t m -> m
  f = defaultF @t @x @m

instance A [] where
  f = defaultF @[]

Now, in the last line the type variable x is not in scope since we do not have an explicit forall x. Even if it were, it is not passed to defaultF as an explicit type argument. So, the last defaultF call could be made on any monoid at all, possibly another one!

For that call, the inference engine generates a fresh x0 type variable, hence the type error message :-(

Maybe GHC's instance deriving mechanism should be updated, now that ambiguous types are allowed (which is a good thing, IMO).

For a simpler case, consider

a :: forall x. Monoid x => Int
a = undefined

b :: forall x. Monoid x => Int
b = a

The last call needs a disambiguating explicit type argument, in Haskell. It would work fine in dependently typed languages like Agda/Idris/Coq/... since these (by default, at least) pass their type arguments explicitly.