Improve partial signatures

This MR fixes #23223. The changes are in two places:

* GHC.Tc.Bind.checkMonomorphismRestriction
  See the new `Note [When the MR applies]`
  We now no longer stupidly attempt to apply the MR when the user
  specifies a context, e.g.   f :: Eq a => _ -> _

* GHC.Tc.Solver.decideQuantification
  See rewritten `Note [Constraints in partial type signatures]`

Fixing this bug apparently breaks three tests:

* partial-sigs/should_compile/T11192
* partial-sigs/should_fail/Defaulting1MROff
* partial-sigs/should_fail/T11122

However they are all symptoms of #23232, so I'm marking them as
expect_broken(23232).

I feel happy about this MR. Nice.

4 files changed, 137 insertions, 104 deletions

diff --git a/compiler/GHC/Tc/Gen/Bind.hs b/compiler/GHC/Tc/Gen/Bind.hs
index 1e9a25c63d..cee24aa395 100644
--- a/compiler/GHC/Tc/Gen/Bind.hs
+++ b/compiler/GHC/Tc/Gen/Bind.hs
@@ -751,57 +751,102 @@ tcPolyInfer rec_tc prag_fn tc_sig_fn bind_list
 
 checkMonomorphismRestriction :: [MonoBindInfo] -> [LHsBind GhcRn] -> TcM Bool
 -- True <=> apply the MR
+-- See Note [When the MR applies]
 checkMonomorphismRestriction mbis lbinds
-  | null partial_sigs  -- The normal case
   = do { mr_on <- xoptM LangExt.MonomorphismRestriction
        ; let mr_applies = mr_on && any (restricted . unLoc) lbinds
-       ; when mr_applies $ mapM_ checkOverloadedSig sigs
+       ; when mr_applies $ mapM_ checkOverloadedSig mbis
        ; return mr_applies }
-
-  | otherwise    -- See Note [Partial type signatures and the monomorphism restriction]
-  = return (all is_mono_psig partial_sigs)
-
   where
-    sigs, partial_sigs :: [TcIdSigInst]
-    sigs          = [sig | MBI { mbi_sig = Just sig } <- mbis]
-    partial_sigs  = [sig | sig@(TISI { sig_inst_sig = PartialSig {} }) <- sigs]
-
-    complete_sig_bndrs :: NameSet
-    complete_sig_bndrs
-      = mkNameSet [ idName bndr
-                  | TISI { sig_inst_sig = CompleteSig { sig_bndr = bndr }} <- sigs ]
-
-    is_mono_psig (TISI { sig_inst_theta = theta, sig_inst_wcx = mb_extra_constraints })
-       = null theta && isNothing mb_extra_constraints
+    no_mr_bndrs :: NameSet
+    no_mr_bndrs = mkNameSet (mapMaybe no_mr_name mbis)
+
+    no_mr_name :: MonoBindInfo -> Maybe Name
+    -- Just n for binders that have a signature that says "no MR needed for me"
+    no_mr_name (MBI { mbi_sig = Just sig })
+       | TISI { sig_inst_sig = info, sig_inst_theta = theta, sig_inst_wcx = wcx } <- sig
+       = case info of
+           CompleteSig { sig_bndr = bndr } -> Just (idName bndr)
+           PartialSig { psig_name = nm }
+             | null theta, isNothing wcx   -> Nothing  -- f :: _ -> _
+             | otherwise                   -> Just nm  -- f :: Num a => a -> _
+             -- For the latter case, we don't want the MR:
+             -- the user has explicitly specified a type-class context
+    no_mr_name _ = Nothing
 
     -- The Haskell 98 monomorphism restriction
     restricted (PatBind {})                              = True
-    restricted (VarBind { var_id = v })                  = no_sig v
+    restricted (VarBind { var_id = v })                  = mr_needed_for v
     restricted (FunBind { fun_id = v, fun_matches = m }) = restricted_match m
