summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSimon Peyton Jones <simon.peytonjones@gmail.com>2023-04-07 22:21:53 +0100
committerKrzysztof Gogolewski <krzysztof.gogolewski@tweag.io>2023-04-14 20:01:02 +0200
commit3f2d0eb826cbd6414fe2f31085aec8e20fb2976f (patch)
treec2e76e07991609e68a4ee9f08ef82687833fe65e
parent99b2734b8a167d27d0066b331bfb4cf220326ce0 (diff)
downloadhaskell-3f2d0eb826cbd6414fe2f31085aec8e20fb2976f.tar.gz
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.
-rw-r--r--compiler/GHC/Tc/Gen/Bind.hs131
-rw-r--r--compiler/GHC/Tc/Gen/Sig.hs4
-rw-r--r--compiler/GHC/Tc/Solver.hs94
-rw-r--r--compiler/GHC/Tc/Types/Origin.hs12
-rw-r--r--testsuite/tests/partial-sigs/should_compile/T10403.stderr38
-rw-r--r--testsuite/tests/partial-sigs/should_compile/T19106.hs7
-rw-r--r--testsuite/tests/partial-sigs/should_compile/T20076.hs9
-rw-r--r--testsuite/tests/partial-sigs/should_compile/all.T3
-rw-r--r--testsuite/tests/partial-sigs/should_fail/T23223.hs5
-rw-r--r--testsuite/tests/partial-sigs/should_fail/T23223.stderr11
-rw-r--r--testsuite/tests/partial-sigs/should_fail/all.T5
11 files changed, 181 insertions, 138 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"
diff --git a/testsuite/tests/partial-sigs/should_compile/T10403.stderr b/testsuite/tests/partial-sigs/should_compile/T10403.stderr
index 37f5ad522b..ff45dc06fc 100644
--- a/testsuite/tests/partial-sigs/should_compile/T10403.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T10403.stderr
@@ -14,41 +14,17 @@ T10403.hs:16:12: warning: [GHC-88464] [-Wpartial-type-signatures (in -Wdefault)]
• In the type signature: h1 :: _ => _
T10403.hs:20:7: warning: [GHC-88464] [-Wpartial-type-signatures (in -Wdefault)]
- • Found type wildcard ‘_’
- standing for ‘(a1 -> a2) -> f0 a1 -> H f0’
- Where: ‘f0’ is an ambiguous type variable
- ‘a2’, ‘a1’ are rigid type variables bound by
- the inferred type of h2 :: (a1 -> a2) -> f0 a1 -> H f0
+ • Found type wildcard ‘_’ standing for ‘(a1 -> a2) -> f a1 -> H f’
+ Where: ‘a2’, ‘a1’, ‘f’ are rigid type variables bound by
+ the inferred type of h2 :: (a1 -> a2) -> f a1 -> H f
at T10403.hs:23:1-41
• In the type signature: h2 :: _
T10403.hs:23:15: warning: [GHC-39999] [-Wdeferred-type-errors (in -Wdefault)]
- • Ambiguous type variable ‘f0’ arising from a use of ‘fmap’
- prevents the constraint ‘(Functor f0)’ from being solved.
- Relevant bindings include
- b :: f0 a1 (bound at T10403.hs:23:6)
- h2 :: (a1 -> a2) -> f0 a1 -> H f0 (bound at T10403.hs:23:1)
- Probable fix: use a type annotation to specify what ‘f0’ should be.
- Potentially matching instances:
- instance Functor IO -- Defined in ‘GHC.Base’
- instance Functor (B t) -- Defined at T10403.hs:11:10
- ...plus 8 others
- ...plus one instance involving out-of-scope types
- (use -fprint-potential-instances to see them all)
+ • No instance for ‘Functor f’ arising from a use of ‘fmap’
+ Possible fix:
+ add (Functor f) to the context of
+ the inferred type of h2 :: (a1 -> a2) -> f a1 -> H f
• In the second argument of ‘(.)’, namely ‘fmap (const ())’
In the expression: (H . fmap (const ())) (fmap f b)
In an equation for ‘h2’: h2 f b = (H . fmap (const ())) (fmap f b)
-
-T10403.hs:29:8: warning: [GHC-46956] [-Wdeferred-type-errors (in -Wdefault)]
- • Couldn't match type ‘f0’ with ‘B t’
- Expected: H (B t)
- Actual: H f0
- • because type variable ‘t’ would escape its scope
- This (rigid, skolem) type variable is bound by
- the type signature for:
- app2 :: forall t. H (B t)
- at T10403.hs:28:1-15
- • In the expression: h2 (H . I) (B ())
- In an equation for ‘app2’: app2 = h2 (H . I) (B ())
- • Relevant bindings include
- app2 :: H (B t) (bound at T10403.hs:29:1)
diff --git a/testsuite/tests/partial-sigs/should_compile/T19106.hs b/testsuite/tests/partial-sigs/should_compile/T19106.hs
index 02f36744a0..9ed7cb058d 100644
--- a/testsuite/tests/partial-sigs/should_compile/T19106.hs
+++ b/testsuite/tests/partial-sigs/should_compile/T19106.hs
@@ -3,6 +3,13 @@
module T19106 where
+-- This is a very subtle program:
+-- From the body of the function we get [W] Show a
+-- That can be satisfied only from the /combination/ of
+-- [G] a ~ [b] from type sig
+-- [G] G a from pattern match (MkT x)
+-- The type instance G [b] = Show b
+
f :: (a ~ [b]) => T a -> _ -> String
f (MkT x) _ = show x
diff --git a/testsuite/tests/partial-sigs/should_compile/T20076.hs b/testsuite/tests/partial-sigs/should_compile/T20076.hs
new file mode 100644
index 0000000000..9d53d030a4
--- /dev/null
+++ b/testsuite/tests/partial-sigs/should_compile/T20076.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE FlexibleContexts, PartialTypeSignatures #-}
+
+module Bug where
+
+f :: Eq [a] => a -> _
+f x = [x] == [x]
+
+-- See Note [Constraints in partial type signatures] in
+-- GHC.Tc.Solver, in particular the bullet about (P2). \ No newline at end of file
diff --git a/testsuite/tests/partial-sigs/should_compile/all.T b/testsuite/tests/partial-sigs/should_compile/all.T
index 935d62231c..d421491b5a 100644
--- a/testsuite/tests/partial-sigs/should_compile/all.T
+++ b/testsuite/tests/partial-sigs/should_compile/all.T
@@ -71,7 +71,7 @@ test('T10519', normal, compile, [''])
test('T10463', normal, compile, [''])
test('ExprSigLocal', normal, compile, [''])
test('T11016', normal, compile, [''])
-test('T11192', normal, compile, [''])
+test('T11192', expect_broken(23232), compile, [''])
test('SuperCls', normal, compile, [''])
test('T12033', normal, compile, [''])
test('T11339a', normal, compile, [''])
@@ -107,3 +107,4 @@ test('InstanceGivenOverlap3', expect_broken(20076), compile, [''])
test('T21667', normal, compile, [''])
test('T22065', normal, compile, [''])
test('T16152', normal, compile, [''])
+test('T20076', expect_broken(20076), compile, [''])
diff --git a/testsuite/tests/partial-sigs/should_fail/T23223.hs b/testsuite/tests/partial-sigs/should_fail/T23223.hs
new file mode 100644
index 0000000000..79ccf61fcd
--- /dev/null
+++ b/testsuite/tests/partial-sigs/should_fail/T23223.hs
@@ -0,0 +1,5 @@
+{-# LANGUAGE PartialTypeSignatures #-}
+module Foo where
+
+f :: (Show a) => a -> _ -> Bool
+f x y = x>x
diff --git a/testsuite/tests/partial-sigs/should_fail/T23223.stderr b/testsuite/tests/partial-sigs/should_fail/T23223.stderr
new file mode 100644
index 0000000000..06c0262dc8
--- /dev/null
+++ b/testsuite/tests/partial-sigs/should_fail/T23223.stderr
@@ -0,0 +1,11 @@
+
+T23223.hs:5:10: error: [GHC-39999]
+ • Could not deduce ‘Ord a’ arising from a use of ‘>’
+ from the context: Show a
+ bound by the inferred type of f :: Show a => a -> w -> Bool
+ at T23223.hs:5:1-11
+ Possible fix:
+ add (Ord a) to the context of
+ the inferred type of f :: Show a => a -> w -> Bool
+ • In the expression: x > x
+ In an equation for ‘f’: f x y = x > x
diff --git a/testsuite/tests/partial-sigs/should_fail/all.T b/testsuite/tests/partial-sigs/should_fail/all.T
index 949f449452..01baa58d1f 100644
--- a/testsuite/tests/partial-sigs/should_fail/all.T
+++ b/testsuite/tests/partial-sigs/should_fail/all.T
@@ -1,6 +1,6 @@
test('AnnotatedConstraint', normal, compile_fail, [''])
test('AnnotatedConstraintNotForgotten', normal, compile_fail, [''])
-test('Defaulting1MROff', normal, compile, [''])
+test('Defaulting1MROff', expect_broken(23232), compile, [''])
test('ExtraConstraintsWildcardInExpressionSignature', normal, compile, [''])
test('ExtraConstraintsWildcardInPatternSignature', normal, compile_fail, [''])
test('ExtraConstraintsWildcardInPatternSplice', [req_interp, normal], compile_fail, [''])
@@ -58,7 +58,7 @@ test('WildcardInTypeSynonymRHS', normal, compile_fail, [''])
test('T10615', normal, compile_fail, [''])
test('T10045', normal, compile_fail, [''])
test('T10999', normalise_fun(normalise_errmsg), compile_fail, [''])
-test('T11122', normal, compile, [''])
+test('T11122', expect_broken(23232), compile, [''])
test('T11515', normal, compile_fail, [''])
test('T11976', normal, compile_fail, [''])
test('PatBind3', normal, compile_fail, [''])
@@ -72,3 +72,4 @@ test('T14449', normal, compile_fail, [''])
test('T14479', normal, compile_fail, [''])
test('T14584', normal, compile, [''])
test('T14584a', normal, compile, [''])
+test('T23223', normal, compile_fail, [''])