From 06c93c0cdcc9d5e2052e58997819ad281b29b0a6 Mon Sep 17 00:00:00 2001 From: Simon Peyton Jones Date: Fri, 5 Feb 2021 15:34:54 +0000 Subject: Fix a long standing bug in constraint solving When combining Inert: [W] C ty1 ty2 Work item: [D] C ty1 ty2 we were simply discarding the Derived one. Not good! We should turn the inert back into [WD] or keep both. E.g. fundeps work only on Derived (see isImprovable). This little patch fixes it. The bug is hard to tickle, but #19315 did so. The fix is a little messy (see Note [KeepBoth] plus the change in addDictCt), but I am disinclined to refine it further because it'll all be swept away when we Kill Deriveds. --- compiler/GHC/Core/Map.hs | 2 +- compiler/GHC/Tc/Solver/Interact.hs | 60 ++++++++++++++++++---- compiler/GHC/Tc/Solver/Monad.hs | 40 ++++++++++++--- testsuite/tests/typecheck/should_compile/T19315.hs | 42 +++++++++++++++ testsuite/tests/typecheck/should_compile/all.T | 2 +- 5 files changed, 126 insertions(+), 20 deletions(-) create mode 100644 testsuite/tests/typecheck/should_compile/T19315.hs diff --git a/compiler/GHC/Core/Map.hs b/compiler/GHC/Core/Map.hs index bf0b56ae40..9a276f76cd 100644 --- a/compiler/GHC/Core/Map.hs +++ b/compiler/GHC/Core/Map.hs @@ -30,7 +30,7 @@ module GHC.Core.Map ( -- * Map for compressing leaves. See Note [Compressed TrieMap] GenMap, -- * 'TrieMap' class - TrieMap(..), insertTM, deleteTM, + TrieMap(..), XT, insertTM, deleteTM, lkDFreeVar, xtDFreeVar, lkDNamed, xtDNamed, (>.>), (|>), (|>>), diff --git a/compiler/GHC/Tc/Solver/Interact.hs b/compiler/GHC/Tc/Solver/Interact.hs index 7d9116405a..9724b1a59f 100644 --- a/compiler/GHC/Tc/Solver/Interact.hs +++ b/compiler/GHC/Tc/Solver/Interact.hs @@ -499,12 +499,32 @@ interactWithInertsStage wi data InteractResult = KeepInert -- Keep the inert item, and solve the work item from it -- (if the latter is Wanted; just discard it if not) - | KeepWork -- Keep the work item, and solve the intert item from it + | KeepWork -- Keep the work item, and solve the inert item from it + + | KeepBoth -- See Note [KeepBoth] instance Outputable InteractResult where + ppr KeepBoth = text "keep both" ppr KeepInert = text "keep inert" ppr KeepWork = text "keep work-item" +{- Note [KeepBoth] +~~~~~~~~~~~~~~~~~~ +Consider + Inert: [WD] C ty1 ty2 + Work item: [D] C ty1 ty2 + +Here we can simply drop the work item. But what about + Inert: [W] C ty1 ty2 + Work item: [D] C ty1 ty2 + +Here we /cannot/ drop the work item, becuase we lose the [D] form, and +that is essential for e.g. fundeps, see isImprovable. We could zap +the inert item to [WD], but the simplest thing to do is simply to keep +both. (They probably started as [WD] and got split; this is relatively +rare and it doesn't seem worth trying to put them back together again.) +-} + solveOneFromTheOther :: CtEvidence -- Inert -> CtEvidence -- WorkItem -> TcS InteractResult @@ -516,22 +536,37 @@ solveOneFromTheOther :: CtEvidence -- Inert -- two wanteds into one by solving one from the other solveOneFromTheOther ev_i ev_w - | isDerived ev_w -- Work item is Derived; just discard it - = return KeepInert - - | isDerived ev_i -- The inert item is Derived, we can just throw it away, - = return KeepWork -- The ev_w is inert wrt earlier inert-set items, - -- so it's safe to continue on from this point - + | CtDerived {} <- ev_w -- Work item is Derived + = case ev_i of + CtWanted { ctev_nosh = WOnly } -> return KeepBoth + _ -> return KeepInert + + | CtDerived {} <- ev_i -- Inert item is Derived + = case ev_w of + CtWanted { ctev_nosh = WOnly } -> return KeepBoth + _ -> return KeepWork + -- The ev_w is inert wrt earlier inert-set items, + -- so it's safe to continue on from this point + + -- After this, neither ev_i or ev_w are Derived | CtWanted { ctev_loc = loc_w } <- ev_w , prohibitedSuperClassSolve (ctEvLoc ev_i) loc_w = -- inert must be Given do { traceTcS "prohibitedClassSolve1" (ppr ev_i $$ ppr ev_w) ; return KeepWork } - | CtWanted {} <- ev_w + | CtWanted { ctev_nosh = nosh_w } <- ev_w -- Inert is Given or Wanted - = return KeepInert + = case ev_i of + CtWanted { ctev_nosh = WOnly } + | WDeriv <- nosh_w -> return KeepWork + _ -> return KeepInert + -- Consider work item [WD] C ty1 ty2 + -- inert item [W] C ty1 ty2 + -- Then we must keep the work item. But if the + -- work item was [W] C ty1 ty2 + -- then we are free to discard the work item in favour of inert + -- Remember, no Deriveds at this point -- From here on the work-item is Given @@ -703,6 +738,7 @@ interactIrred inerts workItem@(CIrredCan { cc_ev = ev_w, cc_status = status }) = do { what_next <- solveOneFromTheOther ev_i ev_w ; traceTcS "iteractIrred" (ppr workItem $$ ppr what_next $$ ppr ct_i) ; case what_next of + KeepBoth -> continueWith workItem 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) @@ -1025,7 +1061,8 @@ Passing along the solved_dicts important for two reasons: interactDict :: InertCans -> Ct -> TcS (StopOrContinue Ct) interactDict inerts workItem@(CDictCan { cc_ev = ev_w, cc_class = cls, cc_tyargs = tys }) - | Just ev_i <- lookupInertDict inerts (ctEvLoc ev_w) cls 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 do { -- First to try to solve it /completely/ from top level instances -- See Note [Shortcut solving] @@ -1040,6 +1077,7 @@ interactDict inerts workItem@(CDictCan { cc_ev = ev_w, cc_class = cls, cc_tyargs what_next <- solveOneFromTheOther ev_i ev_w ; traceTcS "lookupInertDict" (ppr what_next) ; case what_next of + KeepBoth -> continueWith workItem 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) diff --git a/compiler/GHC/Tc/Solver/Monad.hs b/compiler/GHC/Tc/Solver/Monad.hs index 8a64e3a8e4..24fed1485c 100644 --- a/compiler/GHC/Tc/Solver/Monad.hs +++ b/compiler/GHC/Tc/Solver/Monad.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE CPP, DeriveFunctor, TypeFamilies #-} +{-# LANGUAGE CPP, DeriveFunctor, TypeFamilies, ScopedTypeVariables #-} {-# OPTIONS_GHC -Wno-incomplete-record-updates #-} @@ -1648,7 +1648,7 @@ add_item ics@(IC { inert_irreds = irreds, inert_count = count }) add_item ics item@(CDictCan { cc_ev = ev, cc_class = cls, cc_tyargs = tys }) - = ics { inert_dicts = addDict (inert_dicts ics) cls tys item + = ics { inert_dicts = addDictCt (inert_dicts ics) cls tys item , inert_count = bumpUnsolvedCount ev (inert_count ics) } add_item _ item @@ -1912,7 +1912,7 @@ Hence: -------------- addInertSafehask :: InertCans -> Ct -> InertCans addInertSafehask ics item@(CDictCan { cc_class = cls, cc_tyargs = tys }) - = ics { inert_safehask = addDict (inert_dicts ics) cls tys item } + = ics { inert_safehask = addDictCt (inert_dicts ics) cls tys item } addInertSafehask _ item = pprPanic "addInertSafehask: can't happen! Inserting " $ ppr item @@ -2056,7 +2056,7 @@ get_sc_pending this_lvl ic@(IC { inert_dicts = dicts, inert_insts = insts }) add :: Ct -> DictMap Ct -> DictMap Ct add ct@(CDictCan { cc_class = cls, cc_tyargs = tys }) dicts - = addDict dicts cls tys ct + = addDictCt dicts cls tys ct add ct _ = pprPanic "getPendingScDicts" (ppr ct) get_pending_inst :: [Ct] -> QCInst -> ([Ct], QCInst) @@ -2372,16 +2372,16 @@ lookupInInerts loc pty | ClassPred cls tys <- classifyPredType pty = do { inerts <- getTcSInerts ; return (lookupSolvedDict inerts loc cls tys `mplus` - lookupInertDict (inert_cans inerts) loc cls tys) } + fmap ctEvidence (lookupInertDict (inert_cans inerts) loc cls tys)) } | otherwise -- NB: No caching for equalities, IPs, holes, or errors = return Nothing -- | Look up a dictionary inert. NB: the returned 'CtEvidence' might not -- match the input exactly. Note [Use loose types in inert set]. -lookupInertDict :: InertCans -> CtLoc -> Class -> [Type] -> Maybe CtEvidence +lookupInertDict :: InertCans -> CtLoc -> Class -> [Type] -> Maybe Ct lookupInertDict (IC { inert_dicts = dicts }) loc cls tys = case findDict dicts loc cls tys of - Just ct -> Just (ctEvidence ct) + Just ct -> Just ct _ -> Nothing -- | Look up a solved inert. NB: the returned 'CtEvidence' might not @@ -2446,6 +2446,12 @@ insertTcApp m cls tys ct = alterUDFM alter_tm m cls where alter_tm mb_tm = Just (insertTM tys ct (mb_tm `orElse` emptyTM)) +alterTcApp :: forall a. TcAppMap a -> Unique -> [Type] -> XT a -> TcAppMap a +alterTcApp m cls tys xt_ct = alterUDFM alter_tm m cls + where + alter_tm :: Maybe (ListMap LooseTypeMap a) -> Maybe (ListMap LooseTypeMap a) + alter_tm mb_tm = Just (alterTM tys xt_ct (mb_tm `orElse` emptyTM)) + -- mapTcApp :: (a->b) -> TcAppMap a -> TcAppMap b -- mapTcApp f = mapUDFM (mapTM f) @@ -2547,6 +2553,26 @@ delDict m cls tys = delTcApp m (getUnique cls) tys addDict :: DictMap a -> Class -> [Type] -> a -> DictMap a addDict m cls tys item = insertTcApp m (getUnique cls) tys item +addDictCt :: DictMap Ct -> Class -> [Type] -> Ct -> DictMap Ct +-- Like addDict, but combines [W] and [D] to [WD] +-- See Note [KeepBoth] in GHC.Tc.Solver.Interact +addDictCt m cls tys new_ct = alterTcApp m (getUnique cls) tys xt_ct + where + new_ct_ev = ctEvidence new_ct + + xt_ct :: Maybe Ct -> Maybe Ct + xt_ct (Just old_ct) + | CtWanted { ctev_nosh = WOnly } <- old_ct_ev + , CtDerived {} <- new_ct_ev + = Just (old_ct { cc_ev = old_ct_ev { ctev_nosh = WDeriv }}) + | CtDerived {} <- old_ct_ev + , CtWanted { ctev_nosh = WOnly } <- new_ct_ev + = Just (new_ct { cc_ev = new_ct_ev { ctev_nosh = WDeriv }}) + where + old_ct_ev = ctEvidence old_ct + + xt_ct _ = Just new_ct + addDictsByClass :: DictMap Ct -> Class -> Bag Ct -> DictMap Ct addDictsByClass m cls items = addToUDFM_Directly m (getUnique cls) (foldr add emptyTM items) diff --git a/testsuite/tests/typecheck/should_compile/T19315.hs b/testsuite/tests/typecheck/should_compile/T19315.hs new file mode 100644 index 0000000000..d93f42c4d4 --- /dev/null +++ b/testsuite/tests/typecheck/should_compile/T19315.hs @@ -0,0 +1,42 @@ +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE FunctionalDependencies #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeFamilies #-} +module Bug where + +import Control.Monad.Reader +import Data.Kind + +type Lens f s a = (f, s, a) + +view :: MonadReader s m => Lens a s a -> m a +view = undefined + +data TickLabels b n = TickLabels + +type family N a :: Type +type instance N (TickLabels b n) = n + +tickLabelTextFunction :: Lens f a (QDiagram b (N a)) +tickLabelTextFunction = undefined + +class HasTickLabels f a b | a -> b where + tickLabelFunction :: Lens f a (N a -> String) + +instance HasTickLabels f (TickLabels b n) b where + tickLabelFunction = undefined + +data QDiagram b n = QD + +renderColourBar :: forall n b. TickLabels b n -> n -> () +renderColourBar cbTickLabels bnds = () + where + f :: a -> a + f x = x + + tickLabelXs :: String + tickLabelXs = view tickLabelFunction cbTickLabels bnds + + drawTickLabel :: n -> QDiagram b n + drawTickLabel x = view tickLabelTextFunction cbTickLabels + where v = f x diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T index 3f9f2cd406..b99fee4903 100644 --- a/testsuite/tests/typecheck/should_compile/all.T +++ b/testsuite/tests/typecheck/should_compile/all.T @@ -720,6 +720,6 @@ test('T17775-viewpats-d', normal, compile_fail, ['']) test('T18118', normal, multimod_compile, ['T18118', '-v0']) test('T18412', normal, compile, ['']) test('T18470', normal, compile, ['']) - test('T18998', normal, compile, ['']) test('T18998b', normal, compile, ['']) +test('T19315', normal, compile, ['']) -- cgit v1.2.1