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, 121 insertions, 20 deletions

diff --git a/compiler/GHC/Core/Map/Type.hs b/compiler/GHC/Core/Map/Type.hs
index a50549ffdd..050d19cba5 100644
--- a/compiler/GHC/Core/Map/Type.hs
+++ b/compiler/GHC/Core/Map/Type.hs
@@ -9,7 +9,7 @@
 
 module GHC.Core.Map.Type (
      -- * Re-export generic interface
-   TrieMap(..),
+   TrieMap(..), XT,
 
      -- * Maps over 'Type's
    TypeMap, emptyTypeMap, extendTypeMap, lookupTypeMap, foldTypeMap,
diff --git a/compiler/GHC/Tc/Solver/Interact.hs b/compiler/GHC/Tc/Solver/Interact.hs
index 00ee528fdc..b8df1fbae6 100644
--- a/compiler/GHC/Tc/Solver/Interact.hs
+++ b/compiler/GHC/Tc/Solver/Interact.hs
@@ -439,12 +439,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
@@ -456,22 +476,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
 
@@ -643,6 +678,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)
@@ -969,7 +1005,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]
@@ -984,6 +1021,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 4c16f2f56e..d92d8e3d5c 100644
--- a/compiler/GHC/Tc/Solver/Monad.hs
+++ b/compiler/GHC/Tc/Solver/Monad.hs
@@ -1,5 +1,5 @@
 {-# LANGUAGE CPP, DeriveFunctor, TypeFamilies, ScopedTypeVariables, TypeApplications,
-             DerivingStrategies, GeneralizedNewtypeDeriving #-}
+             DerivingStrategies, GeneralizedNewtypeDeriving, ScopedTypeVariables #-}
 
 {-# OPTIONS_GHC -Wno-incomplete-record-updates -Wno-incomplete-uni-patterns #-}
 
@@ -1702,7 +1702,7 @@ add_item tc_lvl ics@(IC { inert_irreds = irreds }) item@(CIrredCan {})
     ics { inert_irreds = irreds `Bag.snocBag` item }
 
 add_item _ ics item@(CDictCan { 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 }
 
 add_item _ _ item
   = pprPanic "upd_inert set: can't happen! Inserting " $
@@ -2071,7 +2071,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
@@ -2214,7 +2214,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)
@@ -2555,15 +2555,15 @@ 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.
-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.
@@ -2673,7 +2673,7 @@ insertTcApp m tc tys ct = alterDTyConEnv alter_tm m tc
   where
     alter_tm mb_tm = Just (insertTM tys ct (mb_tm `orElse` emptyTM))
 
-alterTcApp :: forall a. TcAppMap a -> TyCon -> [Type] -> (Maybe a -> Maybe a) -> TcAppMap a
+alterTcApp :: forall a. TcAppMap a -> TyCon -> [Type] -> XT a -> TcAppMap a
 alterTcApp m tc tys upd = alterDTyConEnv alter_tm m tc
   where
     alter_tm :: Maybe (ListMap LooseTypeMap a) -> Maybe (ListMap LooseTypeMap a)
@@ -2773,6 +2773,26 @@ delDict m cls tys = delTcApp m (classTyCon cls) tys
 addDict :: DictMap a -> Class -> [Type] -> a -> DictMap a
 addDict m cls tys item = insertTcApp m (classTyCon 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 (classTyCon 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
   = extendDTyConEnv m (classTyCon 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 3842a1984c..46f2d088d1 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -770,3 +770,4 @@ test('InlinePatSyn_ExplicitBidiBuilder', [], makefile_test, [])
 test('InlinePatSyn_ExplicitBidiMatcher', [], makefile_test, [])
 test('T18467', normal, compile, [''])
 
+test('T19315', normal, compile, [''])