-                                                           && no_sig (unLoc v)
+                                                           && mr_needed_for (unLoc v)
     restricted b = pprPanic "isRestrictedGroup/unrestricted" (ppr b)
 
     restricted_match mg = matchGroupArity mg == 0
         -- No args => like a pattern binding
         -- Some args => a function binding
 
-    no_sig nm = not (nm `elemNameSet` complete_sig_bndrs)
+    mr_needed_for nm = not (nm `elemNameSet` no_mr_bndrs)
 
-checkOverloadedSig :: TcIdSigInst -> TcM ()
+checkOverloadedSig :: MonoBindInfo -> TcM ()
 -- Example:
 --   f :: Eq a => a -> a
 --   K f = e
 -- The MR applies, but the signature is overloaded, and it's
 -- best to complain about this directly
 -- c.f #11339
-checkOverloadedSig sig
-  | not (null (sig_inst_theta sig))
-  , let orig_sig = sig_inst_sig sig
+checkOverloadedSig (MBI { mbi_sig = mb_sig })
+  | Just (TISI { sig_inst_sig = orig_sig, sig_inst_theta = theta, sig_inst_wcx = wcx }) <- mb_sig
+  , not (null theta && isNothing wcx)
   = setSrcSpan (sig_loc orig_sig) $
     failWith $ TcRnOverloadedSig orig_sig
   | otherwise
   = return ()
 
+{- Note [When the MR applies]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The Monomorphism Restriction (MR) applies as specifies in the Haskell Report:
+
+* If -XMonomorphismRestriction is on, and
+* Any binding is restricted
+
+A binding is restricted if:
+* It is a pattern binding e.g. (x,y) = e
+* Or it is a FunBind with no arguments e.g. f = rhs
+     and the binder `f` lacks a No-MR signature
+
+A binder f has a No-MR signature if
+
+* It has a complete type signature
+    e.g. f :: Num a => a -> a
+
+* Or it has a /partial/ type signature with a /context/
+    e.g.  f :: (_) => a -> _
+          g :: Num a => a -> _
+          h :: (Num a, _) => a -> _
+   All of f,g,h have a No-MR signature.  They say that the function is overloaded
+   so it's silly to try to apply the MR. This means that #19106 works out
+   fine.  Ditto #11016, which looked like
+      f4 :: (?loc :: Int) => _
+      f4 = ?loc
+
+   This partial-signature stuff is a bit ad-hoc but seems to match our
+   use-cases.  See also Note [Constraints in partial type signatures]
+   in GHC.Tc.Solver.
+
+Example: the MR does apply to
+   k :: _ -> _
+   k = rhs
+because k's binding has no arguments, and `k` does not have
+a No-MR signature.
+
+All of this checking takes place after synonym expansion.  For example:
+   type Wombat a = forall b. Eq [b] => ...b...a...
+   f5 :: Wombat _
+This (and does) behave just like
+   f5 :: forall b. Eq [b] => ...b..._...
+
+-}
+
 --------------
 mkExport :: TcPragEnv
          -> WantedConstraints  -- residual constraints, already emitted (for errors only)
@@ -850,15 +895,9 @@ mkExport prag_fn residual insoluble qtvs theta
                   then return idHsWrapper  -- Fast path; also avoids complaint when we infer
                                            -- an ambiguous type and have AllowAmbiguousType
                                            -- e..g infer  x :: forall a. F a -> Int
