[Haskell-beginners] GHC: missing "No instance for ..." errors without the monomorphism restriction

[Daniel Fischer]

On Sunday 25 March 2012, 17:34:45, Máté Kovács wrote:
> Hi guys,
> 
> Give the following code:
> 
> ================
> 
> module Main where
> 
> class C a where
> 
> bar :: C a => a -> a
> bar x = x
> 
> foo = bar bar
> 
> main = do
>   putStrLn "hello"
> 
> ================
> 
> GHC says "No instance for (C (a0 -> a0)) arising from a use of `bar'",
> which is what I would normally expect.
> But with -XNoMonomorphismRestriction, it compiles without even a
> warning, as long as I don't use `foo' somewhere.
> 
> Could someone please explain why this is so?

foo is bound by a simple pattern binding without a type signature.
Therefore it is subject to the monomorphism restriction and all constrained 
type variables in the inferred type must be resolved.

Since

foo = bar something

by bar's type, it is determined that foo's type has the form (C a) => a, 
where a is the type of 'something'. Now, 'something' is bar, so a has the 
form 'a0 -> a0' (disregarding the constraint (C a0) here for the moment).
Altogether, the type inferred for foo is

foo :: forall a. (C a, C (a -> a)) => a -> a

Without the monomorphism restriction, that's the type foo gets, and the 
compiler is happy. With appropriate instances in scope, foo works.

But with the MR, the type variable must be instantiated by a specific type.
In what way exactly that fails depends on the type-checking algorithm.

- The constraining class  C is not defined in one of the standard 
libraries, therefore type defaulting isn't applicable per the language 
report 
(http://www.haskell.org/onlinereport/haskell2010/haskellch4.html#x10-790004.3.4)
- The constraint does not involve a numeric class
- The type variable a appears in a constraint of the form other than (C v), 
namely (C (a -> a))

Each of these points disallows foo with the MR, so could be reported as the 
type error. GHC's algorithm, however, looks first for an instance matching 
the non-(C v) constraint (trying to reduce it to a constraint of the 
admissible shape), doesn't find one and reports that. If you add an

instance C (a -> b)

or

instance (C a, C b) => C (a -> b)

GHC will complain about an ambiguous type variable and suggest disabling 
the MR.