Constraint on method depends on instances in scope?

Question

Consider this code:

{-# language FlexibleInstances, UndecidableInstances #-}

module Y where

class C m where

    x :: m

instance {-# overlappable #-} Monoid m => C m where

    x = mempty

instance C Int where

    x = 53

What is the type of x?

λ :type x
x :: C m => m

So far — so good. Now remove the Int instance. What is the type of x?

λ :type x
x :: Monoid m => m

Surprise!

 

Why is this happening?

Answer 1

This behaviour is explained in the following blog post:

• Opaque constraint synonyms

In short: GHC is smart enough to see that you have only one instance of the C typeclass and decided that it's the only possible instance, so every time it sees C m constraint, it replaces it with Monoid m because they are equivalent.

 

N.B.   As @chi further explains in a comment:

When GHC finds a constraint C t, it tries to solve it. If if finds a matching instance (...) => C t where ..., the constraint is replaced with the context (...). This is repeated as much as possible. The final constraint appears in the type (or triggers a "unsolved" type error). This process is justified since there can only be at most one matching instance. Overlapping instances change this, and prevent this context reduction when multiple instances (in scope!) match, roughly. It is a fragile extension, to be used with some care.