Avoid fundep-caused loop in the typechecker

Ticket #19415 showed a nasty typechecker loop, which can happen with
fundeps that do not satisfy the coverage condition.

This patch fixes the problem.  It's described in GHC.Tc.Solver.Interact
   Note [Fundeps with instances]

It's not a perfect solution, as the Note explains, but it's better
than the status quo.

7 files changed, 178 insertions, 47 deletions

diff --git a/compiler/GHC/Tc/Instance/FunDeps.hs b/compiler/GHC/Tc/Instance/FunDeps.hs
index 623ed147ff..81cf7524e1 100644
--- a/compiler/GHC/Tc/Instance/FunDeps.hs
+++ b/compiler/GHC/Tc/Instance/FunDeps.hs
@@ -206,16 +206,11 @@ pprEquation (FDEqn { fd_qtvs = qtvs, fd_eqs = pairs })
 
 improveFromInstEnv :: InstEnvs
                    -> (PredType -> SrcSpan -> loc)
-                   -> PredType
+                   -> Class -> [Type]
                    -> [FunDepEqn loc] -- Needs to be a FunDepEqn because
                                       -- of quantified variables
 -- Post: Equations oriented from the template (matching instance) to the workitem!
-improveFromInstEnv inst_env mk_loc pred
-  | Just (cls, tys) <- ASSERT2( isClassPred pred, ppr pred )
-                       getClassPredTys_maybe pred
-  , let (cls_tvs, cls_fds) = classTvsFds cls
-        instances          = classInstances inst_env cls
-        rough_tcs          = roughMatchTcs tys
+improveFromInstEnv inst_env mk_loc cls tys
   = [ FDEqn { fd_qtvs = meta_tvs, fd_eqs = eqs
             , fd_pred1 = p_inst, fd_pred2 = pred
             , fd_loc = mk_loc p_inst (getSrcSpan (is_dfun ispec)) }
@@ -231,7 +226,12 @@ improveFromInstEnv inst_env mk_loc pred
                                       tys trimmed_tcs -- NB: orientation
     , let p_inst = mkClassPred cls (is_tys ispec)
     ]
-improveFromInstEnv _ _ _ = []
+  where
+    (cls_tvs, cls_fds) = classTvsFds cls
+    instances          = classInstances inst_env cls
+    rough_tcs          = roughMatchTcs tys
+    pred               = mkClassPred cls tys
+
 
 
 improveClsFD :: [TyVar] -> FunDep TyVar    -- One functional dependency from the class
diff --git a/compiler/GHC/Tc/Solver/Canonical.hs b/compiler/GHC/Tc/Solver/Canonical.hs
index 4df06c2fca..e4020bdfc5 100644
--- a/compiler/GHC/Tc/Solver/Canonical.hs
+++ b/compiler/GHC/Tc/Solver/Canonical.hs
@@ -109,9 +109,10 @@ canonicalize (CIrredCan { cc_ev = ev })
     --    e.g. a ~ [a], where [G] a ~ [Int], can decompose
 
 canonicalize (CDictCan { cc_ev = ev, cc_class  = cls
-                       , cc_tyargs = xis, cc_pend_sc = pend_sc })
+                       , cc_tyargs = xis, cc_pend_sc = pend_sc
+                       , cc_fundeps = fds })
   = {-# SCC "canClass" #-}
-    canClass ev cls xis pend_sc
+    canClass ev cls xis pend_sc fds
 
 canonicalize (CEqCan { cc_ev     = ev
                      , cc_lhs    = lhs
@@ -150,7 +151,7 @@ canClassNC ev cls tys
   | isGiven ev  -- See Note [Eagerly expand given superclasses]
   = do { sc_cts <- mkStrictSuperClasses ev [] [] cls tys
        ; emitWork sc_cts
-       ; canClass ev cls tys False }
+       ; canClass ev cls tys False fds }
 
   | isWanted ev
   , Just ip_name <- isCallStackPred cls tys
@@ -174,15 +175,19 @@ canClassNC ev cls tys
        ; let ev_cs = EvCsPushCall func (ctLocSpan loc) (ctEvExpr new_ev)
        ; solveCallStack ev ev_cs
 
-       ; canClass new_ev cls tys False }
+       ; canClass new_ev cls tys
+                  False -- No superclasses
+                  False -- No top level instances for fundeps
+       }
 
   | otherwise
-  = canClass ev cls tys (has_scs cls)
+  = canClass ev cls tys (has_scs cls) fds
 
   where
     has_scs cls = not (null (classSCTheta cls))
     loc  = ctEvLoc ev
     pred = ctEvPred ev
