diff --git a/compiler/GHC/Tc/Types/Constraint.hs b/compiler/GHC/Tc/Types/Constraint.hs
index fadeab700aadc1469fc36c4934523998fc609b14..6816f80428d5839b2a16c9c8d6b19ad498edf023 100644
--- a/compiler/GHC/Tc/Types/Constraint.hs
+++ b/compiler/GHC/Tc/Types/Constraint.hs
@@ -76,7 +76,7 @@ module GHC.Tc.Types.Constraint (
ctEvPred, ctEvLoc, ctEvOrigin, ctEvEqRel,
ctEvExpr, ctEvTerm, ctEvCoercion, ctEvEvId,
ctEvRewriters, ctEvUnique, tcEvDestUnique,
- ctEvRewriteRole, ctEvRewriteEqRel, setCtEvPredType, setCtEvLoc, arisesFromGivens,
+ ctEvRewriteRole, ctEvRewriteEqRel, setCtEvPredType, setCtEvLoc,
tyCoVarsOfCtEvList, tyCoVarsOfCtEv, tyCoVarsOfCtEvsList,
-- RewriterSet
@@ -1331,10 +1331,10 @@ nonDefaultableTyVarsOfWC (WC { wc_simple = simples, wc_impl = implics, wc_errors
insolubleWC :: WantedConstraints -> Bool
insolubleWC (WC { wc_impl = implics, wc_simple = simples, wc_errors = errors })
= anyBag insolubleWantedCt simples
+ -- insolubleWantedCt: wanteds only: see Note [Given insolubles]
|| anyBag insolubleImplic implics
|| anyBag is_insoluble errors
-
- where
+ where
is_insoluble (DE_Hole hole) = isOutOfScopeHole hole -- See Note [Insoluble holes]
is_insoluble (DE_NotConcrete {}) = True
is_insoluble (DE_Multiplicity {}) = False
@@ -1342,15 +1342,41 @@ insolubleWC (WC { wc_impl = implics, wc_simple = simples, wc_errors = errors })
insolubleWantedCt :: Ct -> Bool
-- Definitely insoluble, in particular /excluding/ type-hole constraints
-- Namely:
--- a) an insoluble constraint as per 'insolubleCt', i.e. either
+-- a) an insoluble constraint as per 'insolubleirredCt', i.e. either
-- - an insoluble equality constraint (e.g. Int ~ Bool), or
-- - a custom type error constraint, TypeError msg :: Constraint
-- b) that does not arise from a Given or a Wanted/Wanted fundep interaction
+-- See Note [Insoluble Wanteds]
+insolubleWantedCt ct
+ | CIrredCan ir_ct <- ct
+ -- CIrredCan: see (IW1) in Note [Insoluble Wanteds]
+ , IrredCt { ir_ev = ev } <- ir_ct
+ , CtWanted { ctev_loc = loc, ctev_rewriters = rewriters } <- ev
+ -- It's a Wanted
+ , insolubleIrredCt ir_ct
+ -- It's insoluble
+ , isEmptyRewriterSet rewriters
+ -- rewriters; see (IW2) in Note [Insoluble Wanteds]
+ , not (isGivenLoc loc)
+ -- isGivenLoc: see (IW3) in Note [Insoluble Wanteds]
+ , not (isWantedWantedFunDepOrigin (ctLocOrigin loc))
+ -- origin check: see (IW4) in Note [Insoluble Wanteds]
+ = True
+
+ | otherwise
+ = False
+
+-- | Returns True of constraints that are definitely insoluble,
+-- as well as TypeError constraints.
+-- Can return 'True' for Given constraints, unlike 'insolubleWantedCt'.
--
--- See Note [Given insolubles].
-insolubleWantedCt ct = insolubleCt ct &&
- not (arisesFromGivens ct) &&
- not (isWantedWantedFunDepOrigin (ctOrigin ct))
+-- The function is tuned for application /after/ constraint solving
+-- i.e. assuming canonicalisation has been done
+-- That's why it looks only for IrredCt; all insoluble constraints
+-- are put into CIrredCan
+insolubleCt :: Ct -> Bool
+insolubleCt (CIrredCan ir_ct) = insolubleIrredCt ir_ct
+insolubleCt _ = False
insolubleIrredCt :: IrredCt -> Bool
-- Returns True of Irred constraints that are /definitely/ insoluble
@@ -1380,18 +1406,6 @@ insolubleIrredCt (IrredCt { ir_ev = ev, ir_reason = reason })
-- > Assert 'True _errMsg = ()
-- > Assert _check errMsg = errMsg
--- | Returns True of constraints that are definitely insoluble,
--- as well as TypeError constraints.
--- Can return 'True' for Given constraints, unlike 'insolubleWantedCt'.
---
--- The function is tuned for application /after/ constraint solving
--- i.e. assuming canonicalisation has been done
--- That's why it looks only for IrredCt; all insoluble constraints
--- are put into CIrredCan
-insolubleCt :: Ct -> Bool
-insolubleCt (CIrredCan ir_ct) = insolubleIrredCt ir_ct
-insolubleCt _ = False
-
-- | Does this hole represent an "out of scope" error?
-- See Note [Insoluble holes]
isOutOfScopeHole :: Hole -> Bool
@@ -1435,6 +1449,31 @@ in GHC.Tc.Errors), so we may fail to report anything at all! Yikes.
Bottom line: insolubleWC (called in GHC.Tc.Solver.setImplicationStatus)
should ignore givens even if they are insoluble.
+Note [Insoluble Wanteds]
+~~~~~~~~~~~~~~~~~~~~~~~~
+insolubleWantedCt returns True of a Wanted constraint that definitely
+can't be solved. But not quite all such constraints; see wrinkles.
+
+(IW1) insolubleWantedCt is tuned for application /after/ constraint
+ solving i.e. assuming canonicalisation has been done. That's why
+ it looks only for IrredCt; all insoluble constraints oare put into
+ CIrredCan
+
+(IW2) We only treat it as insoluble if it has an empty rewriter set.
+ Otherwise #25325 happens: a Wanted constraint A that is /not/ insoluble
+ rewrites some other Wanted constraint B, so B has A in its rewriter
+ set. Now B looks insoluble. The danger is that we'll suppress reporting
+ B becuase of its empty rewriter set; and suppress reporting A because
+ there is an insoluble B lying around. (This suppression happens in
+ GHC.Tc.Errors.) Solution: don't treat B as insoluble.
+
+(IW3) If the Wanted arises from a Given (how can that happen?), don't
+ treat it as a Wanted insoluble (obviously).
+
+(IW4) If the Wanted came from a Wanted/Wanted fundep interaction, don't
+ treat the constraint as insoluble. See Note [Suppressing confusing errors]
+ in GHC.Tc.Errors
+
Note [Insoluble holes]
~~~~~~~~~~~~~~~~~~~~~~
Hole constraints that ARE NOT treated as truly insoluble:
@@ -2095,9 +2134,6 @@ tcEvDestUnique (HoleDest co_hole) = varUnique (coHoleCoVar co_hole)
setCtEvLoc :: CtEvidence -> CtLoc -> CtEvidence
setCtEvLoc ctev loc = ctev { ctev_loc = loc }
-arisesFromGivens :: Ct -> Bool
-arisesFromGivens ct = isGivenCt ct || isGivenLoc (ctLoc ct)
-
-- | Set the type of CtEvidence.
--
-- This function ensures that the invariants on 'CtEvidence' hold, by updating
diff --git a/testsuite/tests/polykinds/T14172.stderr b/testsuite/tests/polykinds/T14172.stderr
index df3868fb6c5bcac01b3d552c7ad5280869115f4f..23fcc6356c466ce9c6a00b7b0c8d5b8ff71f0c9d 100644
--- a/testsuite/tests/polykinds/T14172.stderr
+++ b/testsuite/tests/polykinds/T14172.stderr
@@ -1,10 +1,7 @@
-
T14172.hs:7:46: error: [GHC-88464]
- • Found type wildcard ‘_’ standing for ‘a'’
- Where: ‘a'’ is a rigid type variable bound by
- the inferred type of
- traverseCompose :: (a -> f b) -> g a -> f (h a')
- at T14172.hs:8:1-46
+ • Found type wildcard ‘_’ standing for ‘a'1 :: k0’
+ Where: ‘k0’ is an ambiguous type variable
+ ‘a'1’ is an ambiguous type variable
To use the inferred type, enable PartialTypeSignatures
• In the first argument of ‘h’, namely ‘_’
In the first argument of ‘f’, namely ‘(h _)’
@@ -13,17 +10,19 @@ T14172.hs:7:46: error: [GHC-88464]
T14172.hs:8:19: error: [GHC-25897]
• Couldn't match type ‘a’ with ‘g'1 a'0’
- Expected: (f'0 a -> f (f'0 b)) -> g a -> f (h a')
- Actual: (Unwrapped (Compose f'0 g'1 a'0) -> f (Unwrapped (h a')))
- -> Compose f'0 g'1 a'0 -> f (h a')
+ Expected: (f'0 a -> f (f'0 b)) -> g a -> f (h a'1)
+ Actual: (Unwrapped (Compose f'0 g'1 a'0)
+ -> f (Unwrapped (h a'1)))
+ -> Compose f'0 g'1 a'0 -> f (h a'1)
‘a’ is a rigid type variable bound by
the inferred type of
- traverseCompose :: (a -> f b) -> g a -> f (h a')
+ traverseCompose :: (a -> f b) -> g a -> f (h a'1)
at T14172.hs:7:1-47
• In the first argument of ‘(.)’, namely ‘_Wrapping Compose’
In the expression: _Wrapping Compose . traverse
In an equation for ‘traverseCompose’:
traverseCompose = _Wrapping Compose . traverse
• Relevant bindings include
- traverseCompose :: (a -> f b) -> g a -> f (h a')
+ traverseCompose :: (a -> f b) -> g a -> f (h a'1)
(bound at T14172.hs:8:1)
+
diff --git a/testsuite/tests/typecheck/should_fail/T25325.hs b/testsuite/tests/typecheck/should_fail/T25325.hs
new file mode 100644
index 0000000000000000000000000000000000000000..560325fc55880b22a39792dd2c28835a70607051
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T25325.hs
@@ -0,0 +1,14 @@
+module T25325 where
+
+import Control.Monad.State
+
+data (f :+: g) a = Inl (f a) | Inr (g a)
+
+newtype Buggy f m = Buggy { thing :: m Int }
+
+class GhcBug f where
+ demo :: MonadState (Buggy f m) m => f (m Int) -> m Int
+
+instance (GhcBug f, GhcBug g) => GhcBug (f :+: g) where
+ demo (Inl l) = demo l
+ demo (Inr r) = demo r
diff --git a/testsuite/tests/typecheck/should_fail/T25325.stderr b/testsuite/tests/typecheck/should_fail/T25325.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..96e414cb865a4465c20a1b247a64d8fb6cf20d94
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T25325.stderr
@@ -0,0 +1,15 @@
+T25325.hs:14:20: error: [GHC-39999]
+ • Could not deduce ‘MonadState (Buggy g m) m’
+ arising from a use of ‘demo’
+ from the context: (GhcBug f, GhcBug g)
+ bound by the instance declaration at T25325.hs:12:10-49
+ or from: MonadState (Buggy (f :+: g) m) m
+ bound by the type signature for:
+ demo :: forall (m :: * -> *).
+ MonadState (Buggy (f :+: g) m) m =>
+ (:+:) f g (m Int) -> m Int
+ at T25325.hs:13:5-8
+ • In the expression: demo r
+ In an equation for ‘demo’: demo (Inr r) = demo r
+ In the instance declaration for ‘GhcBug (f :+: g)’
+
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 3b0bf5ac3129595f0223662954924e8ce36185b6..0949e1c33dde7c1f7f768d511ac0e46da9b3a1ba 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -730,3 +730,4 @@ test('T23739b', normal, compile_fail, [''])
test('T23739c', normal, compile_fail, [''])
test('T24868', normal, compile_fail, [''])
test('T24938', normal, compile_fail, [''])
+test('T25325', normal, compile_fail, [''])