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.

5 files changed, 126 insertions, 20 deletions

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, [''])