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:

1. {-# LANGUAGE MonomorphismRestriction #-}
   
   module Mono where
   
   f x = x + y
   y = f 1

2. {-# 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 and y :: Num a => a. Note that the monomorphism restriction is in effect; however, because y is in a recursive group and recursive groups under inference are quantified over the same set of constraints and f is declared to be quantified over Num a, y is too.

However, if we make f's signature a complete type signature by filling the _ in with a, now the program is rejected. While f and y are still in the same recursive group, f has a complete type signature. y is inferred first and monomorphised. Then f is checked. This fails, because no monomorphic y 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 over Num 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.