+    fds  = classHasFds cls
 
 solveCallStack :: CtEvidence -> EvCallStack -> TcS ()
 -- Also called from GHC.Tc.Solver when defaulting call stacks
@@ -197,10 +202,11 @@ solveCallStack ev ev_cs = do
 canClass :: CtEvidence
          -> Class -> [Type]
          -> Bool            -- True <=> un-explored superclasses
+         -> Bool            -- True <=> unexploited fundep(s)
          -> TcS (StopOrContinue Ct)
 -- Precondition: EvVar is class evidence
 
-canClass ev cls tys pend_sc
+canClass ev cls tys pend_sc fds
   =   -- all classes do *nominal* matching
     ASSERT2( ctEvRole ev == Nominal, ppr ev $$ ppr cls $$ ppr tys )
     do { (xis, cos) <- rewriteArgsNom ev cls_tc tys
@@ -209,7 +215,8 @@ canClass ev cls tys pend_sc
              mk_ct new_ev = CDictCan { cc_ev = new_ev
                                      , cc_tyargs = xis
                                      , cc_class = cls
-                                     , cc_pend_sc = pend_sc }
+                                     , cc_pend_sc = pend_sc
+                                     , cc_fundeps = fds }
        ; mb <- rewriteEvidence ev xi co
        ; traceTcS "canClass" (vcat [ ppr ev
                                    , ppr xi, ppr mb ])
@@ -644,7 +651,7 @@ mk_superclasses_of rec_clss ev tvs theta cls tys
 
     this_ct | null tvs, null theta
             = CDictCan { cc_ev = ev, cc_class = cls, cc_tyargs = tys
-                       , cc_pend_sc = loop_found }
+                       , cc_pend_sc = loop_found, cc_fundeps = classHasFds cls }
                  -- NB: If there is a loop, we cut off, so we have not
                  --     added the superclasses, hence cc_pend_sc = True
             | otherwise
diff --git a/compiler/GHC/Tc/Solver/Interact.hs b/compiler/GHC/Tc/Solver/Interact.hs
index 8474ca7007..ec6e1f9853 100644
--- a/compiler/GHC/Tc/Solver/Interact.hs
+++ b/compiler/GHC/Tc/Solver/Interact.hs
@@ -1755,6 +1755,68 @@ Then it is solvable, but its very hard to detect this on the spot.
 It's exactly the same with implicit parameters, except that the
 "aggressive" approach would be much easier to implement.
 
+Note [Fundeps with instances]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+doTopFundepImprovement compares the constraint with all the instance
+declarations, to see if we can produce any derived equalities. E.g
+   class C2 a b | a -> b
+   instance C Int Bool
+Then the constraint (C Int ty) generates the Derived equality [D] ty ~ Bool.
+
+There is a nasty corner in #19415 which led to the typechecker looping:
+   class C s t b | s -> t
+   instance ... => C (T kx x) (T ky y) Int
+   T :: forall k. k -> Type
+
+   work_item: dwrk :: C (T @ka (a::ka)) (T @kb0 (b0::kb0)) Char
+      where kb0, b0 are unification vars
+   ==> {fundeps against instance; k0, y0 fresh unification vars}
+       [D] T kb0 (b0::kb0) ~ T k0 (y0::k0)
+       Add dwrk to inert set
+   ==> {solve that Derived kb0 := k0, b0 := y0
+   Now kick out dwrk, since it mentions kb0
+   But now we are back to the start!  Loop!
+
+NB1: this example relies on an instance that does not satisfy
+the coverage condition (although it may satisfy the weak coverage
+condition), which is known to lead to termination trouble
+
+NB2: if the unification was the other way round, k0:=kb0, all would be
+well.  It's a very delicate problem.
+
+The ticket #19415 discusses various solutions, but the one we adopted
+is very simple:
+
+* There is a flag in CDictCan (cc_fundeps :: Bool)
+
+* cc_fundeps = True means
+    a) The class has fundeps
+    b) We have not had a successful hit against instances yet
+
+* In doTopFundepImprovement, if we emit some Deriveds we flip the flag
+  to False, so that we won't try again with the same CDictCan.  In our
+  example, dwrk will have its flag set to False.
+
+* Not that if we have no "hits" we must /not/ flip the flag. We might have
+      dwrk :: C alpha beta Char
+  which does not yet trigger fundeps from the instance, but later we
+  get alpha := T ka a.  We could be cleverer, and spot that the constraint
+  is such that we will /never/ get any hits (no unifiers) but we don't do
+  that yet.
+
+Easy!  What could go wrong?
+* Maybe the class has multiple fundeps, and we get hit with one but not
+  the other.  Per-fundep flags?
+* Maybe we get a hit against one instance with one fundep but, after
+  the work-item is instantiated a bit more, we get a second hit
+  against a second instance.  (This is a pretty strange and
+  undesirable thing anyway, and can only happen with overlapping
+  instances; one example is in Note [Weird fundeps].)
+
+But both of these seem extremely exotic, and ignoring them threatens
+completeness (fixable with some type signature), but not termination
+(not fixable).  So for now we are just doing the simplest thing.
+
 Note [Weird fundeps]
 ~~~~~~~~~~~~~~~~~~~~
 Consider   class Het a b | a -> b where
