A CFunEqCan can be Derived

This fixes the ASSERTION failures in
  indexed-types/should_fail/T5439
  typecheck/should_fail/T5490
when GHC is compiled with -DDEBUG

See Phab:D202 attached to Trac #6018

3 files changed, 21 insertions, 10 deletions

diff --git a/compiler/typecheck/TcInteract.hs b/compiler/typecheck/TcInteract.hs
index 261d9afa51..773f2ae6fc 100644
--- a/compiler/typecheck/TcInteract.hs
+++ b/compiler/typecheck/TcInteract.hs
@@ -1378,8 +1378,7 @@ reduce_top_fun_eq old_ev fsk ax_co rhs_ty
   = shortCutReduction old_ev fsk ax_co tc tc_args
        -- Try shortcut; see Note [Short cut for top-level reaction]
 
-  | ASSERT( not (isDerived old_ev) )   -- CFunEqCan is never Derived
-    isGiven old_ev  -- Not shortcut
+  | 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 (mkTcEqPred (mkTyVarTy fsk) rhs_ty,
@@ -1387,6 +1386,7 @@ reduce_top_fun_eq old_ev fsk ax_co rhs_ty
        ; emitWorkNC [new_ev] -- Non-cannonical; that will mean we flatten rhs_ty
        ; stopWith old_ev "Fun/Top (given)" }
 
+  -- So old_ev is Wanted or Derived
   | not (fsk `elemVarSet` tyVarsOfType rhs_ty)
   = do { dischargeFmv old_ev fsk ax_co rhs_ty
        ; traceTcS "doTopReactFunEq" $
@@ -1396,8 +1396,16 @@ reduce_top_fun_eq old_ev fsk ax_co rhs_ty
 
   | otherwise -- We must not assign ufsk := ...ufsk...!
   = do { alpha_ty <- newFlexiTcSTy (tyVarKind fsk)
-       ; new_ev <- newWantedEvVarNC loc (mkTcEqPred alpha_ty rhs_ty)
-       ; emitWorkNC [new_ev]
+       ; let pred = mkTcEqPred alpha_ty rhs_ty
+       ; new_ev <- case old_ev of
+           CtWanted {}  -> do { ev <- newWantedEvVarNC loc pred
+                              ; updWorkListTcS (extendWorkListEq (mkNonCanonical ev))
+                              ; return ev }
+           CtDerived {} -> do { ev <- newDerivedNC loc pred
+                              ; updWorkListTcS (extendWorkListDerived loc ev)
+                              ; return ev }
+           _ -> pprPanic "reduce_top_fun_eq" (ppr old_ev)
+
             -- By emitting this as non-canonical, we deal with all
             -- flattening, occurs-check, and ufsk := ufsk issues
        ; let final_co = ax_co `mkTcTransCo` mkTcSymCo (ctEvCoercion new_ev)
@@ -1536,6 +1544,8 @@ dischargeFmv :: CtEvidence -> TcTyVar -> TcCoercion -> TcType -> TcS ()
 -- Then set fmv := xi,
 --      set ev := co
 --      kick out any inert things that are now rewritable
+--
+-- Does not evaluate 'co' if 'ev' is Derived
 dischargeFmv ev fmv co xi
   = ASSERT2( not (fmv `elemVarSet` tyVarsOfType xi), ppr ev $$ ppr fmv $$ ppr xi )
     do { setEvBindIfWanted ev (EvCoercion co)
diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs
index 83dc81b1ed..c4de91de24 100644
--- a/compiler/typecheck/TcRnTypes.hs
+++ b/compiler/typecheck/TcRnTypes.hs
@@ -1146,7 +1146,6 @@ data Ct
        --   * isTypeFamilyTyCon cc_fun
        --   * typeKind (F xis) = tyVarKind fsk
        --   * always Nominal role
-       --   * always Given or Wanted, never Derived
       cc_ev     :: CtEvidence,  -- See Note [Ct/evidence invariant]
       cc_fun    :: TyCon,       -- A type function
 
diff --git a/compiler/typecheck/TcSMonad.hs b/compiler/typecheck/TcSMonad.hs
index 80437ff0f5..b782a20ef2 100644
--- a/compiler/typecheck/TcSMonad.hs
+++ b/compiler/typecheck/TcSMonad.hs
@@ -6,7 +6,7 @@ module TcSMonad (
     -- The work list
     WorkList(..), isEmptyWorkList, emptyWorkList,
     extendWorkListNonEq, extendWorkListCt, extendWorkListDerived,
-    extendWorkListCts, appendWorkList,
+    extendWorkListCts, extendWorkListEq, appendWorkList,
     selectNextWorkItem,
     workListSize, workListWantedCount,
     updWorkListTcS,
@@ -25,7 +25,7 @@ module TcSMonad (
     -- Evidence creation and transformation
     Freshness(..), freshGoals, isFresh,
 
-    newTcEvBinds, newWantedEvVar, newWantedEvVarNC,
+    newTcEvBinds, newWantedEvVar, newWantedEvVarNC, newDerivedNC,
     unifyTyVar, unflattenFmv, reportUnifications,
     setEvBind, setWantedEvBind, setEvBindIfWanted,
     newEvVar, newGivenEvVar, newGivenEvVars,
@@ -539,8 +539,10 @@ data InertCans   -- See Note [Detailed InertCans Invariants] for more
 
        , inert_funeqs :: FunEqMap Ct
               -- All CFunEqCans; index is the whole family head type.
-              -- Hence (by CFunEqCan invariants),
-              -- all Nominal, and all Given/Wanted (no Derived)
+              -- All Nominal (that's an invarint of all CFunEqCans)
+              -- We can get Derived ones from e.g.
+              --   (a) flattening derived equalities
+              --   (b) emitDerivedShadows
 
        , inert_dicts :: DictMap Ct
               -- Dictionaries only, index is the class
@@ -1560,7 +1562,7 @@ After solving the Givens we take two things out of the inert set
            We get [D] 1 <= n, and we must remove it!
          Otherwise we unflatten it more then once, and assign
          to its fmv more than once...disaster.
-     It's ok to remove them because they turned ont not to
+     It's ok to remove them because they turned not not to
      yield an insoluble, and hence have now done their work.
 -}