Deviation from the monomorphism restriction
For any binding f = ...
without a type signature, I would expect to be able to take its inferred type as reported by GHCi and insert it into the source program.
Here are two programs where this property holds:
-
{-# LANGUAGE MonomorphismRestriction #-} module Mono where f x = x + y y = f 1
-
{-# LANGUAGE NoMonomorphismRestriction #-} module Poly where f x = x + y y = f 1
In Mono
, GHC infers y :: Integer
and f :: Integer -> Integer
. I can insert one of these signatures (or both of them) into the source code, and the program will continue to compile:
{-# LANGUAGE MonomorphismRestriction #-}
module Mono where
f :: Integer -> Integer
f x = x + y
y = f 1
In Poly
, GHC infers y :: Num a => a
and f :: Num a => a -> a
. I can insert one of these signatures (or both of them) into the source code, and the program will continue to compile:
{-# LANGUAGE NoMonomorphismRestriction #-}
module Poly where
f :: Num a => a -> a
f x = x + y
y = f 1
However, in #17268 (comment 225491), Richard has come up with a program that violates this property:
{-# LANGUAGE MonomorphismRestriction #-}
{-# LANGUAGE PartialTypeSignatures #-}
module MonoPoly where
f :: Num a => a -> _
f x = x + y
y = f 1
Here, despite the monomorphism restriction, GHC infers f :: Num a => a -> a
and y :: Num a => a
. Then, inserting the type of f
back into the source program leads to an error:
{-# LANGUAGE MonomorphismRestriction #-}
module MonoPoly where
f :: Num a => a -> a
f x = x + y
y = f 1
MonoPoly.hs:6:11: error:
• Couldn't match expected type ‘a’ with actual type ‘Integer’
‘a’ is a rigid type variable bound by
the type signature for:
f :: forall a. Num a => a -> a
at MonoPoly.hs:5:1-20
• In the second argument of ‘(+)’, namely ‘y’
In the expression: x + y
In an equation for ‘f’: f x = x + y
• Relevant bindings include
x :: a (bound at MonoPoly.hs:6:3)
f :: a -> a (bound at MonoPoly.hs:6:1)
|
6 | f x = x + y
|
What went wrong here? Here's Richard's explanation:
This program is accepted, with
f :: Num a => a -> a
andy :: Num a => a
. Note that the monomorphism restriction is in effect; however, becausey
is in a recursive group and recursive groups under inference are quantified over the same set of constraints andf
is declared to be quantified overNum a
,y
is too.However, if we make
f
's signature a complete type signature by filling the_
in witha
, now the program is rejected. Whilef
andy
are still in the same recursive group,f
has a complete type signature.y
is inferred first and monomorphised. Thenf
is checked. This fails, because no monomorphicy
can work.
My hunch is that the problem is that:
recursive groups under inference are quantified over the same set of constraints and
f
is declared to be quantified overNum a
,y
is too.
This seems to go against the definition of monomorphism restriction from the Haskell Report:
the constrained type variables of a restricted declaration group may not be generalized in the generalization step for that group
According to my understanding of this rule, it means that y
should get a monomorphic type y :: Integer
, and I don't see why a partial signature on f
should change that.
The fix, then, is to infer y :: Integer
in MonoPoly
and reject it, thus restoring the property that any inferred type can be inserted back into the source program as a type signature.