-                  else tcSubTypeSigma GhcBug20076
+                  else tcSubTypeSigma (Shouldn'tHappenOrigin "mkExport")
                                       sig_ctxt sel_poly_ty poly_ty
-                       -- as Note [Impedance matching] explains, this should never fail,
-                       -- and thus we'll never see an error message. It *may* do
-                       -- instantiation, but no message will ever be printed to the
-                       -- user, and so we use Shouldn'tHappenOrigin.
-                       -- Actually, there is a bug here: #20076. So we tell the user
-                       -- that they hit the bug. Once #20076 is fixed, change this
-                       -- back to Shouldn'tHappenOrigin.
+                       -- See Note [Impedance matching]
 
         ; localSigWarn poly_id mb_sig
 
@@ -1102,33 +1141,6 @@ It might be possible to fix these difficulties somehow, but there
 doesn't seem much point.  Indeed, adding a partial type signature is a
 way to get per-binding inferred generalisation.
 
-Note [Partial type signatures and the monomorphism restriction]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-We apply the MR if /none/ of the partial signatures has a context. e.g.
-   f :: _ -> Int
-   f x = rhs
-The partial type signature says, in effect, "there is no context", which
-amounts to appplying the MR. Indeed, saying
-   f :: _
-   f = rhs
-is a way for forcing the MR to apply.
-
-But we /don't/ want to apply the MR if the partial signatures do have
-a context  e.g. (#11016):
-   f2 :: (?loc :: Int) => _
-   f2 = ?loc
-It's stupid to apply the MR here.  This test includes an extra-constraints
-wildcard; that is, we don't apply the MR if you write
-   f3 :: _ => blah
-
-But watch out.  We don't want to apply the MR to
-   type Wombat a = forall b. Eq b => ...b...a...
-   f4 :: Wombat _
-Here f4 doesn't /look/ as if it has top-level overloading, but in fact it
-does, hidden under Wombat.  We can't "see" that because we only have access
-to the HsType at the moment.  That's why we do the check in
-checkMonomorphismRestriction.
-
 Note [Quantified variables in partial type signatures]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Consider
@@ -1206,7 +1218,6 @@ considered:
   more indirect, but we need the "don't generalise over Concrete variables"
   stuff anyway.
 
-
 Note [Impedance matching]
 ~~~~~~~~~~~~~~~~~~~~~~~~~
 Consider
diff --git a/compiler/GHC/Tc/Gen/Sig.hs b/compiler/GHC/Tc/Gen/Sig.hs
index 77d61941fc..abd204fa50 100644
--- a/compiler/GHC/Tc/Gen/Sig.hs
+++ b/compiler/GHC/Tc/Gen/Sig.hs
@@ -513,12 +513,12 @@ ppr_tvs tvs = braces (vcat [ ppr tv <+> dcolon <+> ppr (tyVarKind tv)
 
 tcInstSig :: TcIdSigInfo -> TcM TcIdSigInst
 -- Instantiate a type signature; only used with plan InferGen
-tcInstSig sig@(CompleteSig { sig_bndr = poly_id, sig_loc = loc })
+tcInstSig hs_sig@(CompleteSig { sig_bndr = poly_id, sig_loc = loc })
   = setSrcSpan loc $  -- Set the binding site of the tyvars
     do { (tv_prs, theta, tau) <- tcInstTypeBndrs (idType poly_id)
               -- See Note [Pattern bindings and complete signatures]
 
-       ; return (TISI { sig_inst_sig   = sig
+       ; return (TISI { sig_inst_sig   = hs_sig
                       , sig_inst_skols = tv_prs
                       , sig_inst_wcs   = []
                       , sig_inst_wcx   = Nothing
diff --git a/compiler/GHC/Tc/Solver.hs b/compiler/GHC/Tc/Solver.hs
index 3e900a6d9e..6c02ade8d2 100644
--- a/compiler/GHC/Tc/Solver.hs
+++ b/compiler/GHC/Tc/Solver.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE RecursiveDo #-}
+{-# LANGUAGE MultiWayIf, RecursiveDo #-}
 
 module GHC.Tc.Solver(
        InferMode(..), simplifyInfer, findInferredDiff,
@@ -1553,19 +1553,16 @@ decideQuantification skol_info infer_mode rhs_tclvl name_taus psigs candidates
        ; psig_theta <- TcM.zonkTcTypes (concatMap sig_inst_theta psigs)
        ; min_theta  <- pickQuantifiablePreds (mkVarSet qtvs) mono_tvs0 candidates
 
-       -- Add psig_theta back in here, even though it's already
-       -- part of candidates, because we always want to quantify over
-       -- psig_theta, and pickQuantifiableCandidates might have
-       -- dropped some e.g. CallStack constraints.  c.f #14658
-       --                   equalities (a ~ Bool)
-       -- It's helpful to use the same "find difference" algorithm here as
-       -- we use in GHC.Tc.Gen.Bind.chooseInferredQuantifiers (#20921)
+       -- Take account of partial type signatures
        -- See Note [Constraints in partial type signatures]
        ; let min_psig_theta = mkMinimalBySCs id psig_theta
-       ; theta <- if null psig_theta
-                  then return min_theta  -- Fast path for the non-partial-sig case
-                  else do { diff <- findInferredDiff min_psig_theta min_theta
-                          ; return (min_psig_theta ++ diff) }
+       ; theta <- if
+           | null psigs -> return min_theta                 -- Case (P3)
+           | not (all has_extra_constraints_wildcard psigs) -- Case (P2)
+             -> return min_psig_theta
+           | otherwise                                      -- Case (P1)
+             -> do { diff <- findInferredDiff min_psig_theta min_theta
+                   ; return (min_psig_theta ++ diff) }
 
        ; traceTc "decideQuantification"
            (vcat [ text "infer_mode:" <+> ppr infer_mode
@@ -1576,37 +1573,72 @@ decideQuantification skol_info infer_mode rhs_tclvl name_taus psigs candidates
                  , text "theta:"      <+> ppr theta ])
        ; return (qtvs, theta, co_vars) }
 
+  where
+    has_extra_constraints_wildcard (TISI { sig_inst_wcx = Just {} }) = True
+    has_extra_constraints_wildcard _                                 = False
+
 {- Note [Constraints in partial type signatures]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Suppose we have a partial type signature
-    f :: (Eq a, C a, _) => blah
+Suppose we have decided to quantify over min_theta, say (Eq a, C a, Ix a).
+Then we distinguish three cases:
+
+(P1) No partial type signatures: just quantify over min_theta
+
+(P2) Partial type signatures with no extra_constraints wildcard:
+      e.g.   f :: (Eq a, C a) => a -> _
+     Quantify over psig_theta: the user has explicitly specified the
+     entire context.
+
+     That may mean we have an unsolved residual constraint (Ix a) arising
+     from the RHS of the function. But so be it: the user said (Eq a, C a).
+
+(P3) Partial type signature with an extra_constraints wildcard.
+      e.g.   f :: (Eq a, C a, _) => a -> a
+    Quantify over (psig_theta ++ diff)
+      where diff = min_theta - psig_theta, using findInferredDiff.
+    In our example, diff = Ix a
+
+Some rationale and observations
+
+* See Note [When the MR applies] in GHC.Tc.Gen.Bind.
+
+* We always want to quantify over psig_theta (if present).  The user specified
+  it!  And pickQuantifiableCandidates might have dropped some
+  e.g. CallStack constraints.  c.f #14658
+       equalities (a ~ Bool)
 
-We will ultimately quantify f over (Eq a, C a, <diff>), where
+* In case (P3) we ask that /all/ the signatures have an extra-constraints
+  wildcard.  It's a bit arbitrary; not clear what the "right" thing is.
 
-   * <diff> is the result of
-         findInferredDiff (Eq a, C a) <quant-theta>
-     in GHC.Tc.Gen.Bind.chooseInferredQuantifiers
+* In (P2) we encounter #20076:
+     f :: Eq [a] => a -> _
+     f x = [x] == [x]
+  From the RHS we get [W] Eq [a].  We simplify those Wanteds in simplifyInfer,
+  to get (Eq a).  But then we quantify over the user-specified (Eq [a]), leaving
+  a residual implication constraint (forall a. Eq [a] => [W] Eq a), which is
+  insoluble.  Idea: in simplifyInfer we could put the /un-simplified/ constraints
+  in the residual -- at least in the case like #20076 where the partial signature
+  fully specifies the final constraint. Maybe: a battle for another day.
 
-   * <quant-theta> is the theta returned right here,
-     by decideQuantification
+* It's helpful to use the same "find difference" algorithm, `findInferredDiff`,
+  here as we use in GHC.Tc.Gen.Bind.chooseInferredQuantifiers (#20921)
 
-At least for single functions we would like to quantify f over
-precisely the same theta as <quant-theta>, so that we get to take
-the short-cut path in GHC.Tc.Gen.Bind.mkExport, and avoid calling
-tcSubTypeSigma for impedance matching. Why avoid?  Because it falls
-over for ambiguous types (#20921).
+  At least for single functions we would like to quantify f over precisely the
+  same theta as <quant-theta>, so that we get to take the short-cut path in
+  `GHC.Tc.Gen.Bind.mkExport`, and avoid calling `tcSubTypeSigma` for impedance
+  matching. Why avoid?  Because it falls over for ambiguous types (#20921).
 
-We can get precisely the same theta by using the same algorithm,
-findInferredDiff.
+  We can get precisely the same theta by using the same algorithm,
+  `findInferredDiff`.
 
-All of this goes wrong if we have (a) mutual recursion, (b) multiple
-partial type signatures, (c) with different constraints, and (d)
-ambiguous types.  Something like
+* All of this goes wrong if we have (a) mutual recursion, (b) multiple
+  partial type signatures, (c) with different constraints, and (d)
+  ambiguous types.  Something like
     f :: forall a. Eq a => F a -> _
     f x = (undefined :: a) == g x undefined
     g :: forall b. Show b => F b -> _ -> b
     g x y = let _ = (f y, show x) in x
-But that's a battle for another day.
+  But that's a battle for another day.
 -}
 
 decidePromotedTyVars :: InferMode
diff --git a/compiler/GHC/Tc/Types/Origin.hs b/compiler/GHC/Tc/Types/Origin.hs
index 9c72e2ac4e..41b48b6e71 100644
--- a/compiler/GHC/Tc/Types/Origin.hs
+++ b/compiler/GHC/Tc/Types/Origin.hs
@@ -591,9 +591,7 @@ data CtOrigin
   | IfThenElseOrigin    -- An if-then-else expression
   | BracketOrigin       -- An overloaded quotation bracket
   | StaticOrigin        -- A static form
-  | Shouldn'tHappenOrigin String
-                            -- the user should never see this one
-  | GhcBug20076             -- see #20076
+  | Shouldn'tHappenOrigin String  -- The user should never see this one
 
   -- | Testing whether the constraint associated with an instance declaration
   -- in a signature file is satisfied upon instantiation.
@@ -819,13 +817,6 @@ pprCtOrigin (Shouldn'tHappenOrigin note)
          , text "https://gitlab.haskell.org/ghc/ghc/wikis/report-a-bug >>"
          ]
 
-pprCtOrigin GhcBug20076
-  = vcat [ text "GHC Bug #20076 <https://gitlab.haskell.org/ghc/ghc/-/issues/20076>"
-         , text "Assuming you have a partial type signature, you can avoid this error"
-         , text "by either adding an extra-constraints wildcard (like `(..., _) => ...`,"
-         , text "with the underscore at the end of the constraint), or by avoiding the"
-         , text "use of a simplifiable constraint in your partial type signature." ]
-
 pprCtOrigin (ProvCtxtOrigin PSB{ psb_id = (L _ name) })
   = hang (ctoHerald <+> text "the \"provided\" constraints claimed by")
        2 (text "the signature of" <+> quotes (ppr name))
@@ -927,7 +918,6 @@ pprCtO (ProvCtxtOrigin {})          = text "a provided constraint"
 pprCtO (InstProvidedOrigin {})      = text "a provided constraint"
 pprCtO (CycleBreakerOrigin orig)    = pprCtO orig
 pprCtO (FRROrigin {})               = text "a representation-polymorphism check"
-pprCtO GhcBug20076                  = text "GHC Bug #20076"
 pprCtO (WantedSuperclassOrigin {})  = text "a superclass constraint"
 pprCtO (InstanceSigOrigin {})       = text "a type signature in an instance"
 pprCtO (AmbiguityCheckOrigin {})    = text "a type ambiguity check"