[Git][ghc/ghc][wip/andreask/9.10-backports] 4 commits: Consider Wanteds with rewriters as insoluble
Andreas Klebinger (@AndreasK)
gitlab at gitlab.haskell.org
Thu Feb 6 13:08:36 UTC 2025
Andreas Klebinger pushed to branch wip/andreask/9.10-backports at Glasgow Haskell Compiler / GHC
Commits:
128825be by Simon Peyton Jones at 2025-02-06T13:28:48+01:00
Consider Wanteds with rewriters as insoluble
This MR fixes #25325
See GHC.Tc.Types.Constraint, Note [Insoluble Wanteds], especially (IW2)
There is a small change in the error message for T14172, but it looks
entirely acceptable to me.
(cherry picked from commit 083703a12cd34369e7ed2f0efc4a5baee47aedab)
- - - - -
d6f6d927 by Simon Peyton Jones at 2025-02-06T13:29:07+01:00
Wibbles
(cherry picked from commit 0dfaeb66fb8457e7339abbd44d5c53a81ad8ae3a)
- - - - -
8ee0a3df by Simon Peyton Jones at 2025-02-06T13:29:14+01:00
Spelling errors
(cherry picked from commit 09d24d828e48c2588a317e6dad711f8673983703)
- - - - -
68d3ab8b by Arnaud Spiwack at 2025-02-06T13:45:53+01:00
Don't bypass MonoLocalBind in empty patterns
Fixes #25428
(cherry picked from commit 52d97f4ecd37bf598560dbded2d50649db5cfe1d)
- - - - -
8 changed files:
- compiler/GHC/Tc/Errors.hs
- compiler/GHC/Tc/Gen/Bind.hs
- compiler/GHC/Tc/Types/Constraint.hs
- testsuite/tests/linear/should_compile/all.T
- testsuite/tests/polykinds/T14172.stderr
- + testsuite/tests/typecheck/should_fail/T25325.hs
- + testsuite/tests/typecheck/should_fail/T25325.stderr
- testsuite/tests/typecheck/should_fail/all.T
Changes:
=====================================
compiler/GHC/Tc/Errors.hs
=====================================
@@ -465,6 +465,8 @@ mkErrorItem ct
flav = ctFlavour ct
; (suppress, m_evdest) <- case ctEvidence ct of
+ -- For this `suppress` stuff
+ -- see Note [Wanteds rewrite Wanteds] in GHC.Tc.Types.Constraint
CtGiven {} -> return (False, Nothing)
CtWanted { ctev_rewriters = rewriters, ctev_dest = dest }
-> do { rewriters' <- zonkRewriterSet rewriters
=====================================
compiler/GHC/Tc/Gen/Bind.hs
=====================================
@@ -723,7 +723,6 @@ it's all cool; each signature has distinct type variables from the renamer.)
{- Note [Non-variable pattern bindings aren't linear]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
A fundamental limitation of the typechecking algorithm is that we cannot have a
binding which, at the same time,
- is linear in its rhs
@@ -735,17 +734,35 @@ https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0111-linear
To address this we to do a few things
-- When a pattern is annotated with a multiplicity annotation `let %q pat = rhs
+- (NVP1) When a pattern is annotated with a multiplicity annotation `let %q pat = rhs
in body` (note: multiplicity-annotated bindings are always parsed as a
PatBind, see Note [Multiplicity annotations] in Language.Haskell.Syntax.Binds),
- then the let is never generalised (we use the NoGen plan).
-- Whenever the typechecker infers an AbsBind *and* the inner binding is a
+ then the let is never generalised (we use the NoGen plan). We do this with a
+ dedicated test in decideGeneralisationPlan.
+- (NVP2) Whenever the typechecker infers an AbsBind *and* the inner binding is a
non-variable PatBind, then the multiplicity of the binding is inferred to be
- Many. This is a little infelicitous: sometimes the typechecker infers an
- AbsBind where it didn't need to. This may cause some programs to be spuriously
- rejected, when NoMonoLocalBinds is on.
-- LinearLet implies MonoLocalBinds to avoid the AbsBind case altogether.
-
+ Many. We do this by calling manyIfPats in tcPolyInfer. This is a little
+ infelicitous: sometimes the typechecker infers an AbsBind where it didn't need
+ to. This may cause some programs to be spuriously rejected, when
+ NoMonoLocalBinds is on.
+- (NVP3) LinearLet implies MonoLocalBinds to avoid the AbsBind case altogether.
+- (NVP4) Wrinkle: even when other conditions (including MonoLocalBinds), GHC
+ will generalise some binders, namely so-called closed binding groups. We need
+ to make sure that the test for (NVP1) has priority over the test for closed
+ binders.
+- (NVP5) Wrinkle: Closed binding groups (NVP4) are usually fine to type with
+ multiplicity Many. But there's one exception: when there's no binder at all,
+ the binding group is considered closed. Even if the rhs contains arbitrary
+ variables.
+
+ f :: () %1 -> Bool
+ f x = let !() = x in True
+
+ If we consider `!() = x` as a generalisable group (which does nothing anyway),
+ then (NVP2) will infer the pattern as multiplicity Many, and reject the
+ function. We don't want that, see also #25428. So we take care not to
+ generalise in this case, by excluding the no-binder case from automatic
+ generalisation in decideGeneralisationPlan.
-}
tcPolyInfer
@@ -762,7 +779,7 @@ tcPolyInfer rec_tc prag_fn tc_sig_fn bind_list
; apply_mr <- checkMonomorphismRestriction mono_infos bind_list
-- AbsBinds which are PatBinds can't be linear.
- -- See Note [Non-variable pattern bindings aren't linear]
+ -- See (NVP2) in Note [Non-variable pattern bindings aren't linear]
; binds' <- manyIfPats binds'
; traceTc "tcPolyInfer" (ppr apply_mr $$ ppr (map mbi_sig mono_infos))
@@ -1871,12 +1888,17 @@ decideGeneralisationPlan dflags top_lvl closed sig_fn lbinds
-- See Note [Always generalise top-level bindings]
| has_mult_anns_and_pats = False
- -- See Note [Non-variable pattern bindings aren't linear]
+ -- See (NVP1) and (NVP4) in Note [Non-variable pattern bindings aren't linear]
- | IsGroupClosed _ True <- closed = True
+ | IsGroupClosed _ True <- closed
+ , not (null binders) = True
-- The 'True' means that all of the group's
-- free vars have ClosedTypeId=True; so we can ignore
- -- -XMonoLocalBinds, and generalise anyway
+ -- -XMonoLocalBinds, and generalise anyway.
+ -- Except if 'fv' is empty: there is no binder to generalise, so
+ -- generalising does nothing. And trying to generalise hurts linear
+ -- types (see #25428). So we don't force it.
+ -- See (NVP5) in Note [Non-variable pattern bindings aren't linear] in GHC.Tc.Gen.Bind.
| has_partial_sigs = True
-- See Note [Partial type signatures and generalisation]
=====================================
compiler/GHC/Tc/Types/Constraint.hs
=====================================
@@ -83,7 +83,7 @@ module GHC.Tc.Types.Constraint (
ctEvExpr, ctEvTerm, ctEvCoercion, ctEvEvId,
ctEvRewriters, ctEvUnique, tcEvDestUnique,
mkKindEqLoc, toKindLoc, toInvisibleLoc, mkGivenLoc,
- ctEvRole, setCtEvPredType, setCtEvLoc, arisesFromGivens,
+ ctEvRole, setCtEvPredType, setCtEvLoc,
tyCoVarsOfCtEvList, tyCoVarsOfCtEv, tyCoVarsOfCtEvsList,
-- RewriterSet
@@ -1312,25 +1312,51 @@ 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
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
+ -- It has no 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
@@ -1360,18 +1386,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
@@ -1415,6 +1429,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 are put into
+ CIrredCan
+
+(IW2) We only treat it as insoluble if it has an empty rewriter set. (See Note
+ [Wanteds rewrite Wanteds].) 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 because of its empty rewriter set; and suppress
+ reporting A because there is an insoluble B lying around. (This suppression
+ happens in GHC.Tc.Errors.mkErrorItem.) 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:
@@ -2056,9 +2095,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
=====================================
testsuite/tests/linear/should_compile/all.T
=====================================
@@ -46,4 +46,4 @@ test('T23814', normal, compile, [''])
test('LinearLet', normal, compile, [''])
test('LinearLetPoly', normal, compile, [''])
test('LinearListComprehension', normal, compile, ['-dlinear-core-lint'])
-test('T25428', expect_broken(25428), compile, [''])
+test('T25428', normal, compile, [''])
=====================================
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)
+
=====================================
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
=====================================
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)’
+
=====================================
testsuite/tests/typecheck/should_fail/all.T
=====================================
@@ -727,3 +727,4 @@ test('T24470a', normal, compile_fail, [''])
test('T24553', normal, compile_fail, [''])
test('T23739b', normal, compile_fail, [''])
+test('T25325', normal, compile_fail, [''])
\ No newline at end of file
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/e41456fca25b1407193536c4243dd19a82b40ab7...68d3ab8bc994cb540e4ee67aa20fe70cff8e0dfe
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/e41456fca25b1407193536c4243dd19a82b40ab7...68d3ab8bc994cb540e4ee67aa20fe70cff8e0dfe
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20250206/a7b2c48c/attachment-0001.html>
More information about the ghc-commits
mailing list