Order dependence in type checking with the monomorphism restriction
The order in which GHC type-checks definitions can change the outcome of type-checking when the monomorphism restriction is involved. This is because the monomorphism restriction affects all variables mentioned in a constraint; sometimes, though, a constraint can be eagerly solved, making it disappear (and thus not affecting any variables).
A nested example:
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
module Bug where
class C a b where
method :: a -> b -> ()
instance C Char b where
method _ _ = ()
f1 x = let g = \y -> method x y in
(x : "hi", (g True, g Nothing))
f2 x = (x : "hi",
let g = \y -> method x y in
(g True, g Nothing))
f1
is rejected, as method x y
gives rise to [W] C alpha beta
, which cannot be solved. Then, g
is not generalised, so we get g :: beta -> ()
, which is not general enough for its two usages.
f2
is accepted, as method x y
gives rise to [W] C Char beta
, easily solved by the instance. No MR happens.
A top-level example:
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
module Bug2 where
x = 5
class C a b where
method :: a -> b -> ()
instance C Int b where
method _ _ = ()
x2 :: (Int, ((), ()))
x2 = (x + 1, (g True, g 'x')) -- remove references to 'g' to allow module to be accepted
g = \y -> method x y
x3 :: ((), ())
x3 = (g True, g 'x')
This is rejected. Note that x2
depends on g
, and thus g
is type-checked first -- critically, before we know that x :: Int
. So the MR kicks in and prevents generalisation. However if we change to x2 = (x + 1, ((), ()))
, then the module is accepted: x2
gets seen first, we learn that x :: Int
, and then there is no constraint to prevent generalisation in g
. The two different uses in x3
are accepted.
I don't think this will be easy to fix: we would somehow need to delay the computation of whether or not to generalise, and that seems Very Hard. Maybe this just gets filed in the user manual under FlexibleInstances
and how flexibility can sometimes cause trouble? Not sure. Note that "let should not be generalised" is not enough here, because the problem can manifest at top-level.
This is based on a conversation with @simonpj this morning; credit to him for outlining the problem.