[Git][ghc/ghc][master] Introduce warning for loopy superclass solve
Marge Bot (@marge-bot)
gitlab at gitlab.haskell.org
Tue Feb 14 16:32:30 UTC 2023
Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC
Commits:
9fb4ca89 by sheaf at 2023-02-14T11:31:49-05:00
Introduce warning for loopy superclass solve
Commit aed1974e completely re-engineered the treatment of loopy
superclass dictionaries in instance declarations. Unfortunately,
it has the potential to break (albeit in a rather minor way) user code.
To alleviate migration concerns, this commit re-introduces the old
behaviour. Any reliance on this old behaviour triggers a warning,
controlled by `-Wloopy-superclass-solve`. The warning text explains
that GHC might produce bottoming evidence, and provides a migration
strategy.
This allows us to provide a graceful migration period, alerting users
when they are relying on this unsound behaviour.
Fixes #22912 #22891 #20666 #22894 #22905
- - - - -
26 changed files:
- compiler/GHC/Driver/Flags.hs
- compiler/GHC/Tc/Errors/Ppr.hs
- compiler/GHC/Tc/Errors/Types.hs
- compiler/GHC/Tc/Solver/InertSet.hs
- compiler/GHC/Tc/Solver/Interact.hs
- compiler/GHC/Tc/Solver/Monad.hs
- compiler/GHC/Tc/TyCl/Instance.hs
- compiler/GHC/Tc/Types/Origin.hs-boot
- compiler/GHC/Types/Error/Codes.hs
- compiler/GHC/Types/Hint.hs
- compiler/GHC/Types/Hint/Ppr.hs
- docs/users_guide/9.6.1-notes.rst
- docs/users_guide/using-warnings.rst
- testsuite/tests/quantified-constraints/all.T
- + testsuite/tests/typecheck/should_compile/T20666b.hs
- + testsuite/tests/typecheck/should_compile/T20666b.stderr
- + testsuite/tests/typecheck/should_compile/T22891.hs
- + testsuite/tests/typecheck/should_compile/T22891.stderr
- + testsuite/tests/typecheck/should_compile/T22912.hs
- + testsuite/tests/typecheck/should_compile/T22912.stderr
- testsuite/tests/typecheck/should_compile/all.T
- testsuite/tests/typecheck/should_fail/T20666.stderr
- testsuite/tests/typecheck/should_fail/T20666a.stderr
- testsuite/tests/typecheck/should_fail/T6161.stderr
- testsuite/tests/typecheck/should_fail/all.T
- testsuite/tests/typecheck/should_fail/tcfail223.stderr
Changes:
=====================================
compiler/GHC/Driver/Flags.hs
=====================================
@@ -631,6 +631,7 @@ data WarningFlag =
| Opt_WarnGADTMonoLocalBinds -- Since 9.4
| Opt_WarnTypeEqualityOutOfScope -- Since 9.4
| Opt_WarnTypeEqualityRequiresOperators -- Since 9.4
+ | Opt_WarnLoopySuperclassSolve -- Since 9.6
| Opt_WarnTermVariableCapture -- Since 9.8
deriving (Eq, Ord, Show, Enum)
@@ -737,6 +738,7 @@ warnFlagNames wflag = case wflag of
Opt_WarnUnicodeBidirectionalFormatCharacters -> "unicode-bidirectional-format-characters" :| []
Opt_WarnGADTMonoLocalBinds -> "gadt-mono-local-binds" :| []
Opt_WarnTypeEqualityOutOfScope -> "type-equality-out-of-scope" :| []
+ Opt_WarnLoopySuperclassSolve -> "loopy-superclass-solve" :| []
Opt_WarnTypeEqualityRequiresOperators -> "type-equality-requires-operators" :| []
-- -----------------------------------------------------------------------------
@@ -853,6 +855,7 @@ standardWarnings -- see Note [Documenting warning flags]
Opt_WarnForallIdentifier,
Opt_WarnUnicodeBidirectionalFormatCharacters,
Opt_WarnGADTMonoLocalBinds,
+ Opt_WarnLoopySuperclassSolve,
Opt_WarnTypeEqualityRequiresOperators
]
=====================================
compiler/GHC/Tc/Errors/Ppr.hs
=====================================
@@ -8,6 +8,7 @@
{-# LANGUAGE TypeFamilies #-}
{-# OPTIONS_GHC -fno-warn-orphans #-} -- instance Diagnostic TcRnMessage
+{-# LANGUAGE InstanceSigs #-}
module GHC.Tc.Errors.Ppr
( pprTypeDoesNotHaveFixedRuntimeRep
@@ -1305,7 +1306,18 @@ instance Diagnostic TcRnMessage where
, text "Combine alternative minimal complete definitions with `|'" ]
where
sigs = sig1 : sig2 : otherSigs
-
+ TcRnLoopySuperclassSolve wtd_loc wtd_pty ->
+ mkSimpleDecorated $ vcat [ header, warning, user_manual ]
+ where
+ header, warning, user_manual :: SDoc
+ header
+ = vcat [ text "I am solving the constraint" <+> quotes (ppr wtd_pty) <> comma
+ , nest 2 $ pprCtOrigin (ctLocOrigin wtd_loc) <> comma
+ , text "in a way that might turn out to loop at runtime." ]
+ warning
+ = vcat [ text "Future versions of GHC will turn this warning into an error." ]
+ user_manual =
+ vcat [ text "See the user manual, § Undecidable instances and loopy superclasses." ]
diagnosticReason = \case
TcRnUnknownMessage m
@@ -1734,6 +1746,8 @@ instance Diagnostic TcRnMessage where
-> ErrorWithoutFlag
TcRnDuplicateMinimalSig{}
-> ErrorWithoutFlag
+ TcRnLoopySuperclassSolve{}
+ -> WarningWithFlag Opt_WarnLoopySuperclassSolve
diagnosticHints = \case
TcRnUnknownMessage m
@@ -2173,6 +2187,13 @@ instance Diagnostic TcRnMessage where
-> noHints
TcRnDuplicateMinimalSig{}
-> noHints
+ TcRnLoopySuperclassSolve wtd_loc wtd_pty
+ -> [LoopySuperclassSolveHint wtd_pty cls_or_qc]
+ where
+ cls_or_qc :: ClsInstOrQC
+ cls_or_qc = case ctLocOrigin wtd_loc of
+ ScOrigin c_or_q _ -> c_or_q
+ _ -> IsClsInst -- shouldn't happen
diagnosticCode = constructorCode
=====================================
compiler/GHC/Tc/Errors/Types.hs
=====================================
@@ -2924,6 +2924,23 @@ data TcRnMessage where
-}
TcRnDuplicateMinimalSig :: LSig GhcPs -> LSig GhcPs -> [LSig GhcPs] -> TcRnMessage
+ {-| TcRnLoopySuperclassSolve is a warning, controlled by @-Wloopy-superclass-solve@,
+ that is triggered when GHC solves a constraint in a possibly-loopy way,
+ violating the class instance termination rules described in the section
+ "Undecidable instances and loopy superclasses" of the user's guide.
+
+ Example:
+
+ class Foo f
+ class Foo f => Bar f g
+ instance Bar f f => Bar f (h k)
+
+ Test cases: T20666, T20666{a,b}, T22891, T22912.
+ -}
+ TcRnLoopySuperclassSolve :: CtLoc -- ^ Wanted 'CtLoc'
+ -> PredType -- ^ Wanted 'PredType'
+ -> TcRnMessage
+
deriving Generic
-- | Things forbidden in @type data@ declarations.
=====================================
compiler/GHC/Tc/Solver/InertSet.hs
=====================================
@@ -1633,10 +1633,17 @@ mightEqualLater inert_set given_pred given_loc wanted_pred wanted_loc
= False
can_unify lhs_tv _other _rhs_ty = mentions_meta_ty_var lhs_tv
-prohibitedSuperClassSolve :: CtLoc -- ^ is it loopy to use this one ...
- -> CtLoc -- ^ ... to solve this one?
- -> Bool -- ^ True ==> don't solve it
--- See Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance, (sc2)
+-- | Is it (potentially) loopy to use the first @ct1@ to solve @ct2@?
+--
+-- Necessary (but not sufficient) conditions for this function to return @True@:
+--
+-- - @ct1@ and @ct2@ both arise from superclass expansion,
+-- - @ct1@ is a Given and @ct2@ is a Wanted.
+--
+-- See Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance, (sc2).
+prohibitedSuperClassSolve :: CtLoc -- ^ is it loopy to use this one ...
+ -> CtLoc -- ^ ... to solve this one?
+ -> Bool -- ^ True ==> don't solve it
prohibitedSuperClassSolve given_loc wanted_loc
| GivenSCOrigin _ _ blocked <- ctLocOrigin given_loc
, blocked
=====================================
compiler/GHC/Tc/Solver/Interact.hs
=====================================
@@ -449,7 +449,7 @@ instance Outputable InteractResult where
solveOneFromTheOther :: Ct -- Inert (Dict or Irred)
-> Ct -- WorkItem (same predicate as inert)
- -> TcS InteractResult
+ -> InteractResult
-- Precondition:
-- * inert and work item represent evidence for the /same/ predicate
-- * Both are CDictCan or CIrredCan
@@ -461,28 +461,28 @@ solveOneFromTheOther :: Ct -- Inert (Dict or Irred)
solveOneFromTheOther ct_i ct_w
| CtWanted { ctev_loc = loc_w } <- ev_w
, prohibitedSuperClassSolve loc_i loc_w
+ -- See Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance
= -- Inert must be Given
- do { traceTcS "prohibitedClassSolve1" (ppr ev_i $$ ppr ev_w)
- ; return KeepWork }
+ KeepWork
| CtWanted {} <- ev_w
= -- Inert is Given or Wanted
case ev_i of
- CtGiven {} -> return KeepInert
+ CtGiven {} -> KeepInert
-- work is Wanted; inert is Given: easy choice.
CtWanted {} -- Both are Wanted
-- If only one has no pending superclasses, use it
-- Otherwise we can get infinite superclass expansion (#22516)
-- in silly cases like class C T b => C a b where ...
- | not is_psc_i, is_psc_w -> return KeepInert
- | is_psc_i, not is_psc_w -> return KeepWork
+ | not is_psc_i, is_psc_w -> KeepInert
+ | is_psc_i, not is_psc_w -> KeepWork
-- If only one is a WantedSuperclassOrigin (arising from expanding
-- a Wanted class constraint), keep the other: wanted superclasses
-- may be unexpected by users
- | not is_wsc_orig_i, is_wsc_orig_w -> return KeepInert
- | is_wsc_orig_i, not is_wsc_orig_w -> return KeepWork
+ | not is_wsc_orig_i, is_wsc_orig_w -> KeepInert
+ | is_wsc_orig_i, not is_wsc_orig_w -> KeepWork
-- otherwise, just choose the lower span
-- reason: if we have something like (abs 1) (where the
@@ -490,29 +490,28 @@ solveOneFromTheOther ct_i ct_w
-- get an error about abs than about 1.
-- This test might become more elaborate if we see an
-- opportunity to improve the error messages
- | ((<) `on` ctLocSpan) loc_i loc_w -> return KeepInert
- | otherwise -> return KeepWork
+ | ((<) `on` ctLocSpan) loc_i loc_w -> KeepInert
+ | otherwise -> KeepWork
-- From here on the work-item is Given
| CtWanted { ctev_loc = loc_i } <- ev_i
, prohibitedSuperClassSolve loc_w loc_i
- = do { traceTcS "prohibitedClassSolve2" (ppr ev_i $$ ppr ev_w)
- ; return KeepInert } -- Just discard the un-usable Given
- -- This never actually happens because
- -- Givens get processed first
+ = KeepInert -- Just discard the un-usable Given
+ -- This never actually happens because
+ -- Givens get processed first
| CtWanted {} <- ev_i
- = return KeepWork
+ = KeepWork
-- From here on both are Given
-- See Note [Replacement vs keeping]
| lvl_i == lvl_w
- = return same_level_strategy
+ = same_level_strategy
| otherwise -- Both are Given, levels differ
- = return different_level_strategy
+ = different_level_strategy
where
ev_i = ctEvidence ct_i
ev_w = ctEvidence ct_w
@@ -662,14 +661,12 @@ interactIrred inerts ct_w@(CIrredCan { cc_ev = ev_w, cc_reason = reason })
, ((ct_i, swap) : _rest) <- bagToList matching_irreds
-- See Note [Multiple matching irreds]
, let ev_i = ctEvidence ct_i
- = do { what_next <- solveOneFromTheOther ct_i ct_w
- ; traceTcS "iteractIrred" $
+ = do { traceTcS "iteractIrred" $
vcat [ text "wanted:" <+> (ppr ct_w $$ ppr (ctOrigin ct_w))
- , text "inert: " <+> (ppr ct_i $$ ppr (ctOrigin ct_i))
- , ppr what_next ]
- ; case what_next of
+ , text "inert: " <+> (ppr ct_i $$ ppr (ctOrigin ct_i)) ]
+ ; case solveOneFromTheOther ct_i ct_w of
KeepInert -> do { setEvBindIfWanted ev_w (swap_me swap ev_i)
- ; return (Stop ev_w (text "Irred equal" <+> parens (ppr what_next))) }
+ ; return (Stop ev_w (text "Irred equal:KeepInert" <+> ppr ct_w)) }
KeepWork -> do { setEvBindIfWanted ev_i (swap_me swap ev_w)
; updInertIrreds (\_ -> others)
; continueWith ct_w } }
@@ -1007,7 +1004,9 @@ and Given/instance fundeps entirely.
interactDict :: InertCans -> Ct -> TcS (StopOrContinue Ct)
interactDict inerts ct_w@(CDictCan { cc_ev = ev_w, cc_class = cls, cc_tyargs = tys })
| Just ct_i <- lookupInertDict inerts (ctEvLoc ev_w) cls tys
- , let ev_i = ctEvidence ct_i
+ , let ev_i = ctEvidence ct_i
+ loc_i = ctEvLoc ev_i
+ loc_w = ctEvLoc ev_w
= -- There is a matching dictionary in the inert set
do { -- First to try to solve it /completely/ from top level instances
-- See Note [Shortcut solving]
@@ -1015,16 +1014,24 @@ interactDict inerts ct_w@(CDictCan { cc_ev = ev_w, cc_class = cls, cc_tyargs = t
; short_cut_worked <- shortCutSolver dflags ev_w ev_i
; if short_cut_worked
then stopWith ev_w "interactDict/solved from instance"
- else
- do { -- Ths short-cut solver didn't fire, so we
- -- solve ev_w from the matching inert ev_i we found
- what_next <- solveOneFromTheOther ct_i ct_w
- ; traceTcS "lookupInertDict" (ppr what_next)
- ; case what_next of
- KeepInert -> do { setEvBindIfWanted ev_w (ctEvTerm ev_i)
- ; return $ Stop ev_w (text "Dict equal" <+> parens (ppr what_next)) }
- KeepWork -> do { setEvBindIfWanted ev_i (ctEvTerm ev_w)
+ -- Next see if we are in "loopy-superclass" land. If so,
+ -- we don't want to replace the (Given) inert with the
+ -- (Wanted) work-item, or vice versa; we want to hang on
+ -- to both, and try to solve the work-item via an instance.
+ -- See Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance
+ else if prohibitedSuperClassSolve loc_i loc_w
+ then continueWith ct_w
+ else
+ do { -- The short-cut solver didn't fire, and loopy superclasses
+ -- are dealt with, so we can either solve
+ -- the inert from the work-item or vice-versa.
+ ; case solveOneFromTheOther ct_i ct_w of
+ KeepInert -> do { traceTcS "lookupInertDict:KeepInert" (ppr ct_w)
+ ; setEvBindIfWanted ev_w (ctEvTerm ev_i)
+ ; return $ Stop ev_w (text "Dict equal" <+> ppr ct_w) }
+ KeepWork -> do { traceTcS "lookupInertDict:KeepWork" (ppr ct_w)
+ ; setEvBindIfWanted ev_i (ctEvTerm ev_w)
; updInertDicts $ \ ds -> delDict ds cls tys
; continueWith ct_w } } }
@@ -1894,7 +1901,7 @@ as the fundeps.
#7875 is a case in point.
-}
-doTopFundepImprovement :: Ct -> TcS (StopOrContinue Ct)
+doTopFundepImprovement :: Ct -> TcS ()
-- Try to functional-dependency improvement between the constraint
-- and the top-level instance declarations
-- See Note [Fundeps with instances, and equality orientation]
@@ -1904,8 +1911,7 @@ doTopFundepImprovement work_item@(CDictCan { cc_ev = ev, cc_class = cls
= do { traceTcS "try_fundeps" (ppr work_item)
; instEnvs <- getInstEnvs
; let fundep_eqns = improveFromInstEnv instEnvs mk_ct_loc cls xis
- ; emitFunDepWanteds (ctEvRewriters ev) fundep_eqns
- ; continueWith work_item }
+ ; emitFunDepWanteds (ctEvRewriters ev) fundep_eqns }
where
dict_pred = mkClassPred cls xis
dict_loc = ctEvLoc ev
@@ -2276,14 +2282,35 @@ doTopReactDict inerts work_item@(CDictCan { cc_ev = ev, cc_class = cls
; chooseInstance work_item lkup_res }
_ -> -- NoInstance or NotSure
-- We didn't solve it; so try functional dependencies with
- -- the instance environment, and return
- doTopFundepImprovement work_item }
+ -- the instance environment
+ do { doTopFundepImprovement work_item
+ ; tryLastResortProhibitedSuperclass inerts work_item } }
where
dict_loc = ctEvLoc ev
doTopReactDict _ w = pprPanic "doTopReactDict" (ppr w)
+-- | As a last resort, we TEMPORARILY allow a prohibited superclass solve,
+-- emitting a loud warning when doing so: we might be creating non-terminating
+-- evidence (as we are in T22912 for example).
+--
+-- See Note [Migrating away from loopy superclass solving] in GHC.Tc.TyCl.Instance.
+tryLastResortProhibitedSuperclass :: InertSet -> Ct -> TcS (StopOrContinue Ct)
+tryLastResortProhibitedSuperclass inerts
+ work_item@(CDictCan { cc_ev = ev_w, cc_class = cls, cc_tyargs = xis })
+ | let loc_w = ctEvLoc ev_w
+ orig_w = ctLocOrigin loc_w
+ , ScOrigin _ NakedSc <- orig_w -- work_item is definitely Wanted
+ , Just ct_i <- lookupInertDict (inert_cans inerts) loc_w cls xis
+ , let ev_i = ctEvidence ct_i
+ , isGiven ev_i
+ = do { setEvBindIfWanted ev_w (ctEvTerm ev_i)
+ ; ctLocWarnTcS loc_w $
+ TcRnLoopySuperclassSolve loc_w (ctPred work_item)
+ ; return $ Stop ev_w (text "Loopy superclass") }
+tryLastResortProhibitedSuperclass _ work_item
+ = continueWith work_item
chooseInstance :: Ct -> ClsInstResult -> TcS (StopOrContinue Ct)
chooseInstance work_item
=====================================
compiler/GHC/Tc/Solver/Monad.hs
=====================================
@@ -15,7 +15,7 @@ module GHC.Tc.Solver.Monad (
-- The TcS monad
TcS, runTcS, runTcSEarlyAbort, runTcSWithEvBinds, runTcSInerts,
- failTcS, warnTcS, addErrTcS, wrapTcS,
+ failTcS, warnTcS, addErrTcS, wrapTcS, ctLocWarnTcS,
runTcSEqualities,
nestTcS, nestImplicTcS, setEvBindsTcS,
emitImplicationTcS, emitTvImplicationTcS,
@@ -673,16 +673,18 @@ lookupInInerts :: CtLoc -> TcPredType -> TcS (Maybe CtEvidence)
lookupInInerts loc pty
| ClassPred cls tys <- classifyPredType pty
= do { inerts <- getTcSInerts
- ; return $ -- Maybe monad
- do { found_ev <-
- lookupSolvedDict inerts loc cls tys `mplus`
- fmap ctEvidence (lookupInertDict (inert_cans inerts) loc cls tys)
- ; guard (not (prohibitedSuperClassSolve (ctEvLoc found_ev) loc))
- -- We're about to "solve" the wanted we're looking up, so we
- -- must make sure doing so wouldn't run afoul of
- -- Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance.
- -- Forgetting this led to #20666.
- ; return found_ev }}
+ ; let mb_solved = lookupSolvedDict inerts loc cls tys
+ mb_inert = fmap ctEvidence (lookupInertDict (inert_cans inerts) loc cls tys)
+ ; return $ do -- Maybe monad
+ found_ev <- mb_solved `mplus` mb_inert
+
+ -- We're about to "solve" the wanted we're looking up, so we
+ -- must make sure doing so wouldn't run afoul of
+ -- Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance.
+ -- Forgetting this led to #20666.
+ guard $ not (prohibitedSuperClassSolve (ctEvLoc found_ev) loc)
+
+ return found_ev }
| otherwise -- NB: No caching for equalities, IPs, holes, or errors
= return Nothing
@@ -855,6 +857,10 @@ warnTcS msg = wrapTcS (TcM.addDiagnostic msg)
addErrTcS = wrapTcS . TcM.addErr
panicTcS doc = pprPanic "GHC.Tc.Solver.Canonical" doc
+-- | Emit a warning within the 'TcS' monad at the location given by the 'CtLoc'.
+ctLocWarnTcS :: CtLoc -> TcRnMessage -> TcS ()
+ctLocWarnTcS loc msg = wrapTcS $ TcM.setCtLocM loc $ TcM.addDiagnostic msg
+
traceTcS :: String -> SDoc -> TcS ()
traceTcS herald doc = wrapTcS (TcM.traceTc herald doc)
{-# INLINE traceTcS #-} -- see Note [INLINE conditional tracing utilities]
=====================================
compiler/GHC/Tc/TyCl/Instance.hs
=====================================
@@ -1661,6 +1661,20 @@ Answer:
superclass selection, except at a smaller type. This test is
implemented by GHC.Tc.Solver.InertSet.prohibitedSuperClassSolve
+Note [Migrating away from loopy superclass solving]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The logic from Note [Solving superclass constraints] was implemented in GHC 9.6.
+However, we want to provide a migration strategy for users, to avoid suddenly
+breaking their code going when upgrading to GHC 9.6. To this effect, we temporarily
+continue to allow the constraint solver to create these potentially non-terminating
+solutions, but emit a loud warning when doing so: see
+GHC.Tc.Solver.Interact.tryLastResortProhibitedSuperclass.
+
+Users can silence the warning by manually adding the necessary constraint to the
+context. GHC will then keep this user-written Given, dropping the Given arising
+from superclass expansion which has greater SC depth, as explained in
+Note [Replacement vs keeping] in GHC.Tc.Solver.Interact.
+
Note [Silent superclass arguments] (historical interest only)
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
NB1: this note describes our *old* solution to the
=====================================
compiler/GHC/Tc/Types/Origin.hs-boot
=====================================
@@ -7,4 +7,8 @@ data SkolemInfo
data FixedRuntimeRepContext
data FixedRuntimeRepOrigin
+data CtOrigin
+data ClsInstOrQC = IsClsInst
+ | IsQC CtOrigin
+
unkSkol :: HasCallStack => SkolemInfo
=====================================
compiler/GHC/Types/Error/Codes.hs
=====================================
@@ -512,6 +512,7 @@ type family GhcDiagnosticCode c = n | n -> c where
GhcDiagnosticCode "TcRnUnexpectedDefaultSig" = 40700
GhcDiagnosticCode "TcRnBindInBootFile" = 11247
GhcDiagnosticCode "TcRnDuplicateMinimalSig" = 85346
+ GhcDiagnosticCode "TcRnLoopySuperclassSolve" = 36038
-- IllegalNewtypeReason
GhcDiagnosticCode "DoesNotHaveSingleField" = 23517
=====================================
compiler/GHC/Types/Hint.hs
=====================================
@@ -32,11 +32,13 @@ import GHC.Unit.Module (ModuleName, Module)
import GHC.Hs.Extension (GhcTc)
import GHC.Core.Coercion
import GHC.Core.FamInstEnv (FamFlavor)
+import GHC.Core.Type (PredType)
import GHC.Types.Fixity (LexicalFixity(..))
import GHC.Types.Name (Name, NameSpace, OccName (occNameFS), isSymOcc, nameOccName)
import GHC.Types.Name.Reader (RdrName (Unqual), ImpDeclSpec)
import GHC.Types.SrcLoc (SrcSpan)
import GHC.Types.Basic (Activation, RuleName)
+import {-# SOURCE #-} GHC.Tc.Types.Origin ( ClsInstOrQC(..) )
import GHC.Parser.Errors.Basic
import {-# SOURCE #-} Language.Haskell.Syntax.Expr
import GHC.Unit.Module.Imported (ImportedModsVal)
@@ -429,6 +431,8 @@ data GhcHint
-}
| SuggestRenameTypeVariable
+ | LoopySuperclassSolveHint PredType ClsInstOrQC
+
-- | An 'InstantiationSuggestion' for a '.hsig' file. This is generated
-- by GHC in case of a 'DriverUnexpectedSignature' and suggests a way
-- to instantiate a particular signature, where the first argument is
=====================================
compiler/GHC/Types/Hint/Ppr.hs
=====================================
@@ -14,6 +14,7 @@ import GHC.Types.Hint
import GHC.Core.FamInstEnv (FamFlavor(..))
import GHC.Hs.Expr () -- instance Outputable
+import {-# SOURCE #-} GHC.Tc.Types.Origin ( ClsInstOrQC(..) )
import GHC.Types.Id
import GHC.Types.Name (NameSpace, pprDefinedAt, occNameSpace, pprNameSpace, isValNameSpace, nameModule)
import GHC.Types.Name.Reader (RdrName,ImpDeclSpec (..), rdrNameOcc, rdrNameSpace)
@@ -214,6 +215,14 @@ instance Outputable GhcHint where
mod = nameModule name
SuggestRenameTypeVariable
-> text "Consider renaming the type variable."
+ LoopySuperclassSolveHint pty cls_or_qc
+ -> vcat [ text "Add the constraint" <+> quotes (ppr pty) <+> text "to the" <+> what <> comma
+ , text "even though it seems logically implied by other constraints in the context." ]
+ where
+ what :: SDoc
+ what = case cls_or_qc of
+ IsClsInst -> text "instance context"
+ IsQC {} -> text "context of the quantified constraint"
perhapsAsPat :: SDoc
perhapsAsPat = text "Perhaps you meant an as-pattern, which must not be surrounded by whitespace"
=====================================
docs/users_guide/9.6.1-notes.rst
=====================================
@@ -3,10 +3,36 @@
Version 9.6.1
==============
-
Language
~~~~~~~~
+- GHC is now more conservative when solving constraints that arise from
+ superclass expansion in terms of other constraints that also arise from
+ superclass expansion.
+
+ For example: ::
+
+ class C a
+ class C a => D a b
+ instance D a a => D a b
+
+ When typechecking the instance, we need to also solve the constraints arising
+ from the superclasses of ``D``; in this case, we need ``C a``. We could obtain
+ evidence for this constraint by expanding the superclasses of the context,
+ as ``D a a`` also has a superclass context of ``C a``.
+ However, is it unsound to do so in general, as we might be assuming precisely
+ the predicate we want to prove! This can lead to programs that loop at runtime.
+
+ When such potentially-loopy situations arise, GHC now emits a warning.
+ In future releases, this behaviour will no longer be supported, and the
+ typechecker will outright refuse to solve these constraints, emitting a
+ ``Could not deduce`` error.
+
+ In practice, you should be able to fix these issues by adding the necessary
+ constraint to the context, e.g. for the above example: ::
+
+ instance (C a, D a a) => D a b
+
- Record updates for GADTs and other existential datatypes are now
fully supported.
=====================================
docs/users_guide/using-warnings.rst
=====================================
@@ -2319,6 +2319,22 @@ of ``-W(no-)*``.
triggered whenever this happens, and can be addressed by enabling the
extension.
+.. ghc-flag:: -Wloopy-superclass-solve
+ :shortdesc: warn when creating potentially-loopy superclass constraint evidence
+ :type: dynamic
+ :reverse: -Wno-loopy-superclass-solve
+
+ :since: 9.6.1
+
+ As explained in :ref:`undecidable_instances`, when using
+ :extension:`UndecidableInstances` it is possible for GHC to construct
+ non-terminating evidence for certain superclass constraints.
+
+ This behaviour is scheduled to be removed in a future GHC version.
+ In the meantime, GHC emits this warning to inform users of potential
+ non-termination. Users can manually add the required constraint to the context
+ to avoid the problem (thus silencing the warning).
+
.. ghc-flag:: -Wterm-variable-capture
:shortdesc: warn when an implicitly quantified type variable captures a term's name
:type: dynamic
=====================================
testsuite/tests/quantified-constraints/all.T
=====================================
@@ -41,3 +41,4 @@ test('T22216d', normal, compile, [''])
test('T22216e', normal, compile, [''])
test('T22223', normal, compile, [''])
test('T19690', normal, compile_fail, [''])
+
=====================================
testsuite/tests/typecheck/should_compile/T20666b.hs
=====================================
@@ -0,0 +1,12 @@
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE TypeFamilies #-}
+
+module T20666b where
+
+type family F a
+
+class Eq (F a) => D a
+class Eq (F a) => C a
+
+instance D [a] => C [a]
+
=====================================
testsuite/tests/typecheck/should_compile/T20666b.stderr
=====================================
@@ -0,0 +1,10 @@
+
+T20666b.hs:11:10: warning: [GHC-36038] [-Wloopy-superclass-solve (in -Wdefault)]
+ I am solving the constraint ‘Eq (F [a])’,
+ arising from the superclasses of an instance declaration,
+ in a way that might turn out to loop at runtime.
+ Future versions of GHC will turn this warning into an error.
+ See the user manual, § Undecidable instances and loopy superclasses.
+ Suggested fix:
+ Add the constraint ‘Eq (F [a])’ to the instance context,
+ even though it seems logically implied by other constraints in the context.
=====================================
testsuite/tests/typecheck/should_compile/T22891.hs
=====================================
@@ -0,0 +1,9 @@
+{-# LANGUAGE UndecidableInstances #-}
+
+module T22891 where
+
+class Foo f
+
+class Foo f => Bar f g
+
+instance Bar f f => Bar f (h k)
=====================================
testsuite/tests/typecheck/should_compile/T22891.stderr
=====================================
@@ -0,0 +1,10 @@
+
+T22891.hs:9:10: warning: [GHC-36038] [-Wloopy-superclass-solve (in -Wdefault)]
+ I am solving the constraint ‘Foo f’,
+ arising from the superclasses of an instance declaration,
+ in a way that might turn out to loop at runtime.
+ Future versions of GHC will turn this warning into an error.
+ See the user manual, § Undecidable instances and loopy superclasses.
+ Suggested fix:
+ Add the constraint ‘Foo f’ to the instance context,
+ even though it seems logically implied by other constraints in the context.
=====================================
testsuite/tests/typecheck/should_compile/T22912.hs
=====================================
@@ -0,0 +1,26 @@
+{-# LANGUAGE MonoLocalBinds #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE UndecidableSuperClasses #-}
+
+module T22912 where
+
+
+class c => Exactly c
+instance c => Exactly c
+class c => Implies c
+
+data Dict c = c => Dict
+
+anythingDict :: forall c. Dict c
+anythingDict = go
+ where
+ go :: (Exactly (Implies c) => Implies c) => Dict c
+ go = Dict
+
+-- This is clearly wrong: we shouldn't be able to produce evidence
+-- for any constraint whatsoever! However, GHC can be tricked into
+-- producing a bottom dictionary.
+-- This test checks that it emits an appropriate warning when doing so,
+-- to allow users to adapt their code before we plug the hole completely.
=====================================
testsuite/tests/typecheck/should_compile/T22912.stderr
=====================================
@@ -0,0 +1,12 @@
+
+T22912.hs:17:16: warning: [GHC-36038] [-Wloopy-superclass-solve (in -Wdefault)]
+ I am solving the constraint ‘Implies c’,
+ arising from the head of a quantified constraint
+ arising from a use of ‘go’,
+ in a way that might turn out to loop at runtime.
+ Future versions of GHC will turn this warning into an error.
+ See the user manual, § Undecidable instances and loopy superclasses.
+ Suggested fix:
+ Add the constraint ‘Implies
+ c’ to the context of the quantified constraint,
+ even though it seems logically implied by other constraints in the context.
=====================================
testsuite/tests/typecheck/should_compile/all.T
=====================================
@@ -857,3 +857,6 @@ test('T22647', normal, compile, [''])
test('T19577', normal, compile, [''])
test('T22383', normal, compile, [''])
test('T21501', normal, compile, [''])
+test('T20666b', normal, compile, [''])
+test('T22891', normal, compile, [''])
+test('T22912', normal, compile, [''])
=====================================
testsuite/tests/typecheck/should_fail/T20666.stderr
=====================================
@@ -1,20 +1,20 @@
-T20666.hs:13:10: error: [GHC-39999]
- • Could not deduce ‘Show (T c)’
- arising from the superclasses of an instance declaration
- from the context: (D d, c ~ S d)
- bound by the instance declaration at T20666.hs:13:10-31
- Possible fix:
- If the constraint looks soluble from a superclass of the instance context,
- read 'Undecidable instances and loopy superclasses' in the user manual
- • In the instance declaration for ‘C1 c’
+T20666.hs:13:10: warning: [GHC-36038] [-Wloopy-superclass-solve (in -Wdefault)]
+ I am solving the constraint ‘Show (T c)’,
+ arising from the superclasses of an instance declaration,
+ in a way that might turn out to loop at runtime.
+ Future versions of GHC will turn this warning into an error.
+ See the user manual, § Undecidable instances and loopy superclasses.
+ Suggested fix:
+ Add the constraint ‘Show (T c)’ to the instance context,
+ even though it seems logically implied by other constraints in the context.
-T20666.hs:17:10: error: [GHC-39999]
- • Could not deduce ‘Show (T c)’
- arising from the superclasses of an instance declaration
- from the context: (D d, c ~ S d, c' ~ c)
- bound by the instance declaration at T20666.hs:17:10-40
- Possible fix:
- If the constraint looks soluble from a superclass of the instance context,
- read 'Undecidable instances and loopy superclasses' in the user manual
- • In the instance declaration for ‘C2 c'’
+T20666.hs:17:10: warning: [GHC-36038] [-Wloopy-superclass-solve (in -Wdefault)]
+ I am solving the constraint ‘Show (T c)’,
+ arising from the superclasses of an instance declaration,
+ in a way that might turn out to loop at runtime.
+ Future versions of GHC will turn this warning into an error.
+ See the user manual, § Undecidable instances and loopy superclasses.
+ Suggested fix:
+ Add the constraint ‘Show (T c)’ to the instance context,
+ even though it seems logically implied by other constraints in the context.
=====================================
testsuite/tests/typecheck/should_fail/T20666a.stderr
=====================================
@@ -1,10 +1,10 @@
-T20666a.hs:11:10: error: [GHC-39999]
- • Could not deduce ‘Eq (F [a])’
- arising from the superclasses of an instance declaration
- from the context: D [a]
- bound by the instance declaration at T20666a.hs:11:10-23
- Possible fix:
- If the constraint looks soluble from a superclass of the instance context,
- read 'Undecidable instances and loopy superclasses' in the user manual
- • In the instance declaration for ‘C [a]’
+T20666a.hs:11:10: warning: [GHC-36038] [-Wloopy-superclass-solve (in -Wdefault)]
+ I am solving the constraint ‘Eq (F [a])’,
+ arising from the superclasses of an instance declaration,
+ in a way that might turn out to loop at runtime.
+ Future versions of GHC will turn this warning into an error.
+ See the user manual, § Undecidable instances and loopy superclasses.
+ Suggested fix:
+ Add the constraint ‘Eq (F [a])’ to the instance context,
+ even though it seems logically implied by other constraints in the context.
=====================================
testsuite/tests/typecheck/should_fail/T6161.stderr
=====================================
@@ -1,7 +1,10 @@
-T6161.hs:19:10: error: [GHC-39999]
- • Could not deduce ‘Super (Fam a)’
- arising from the superclasses of an instance declaration
- from the context: Foo a
- bound by the instance declaration at T6161.hs:19:10-31
- • In the instance declaration for ‘Duper (Fam a)’
+T6161.hs:19:10: warning: [GHC-36038] [-Wloopy-superclass-solve (in -Wdefault)]
+ I am solving the constraint ‘Super (Fam a)’,
+ arising from the superclasses of an instance declaration,
+ in a way that might turn out to loop at runtime.
+ Future versions of GHC will turn this warning into an error.
+ See the user manual, § Undecidable instances and loopy superclasses.
+ Suggested fix:
+ Add the constraint ‘Super (Fam a)’ to the instance context,
+ even though it seems logically implied by other constraints in the context.
=====================================
testsuite/tests/typecheck/should_fail/all.T
=====================================
@@ -241,7 +241,7 @@ test('tcfail215', normal, compile_fail, [''])
test('tcfail216', normal, compile_fail, [''])
test('tcfail217', normal, compile_fail, [''])
test('tcfail218', normal, compile_fail, [''])
-test('tcfail223', normal, compile_fail, [''])
+test('tcfail223', normal, compile, ['']) # To become compile_fail after migration period (see #22912)
test('tcfail224', normal, compile_fail, [''])
test('tcfail225', normal, compile_fail, [''])
@@ -294,7 +294,7 @@ test('T19187a', normal, compile_fail, [''])
test('T2534', normal, compile_fail, [''])
test('T7175', normal, compile_fail, [''])
test('T7210', normal, compile_fail, [''])
-test('T6161', normal, compile_fail, [''])
+test('T6161', normal, compile, ['']) # To become compile_fail after migration period (see #22912)
test('T7368', normal, compile_fail, [''])
test('T7264', normal, compile_fail, [''])
test('T6069', normal, compile_fail, [''])
@@ -665,5 +665,5 @@ test('T21530a', normal, compile_fail, [''])
test('T21530b', normal, compile_fail, [''])
test('T22570', normal, compile_fail, [''])
test('T22645', normal, compile_fail, [''])
-test('T20666', normal, compile_fail, [''])
-test('T20666a', normal, compile_fail, [''])
+test('T20666', normal, compile, ['']) # To become compile_fail after migration period (see #22912)
+test('T20666a', normal, compile, ['']) # To become compile_fail after migration period (see #22912)
=====================================
testsuite/tests/typecheck/should_fail/tcfail223.stderr
=====================================
@@ -1,9 +1,10 @@
-tcfail223.hs:10:10: error: [GHC-39999]
- • Could not deduce ‘Class1 a’
- arising from the superclasses of an instance declaration
- from the context: Class3 a
- bound by the instance declaration at tcfail223.hs:10:10-29
- Possible fix:
- add (Class1 a) to the context of the instance declaration
- • In the instance declaration for ‘Class2 a’
+tcfail223.hs:10:10: warning: [GHC-36038] [-Wloopy-superclass-solve (in -Wdefault)]
+ I am solving the constraint ‘Class1 a’,
+ arising from the superclasses of an instance declaration,
+ in a way that might turn out to loop at runtime.
+ Future versions of GHC will turn this warning into an error.
+ See the user manual, § Undecidable instances and loopy superclasses.
+ Suggested fix:
+ Add the constraint ‘Class1 a’ to the instance context,
+ even though it seems logically implied by other constraints in the context.
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/9fb4ca89bff9873e5f6a6849fa22a349c94deaae
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/9fb4ca89bff9873e5f6a6849fa22a349c94deaae
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/20230214/164fea99/attachment-0001.html>
More information about the ghc-commits
mailing list