@@ -1777,6 +1839,39 @@ as the fundeps.
 #7875 is a case in point.
 -}
 
+doTopFundepImprovement ::Ct -> TcS (StopOrContinue Ct)
+-- Try to functional-dependency improvement betweeen the constraint
+-- and the top-level instance declarations
+-- See Note [Fundeps with instances]
+-- See also Note [Weird fundeps]
+doTopFundepImprovement work_item@(CDictCan { cc_ev = ev, cc_class = cls
+                                           , cc_tyargs = xis
+                                           , cc_fundeps = has_fds })
+  | has_fds, isImprovable ev
+  = do { traceTcS "try_fundeps" (ppr work_item)
+       ; instEnvs <- getInstEnvs
+       ; let fundep_eqns = improveFromInstEnv instEnvs mk_ct_loc cls xis
+       ; case fundep_eqns of
+           [] -> continueWith work_item  -- No improvement
+           _  -> do { emitFunDepDeriveds fundep_eqns
+                    ; continueWith (work_item { cc_fundeps = False }) } }
+  | otherwise
+  = continueWith work_item
+
+  where
+     dict_pred   = mkClassPred cls xis
+     dict_loc    = ctEvLoc ev
+     dict_origin = ctLocOrigin dict_loc
+
+     mk_ct_loc :: PredType   -- From instance decl
+               -> SrcSpan    -- also from instance deol
+               -> CtLoc
+     mk_ct_loc inst_pred inst_loc
+       = dict_loc { ctl_origin = FunDepOrigin2 dict_pred dict_origin
+                                               inst_pred inst_loc }
+
+doTopFundepImprovement work_item = pprPanic "doTopFundepImprovement" (ppr work_item)
+
 emitFunDepDeriveds :: [FunDepEqn CtLoc] -> TcS ()
 -- See Note [FunDep and implicit parameter reactions]
 emitFunDepDeriveds fd_eqns
@@ -2033,8 +2128,7 @@ doTopReactDict :: InertSet -> Ct -> TcS (StopOrContinue Ct)
 doTopReactDict inerts work_item@(CDictCan { cc_ev = ev, cc_class = cls
                                           , cc_tyargs = xis })
   | isGiven ev   -- Never use instances for Given constraints
