-XNoMonomorphismRestriction: Named holes aren't shared

[xnyhps]

Probably directly a consequence of #1.

With -XNoMonomorphismRestriction the holes that are found (which are only visible in the debug messages from the constraint solver, because #1), don't share their type with the holes in other functions in the same module. For example:

f = _?h >>= _?g

g = [_?h, Just ()]

Logs:

tcRnSrcDecls: WC {wc_impl = Implic {Untouchables =  No untouchables
                                    Skolems =  []
                                    Given =  _?h :: _?h (Maybe ())
                                    Wanted =  WC {wc_flat = [W] _?h :: _?h
                                                                         (Maybe
                                                                            ()) {0} (CNonCanonical)}
                                    Binds =  EvBindsVar<auS>
                                    the inferred type of g :: (_?h (Maybe ())) => t_a
                                    test.hs:3:1-18}
                            Implic {Untouchables =  No untouchables
                                    Skolems =  [m, a, b]
                                    Given =  $dMonad :: Monad m_f
                                             _?h :: _?h (m_f a_g)
                                             _?g :: _?g (a_g -> m_f b_h)
                                    Wanted =  WC {wc_flat = [W] $dMonad :: Monad
                                                                             m_f {0} (CNonCanonical)
                                                            [W] _?h :: _?h
                                                                         (m_f a_g) {0} (CNonCanonical)
                                                            [W] _?g :: _?g
                                                                         (a_g
                                                                          -> m_f b_h) {0} (CNonCanonical)}
                                    Binds =  EvBindsVar<avb>
                                    the inferred type of
                                    f :: (Monad m_f, _?h (m_f a_g), _?g (a_g -> m_f b_h)) => t_e
                                    test.hs:1:1-15}}

Without -XNoMonomorphismRestriction, the result is:

tcRnSrcDecls: WC {wc_flat = [W] _?h :: _?h
                                         (Maybe ()) {0} (CNonCanonical)
                            [W] $dMonad :: Monad m_f {0} (CNonCanonical)
                            [W] _?h :: _?h (m_f a_g) {0} (CNonCanonical)
                            [W] _?g :: _?g (a_g -> m_f b_h) {0} (CNonCanonical)}

After that, _?h becomes shared (and this information propagates to _?g):

test.hs:1:13: Warning:
    Found hole _?g with type () -> Maybe b0
    In the second argument of `(>>=)', namely `_?g'
    In the expression: _?h >>= _?g
    In an equation for `f': f = _?h >>= _?g

test.hs:3:6: Warning:
    Found hole _?h with type Maybe ()
    In the expression: _?h
    In the expression: [_?h, Just ()]
    In an equation for `g': g = [_?h, Just ()]
Ok, modules loaded: Main.

[xnyhps]

Contrary to #1 (comment), adding (the simplest) type signatures to both f and g does not make this problem go away:

f :: (Monad m) => m b
f = _?h >>= _?g

g :: [Maybe ()]
g = [_?h, Just ()]

gives:

test.hs:2:5: Warning:
    Found hole _?h with type m a0
    In the first argument of `(>>=)', namely `_?h'
    In the expression: _?h >>= _?g
    In an equation for `f': f = _?h >>= _?g

test.hs:2:13: Warning:
    Found hole _?g with type a0 -> m b
    In the second argument of `(>>=)', namely `_?g'
    In the expression: _?h >>= _?g
    In an equation for `f': f = _?h >>= _?g

test.hs:5:6: Warning:
    Found hole _?h with type Maybe ()
    In the expression: _?h
    In the expression: [_?h, Just ()]
    In an equation for `g': g = [_?h, Just ()]

However, this example does work:

f :: ()
f = const () (_?h >>= _?g)

g :: [Maybe ()]
g = [_?h, Just ()]

test.hs:2:23: Warning:
    Found hole _?g with type () -> Maybe b0
    In the second argument of `(>>=)', namely `_?g'
    In the second argument of `const', namely `(_?h >>= _?g)'
    In the expression: const () (_?h >>= _?g)

test.hs:5:6: Warning:
    Found hole _?h with type Maybe ()
    In the expression: _?h
    In the expression: [_?h, Just ()]
    In an equation for `g': g = [_?h, Just ()]
Ok, modules loaded: Main.

---

My theory is that turning off the monomorphism restriction causes the residual constraints to not be "forced" if that's not necessary to satisfy the type signature. This causes the holes to not be reported (#1) and the constraints from different holes don't interact with each other. The first example here probably fails because f states that in f _?h is m a for any Monad m, while g specifies that _?h must be of type Maybe (), and these two things contradict each other.