Use dischargeFunEq consistently

Trac #15122 turned out to be interesting.

* Were calling dischargeFmv in three places.

* In all three cases we dealt with the Given case
  separately.

* In two of the three cases the Given code was right,
  (albeit duplicated).

* In the third case (in TcCanonical.canCFunEqCan), we had
     ; case flav of
         Given -> return () -- nothing more to do.
  which was utterly wrong.

The solution is easy: move the Given-case handling into
dischargeFmv (now reenamed dischargeFunEq), and delete it
from the call sites.

Result: less code, easier to understand (dischargeFunEq handles
all three cases, not just two out of three), and Trac #15122 is fixed.

5 files changed, 64 insertions, 72 deletions

diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs
index dfebb87813..d540272a53 100644
--- a/compiler/typecheck/TcCanonical.hs
+++ b/compiler/typecheck/TcCanonical.hs
@@ -1483,19 +1483,15 @@ canCFunEqCan ev fn tys fsk
                       ; return (ev', fsk) }
               else do { (ev', new_co, new_fsk)
                           <- newFlattenSkolem flav (ctEvLoc ev) fn tys'
-                      ; case flav of
-                          Given -> return () -- nothing more to do.
-                                             -- NB: new_co is stored within ev',
-                                             -- and will be put in the flat_cache below
-                          _     -> do { let xi = mkTyVarTy new_fsk `mkCastTy` kind_co
-                                               -- sym lhs_co :: F tys ~ F tys'
-                                               -- new_co     :: F tys' ~ new_fsk
-                                               -- co         :: F tys ~ (new_fsk |> kind_co)
-                                            co = mkTcSymCo lhs_co `mkTcTransCo`
-                                                 (new_co `mkTcCoherenceRightCo` kind_co)
-
-                                      ; traceTcS "Discharging fmv due to hetero flattening" empty
-                                      ; dischargeFmv ev fsk co xi }
+                      ; let xi = mkTyVarTy new_fsk `mkCastTy` kind_co
+                               -- sym lhs_co :: F tys ~ F tys'
+                               -- new_co     :: F tys' ~ new_fsk
+                               -- co         :: F tys ~ (new_fsk |> kind_co)
+                            co = mkTcSymCo lhs_co `mkTcTransCo`
+                                 (new_co `mkTcCoherenceRightCo` kind_co)
+
+                      ; traceTcS "Discharging fmv/fsk due to hetero flattening" (ppr ev)
+                      ; dischargeFunEq ev fsk co xi
                       ; return (ev', new_fsk) }
 
        ; extendFlatCache fn tys' (ctEvCoercion ev', mkTyVarTy fsk', ctEvFlavour ev')
@@ -1588,16 +1584,12 @@ canEqTyVarHetero ev eq_rel tv1 co1 ki1 ps_tv1 xi2 ki2 ps_xi2
   | CtGiven { ctev_evar = evar } <- ev
     -- unswapped: tm :: (lhs :: ki1) ~ (rhs :: ki2)
     -- swapped  : tm :: (rhs :: ki2) ~ (lhs :: ki1)
-  = do { kind_ev_id <- newBoundEvVarId kind_pty
-                                       (evCoercion $ mkTcKindCo $ mkTcCoVarCo evar)
-           -- kind_ev_id :: (ki1 :: *) ~ (ki2 :: *)   (whether swapped or not)
-       ; let kind_ev = CtGiven { ctev_pred = kind_pty
-                               , ctev_evar = kind_ev_id
-                               , ctev_loc  = kind_loc }
+  = do { let kind_co = mkTcKindCo (mkTcCoVarCo evar)
+       ; kind_ev <- newGivenEvVar kind_loc (kind_pty, evCoercion kind_co)
+       ; let  -- kind_ev :: (ki1 :: *) ~ (ki2 :: *)   (whether swapped or not)
               -- co1     :: kind(tv1) ~N ki1
               -- homo_co :: ki2 ~N kind(tv1)
-             homo_co = mkTcSymCo (mkCoVarCo kind_ev_id) `mkTcTransCo` mkTcSymCo co1
-
+             homo_co = mkTcSymCo (ctEvCoercion kind_ev) `mkTcTransCo` mkTcSymCo co1
              rhs'    = mkCastTy xi2 homo_co     -- :: kind(tv1)
              ps_rhs' = mkCastTy ps_xi2 homo_co  -- :: kind(tv1)
              rhs_co  = mkReflCo role xi2 `mkTcCoherenceLeftCo` homo_co
@@ -1608,7 +1600,7 @@ canEqTyVarHetero ev eq_rel tv1 co1 ki1 ps_tv1 xi2 ki2 ps_xi2
                -- lhs_co :: (tv1 :: kind(tv1)) ~ (tv1 |> co1 :: ki1)
 
        ; traceTcS "Hetero equality gives rise to given kind equality"
-           (ppr kind_ev_id <+> dcolon <+> ppr kind_pty)
+           (ppr kind_ev <+> dcolon <+> ppr kind_pty)
        ; emitWorkNC [kind_ev]
        ; type_ev <- rewriteEqEvidence ev NotSwapped lhs' rhs' lhs_co rhs_co
        ; canEqTyVarHomo type_ev eq_rel NotSwapped tv1 ps_tv1 rhs' ps_rhs' }
diff --git a/compiler/typecheck/TcInteract.hs b/compiler/typecheck/TcInteract.hs
index 09cfd15a30..b2be509b69 100644
--- a/compiler/typecheck/TcInteract.hs
+++ b/compiler/typecheck/TcInteract.hs
@@ -1432,20 +1432,9 @@ reactFunEq :: CtEvidence -> TcTyVar    -- From this  :: F args1 ~ fsk1
            -> CtEvidence -> TcTyVar    -- Solve this :: F args2 ~ fsk2
            -> TcS ()
 reactFunEq from_this fsk1 solve_this fsk2
-  | CtGiven { ctev_evar = evar, ctev_loc = loc } <- solve_this
-  = do { let fsk_eq_co = mkTcSymCo (mkTcCoVarCo evar) `mkTcTransCo`
-                         ctEvCoercion from_this
-                         -- :: fsk2 ~ fsk1
-             fsk_eq_pred = mkTcEqPredLikeEv solve_this
-                             (mkTyVarTy fsk2) (mkTyVarTy fsk1)
-
-       ; new_ev <- newGivenEvVar loc (fsk_eq_pred, evCoercion fsk_eq_co)
-       ; emitWorkNC [new_ev] }
-
-  | otherwise  -- Wanted
-  = do { traceTcS "reactFunEq (Wanted/Derived)"
+  = do { traceTcS "reactFunEq"
             (vcat [ppr from_this, ppr fsk1, ppr solve_this, ppr fsk2])
-       ; dischargeFmv solve_this fsk2 (ctEvCoercion from_this) (mkTyVarTy fsk1)
+       ; dischargeFunEq solve_this fsk2 (ctEvCoercion from_this) (mkTyVarTy fsk1)
        ; traceTcS "reactFunEq done" (ppr from_this $$ ppr fsk1 $$
                                      ppr solve_this $$ ppr fsk2) }
 
@@ -1892,40 +1881,25 @@ reduce_top_fun_eq :: CtEvidence -> TcTyVar -> (TcCoercion, TcType)
                   -> TcS (StopOrContinue Ct)
 -- We have found an applicable top-level axiom: use it to reduce
 -- Precondition: fsk is not free in rhs_ty
---               old_ev is not Derived
 reduce_top_fun_eq old_ev fsk (ax_co, rhs_ty)
-  | isDerived old_ev
-  = do { emitNewDerivedEq loc Nominal (mkTyVarTy fsk) rhs_ty
-       ; stopWith old_ev "Fun/Top (derived)" }
-
-  | Just (tc, tc_args) <- tcSplitTyConApp_maybe rhs_ty
+  | not (isDerived old_ev)  -- Precondition of shortCutReduction
+  , Just (tc, tc_args) <- tcSplitTyConApp_maybe rhs_ty
   , isTypeFamilyTyCon tc
   , tc_args `lengthIs` tyConArity tc    -- Short-cut
   = -- RHS is another type-family application
     -- Try shortcut; see Note [Top-level reductions for type functions]
-    shortCutReduction old_ev fsk ax_co tc tc_args
-
-  | isGiven old_ev  -- Not shortcut
-  = do { let final_co = mkTcSymCo (ctEvCoercion old_ev) `mkTcTransCo` ax_co
-              -- final_co :: fsk ~ rhs_ty
-       ; new_ev <- newGivenEvVar deeper_loc (mkPrimEqPred (mkTyVarTy fsk) rhs_ty,
-                                             evCoercion final_co)
-       ; emitWorkNC [new_ev] -- Non-cannonical; that will mean we flatten rhs_ty
-       ; stopWith old_ev "Fun/Top (given)" }
+    do { shortCutReduction old_ev fsk ax_co tc tc_args
+       ; stopWith old_ev "Fun/Top (shortcut)" }
 
-  | otherwise   -- So old_ev is Wanted (cannot be Derived)
+  | otherwise
   = ASSERT2( not (fsk `elemVarSet` tyCoVarsOfType rhs_ty)
            , ppr old_ev $$ ppr rhs_ty )
            -- Guaranteed by Note [FunEq occurs-check principle]
-    do { dischargeFmv old_ev fsk ax_co rhs_ty
+    do { dischargeFunEq old_ev fsk ax_co rhs_ty
        ; traceTcS "doTopReactFunEq" $
          vcat [ text "old_ev:" <+> ppr old_ev
               , nest 2 (text ":=") <+> ppr ax_co ]
-       ; stopWith old_ev "Fun/Top (wanted)" }
-
-  where
-    loc = ctEvLoc old_ev
-    deeper_loc = bumpCtLocDepth loc
+       ; stopWith old_ev "Fun/Top" }
 
 improveTopFunEqs :: CtEvidence -> TyCon -> [TcType] -> TcTyVar -> TcS ()
 -- See Note [FunDep and implicit parameter reactions]
@@ -2020,7 +1994,7 @@ improve_top_fun_eqs fam_envs fam_tc args rhs_ty
 
 
 shortCutReduction :: CtEvidence -> TcTyVar -> TcCoercion
-                  -> TyCon -> [TcType] -> TcS (StopOrContinue Ct)
+                  -> TyCon -> [TcType] -> TcS ()
 -- See Note [Top-level reductions for type functions]
 -- Previously, we flattened the tc_args here, but there's no need to do so.
 -- And, if we did, this function would have all the complication of
@@ -2045,8 +2019,7 @@ shortCutReduction old_ev fsk ax_co fam_tc tc_args
 
        ; let new_ct = CFunEqCan { cc_ev = new_ev, cc_fun = fam_tc
                                 , cc_tyargs = tc_args, cc_fsk = fsk }
-       ; updWorkListTcS (extendWorkListFunEq new_ct)
-       ; stopWith old_ev "Fun/Top (shortcut)" }
+       ; updWorkListTcS (extendWorkListFunEq new_ct) }
   where
     deeper_loc = bumpCtLocDepth (ctEvLoc old_ev)
 
diff --git a/compiler/typecheck/TcSMonad.hs b/compiler/typecheck/TcSMonad.hs
index f5d6ca9aa7..d26275b839 100644
--- a/compiler/typecheck/TcSMonad.hs
+++ b/compiler/typecheck/TcSMonad.hs
@@ -83,7 +83,7 @@ module TcSMonad (
 
     -- The flattening cache
     lookupFlatCache, extendFlatCache, newFlattenSkolem,            -- Flatten skolems
-    dischargeFmv, pprKicked,
+    dischargeFunEq, pprKicked,
 
     -- Inert CFunEqCans
     updInertFunEqs, findFunEq,
@@ -3044,12 +3044,14 @@ demoteUnfilledFmv fmv
                       ; TcM.writeMetaTyVar fmv tv_ty } }
 
 -----------------------------
-dischargeFmv :: CtEvidence -> TcTyVar -> TcCoercion -> TcType -> TcS ()
--- (dischargeFmv ev fmv co ty)
---     [W] ev :: F tys ~ fmv
---         co :: F tys ~ xi
--- Precondition: fmv is not filled, and fmv `notElem` xi
---               ev is Wanted or Derived
+dischargeFunEq :: CtEvidence -> TcTyVar -> TcCoercion -> TcType -> TcS ()
+-- (dischargeFunEqCan ev tv co ty)
+--     Preconditions
+--       - ev :: F tys ~ tv   is a CFunEqCan
+--       - tv is a FlatMetaTv of FlatSkolTv
+--       - co :: F tys ~ xi
+--       - fmv/fsk `notElem` xi
+--       - fmv not filled (for Wanteds)
 --
 -- Then for [W] or [WD], we actually fill in the fmv:
 --      set fmv := xi,
@@ -3057,24 +3059,32 @@ dischargeFmv :: CtEvidence -> TcTyVar -> TcCoercion -> TcType -> TcS ()
 --      kick out any inert things that are now rewritable
 --
 -- For [D], we instead emit an equality that must ultimately hold
---      emit  xi ~ fmv
+--      [D] xi ~ fmv
 --      Does not evaluate 'co' if 'ev' is Derived
 --
+-- For [G], emit this equality
+--     [G] (sym ev; co) :: fsk ~ xi
+
 -- See TcFlatten Note [The flattening story],
 -- especially "Ownership of fsk/fmv"
-dischargeFmv ev@(CtWanted { ctev_dest = dest }) fmv co xi
+dischargeFunEq (CtGiven { ctev_evar = old_evar, ctev_loc = loc }) fsk co xi
+  = do { new_ev <- newGivenEvVar loc ( new_pred, evCoercion new_co  )
+       ; emitWorkNC [new_ev] }
+  where
+    new_pred = mkPrimEqPred (mkTyVarTy fsk) xi
+    new_co   = mkTcSymCo (mkTcCoVarCo old_evar) `mkTcTransCo` co
+
+dischargeFunEq ev@(CtWanted { ctev_dest = dest }) fmv co xi
   = ASSERT2( not (fmv `elemVarSet` tyCoVarsOfType xi), ppr ev $$ ppr fmv $$ ppr xi )
     do { setWantedEvTerm dest (EvExpr (evCoercion co))
        ; unflattenFmv fmv xi
        ; n_kicked <- kickOutAfterUnification fmv
        ; traceTcS "dischargeFmv" (ppr fmv <+> equals <+> ppr xi $$ pprKicked n_kicked) }
 
-dischargeFmv (CtDerived { ctev_loc = loc }) fmv _co xi
+dischargeFunEq (CtDerived { ctev_loc = loc }) fmv _co xi
   = emitNewDerivedEq loc Nominal xi (mkTyVarTy fmv)
               -- FunEqs are always at Nominal role
 
-dischargeFmv ev _ _ _ = pprPanic "dischargeFmv" (ppr ev)
-
 pprKicked :: Int -> SDoc
 pprKicked 0 = empty
 pprKicked n = parens (int n <+> text "kicked out")
diff --git a/testsuite/tests/indexed-types/should_compile/T15122.hs b/testsuite/tests/indexed-types/should_compile/T15122.hs
new file mode 100644
index 0000000000..44a3c0523f
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T15122.hs
@@ -0,0 +1,16 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+module T15122 where
+
+import Data.Kind
+import Data.Proxy
+
+data IsStar (a :: k) where
+  IsStar :: IsStar (a :: *)
+
+type family F (a :: k) :: k
+
+foo :: (F a ~ F b) => IsStar a -> Proxy b
+                   -> Proxy (F a) -> Proxy (F b)
+foo IsStar _ p = p
diff --git a/testsuite/tests/indexed-types/should_compile/all.T b/testsuite/tests/indexed-types/should_compile/all.T
index 9f0d9b4a8d..5a6ae27aac 100644
--- a/testsuite/tests/indexed-types/should_compile/all.T
+++ b/testsuite/tests/indexed-types/should_compile/all.T
@@ -281,3 +281,4 @@ test('T14554', normal, compile, [''])
 test('T14680', normal, compile, [''])
 test('T15057', normal, compile, [''])
 test('T15144', normal, compile, [''])
+test('T15122', normal, compile, [''])