-  = do { try_fundep_improvement
-       ; continueWith work_item }
+  = doTopFundepImprovement work_item
 
   | Just solved_ev <- lookupSolvedDict inerts dict_loc cls xis   -- Cached
   = do { setEvBindIfWanted ev (ctEvTerm solved_ev)
@@ -2048,30 +2142,13 @@ doTopReactDict inerts work_item@(CDictCan { cc_ev = ev, cc_class = cls
                   -> do { insertSafeOverlapFailureTcS what work_item
                         ; addSolvedDict what ev cls xis
                         ; chooseInstance work_item lkup_res }
-               _  ->  -- NoInstance or NotSure
-                     do { when (isImprovable ev) $
-                          try_fundep_improvement
-                        ; continueWith work_item } }
+               _  -> -- NoInstance or NotSure
+                     -- We didn't solve it; so try functional dependencies with
+                     -- the instance environment, and return
+                     doTopFundepImprovement work_item }
    where
-     dict_pred   = mkClassPred cls xis
-     dict_loc    = ctEvLoc ev
-     dict_origin = ctLocOrigin dict_loc
+     dict_loc = ctEvLoc ev
 
-     -- We didn't solve it; so try functional dependencies with
-     -- the instance environment, and return
-     -- See also Note [Weird fundeps]
-     try_fundep_improvement
-        = do { traceTcS "try_fundeps" (ppr work_item)
-             ; instEnvs <- getInstEnvs
-             ; emitFunDepDeriveds $
-               improveFromInstEnv instEnvs mk_ct_loc dict_pred }
-
-     mk_ct_loc :: PredType   -- From instance decl
-               -> SrcSpan    -- also from instance deol
-               -> CtLoc
-     mk_ct_loc inst_pred inst_loc
-       = dict_loc { ctl_origin = FunDepOrigin2 dict_pred dict_origin
-                                               inst_pred inst_loc }
 
 doTopReactDict _ w = pprPanic "doTopReactDict" (ppr w)
 
diff --git a/compiler/GHC/Tc/Types/Constraint.hs b/compiler/GHC/Tc/Types/Constraint.hs
index 29344b17d7..03aff4fff4 100644
--- a/compiler/GHC/Tc/Types/Constraint.hs
+++ b/compiler/GHC/Tc/Types/Constraint.hs
@@ -163,10 +163,17 @@ data Ct
       cc_class  :: Class,
       cc_tyargs :: [Xi],   -- cc_tyargs are rewritten w.r.t. inerts, so Xi
 
-      cc_pend_sc :: Bool   -- See Note [The superclass story] in GHC.Tc.Solver.Canonical
-                           -- True <=> (a) cc_class has superclasses
-                           --          (b) we have not (yet) added those
-                           --              superclasses as Givens
+      cc_pend_sc :: Bool,
+          -- See Note [The superclass story] in GHC.Tc.Solver.Canonical
+          -- True <=> (a) cc_class has superclasses
+          --          (b) we have not (yet) added those
+          --              superclasses as Givens
+
+      cc_fundeps :: Bool
+          -- See Note [Fundeps with instances] in GHC.Tc.Solver.Interact
+          -- True <=> the class has fundeps, and we have not yet
+          --          compared this constraint with the global
+          --          instances for fundep improvement
     }
 
   | CIrredCan {  -- These stand for yet-unusable predicates
@@ -447,9 +454,11 @@ instance Outputable Ct where
       pp_sort = case ct of
          CEqCan {}        -> text "CEqCan"
          CNonCanonical {} -> text "CNonCanonical"
-         CDictCan { cc_pend_sc = pend_sc }
-            | pend_sc   -> text "CDictCan(psc)"
-            | otherwise -> text "CDictCan"
+         CDictCan { cc_pend_sc = psc, cc_fundeps = fds }
+            | psc, fds     -> text "CDictCan(psc,fds)"
+            | psc, not fds -> text "CDictCan(psc)"
+            | not psc, fds -> text "CDictCan(fds)"
+            | otherwise    -> text "CDictCan"
          CIrredCan { cc_status = status } -> text "CIrredCan" <> ppr status
          CQuantCan (QCI { qci_pend_sc = pend_sc })
             | pend_sc   -> text "CQuantCan(psc)"
diff --git a/testsuite/tests/typecheck/should_fail/T19415.hs b/testsuite/tests/typecheck/should_fail/T19415.hs
new file mode 100644
index 0000000000..667c309da1
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T19415.hs
@@ -0,0 +1,27 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+module Test where
+
+import GHC.TypeLits
+
+data Pet (a :: k) = Pet
+  { name :: String
+  } deriving Show
+
+class SetField (name :: Symbol) s t b | name t -> s b
+                                      , name s -> t b where
+  setField :: b -> s -> t
+
+instance
+  ( SetField "name" (Pet a) (Pet b) String
+  ) => SetField "name" (Pet (a :: k)) (Pet (b :: k')) String where
+  setField v d = d { name = v }
+
+loop = setField @"name" 'c' (Pet "hi")
diff --git a/testsuite/tests/typecheck/should_fail/T19415.stderr b/testsuite/tests/typecheck/should_fail/T19415.stderr
new file mode 100644
index 0000000000..899137c427
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T19415.stderr
@@ -0,0 +1,10 @@
+
+T19415.hs:27:8: error:
+    • Couldn't match type ‘[Char]’ with ‘Char’
+        arising from a functional dependency between:
+          constraint ‘SetField "name" (Pet a0) (Pet b) Char’
+            arising from a use of ‘setField’
+          instance ‘SetField "name" (Pet a) (Pet b1) String’
+            at T19415.hs:(23,3)-(24,60)
+    • In the expression: setField @"name" 'c' (Pet "hi")
+      In an equation for ‘loop’: loop = setField @"name" 'c' (Pet "hi")
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index cdf26c15be..d875b75909 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -626,3 +626,4 @@ test('T19397E3', extra_files(['T19397S.hs']), multimod_compile_fail,
     ['T19397E3.hs', '-v0 -main-is foo'])
 test('T19397E4', extra_files(['T19397S.hs']), multimod_compile_fail,
     ['T19397E4.hs', '-v0 -main-is foo'])
+test('T19415', normal, compile_fail, [''])