From a3a8e9e968ff9b10c6785d53a5f1c8fcef6db72b Mon Sep 17 00:00:00 2001 From: Simon Peyton Jones Date: Mon, 28 Nov 2022 14:56:17 +0000 Subject: Be more careful in GHC.Tc.Solver.Interact.solveOneFromTheOther We were failing to account for the cc_pend_sc flag in this important function, with the result that we expanded superclasses forever. Fixes #22516. --- compiler/GHC/Tc/Solver/Canonical.hs | 4 +- compiler/GHC/Tc/Solver/Interact.hs | 89 +++++++++++---------- compiler/GHC/Tc/Solver/Monad.hs | 4 +- compiler/GHC/Tc/Types/Constraint.hs | 29 ++++--- testsuite/tests/typecheck/should_compile/T22516.hs | 91 ++++++++++++++++++++++ testsuite/tests/typecheck/should_compile/all.T | 1 + 6 files changed, 162 insertions(+), 56 deletions(-) create mode 100644 testsuite/tests/typecheck/should_compile/T22516.hs diff --git a/compiler/GHC/Tc/Solver/Canonical.hs b/compiler/GHC/Tc/Solver/Canonical.hs index 41ae8fab36..33ee8e854c 100644 --- a/compiler/GHC/Tc/Solver/Canonical.hs +++ b/compiler/GHC/Tc/Solver/Canonical.hs @@ -1815,8 +1815,8 @@ only about /completeness/. Note [Decomposing newtypes a bit more aggressively] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -c.f. https://github.com/ghc-proposals/ghc-proposals/pull/549 -and discussion on !9282. +c.f. https://github.com/ghc-proposals/ghc-proposals/pull/549, +issue #22441, and discussion on !9282. Consider [G] c, [W] (IO Int) ~R (IO Age) where IO is abstract, and diff --git a/compiler/GHC/Tc/Solver/Interact.hs b/compiler/GHC/Tc/Solver/Interact.hs index 37c8dd6d01..c3aa2d2695 100644 --- a/compiler/GHC/Tc/Solver/Interact.hs +++ b/compiler/GHC/Tc/Solver/Interact.hs @@ -448,8 +448,8 @@ instance Outputable InteractResult where ppr KeepInert = text "keep inert" ppr KeepWork = text "keep work-item" -solveOneFromTheOther :: CtEvidence -- Inert (Dict or Irred) - -> CtEvidence -- WorkItem (same predicate as inert) +solveOneFromTheOther :: Ct -- Inert (Dict or Irred) + -> Ct -- WorkItem (same predicate as inert) -> TcS InteractResult -- Precondition: -- * inert and work item represent evidence for the /same/ predicate @@ -459,23 +459,40 @@ solveOneFromTheOther :: CtEvidence -- Inert (Dict or Irred) -- although we don't rewrite wanteds with wanteds, we can combine -- two wanteds into one by solving one from the other -solveOneFromTheOther ev_i ev_w +solveOneFromTheOther ct_i ct_w | CtWanted { ctev_loc = loc_w } <- ev_w , prohibitedSuperClassSolve loc_i loc_w - = -- inert must be Given + = -- Inert must be Given do { traceTcS "prohibitedClassSolve1" (ppr ev_i $$ ppr ev_w) ; return KeepWork } | CtWanted {} <- ev_w - -- Inert is Given or Wanted - = return $ case ev_i of - CtWanted {} -> choose_better_loc - -- both are Wanted; choice of which to keep is - -- arbitrary. So we look at the context to choose - -- which would make a better error message + = -- Inert is Given or Wanted + case ev_i of + CtGiven {} -> return 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 + + -- 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 - _ -> KeepInert - -- work is Wanted; inert is Given: easy choice. + -- otherwise, just choose the lower span + -- reason: if we have something like (abs 1) (where the + -- Num constraint cannot be satisfied), it's better to + -- 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 -- From here on the work-item is Given @@ -498,31 +515,21 @@ solveOneFromTheOther ev_i ev_w | otherwise -- Both are Given, levels differ = return different_level_strategy where + ev_i = ctEvidence ct_i + ev_w = ctEvidence ct_w + pred = ctEvPred ev_i + loc_i = ctEvLoc ev_i loc_w = ctEvLoc ev_w lvl_i = ctLocLevel loc_i lvl_w = ctLocLevel loc_w - choose_better_loc - -- if only one is a WantedSuperclassOrigin (arising from expanding - -- a Wanted class constraint), keep the other: wanted superclasses - -- may be unexpected by users - | is_wanted_superclass_loc loc_i - , not (is_wanted_superclass_loc loc_w) = KeepWork - - | not (is_wanted_superclass_loc loc_i) - , is_wanted_superclass_loc loc_w = KeepInert - - -- otherwise, just choose the lower span - -- reason: if we have something like (abs 1) (where the - -- Num constraint cannot be satisfied), it's better to - -- 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 = KeepInert - | otherwise = KeepWork + is_psc_w = isPendingScDict ct_w + is_psc_i = isPendingScDict ct_i + is_wsc_orig_i = is_wanted_superclass_loc loc_i + is_wsc_orig_w = is_wanted_superclass_loc loc_w is_wanted_superclass_loc = isWantedSuperclassOrigin . ctLocOrigin different_level_strategy -- Both Given @@ -650,28 +657,28 @@ once had done). This problem can be tickled by typecheck/should_compile/holes. -- mean that (ty1 ~ ty2) interactIrred :: InertCans -> Ct -> TcS (StopOrContinue Ct) -interactIrred inerts workItem@(CIrredCan { cc_ev = ev_w, cc_reason = reason }) +interactIrred inerts ct_w@(CIrredCan { cc_ev = ev_w, cc_reason = reason }) | isInsolubleReason reason -- For insolubles, don't allow the constraint to be dropped -- which can happen with solveOneFromTheOther, so that -- we get distinct error messages with -fdefer-type-errors - = continueWith workItem + = continueWith ct_w | let (matching_irreds, others) = findMatchingIrreds (inert_irreds inerts) ev_w , ((ct_i, swap) : _rest) <- bagToList matching_irreds -- See Note [Multiple matching irreds] , let ev_i = ctEvidence ct_i - = do { what_next <- solveOneFromTheOther ev_i ev_w - ; traceTcS "iteractIrred" (ppr workItem $$ ppr what_next $$ ppr ct_i) + = do { what_next <- solveOneFromTheOther ct_i ct_w + ; traceTcS "iteractIrred" (ppr ct_w $$ ppr what_next $$ ppr ct_i) ; case what_next of KeepInert -> do { setEvBindIfWanted ev_w (swap_me swap ev_i) ; return (Stop ev_w (text "Irred equal" <+> parens (ppr what_next))) } KeepWork -> do { setEvBindIfWanted ev_i (swap_me swap ev_w) ; updInertIrreds (\_ -> others) - ; continueWith workItem } } + ; continueWith ct_w } } | otherwise - = continueWith workItem + = continueWith ct_w where swap_me :: SwapFlag -> CtEvidence -> EvTerm @@ -1001,7 +1008,7 @@ and Given/instance fundeps entirely. -} interactDict :: InertCans -> Ct -> TcS (StopOrContinue Ct) -interactDict inerts workItem@(CDictCan { cc_ev = ev_w, cc_class = cls, cc_tyargs = tys }) +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 = -- There is a matching dictionary in the inert set @@ -1015,22 +1022,22 @@ interactDict inerts workItem@(CDictCan { cc_ev = ev_w, cc_class = cls, cc_tyargs do { -- Ths short-cut solver didn't fire, so we -- solve ev_w from the matching inert ev_i we found - what_next <- solveOneFromTheOther ev_i ev_w + 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) ; updInertDicts $ \ ds -> delDict ds cls tys - ; continueWith workItem } } } + ; continueWith ct_w } } } | cls `hasKey` ipClassKey , isGiven ev_w - = interactGivenIP inerts workItem + = interactGivenIP inerts ct_w | otherwise = do { addFunDepWork inerts ev_w cls - ; continueWith workItem } + ; continueWith ct_w } interactDict _ wi = pprPanic "interactDict" (ppr wi) diff --git a/compiler/GHC/Tc/Solver/Monad.hs b/compiler/GHC/Tc/Solver/Monad.hs index 12b6fcc69f..67c90dcd80 100644 --- a/compiler/GHC/Tc/Solver/Monad.hs +++ b/compiler/GHC/Tc/Solver/Monad.hs @@ -536,7 +536,7 @@ get_sc_pending this_lvl ic@(IC { inert_dicts = dicts, inert_insts = insts }) get_pending :: Ct -> [Ct] -> [Ct] -- Get dicts with cc_pend_sc = True -- but flipping the flag get_pending dict dicts - | Just dict' <- isPendingScDict dict + | Just dict' <- pendingScDict_maybe dict , belongs_to_this_level (ctEvidence dict) = dict' : dicts | otherwise @@ -549,7 +549,7 @@ get_sc_pending this_lvl ic@(IC { inert_dicts = dicts, inert_insts = insts }) get_pending_inst :: [Ct] -> QCInst -> ([Ct], QCInst) get_pending_inst cts qci@(QCI { qci_ev = ev }) - | Just qci' <- isPendingScInst qci + | Just qci' <- pendingScInst_maybe qci , belongs_to_this_level ev = (CQuantCan qci' : cts, qci') | otherwise diff --git a/compiler/GHC/Tc/Types/Constraint.hs b/compiler/GHC/Tc/Types/Constraint.hs index a876522913..62412cdb65 100644 --- a/compiler/GHC/Tc/Types/Constraint.hs +++ b/compiler/GHC/Tc/Types/Constraint.hs @@ -7,14 +7,15 @@ -- in the type-checker and constraint solver. module GHC.Tc.Types.Constraint ( -- QCInst - QCInst(..), isPendingScInst, + QCInst(..), pendingScInst_maybe, -- Canonical constraints Xi, Ct(..), Cts, emptyCts, andCts, andManyCts, pprCts, singleCt, listToCts, ctsElts, consCts, snocCts, extendCtsList, isEmptyCts, - isPendingScDict, superClassesMightHelp, getPendingWantedScs, + isPendingScDict, pendingScDict_maybe, + superClassesMightHelp, getPendingWantedScs, isWantedCt, isGivenCt, isUserTypeError, getUserTypeErrorMsg, ctEvidence, ctLoc, ctPred, ctFlavour, ctEqRel, ctOrigin, @@ -890,18 +891,24 @@ isUserTypeError pred = case getUserTypeErrorMsg pred of Just _ -> True _ -> False -isPendingScDict :: Ct -> Maybe Ct +isPendingScDict :: Ct -> Bool +isPendingScDict (CDictCan { cc_pend_sc = psc }) = psc +-- Says whether this is a CDictCan with cc_pend_sc is True; +-- i.e. pending un-expanded superclasses +isPendingScDict _ = False + +pendingScDict_maybe :: Ct -> Maybe Ct -- Says whether this is a CDictCan with cc_pend_sc is True, -- AND if so flips the flag -isPendingScDict ct@(CDictCan { cc_pend_sc = True }) - = Just (ct { cc_pend_sc = False }) -isPendingScDict _ = Nothing +pendingScDict_maybe ct@(CDictCan { cc_pend_sc = True }) + = Just (ct { cc_pend_sc = False }) +pendingScDict_maybe _ = Nothing -isPendingScInst :: QCInst -> Maybe QCInst +pendingScInst_maybe :: QCInst -> Maybe QCInst -- Same as isPendingScDict, but for QCInsts -isPendingScInst qci@(QCI { qci_pend_sc = True }) - = Just (qci { qci_pend_sc = False }) -isPendingScInst _ = Nothing +pendingScInst_maybe qci@(QCI { qci_pend_sc = True }) + = Just (qci { qci_pend_sc = False }) +pendingScInst_maybe _ = Nothing superClassesMightHelp :: WantedConstraints -> Bool -- ^ True if taking superclasses of givens, or of wanteds (to perhaps @@ -923,7 +930,7 @@ getPendingWantedScs :: Cts -> ([Ct], Cts) getPendingWantedScs simples = mapAccumBagL get [] simples where - get acc ct | Just ct' <- isPendingScDict ct + get acc ct | Just ct' <- pendingScDict_maybe ct = (ct':acc, ct') | otherwise = (acc, ct) diff --git a/testsuite/tests/typecheck/should_compile/T22516.hs b/testsuite/tests/typecheck/should_compile/T22516.hs new file mode 100644 index 0000000000..6bc481d3ee --- /dev/null +++ b/testsuite/tests/typecheck/should_compile/T22516.hs @@ -0,0 +1,91 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveAnyClass #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE UndecidableSuperClasses #-} +module Bug where + +import Data.Kind (Constraint, Type) + +data D a + +f :: Generic (D a) => () +f = () + +type family + AllF (c :: k -> Constraint) (xs :: [k]) :: Constraint where + AllF _c '[] = () + AllF c (x ': xs) = (c x, All c xs) + +class (AllF c xs, SListI xs) => All (c :: k -> Constraint) (xs :: [k]) where + +type SListI = All Top + +class Top x +instance Top x + +class All SListI (Code a) => Generic a where + type Code a :: [[Type]] + + +{- + final wc = WC {wc_impl = + Implic { + TcLevel = 1 + Skolems = k_aG9[sk:1] (a_aGa[sk:1] :: k_aG9[sk:1]) + Given-eqs = LocalGivenEqs + Status = Unsolved + Given = $dGeneric_aGb :: Generic (D a_aGa[sk:1]) + Wanted = + WC {wc_simple = + [W] irred_aGo {0}:: AllF + SListI (Code (D a_aGe[tau:1])) (CIrredCan(irred)) + [W] irred_aGu {0}:: AllF + Top (Code (D a_aGe[tau:1])) (CIrredCan(irred)) + [W] $dGeneric_aGf {0}:: Generic (D a_aGe[tau:1]) (CDictCan) + [W] $dAll_aGn {0}:: All SListI (Code (D a_aGe[tau:1])) (CDictCan) + [W] $dAll_aGv {0}:: All + Top (Code (D a_aGe[tau:1])) (CDictCan(psc))} + Binds = EvBindsVar + the type signature for: + f :: forall {k} (a :: k). Generic (D a) => () }} + + + +-------------------------- +-- Given +[G] Generic (D a) +==> superclass +[G] All SListI (Code (D a)) = All (All Top) (Code (D a)) +==> superclass +[G] AllF SLIstI (Code (D a)) = AllF (All Top) (Code (D a)) +[G] SListI (Code (D a)) = All Top (Code (D a)) {loop} + +Next iteration +===> +[G] AllF Top (Code (D a)) +[G] SListI (Code (D a)) = All Top (Code (D a)) (already there) + +-------------------------- +-- Wanted +[W] Generic (D a) +==> superclass +[W] All SListI (Code (D a)) = All (All Top) (Code (D a)) +==> superclass +[W] AllF SLIstI (Code (D a)) = AllF (All Top) (Code (D a)) +[W] SListI (Code (D a)) = All Top (Code (D a)) {loop} + +Next iteration +===> +[W] AllF Top (Code (D a)) +[W] SListI (Code (D a)) = All Top (Code (D a)) (already there) + +-} \ No newline at end of file diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T index 6413034c05..1f1e7d8d1f 100644 --- a/testsuite/tests/typecheck/should_compile/all.T +++ b/testsuite/tests/typecheck/should_compile/all.T @@ -852,3 +852,4 @@ test('T21951b', normal, compile, ['-Wredundant-strictness-flags']) test('T21550', normal, compile, ['']) test('T22310', normal, compile, ['']) test('T22331', normal, compile, ['']) +test('T22516', normal, compile, ['']) -- cgit v1.2.1