Another major constraint-solver refactoring
authorSimon Peyton Jones <simonpj@microsoft.com>
Tue, 25 Oct 2016 16:41:45 +0000 (17:41 +0100)
committerSimon Peyton Jones <simonpj@microsoft.com>
Fri, 25 Nov 2016 11:18:52 +0000 (11:18 +0000)
This patch takes further my refactoring of the constraint
solver, which I've been doing over the last couple of months
in consultation with Richard.

It fixes a number of tricky bugs that made the constraint
solver actually go into a loop, including

  Trac #12526
  Trac #12444
  Trac #12538

The main changes are these

* Flatten unification variables (fmvs/fuvs) appear on the LHS
  of a tvar/tyvar equality; thus
           fmv ~ alpha
  and not
           alpha ~ fmv

  See Note [Put flatten unification variables on the left]
  in TcUnify.  This is implemented by TcUnify.swapOverTyVars.

* Don't reduce a "loopy" CFunEqCan where the fsk appears on
  the LHS:
      F t1 .. tn ~ fsk
  where 'fsk' is free in t1..tn.
  See Note [FunEq occurs-check principle] in TcInteract

  This neatly stops some infinite loops that people reported;
  and it allows us to delete some crufty code in reduce_top_fun_eq.
  And it appears to be no loss whatsoever.

  As well as fixing loops, ContextStack2 and T5837 both terminate
  when they didn't before.

* Previously we generated "derived shadow" constraints from
  Wanteds, but we could (and sometimes did; Trac #xxxx) repeatedly
  generate a derived shadow from the same Wanted.

  A big change in this patch is to have two kinds of Wanteds:
     [WD] behaves like a pair of a Wanted and a Derived
     [W]  behaves like a Wanted only
  See CtFlavour and ShadowInfo in TcRnTypes, and the ctev_nosh
  field of a Wanted.

  This turned out to be a lot simpler.  A [WD] gets split into a
  [W] and a [D] in TcSMonad.maybeEmitShaodow.

  See TcSMonad Note [The improvement story and derived shadows]

* Rather than have a separate inert_model in the InertCans, I've
  put the derived equalities back into inert_eqs.  We weren't
  gaining anything from a separate field.

* Previously we had a mode for the constraint solver in which it
  would more aggressively solve Derived constraints; it was used
  for simplifying the context of a 'deriving' clause, or a 'default'
  delcaration, for example.

  But the complexity wasn't worth it; now I just make proper Wanted
  constraints.  See TcMType.cloneWC

* Don't generate injectivity improvement for Givens; see
  Note [No FunEq improvement for Givens] in TcInteract

* solveSimpleWanteds leaves the insolubles in-place rather than
  returning them.  Simpler.

I also did lots of work on comments, including fixing Trac #12821.

48 files changed:
compiler/iface/ToIface.hs
compiler/typecheck/TcCanonical.hs
compiler/typecheck/TcErrors.hs
compiler/typecheck/TcExpr.hs
compiler/typecheck/TcFlatten.hs
compiler/typecheck/TcInteract.hs
compiler/typecheck/TcMType.hs
compiler/typecheck/TcRnTypes.hs
compiler/typecheck/TcRules.hs
compiler/typecheck/TcSMonad.hs
compiler/typecheck/TcSimplify.hs
compiler/typecheck/TcType.hs
compiler/typecheck/TcUnify.hs
testsuite/tests/indexed-types/should_compile/T10226.hs
testsuite/tests/indexed-types/should_compile/T10634.hs
testsuite/tests/indexed-types/should_compile/T12526.hs [new file with mode: 0644]
testsuite/tests/indexed-types/should_compile/T12538.hs [new file with mode: 0644]
testsuite/tests/indexed-types/should_compile/T12538.stderr [new file with mode: 0644]
testsuite/tests/indexed-types/should_compile/T3017.stderr
testsuite/tests/indexed-types/should_compile/T4338.hs
testsuite/tests/indexed-types/should_compile/all.T
testsuite/tests/indexed-types/should_fail/T2544.stderr
testsuite/tests/indexed-types/should_fail/T2627b.stderr
testsuite/tests/indexed-types/should_fail/T3330c.stderr
testsuite/tests/indexed-types/should_fail/T4179.stderr
testsuite/tests/indexed-types/should_fail/T6123.stderr
testsuite/tests/indexed-types/should_fail/T7786.hs
testsuite/tests/indexed-types/should_fail/T7786.stderr
testsuite/tests/indexed-types/should_fail/T8227.stderr
testsuite/tests/partial-sigs/should_compile/T10403.stderr
testsuite/tests/perf/compiler/T5837.hs
testsuite/tests/perf/compiler/T5837.stderr [deleted file]
testsuite/tests/perf/compiler/all.T
testsuite/tests/polykinds/T12444.hs [new file with mode: 0644]
testsuite/tests/polykinds/T12444.stderr [new file with mode: 0644]
testsuite/tests/polykinds/T9222.stderr
testsuite/tests/polykinds/all.T
testsuite/tests/typecheck/should_compile/Improvement.hs
testsuite/tests/typecheck/should_compile/T6018.hs
testsuite/tests/typecheck/should_compile/T6018.stderr
testsuite/tests/typecheck/should_fail/ContextStack2.hs
testsuite/tests/typecheck/should_fail/ContextStack2.stderr [deleted file]
testsuite/tests/typecheck/should_fail/Makefile
testsuite/tests/typecheck/should_fail/T5691.stderr
testsuite/tests/typecheck/should_fail/T5853.stderr
testsuite/tests/typecheck/should_fail/T8450.stderr
testsuite/tests/typecheck/should_fail/T9260.stderr
testsuite/tests/typecheck/should_fail/all.T

index 48a95a9..7e892b6 100644 (file)
@@ -107,6 +107,8 @@ toIfaceKind = toIfaceType
 toIfaceType :: Type -> IfaceType
 -- Synonyms are retained in the interface type
 toIfaceType (TyVarTy tv)      = IfaceTyVar (toIfaceTyVar tv)
+--  | isTcTyVar tv = IfaceTyVar (toIfaceTyVar tv `appendFS` consFS '_' (mkFastString (showSDocUnsafe (ppr (getUnique tv)))))
+--  | otherwise
 toIfaceType (AppTy t1 t2)     = IfaceAppTy (toIfaceType t1) (toIfaceType t2)
 toIfaceType (LitTy n)         = IfaceLitTy (toIfaceTyLit n)
 toIfaceType (ForAllTy b t)    = IfaceForAllTy (toIfaceForAllBndr b) (toIfaceType t)
index 209eec9..5aeeeb8 100644 (file)
@@ -3,7 +3,7 @@
 module TcCanonical(
      canonicalize,
      unifyDerived,
-     makeSuperClasses,
+     makeSuperClasses, maybeSym,
      StopOrContinue(..), stopWith, continueWith
   ) where
 
index d73c94f..276a6b8 100644 (file)
@@ -2682,13 +2682,14 @@ relevantBindings want_filtering ctxt ct
                    -- et really should be filled in by now. But there's a chance
                    -- it hasn't, if, say, we're reporting a kind error en route to
                    -- checking a term. See test indexed-types/should_fail/T8129
-               ; ty <- case mb_ty of
-                   Just ty -> return ty
-                   Nothing -> do { traceTc "Defaulting an ExpType in relevantBindings"
-                                     (ppr et)
-                                 ; expTypeToType et }
-               ; go2 name ty top_lvl }
+                   -- Or we are reporting errors from the ambiguity check on
+                   -- a local type signature
+               ; case mb_ty of
+                   Just ty -> go2 name ty top_lvl
+                   Nothing -> discard_it  -- No info; discard
+               }
       where
+        discard_it = go tidy_env ct_tvs n_left tvs_seen docs discards tc_bndrs
         go2 id_name id_type top_lvl
           = do { (tidy_env', tidy_ty) <- zonkTidyTcType tidy_env id_type
                ; traceTc "relevantBindings 1" (ppr id_name <+> dcolon <+> ppr tidy_ty)
@@ -2702,17 +2703,19 @@ relevantBindings want_filtering ctxt ct
                                     && id_tvs `disjointVarSet` ct_tvs)
                           -- We want to filter out this binding anyway
                           -- so discard it silently
-                 then go tidy_env ct_tvs n_left tvs_seen docs discards tc_bndrs
+                 then discard_it
 
                  else if isTopLevel top_lvl && not (isNothing n_left)
                           -- It's a top-level binding and we have not specified
                           -- -fno-max-relevant-bindings, so discard it silently
-                 then go tidy_env ct_tvs n_left tvs_seen docs discards tc_bndrs
+                 then discard_it
 
                  else if run_out n_left && id_tvs `subVarSet` tvs_seen
                           -- We've run out of n_left fuel and this binding only
                           -- mentions aleady-seen type variables, so discard it
-                 then go tidy_env ct_tvs n_left tvs_seen docs True tc_bndrs
+                 then go tidy_env ct_tvs n_left tvs_seen docs
+                         True      -- Record that we have now discarded something
+                         tc_bndrs
 
                           -- Keep this binding, decrement fuel
                  else go tidy_env' ct_tvs (dec_max n_left) new_seen (doc:docs) discards tc_bndrs }
index 4c7417f..39a8884 100644 (file)
@@ -1669,6 +1669,7 @@ tcUnboundId unbound res_ty
       ; loc <- getCtLocM HoleOrigin Nothing
       ; let can = CHoleCan { cc_ev = CtWanted { ctev_pred = ty
                                               , ctev_dest = EvVarDest ev
+                                              , ctev_nosh = WDeriv
                                               , ctev_loc  = loc}
                            , cc_hole = ExprHole unbound }
       ; emitInsoluble can
index 6987191..3adbee1 100644 (file)
@@ -22,6 +22,7 @@ import VarEnv
 import NameEnv
 import Outputable
 import TcSMonad as TcS
+import BasicTypes( SwapFlag(..) )
 
 import Util
 import Bag
@@ -62,11 +63,16 @@ Note [The flattening story]
                        then xis1 /= xis2
   i.e. at most one CFunEqCan with a particular LHS
 
-* Each canonical CFunEqCan x : F xis ~ fsk/fmv has its own
-  distinct evidence variable x and flatten-skolem fsk/fmv.
+* Each canonical [G], [W], or [WD] CFunEqCan x : F xis ~ fsk/fmv
+  has its own distinct evidence variable x and flatten-skolem fsk/fmv.
   Why? We make a fresh fsk/fmv when the constraint is born;
   and we never rewrite the RHS of a CFunEqCan.
 
+  In contrast a [D] CFunEqCan shares its fmv with its partner [W],
+  but does not "own" it.  If we reduce a [D] F Int ~ fmv, where
+  say type instance F Int = ty, then we don't discharge fmv := ty.
+  Rather we simply generate [D] fmv ~ ty
+
 * Function applications can occur in the RHS of a CTyEqCan.  No reason
   not allow this, and it reduces the amount of flattening that must occur.
 
@@ -144,7 +150,7 @@ But since fsk = F alpha Int, this is really an occurs check error.  If
 that is all we know about alpha, we will succeed in constraint
 solving, producing a program with an infinite type.
 
-Even if we did finally get (g : fsk ~ Boo)l by solving (F alpha Int ~ fsk)
+Even if we did finally get (g : fsk ~ Bool) by solving (F alpha Int ~ fsk)
 using axiom, zonking would not see it, so (x::alpha) sitting in the
 tree will get zonked to an infinite type.  (Zonking always only does
 refl stuff.)
@@ -161,8 +167,9 @@ Look at Simple13, with unification-fmvs only
   [W] x : F a ~ fmv
 
 --> subst a in x
-       x = F g' ; x2
-   [W] x2 : F [fmv] ~ fmv
+  g' = g;[x]
+  x = F g' ; x2
+  [W] x2 : F [fmv] ~ fmv
 
 And now we have an evidence cycle between g' and x!
 
@@ -203,67 +210,32 @@ Moreover these two errors could arise in entirely unrelated parts of
 the code.  (In the alpha case, there must be *some* connection (eg
 v:alpha in common envt).)
 
-Note [Orientation of equalities with fmvs] and
 Note [Unflattening can force the solver to iterate]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Here is a bad dilemma concerning flatten meta-vars (fmvs).
-
-This example comes from IndTypesPerfMerge, T10226, T10009.
-From the ambiguity check for
-  f :: (F a ~ a) => a
-we get:
-      [G] F a ~ a
-      [W] F alpha ~ alpha, alpha ~ a
-
-From Givens we get
-      [G] F a ~ fsk, fsk ~ a
-
-Now if we flatten we get
-      [W] alpha ~ fmv, F alpha ~ fmv, alpha ~ a
-
-Now, processing the first one first, choosing alpha := fmv
-      [W] F fmv ~ fmv, fmv ~ a
-
-And now we are stuck.  We must either *unify* fmv := a, or
-use the fmv ~ a to rewrite F fmv ~ fmv, so we can make it
-meet up with the given F a ~ blah.
+Look at Trac #10340:
+   type family Any :: *   -- No instances
+   get :: MonadState s m => m s
+   instance MonadState s (State s) where ...
 
-Old solution: always put fmvs on the left, so we get
-      [W] fmv ~ alpha, F alpha ~ fmv, alpha ~ a
-
-BUT this works badly for Trac #10340:
-     get :: MonadState s m => m s
-     instance MonadState s (State s) where ...
-
-     foo :: State Any Any
-     foo = get
+   foo :: State Any Any
+   foo = get
 
 For 'foo' we instantiate 'get' at types mm ss
-       [W] MonadState ss mm, [W] mm ss ~ State Any Any
+   [WD] MonadState ss mm, [WD] mm ss ~ State Any Any
 Flatten, and decompose
-       [W] MonadState ss mm, [W] Any ~ fmv, [W] mm ~ State fmv, [W] fmv ~ ss
+   [WD] MonadState ss mm, [WD] Any ~ fmv
+   [WD] mm ~ State fmv, [WD] fmv ~ ss
 Unify mm := State fmv:
-       [W] MonadState ss (State fmv), [W] Any ~ fmv, [W] fmv ~ ss
-If we orient with (untouchable) fmv on the left we are now stuck:
-alas, the instance does not match!!  But if instead we orient with
-(touchable) ss on the left, we unify ss:=fmv, to get
-       [W] MonadState fmv (State fmv), [W] Any ~ fmv
-Now we can solve.
-
-This is a real dilemma. CURRENT SOLUTION:
- * Orient with touchable variables on the left.  This is the
-   simple, uniform thing to do.  So we would orient ss ~ fmv,
-   not the other way round.
-
- * In the 'f' example, we get stuck with
-        F fmv ~ fmv, fmv ~ a
-   But during unflattening we will fail to dischargeFmv for the
-   CFunEqCan F fmv ~ fmv, because fmv := F fmv would make an ininite
-   type.  Instead we unify fmv:=a, AND record that we have done so.
-
-   If any such "non-CFunEqCan unifications" take place (in
-   unflatten_eq in TcFlatten.unflatten) iterate the entire process.
-   This is done by the 'go' loop in solveSimpleWanteds.
+   [WD] MonadState ss (State fmv)
+   [WD] Any ~ fmv, [WD] fmv ~ ss
+Now we are stuck; the instance does not match!!  So unflatten:
+   fmv := Any
+   ss := Any    (*)
+   [WD] MonadState Any (State Any)
+
+The unification (*) represents progress, so we must do a second
+round of solving; this time it succeeds. This is done by the 'go'
+loop in solveSimpleWanteds.
 
 This story does not feel right but it's the best I can do; and the
 iteration only happens in pretty obscure circumstances.
@@ -271,26 +243,6 @@ iteration only happens in pretty obscure circumstances.
 
 ************************************************************************
 *                                                                      *
-*                  Other notes (Oct 14)
-      I have not revisted these, but I didn't want to discard them
-*                                                                      *
-************************************************************************
-
-
-Try: rewrite wanted with wanted only for fmvs (not all meta-tyvars)
-
-But:   fmv ~ alpha[0]
-       alpha[0] ~ fmv’
-Now we don’t see that fmv ~ fmv’, which is a problem for injectivity detection.
-
-Conclusion: rewrite wanteds with wanted for all untouchables.
-
-skol ~ untch, must re-orieint to untch ~ skol, so that we can use it to rewrite.
-
-
-
-************************************************************************
-*                                                                      *
 *                  Examples
      Here is a long series of examples I had to work through
 *                                                                      *
@@ -313,9 +265,6 @@ axiom F [a] = [F a]
  [G] a ~ [fsk2]
  [G] fsk ~ a
 
-
------------------------------------
-
 ----------------------------------------
 indexed-types/should_compile/T44984
 
@@ -510,6 +459,16 @@ data FlattenMode  -- Postcondition for all three: inert wrt the type substitutio
 --                           --  * If flat_top is True, top level is not a function application
 --                           --   (but under type constructors is ok e.g. [F a])
 
+instance Outputable FlattenMode where
+  ppr FM_FlattenAll = text "FM_FlattenAll"
+  ppr FM_SubstOnly  = text "FM_SubstOnly"
+
+eqFlattenMode :: FlattenMode -> FlattenMode -> Bool
+eqFlattenMode FM_FlattenAll FM_FlattenAll = True
+eqFlattenMode FM_SubstOnly  FM_SubstOnly  = True
+--  FM_Avoid tv1 b1 `eq` FM_Avoid tv2 b2 = tv1 == tv2 && b1 == b2
+eqFlattenMode _  _ = False
+
 mkFlattenEnv :: FlattenMode -> CtEvidence -> FlatWorkListRef -> FlattenEnv
 mkFlattenEnv fm ctev ref = FE { fe_mode    = fm
                               , fe_loc     = ctEvLoc ctev
@@ -612,14 +571,9 @@ setEqRel new_eq_rel thing_inside
 setMode :: FlattenMode -> FlatM a -> FlatM a
 setMode new_mode thing_inside
   = FlatM $ \env ->
-    if new_mode `eq` fe_mode env
+    if new_mode `eqFlattenMode` fe_mode env
     then runFlatM thing_inside env
     else runFlatM thing_inside (env { fe_mode = new_mode })
-  where
-    FM_FlattenAll   `eq` FM_FlattenAll   = True
-    FM_SubstOnly    `eq` FM_SubstOnly    = True
---  FM_Avoid tv1 b1 `eq` FM_Avoid tv2 b2 = tv1 == tv2 && b1 == b2
-    _               `eq` _               = False
 
 -- | Use when flattening kinds/kind coercions. See
 -- Note [No derived kind equalities] in TcCanonical
@@ -628,7 +582,7 @@ flattenKinds thing_inside
   = FlatM $ \env ->
     let kind_flav = case fe_flavour env of
                       Given -> Given
-                      _     -> Wanted
+                      _     -> Wanted WDeriv
     in
     runFlatM thing_inside (env { fe_eq_rel = NomEq, fe_flavour = kind_flav })
 
@@ -637,15 +591,6 @@ bumpDepth (FlatM thing_inside)
   = FlatM $ \env -> do { let env' = env { fe_loc = bumpCtLocDepth (fe_loc env) }
                        ; thing_inside env' }
 
--- Flatten skolems
--- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-newFlattenSkolemFlatM :: TcType         -- F xis
-                      -> FlatM (CtEvidence, Coercion, TcTyVar) -- [W] x:: F xis ~ fsk
-newFlattenSkolemFlatM ty
-  = do { flavour <- getFlavour
-       ; loc <- getLoc
-       ; liftTcS $ newFlattenSkolem flavour loc ty }
-
 {-
 Note [The flattening work list]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -795,6 +740,7 @@ flattenManyNom ev tys
        ; traceTcS "flatten }" (vcat (map ppr tys'))
        ; return (tys', cos) }
 
+
 {- *********************************************************************
 *                                                                      *
 *           The main flattening functions
@@ -1113,15 +1059,14 @@ flatten_exact_fam_app tc tys
   = do { mode <- getMode
        ; role <- getRole
        ; case mode of
-           FM_FlattenAll -> flatten_exact_fam_app_fully tc tys
-
-           FM_SubstOnly -> do { (xis, cos) <- flatten_many roles tys
+               -- These roles are always going to be Nominal for now,
+               -- but not if #8177 is implemented
+           FM_SubstOnly -> do { let roles = tyConRolesX role tc
+                              ; (xis, cos) <- flatten_many roles tys
                               ; return ( mkTyConApp tc xis
                                        , mkTyConAppCo role tc cos ) }
-             where
-               -- These are always going to be Nominal for now,
-               -- but not if #8177 is implemented
-               roles = tyConRolesX role tc }
+
+           FM_FlattenAll -> flatten_exact_fam_app_fully tc tys }
 
 --       FM_Avoid tv flat_top ->
 --         do { (xis, cos) <- flatten_many fmode roles tys
@@ -1134,20 +1079,22 @@ flatten_exact_fam_app_fully tc tys
   -- See Note [Reduce type family applications eagerly]
   = try_to_reduce tc tys False id $
     do { -- First, flatten the arguments
-       ; (xis, cos) <- setEqRel NomEq $ flatten_many_nom tys
-       ; eq_rel <- getEqRel
+       ; (xis, cos) <- setEqRel NomEq    $
+                       flatten_many_nom tys
+       ; eq_rel   <- getEqRel
+       ; cur_flav <- getFlavour
        ; let role   = eqRelRole eq_rel
              ret_co = mkTyConAppCo role tc cos
               -- ret_co :: F xis ~ F tys
 
         -- Now, look in the cache
        ; mb_ct <- liftTcS $ lookupFlatCache tc xis
-       ; fr <- getFlavourRole
        ; case mb_ct of
            Just (co, rhs_ty, flav)  -- co :: F xis ~ fsk
-             | (flav, NomEq) `funEqCanDischargeFR` fr
+                -- flav is [G] or [WD]
+                -- See Note [Type family equations] in TcSMonad
+             | (NotSwapped, _) <- flav `funEqCanDischargeF` cur_flav
              ->  -- Usable hit in the flat-cache
-                 -- We certainly *can* use a Wanted for a Wanted
                 do { traceFlat "flatten/flat-cache hit" $ (ppr tc <+> ppr xis $$ ppr rhs_ty)
                    ; (fsk_xi, fsk_co) <- flatten_one rhs_ty
                           -- The fsk may already have been unified, so flatten it
@@ -1161,11 +1108,8 @@ flatten_exact_fam_app_fully tc tys
            -- Try to reduce the family application right now
            -- See Note [Reduce type family applications eagerly]
            _ -> try_to_reduce tc xis True (`mkTransCo` ret_co) $
-                do { let fam_ty = mkTyConApp tc xis
-                   ; (ev, co, fsk) <- newFlattenSkolemFlatM fam_ty
-                   ; let fsk_ty = mkTyVarTy fsk
-                   ; liftTcS $ extendFlatCache tc xis ( co
-                                                      , fsk_ty, ctEvFlavour ev)
+                do { loc <- getLoc
+                   ; (ev, co, fsk) <- liftTcS $ newFlattenSkolem cur_flav loc tc xis
 
                    -- The new constraint (F xis ~ fsk) is not necessarily inert
                    -- (e.g. the LHS may be a redex) so we must put it in the work list
@@ -1175,12 +1119,13 @@ flatten_exact_fam_app_fully tc tys
                                         , cc_fsk    = fsk }
                    ; emitFlatWork ct
 
-                   ; traceFlat "flatten/flat-cache miss" $ (ppr fam_ty $$ ppr fsk $$ ppr ev)
-                   ; (fsk_xi, fsk_co) <- flatten_one fsk_ty
-                   ; return (fsk_xi, fsk_co
-                                     `mkTransCo`
-                                     maybeSubCo eq_rel (mkSymCo co)
-                                     `mkTransCo` ret_co ) }
+                   ; traceFlat "flatten/flat-cache miss" $
+                         (ppr tc <+> ppr xis $$ ppr fsk $$ ppr ev)
+
+                   -- NB: fsk's kind is already flattend because
+                   --     the xis are flattened
+                   ; return (mkTyVarTy fsk, maybeSubCo eq_rel (mkSymCo co)
+                                            `mkTransCo` ret_co ) }
         }
 
   where
@@ -1322,31 +1267,25 @@ flatten_tyvar1 tv
                          ; return (FTRFollowed ty (mkReflCo role ty)) } ;
            Nothing -> do { traceFlat "Unfilled tyvar" (ppr tv)
                          ; fr <- getFlavourRole
-                         ; flatten_tyvar2  tv fr } }
+                         ; flatten_tyvar2 tv fr } }
 
 flatten_tyvar2 :: TcTyVar -> CtFlavourRole -> FlatM FlattenTvResult
+-- The tyvar is not a filled-in meta-tyvar
 -- Try in the inert equalities
 -- See Definition [Applying a generalised substitution] in TcSMonad
 -- See Note [Stability of flattening] in TcSMonad
 
-flatten_tyvar2 tv fr@(flavour, eq_rel)
-  | Derived <- flavour  -- For derived equalities, consult the inert_model (only)
-  = do { model <- liftTcS $ getInertModel
-       ; case lookupDVarEnv model tv of
-           Just (CTyEqCan { cc_rhs = rhs })
-             -> return (FTRFollowed rhs (pprPanic "flatten_tyvar2" (ppr tv $$ ppr rhs)))
-                              -- Evidence is irrelevant for Derived contexts
-           _ -> return FTRNotFollowed }
-
-  | otherwise   -- For non-derived equalities, consult the inert_eqs (only)
+flatten_tyvar2 tv fr@(_, eq_rel)
   = do { ieqs <- liftTcS $ getInertEqs
+       ; mode <- getMode
        ; case lookupDVarEnv ieqs tv of
            Just (ct:_)   -- If the first doesn't work,
                          -- the subsequent ones won't either
              | CTyEqCan { cc_ev = ctev, cc_tyvar = tv, cc_rhs = rhs_ty } <- ct
-             , ctEvFlavourRole ctev `eqCanRewriteFR` fr
-             ->  do { traceFlat "Following inert tyvar" (ppr tv <+> equals <+> ppr rhs_ty $$ ppr ctev)
-                    ; let rewrite_co1 = mkSymCo $ ctEvCoercion ctev
+             , let ct_fr = ctEvFlavourRole ctev
+             , ct_fr `eqCanRewriteFR` fr  -- This is THE key call of eqCanRewriteFR
+             ->  do { traceFlat "Following inert tyvar" (ppr mode <+> ppr tv <+> equals <+> ppr rhs_ty $$ ppr ctev)
+                    ; let rewrite_co1 = mkSymCo (ctEvCoercion ctev)
                           rewrite_co  = case (ctEvEqRel ctev, eq_rel) of
                             (ReprEq, _rel)  -> ASSERT( _rel == ReprEq )
                                     -- if this ASSERT fails, then
@@ -1366,7 +1305,7 @@ flatten_tyvar2 tv fr@(flavour, eq_rel)
 Note [An alternative story for the inert substitution]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 (This entire note is just background, left here in case we ever want
- to return the the previousl state of affairs)
+ to return the the previous state of affairs)
 
 We used (GHC 7.8) to have this story for the inert substitution inert_eqs
 
@@ -1484,7 +1423,7 @@ unflatten tv_eqs funeqs
     ----------------
     unflatten_funeq :: Ct -> Cts -> TcS Cts
     unflatten_funeq ct@(CFunEqCan { cc_fun = tc, cc_tyargs = xis
-                                         , cc_fsk = fmv, cc_ev = ev }) rest
+                                  , cc_fsk = fmv, cc_ev = ev }) rest
       = do {   -- fmv should be an un-filled flatten meta-tv;
                -- we now fix its final value by filling it, being careful
                -- to observe the occurs check.  Zonking will eliminate it
@@ -1492,8 +1431,7 @@ unflatten tv_eqs funeqs
              rhs' <- zonkTcType (mkTyConApp tc xis)
            ; case occCheckExpand fmv rhs' of
                Just rhs''    -- Normal case: fill the tyvar
-                 -> do { setEvBindIfWanted ev
-                               (EvCoercion (mkTcReflCo (ctEvRole ev) rhs''))
+                 -> do { setReflEvidence ev NomEq rhs''
                        ; unflattenFmv fmv rhs''
                        ; return rest }
 
@@ -1512,17 +1450,22 @@ unflatten tv_eqs funeqs
 
     ----------------
     unflatten_eq :: TcLevel -> Ct -> Cts -> TcS Cts
-    unflatten_eq tclvl ct@(CTyEqCan { cc_ev = ev, cc_tyvar = tv, cc_rhs = rhs }) rest
+    unflatten_eq tclvl ct@(CTyEqCan { cc_ev = ev, cc_tyvar = tv
+                                    , cc_rhs = rhs, cc_eq_rel = eq_rel }) rest
       | isFmvTyVar tv   -- Previously these fmvs were untouchable,
                         -- but now they are touchable
-                        -- NB: unlike unflattenFmv, filling a fmv here does
+                        -- NB: unlike unflattenFmv, filling a fmv here /does/
                         --     bump the unification count; it is "improvement"
                         -- Note [Unflattening can force the solver to iterate]
-      = do { lhs_elim <- tryFill tv rhs ev
-           ; if lhs_elim then return rest else
-        do { rhs_elim <- try_fill tclvl ev rhs (mkTyVarTy tv)
-           ; if rhs_elim then return rest else
-             return (ct `consCts` rest) } }
+      , tyVarKind tv `eqType` typeKind rhs
+      = do { is_filled <- isFilledMetaTyVar tv
+           ; elim <- case is_filled of
+               False -> do { traceTcS "unflatten_eq 2" (ppr ct)
+                           ; tryFill      ev eq_rel       tv rhs }
+               True  -> do { traceTcS "unflatten_eq 2" (ppr ct)
+                           ; try_fill_rhs ev eq_rel tclvl tv rhs }
+           ; if elim then return rest
+                     else return (ct `consCts` rest) }
 
       | otherwise
       = return (ct `consCts` rest)
@@ -1530,51 +1473,67 @@ unflatten tv_eqs funeqs
     unflatten_eq _ ct _ = pprPanic "unflatten_irred" (ppr ct)
 
     ----------------
+    try_fill_rhs ev eq_rel tclvl lhs_tv rhs
+         -- Constraint is lhs_tv ~ rhs_tv,
+         -- and lhs_tv is filled, so try RHS
+      | Just (rhs_tv, co) <- getCastedTyVar_maybe rhs
+                             -- co :: kind(rhs_tv) ~ kind(lhs_tv)
+      , isFmvTyVar rhs_tv || (isTouchableMetaTyVar tclvl rhs_tv
+                              && not (isSigTyVar rhs_tv))
+                              -- LHS is a filled fmv, and so is a type
+                              -- family application, which a SigTv should
+                              -- not unify with
+      = do { is_filled <- isFilledMetaTyVar rhs_tv
+           ; if is_filled then return False
+             else tryFill ev eq_rel rhs_tv
+                          (mkTyVarTy lhs_tv `mkCastTy` mkSymCo co) }
+
+      | otherwise
+      = return False
+
+    ----------------
     finalise_eq :: Ct -> Cts -> TcS Cts
     finalise_eq (CTyEqCan { cc_ev = ev, cc_tyvar = tv
                           , cc_rhs = rhs, cc_eq_rel = eq_rel }) rest
       | isFmvTyVar tv
       = do { ty1 <- zonkTcTyVar tv
-           ; ty2 <- zonkTcType rhs
-           ; let is_refl = ty1 `tcEqType` ty2
-           ; if is_refl then do { setEvBindIfWanted ev
-                                            (EvCoercion $
-                                             mkTcReflCo (eqRelRole eq_rel) rhs)
-                                ; return rest }
-                        else return (mkNonCanonical ev `consCts` rest) }
+           ; rhs' <- zonkTcType rhs
+           ; if ty1 `tcEqType` rhs'
+             then do { setReflEvidence ev eq_rel rhs'
+                     ; return rest }
+             else return (mkNonCanonical ev `consCts` rest) }
+
       | otherwise
       = return (mkNonCanonical ev `consCts` rest)
 
     finalise_eq ct _ = pprPanic "finalise_irred" (ppr ct)
 
-    ----------------
-    try_fill tclvl ev ty1 ty2
-      | Just tv1 <- tcGetTyVar_maybe ty1
-      , isTouchableOrFmv tclvl tv1
-      , typeKind ty1 `eqType` tyVarKind tv1
-      = tryFill tv1 ty2 ev
-      | otherwise
-      = return False
-
-tryFill :: TcTyVar -> TcType -> CtEvidence -> TcS Bool
--- (tryFill tv rhs ev) sees if 'tv' is an un-filled MetaTv
--- If so, and if tv does not appear in 'rhs', set tv := rhs
--- bind the evidence (which should be a CtWanted) to Refl<rhs>
--- and return True.  Otherwise return False
-tryFill tv rhs ev
+tryFill :: CtEvidence -> EqRel -> TcTyVar -> TcType -> TcS Bool
+-- (tryFill tv rhs ev) assumes 'tv' is an /un-filled/ MetaTv
+-- If tv does not appear in 'rhs', it set tv := rhs,
+-- binds the evidence (which should be a CtWanted) to Refl<rhs>
+-- and return True.  Otherwise returns False
+tryFill ev eq_rel tv rhs
   = ASSERT2( not (isGiven ev), ppr ev )
-    do { is_filled <- isFilledMetaTyVar tv
-       ; if is_filled then return False else
     do { rhs' <- zonkTcType rhs
-       ; case occCheckExpand tv rhs' of
+       ; case tcGetTyVar_maybe rhs' of {
+            Just tv' | tv == tv' -> do { setReflEvidence ev eq_rel rhs
+                                       ; return True } ;
+            _other ->
+    do { case occCheckExpand tv rhs' of
            Just rhs''    -- Normal case: fill the tyvar
-             -> do { setEvBindIfWanted ev
-                               (EvCoercion (mkTcReflCo (ctEvRole ev) rhs''))
+             -> do { setReflEvidence ev eq_rel rhs''
                    ; unifyTyVar tv rhs''
                    ; return True }
 
            Nothing ->  -- Occurs check
-                      return False } }
+                      return False } } }
+
+setReflEvidence :: CtEvidence -> EqRel -> TcType -> TcS ()
+setReflEvidence ev eq_rel rhs
+  = setEvBindIfWanted ev (EvCoercion refl_co)
+  where
+    refl_co = mkTcReflCo (eqRelRole eq_rel) rhs
 
 {-
 Note [Unflatten using funeqs first]
index 005be19..cb0b44f 100644 (file)
@@ -9,7 +9,8 @@ module TcInteract (
 
 #include "HsVersions.h"
 
-import BasicTypes ( infinity, IntWithInf, intGtLimit )
+import BasicTypes ( SwapFlag(..), isSwapped,
+                    infinity, IntWithInf, intGtLimit )
 import HsTypes ( HsIPName(..) )
 import TcCanonical
 import TcFlatten
@@ -133,16 +134,14 @@ that prepareInertsForImplications will discard the insolubles, so we
 must keep track of them separately.
 -}
 
-solveSimpleGivens :: [Ct] -> TcS Cts
+solveSimpleGivens :: [Ct] -> TcS ()
 solveSimpleGivens givens
   | null givens  -- Shortcut for common case
-  = return emptyCts
+  = return ()
   | otherwise
   = do { traceTcS "solveSimpleGivens {" (ppr givens)
        ; go givens
-       ; given_insols <- takeGivenInsolubles
-       ; traceTcS "End solveSimpleGivens }" (text "Insoluble:" <+> pprCts given_insols)
-       ; return given_insols }
+       ; traceTcS "End solveSimpleGivens }" empty }
   where
     go givens = do { solveSimples (listToBag givens)
                    ; new_givens <- runTcPluginsGiven
@@ -183,7 +182,8 @@ solveSimpleWanteds simples
 
           ; if unif_count == 0 && not rerun_plugin
             then return (n, wc2)             -- Done
-            else do { traceTcS "solveSimple going round again:" (ppr rerun_plugin)
+            else do { traceTcS "solveSimple going round again:" $
+                      ppr unif_count $$ ppr rerun_plugin
                     ; go (n+1) limit wc2 } }      -- Loop
 
 
@@ -355,11 +355,8 @@ runTcPlugins plugins all_cts
     without = deleteFirstsBy eqCt
 
     eqCt :: Ct -> Ct -> Bool
-    eqCt c c' = case (ctEvidence c, ctEvidence c') of
-      (CtGiven   pred _ _, CtGiven   pred' _ _) -> pred `eqType` pred'
-      (CtWanted  pred _ _, CtWanted  pred' _ _) -> pred `eqType` pred'
-      (CtDerived pred _  , CtDerived pred' _  ) -> pred `eqType` pred'
-      (_                 , _                  ) -> False
+    eqCt c c' = ctFlavour c == ctFlavour c'
+             && ctPred c `tcEqType` ctPred c'
 
     add :: [(EvTerm,Ct)] -> SolvedCts -> SolvedCts
     add xs scs = foldl' addOne scs xs
@@ -386,19 +383,19 @@ runSolverPipeline pipeline workItem
 
        ; bumpStepCountTcS    -- One step for each constraint processed
        ; final_res  <- run_pipeline pipeline (ContinueWith workItem)
-
-       ; final_is <- getTcSInerts
        ; case final_res of
            Stop ev s       -> do { traceFireTcS ev s
+                                 ; final_is <- getTcSInerts
                                  ; traceTcS "End solver pipeline (discharged) }"
                                        (text "inerts =" <+> ppr final_is)
                                  ; return () }
            ContinueWith ct -> do { traceFireTcS (ctEvidence ct) (text "Kept as inert")
+                                 ; addInertCan ct
+                                 ; final_is <- getTcSInerts
                                  ; traceTcS "End solver pipeline (kept as inert) }" $
                                        vcat [ text "final_item =" <+> ppr ct
                                             , pprTyVars $ tyCoVarsOfCtList ct
-                                            , text "inerts     =" <+> ppr final_is]
-                                 ; addInertCan ct }
+                                            , text "inerts     =" <+> ppr final_is] }
        }
   where run_pipeline :: [(String,SimplifierStage)] -> StopOrContinue Ct
                      -> TcS (StopOrContinue Ct)
@@ -740,6 +737,7 @@ addFunDepWork inerts work_ev cls
   where
     work_pred = ctEvPred work_ev
     work_loc  = ctEvLoc work_ev
+
     add_fds inert_ct
       = emitFunDepDeriveds $
         improveFromAnother derived_loc inert_pred work_pred
@@ -819,7 +817,6 @@ So the inner binding for ?x::Bool *overrides* the outer one.
 
 All this works for the normal cases but it has an odd side effect in
 some pathological programs like this:
-
 -- This is accepted, the second parameter shadows
 f1 :: (?x :: Int, ?x :: Char) => Char
 f1 = ?x
@@ -852,57 +849,77 @@ I can think of two ways to fix this:
 
 interactFunEq :: InertCans -> Ct -> TcS (StopOrContinue Ct)
 -- Try interacting the work item with the inert set
-interactFunEq inerts workItem@(CFunEqCan { cc_ev = ev, cc_fun = tc
-                                         , cc_tyargs = args, cc_fsk = fsk })
-  | Just (CFunEqCan { cc_ev = ev_i
-                    , cc_fsk = fsk_i }) <- matching_inerts
-  = if ev_i `funEqCanDischarge` ev
-    then  -- Rewrite work-item using inert
-      do { traceTcS "reactFunEq (discharge work item):" $
-           vcat [ text "workItem =" <+> ppr workItem
-                , text "inertItem=" <+> ppr ev_i ]
-         ; reactFunEq ev_i fsk_i ev fsk
-         ; stopWith ev "Inert rewrites work item" }
-    else  -- Rewrite inert using work-item
-      ASSERT2( ev `funEqCanDischarge` ev_i, ppr ev $$ ppr ev_i )
-      do { traceTcS "reactFunEq (rewrite inert item):" $
-           vcat [ text "workItem =" <+> ppr workItem
-                , text "inertItem=" <+> ppr ev_i ]
-         ; updInertFunEqs $ \ feqs -> insertFunEq feqs tc args workItem
-               -- Do the updInertFunEqs before the reactFunEq, so that
-               -- we don't kick out the inertItem as well as consuming it!
-         ; reactFunEq ev fsk ev_i fsk_i
-         ; stopWith ev "Work item rewrites inert" }
+interactFunEq inerts work_item@(CFunEqCan { cc_ev = ev, cc_fun = tc
+                                          , cc_tyargs = args, cc_fsk = fsk })
+  | Just inert_ct@(CFunEqCan { cc_ev = ev_i
+                             , cc_fsk = fsk_i })
+         <- findFunEq (inert_funeqs inerts) tc args
+  , pr@(swap_flag, upgrade_flag) <- ev_i `funEqCanDischarge` ev
+  = do { traceTcS "reactFunEq (rewrite inert item):" $
+         vcat [ text "work_item =" <+> ppr work_item
+              , text "inertItem=" <+> ppr ev_i
+              , text "(swap_flag, upgrade)" <+> ppr pr ]
+       ; if isSwapped swap_flag
+         then do {   -- Rewrite inert using work-item
+                   let work_item' | upgrade_flag = upgradeWanted work_item
+                                  | otherwise    = work_item
+                 ; updInertFunEqs $ \ feqs -> insertFunEq feqs tc args work_item'
+                      -- Do the updInertFunEqs before the reactFunEq, so that
+                      -- we don't kick out the inertItem as well as consuming it!
+                 ; reactFunEq ev fsk ev_i fsk_i
+                 ; stopWith ev "Work item rewrites inert" }
+         else do {   -- Rewrite work-item using inert
+                 ; when upgrade_flag $
+                   updInertFunEqs $ \ feqs -> insertFunEq feqs tc args
+                                                 (upgradeWanted inert_ct)
+                 ; reactFunEq ev_i fsk_i ev fsk
+                 ; stopWith ev "Inert rewrites work item" } }
 
   | otherwise   -- Try improvement
-  = do { improveLocalFunEqs loc inerts tc args fsk
-       ; continueWith workItem }
-  where
-    loc             = ctEvLoc ev
-    funeqs          = inert_funeqs inerts
-    matching_inerts = findFunEq funeqs tc args
+  = do { improveLocalFunEqs ev inerts tc args fsk
+       ; continueWith work_item }
 
-interactFunEq _ workItem = pprPanic "interactFunEq" (ppr workItem)
+interactFunEq _ work_item = pprPanic "interactFunEq" (ppr work_item)
 
-improveLocalFunEqs :: CtLoc -> InertCans -> TyCon -> [TcType] -> TcTyVar
+upgradeWanted :: Ct -> Ct
+-- We are combining a [W] F tys ~ fmv1 and [D] F tys ~ fmv2
+-- so upgrade the [W] to [WD] before putting it in the inert set
+upgradeWanted ct = ct { cc_ev = upgrade_ev (cc_ev ct) }
+  where
+    upgrade_ev ev = ASSERT2( isWanted ev, ppr ct )
+                    ev { ctev_nosh = WDeriv }
+
+improveLocalFunEqs :: CtEvidence -> InertCans -> TyCon -> [TcType] -> TcTyVar
                    -> TcS ()
 -- Generate derived improvement equalities, by comparing
 -- the current work item with inert CFunEqs
 -- E.g.   x + y ~ z,   x + y' ~ z   =>   [D] y ~ y'
-improveLocalFunEqs loc inerts fam_tc args fsk
-  | not (null improvement_eqns)
-  = do { traceTcS "interactFunEq improvements: " $
+--
+-- See Note [FunDep and implicit parameter reactions]
+improveLocalFunEqs ev inerts fam_tc args fsk
+  | isGiven ev   -- See Note [No FunEq improvement for Givens]
+  = return ()
+
+  | null improvement_eqns
+  = do { traceTcS "improveLocalFunEqs no improvements: " $
+         vcat [ text "Candidates:" <+> ppr funeqs_for_tc
+              , text "Inert eqs:" <+> ppr ieqs ]
+       ; return () }
+
+  | otherwise
+  = do { traceTcS "improveLocalFunEqs improvements: " $
          vcat [ text "Eqns:" <+> ppr improvement_eqns
               , text "Candidates:" <+> ppr funeqs_for_tc
-              , text "Model:" <+> ppr model ]
+              , text "Inert eqs:" <+> ppr ieqs ]
        ; mapM_ (unifyDerived loc Nominal) improvement_eqns }
-  | otherwise
-  = return ()
+
   where
-    model         = inert_model inerts
+    loc           = ctEvLoc ev
+    ieqs          = inert_eqs inerts
     funeqs        = inert_funeqs inerts
     funeqs_for_tc = findFunEqsByTyCon funeqs fam_tc
-    rhs           = lookupFlattenTyVar model fsk
+    rhs           = lookupFlattenTyVar ieqs fsk
+    fam_inj_info  = familyTyConInjectivityInfo fam_tc
 
     --------------------
     improvement_eqns
@@ -910,37 +927,30 @@ improveLocalFunEqs loc inerts fam_tc args fsk
       =    -- Try built-in families, notably for arithmethic
          concatMap (do_one_built_in ops) funeqs_for_tc
 
-      | Injective injective_args <- familyTyConInjectivityInfo fam_tc
+      | Injective injective_args <- fam_inj_info
       =    -- Try improvement from type families with injectivity annotations
-         concatMap (do_one_injective injective_args) funeqs_for_tc
+        concatMap (do_one_injective injective_args) funeqs_for_tc
 
       | otherwise
       = []
 
     --------------------
     do_one_built_in ops (CFunEqCan { cc_tyargs = iargs, cc_fsk = ifsk })
-      = sfInteractInert ops args rhs iargs (lookupFlattenTyVar model ifsk)
+      = sfInteractInert ops args rhs iargs (lookupFlattenTyVar ieqs ifsk)
     do_one_built_in _ _ = pprPanic "interactFunEq 1" (ppr fam_tc)
 
     --------------------
     -- See Note [Type inference for type families with injectivity]
-    do_one_injective injective_args
-                    (CFunEqCan { cc_tyargs = iargs, cc_fsk = ifsk })
-      | rhs `tcEqType` lookupFlattenTyVar model ifsk
-      = [Pair arg iarg | (arg, iarg, True)
-                           <- zip3 args iargs injective_args ]
-      | otherwise
-      = []
+    do_one_injective inj_args (CFunEqCan { cc_tyargs = iargs, cc_fsk = ifsk })
+      | rhs `tcEqType` lookupFlattenTyVar ieqs ifsk
+      = [ Pair arg iarg
+        | (arg, iarg, True) <- zip3 args iargs inj_args ]
+
+      | otherwise = []
+
     do_one_injective _ _ = pprPanic "interactFunEq 2" (ppr fam_tc)
 
 -------------
-lookupFlattenTyVar :: InertModel -> TcTyVar -> TcType
--- See Note [lookupFlattenTyVar]
-lookupFlattenTyVar model ftv
-  = case lookupDVarEnv model ftv of
-      Just (CTyEqCan { cc_rhs = rhs, cc_eq_rel = NomEq }) -> rhs
-      _                                                   -> mkTyVarTy ftv
-
 reactFunEq :: CtEvidence -> TcTyVar    -- From this  :: F args1 ~ fsk1
            -> CtEvidence -> TcTyVar    -- Solve this :: F args2 ~ fsk2
            -> TcS ()
@@ -955,26 +965,20 @@ reactFunEq from_this fsk1 solve_this fsk2
        ; new_ev <- newGivenEvVar loc (fsk_eq_pred, EvCoercion fsk_eq_co)
        ; emitWorkNC [new_ev] }
 
-  | otherwise
+  | CtDerived { ctev_loc = loc } <- solve_this
+  = do { traceTcS "reactFunEq (Derived)" (ppr from_this $$ ppr fsk1 $$
+                                          ppr solve_this $$ ppr fsk2)
+       ; emitNewDerivedEq loc Nominal (mkTyVarTy fsk1) (mkTyVarTy fsk2) }
+              -- FunEqs are always at Nominal role
+
+  | otherwise  -- Wanted
   = do { traceTcS "reactFunEq" (ppr from_this $$ ppr fsk1 $$
                                 ppr solve_this $$ ppr fsk2)
        ; dischargeFmv solve_this fsk2 (ctEvCoercion from_this) (mkTyVarTy fsk1)
        ; traceTcS "reactFunEq done" (ppr from_this $$ ppr fsk1 $$
                                      ppr solve_this $$ ppr fsk2) }
 
-{- Note [lookupFlattenTyVar]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Supppose we have an injective function F and
-  inert_funeqs:   F t1 ~ fsk1
-                  F t2 ~ fsk2
-  model           fsk1 ~ fsk2
-
-We never rewrite the RHS (cc_fsk) of a CFunEqCan.  But we /do/ want to
-get the [D] t1 ~ t2 from the injectiveness of F.  So we look up the
-cc_fsk of CFunEqCans in the model when trying to find derived
-equalities arising from injectivity.
-
-Note [Type inference for type families with injectivity]
+{- Note [Type inference for type families with injectivity]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Suppose we have a type family with an injectivity annotation:
     type family F a b = r | r -> b
@@ -1101,24 +1105,19 @@ test when solving pairwise CFunEqCan.
 **********************************************************************
 -}
 
-interactTyVarEq :: InertCans -> Ct -> TcS (StopOrContinue Ct)
--- CTyEqCans are always consumed, so always returns Stop
-interactTyVarEq inerts workItem@(CTyEqCan { cc_tyvar = tv
-                                          , cc_rhs = rhs
-                                          , cc_ev = ev
-                                          , cc_eq_rel = eq_rel })
+inertsCanDischarge :: InertCans -> TcTyVar -> TcType -> CtEvidence
+                   -> Maybe ( CtEvidence  -- The evidence for the inert
+                            , SwapFlag    -- Whether we need mkSymCo
+                            , Bool)       -- True <=> keep a [D] version
+                                          --          of the [WD] constraint
+inertsCanDischarge inerts tv rhs ev
   | (ev_i : _) <- [ ev_i | CTyEqCan { cc_ev = ev_i, cc_rhs = rhs_i }
                              <- findTyEqs inerts tv
                          , ev_i `eqCanDischarge` ev
                          , rhs_i `tcEqType` rhs ]
   =  -- Inert:     a ~ ty
      -- Work item: a ~ ty
-    do { setEvBindIfWanted ev $
-          EvCoercion (tcDowngradeRole (eqRelRole eq_rel)
-                                      (ctEvRole ev_i)
-                                      (ctEvCoercion ev_i))
-
-       ; stopWith ev "Solved from inert" }
+    Just (ev_i, NotSwapped, keep_deriv ev_i)
 
   | Just tv_rhs <- getTyVar_maybe rhs
   , (ev_i : _) <- [ ev_i | CTyEqCan { cc_ev = ev_i, cc_rhs = rhs_i }
@@ -1127,13 +1126,41 @@ interactTyVarEq inerts workItem@(CTyEqCan { cc_tyvar = tv
                          , rhs_i `tcEqType` mkTyVarTy tv ]
   =  -- Inert:     a ~ b
      -- Work item: b ~ a
-    do { setEvBindIfWanted ev $
-           EvCoercion (mkTcSymCo $
-                       tcDowngradeRole (eqRelRole eq_rel)
-                                       (ctEvRole ev_i)
-                                       (ctEvCoercion ev_i))
+     Just (ev_i, IsSwapped, keep_deriv ev_i)
+
+  | otherwise
+  = Nothing
+
+  where
+    keep_deriv ev_i
+      | Wanted WOnly  <- ctEvFlavour ev_i  -- inert is [W]
+      , Wanted WDeriv <- ctEvFlavour ev    -- work item is [WD]
+      = True   -- Keep a derived verison of the work item
+      | otherwise
+      = False  -- Work item is fully discharged
+
+interactTyVarEq :: InertCans -> Ct -> TcS (StopOrContinue Ct)
+-- CTyEqCans are always consumed, so always returns Stop
+interactTyVarEq inerts workItem@(CTyEqCan { cc_tyvar = tv
+                                          , cc_rhs = rhs
+                                          , cc_ev = ev
+                                          , cc_eq_rel = eq_rel })
+  | Just (ev_i, swapped, keep_deriv)
+       <- inertsCanDischarge inerts tv rhs ev
+  = do { setEvBindIfWanted ev $
+         EvCoercion (maybeSym swapped $
+                     tcDowngradeRole (eqRelRole eq_rel)
+                                     (ctEvRole ev_i)
+                                     (ctEvCoercion ev_i))
+
+       ; let deriv_ev = CtDerived { ctev_pred = ctEvPred ev
+                                  , ctev_loc  = ctEvLoc  ev }
+       ; when keep_deriv $
+         emitWork [workItem { cc_ev = deriv_ev }]
+         -- As a Derived it might not be fully rewritten,
+         -- so we emit it as new work
 
-       ; stopWith ev "Solved from inert (r)" }
+       ; stopWith ev "Solved from inert" }
 
   | ReprEq <- eq_rel   -- We never solve representational
   = unsolved_inert     -- equalities by unification
@@ -1159,7 +1186,7 @@ interactTyVarEq inerts workItem@(CTyEqCan { cc_tyvar = tv
                                 <+> text "is" <+> ppr (metaTyVarTcLevel tv))
                       , text "RHS:" <+> ppr rhs <+> dcolon <+> ppr (typeKind rhs) ])
            ; addInertEq workItem
-           ; return (Stop ev (text "Kept as inert")) }
+           ; stopWith ev "Kept as inert" }
 
 interactTyVarEq _ wi = pprPanic "interactTyVarEq" (ppr wi)
 
@@ -1233,9 +1260,78 @@ constraint right away.  This avoids two dangers
 
 To achieve this required some refactoring of FunDeps.hs (nicer
 now!).
+
+Note [FunDep and implicit parameter reactions]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Currently, our story of interacting two dictionaries (or a dictionary
+and top-level instances) for functional dependencies, and implicit
+parameters, is that we simply produce new Derived equalities.  So for example
+
+        class D a b | a -> b where ...
+    Inert:
+        d1 :g D Int Bool
+    WorkItem:
+        d2 :w D Int alpha
+
+    We generate the extra work item
+        cv :d alpha ~ Bool
+    where 'cv' is currently unused.  However, this new item can perhaps be
+    spontaneously solved to become given and react with d2,
+    discharging it in favour of a new constraint d2' thus:
+        d2' :w D Int Bool
+        d2 := d2' |> D Int cv
+    Now d2' can be discharged from d1
+
+We could be more aggressive and try to *immediately* solve the dictionary
+using those extra equalities, but that requires those equalities to carry
+evidence and derived do not carry evidence.
+
+If that were the case with the same inert set and work item we might dischard
+d2 directly:
+
+        cv :w alpha ~ Bool
+        d2 := d1 |> D Int cv
+
+But in general it's a bit painful to figure out the necessary coercion,
+so we just take the first approach. Here is a better example. Consider:
+    class C a b c | a -> b
+And:
+     [Given]  d1 : C T Int Char
+     [Wanted] d2 : C T beta Int
+In this case, it's *not even possible* to solve the wanted immediately.
+So we should simply output the functional dependency and add this guy
+[but NOT its superclasses] back in the worklist. Even worse:
+     [Given] d1 : C T Int beta
+     [Wanted] d2: C T beta Int
+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 [Weird fundeps]
+~~~~~~~~~~~~~~~~~~~~
+Consider   class Het a b | a -> b where
+              het :: m (f c) -> a -> m b
+
+           class GHet (a :: * -> *) (b :: * -> *) | a -> b
+           instance            GHet (K a) (K [a])
+           instance Het a b => GHet (K a) (K b)
+
+The two instances don't actually conflict on their fundeps,
+although it's pretty strange.  So they are both accepted. Now
+try   [W] GHet (K Int) (K Bool)
+This triggers fundeps from both instance decls;
+      [D] K Bool ~ K [a]
+      [D] K Bool ~ K beta
+And there's a risk of complaining about Bool ~ [a].  But in fact
+the Wanted matches the second instance, so we never get as far
+as the fundeps.
+
+Trac #7875 is a case in point.
 -}
 
 emitFunDepDeriveds :: [FunDepEqn CtLoc] -> TcS ()
+-- See Note [FunDep and implicit parameter reactions]
 emitFunDepDeriveds fd_eqns
   = mapM_ do_one_FDEqn fd_eqns
   where
@@ -1282,121 +1378,45 @@ doTopReact work_item
            _  -> -- Any other work item does not react with any top-level equations
                  continueWith work_item  }
 
---------------------
-doTopReactDict :: InertSet -> Ct -> TcS (StopOrContinue Ct)
--- Try to use type-class instance declarations to simplify the constraint
-doTopReactDict inerts work_item@(CDictCan { cc_ev = fl, cc_class = cls
-                                          , cc_tyargs = xis })
-  | isGiven fl   -- Never use instances for Given constraints
-  = do { try_fundep_improvement
-       ; continueWith work_item }
-
-  | Just ev <- lookupSolvedDict inerts cls xis   -- Cached
-  = do { setEvBindIfWanted fl (ctEvTerm ev)
-       ; stopWith fl "Dict/Top (cached)" }
-
-  | isDerived fl  -- Use type-class instances for Deriveds, in the hope
-                  -- of generating some improvements
-                  -- C.f. Example 3 of Note [The improvement story]
-                  -- It's easy because no evidence is involved
-   = do { dflags <- getDynFlags
-        ; lkup_inst_res <- matchClassInst dflags inerts cls xis dict_loc
-        ; case lkup_inst_res of
-               GenInst { lir_new_theta = preds
-                       , lir_safe_over = s } ->
-                 do { emitNewDeriveds dict_loc preds
-                    ; unless s $ insertSafeOverlapFailureTcS work_item
-                    ; stopWith fl "Dict/Top (solved)" }
-
-               NoInstance ->
-                 do { -- If there is no instance, try improvement
-                      try_fundep_improvement
-                    ; continueWith work_item } }
-
-  | otherwise  -- Wanted, but not cached
-   = do { dflags <- getDynFlags
-        ; lkup_inst_res <- matchClassInst dflags inerts cls xis dict_loc
-        ; case lkup_inst_res of
-               GenInst { lir_new_theta = theta
-                       , lir_mk_ev     = mk_ev
-                       , lir_safe_over = s } ->
-                 do { addSolvedDict fl cls xis
-                    ; unless s $ insertSafeOverlapFailureTcS work_item
-                    ; solve_from_instance theta mk_ev }
-               NoInstance ->
-                 do { try_fundep_improvement
-                    ; continueWith work_item } }
-   where
-     dict_pred   = mkClassPred cls xis
-     dict_loc    = ctEvLoc fl
-     dict_origin = ctLocOrigin dict_loc
-     deeper_loc  = zap_origin (bumpCtLocDepth dict_loc)
-
-     zap_origin loc  -- After applying an instance we can set ScOrigin to
-                     -- infinity, so that prohibitedSuperClassSolve never fires
-       | ScOrigin {} <- dict_origin
-       = setCtLocOrigin loc (ScOrigin infinity)
-       | otherwise
-       = loc
-
-     solve_from_instance :: [TcPredType]
-                         -> ([EvTerm] -> EvTerm) -> TcS (StopOrContinue Ct)
-      -- Precondition: evidence term matches the predicate workItem
-     solve_from_instance theta mk_ev
-        | null theta
-        = do { traceTcS "doTopReact/found nullary instance for" $ ppr fl
-             ; setWantedEvBind (ctEvId fl) (mk_ev [])
-             ; stopWith fl "Dict/Top (solved, no new work)" }
-        | otherwise
-        = do { checkReductionDepth deeper_loc dict_pred
-             ; traceTcS "doTopReact/found non-nullary instance for" $ ppr fl
-             ; evc_vars <- mapM (newWanted deeper_loc) theta
-             ; setWantedEvBind (ctEvId fl) (mk_ev (map getEvTerm evc_vars))
-             ; emitWorkNC (freshGoals evc_vars)
-             ; stopWith fl "Dict/Top (solved, more work)" }
-
-     -- 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)
 
 --------------------
 doTopReactFunEq :: Ct -> TcS (StopOrContinue Ct)
 doTopReactFunEq work_item@(CFunEqCan { cc_ev = old_ev, cc_fun = fam_tc
                                      , cc_tyargs = args, cc_fsk = fsk })
+
+  | fsk `elemVarSet` tyCoVarsOfTypes args
+  = no_reduction    -- See Note [FunEq occurs-check principle]
+
+  | otherwise  -- Note [Reduction for Derived CFunEqCans]
   = do { match_res <- matchFam fam_tc args
                            -- Look up in top-level instances, or built-in axiom
                            -- See Note [MATCHING-SYNONYMS]
        ; case match_res of
-           Nothing -> do { improveTopFunEqs (ctEvLoc old_ev) fam_tc args fsk
-                         ; continueWith work_item }
-           Just (ax_co, rhs_ty)
-             -> reduce_top_fun_eq old_ev fsk ax_co rhs_ty }
+           Nothing         -> no_reduction
+           Just match_info -> reduce_top_fun_eq old_ev fsk match_info }
+  where
+    no_reduction
+      = do { improveTopFunEqs old_ev fam_tc args fsk
+           ; continueWith work_item }
 
 doTopReactFunEq w = pprPanic "doTopReactFunEq" (ppr w)
 
-reduce_top_fun_eq :: CtEvidence -> TcTyVar -> TcCoercion -> TcType
+reduce_top_fun_eq :: CtEvidence -> TcTyVar -> (TcCoercion, TcType)
                   -> TcS (StopOrContinue Ct)
--- Found an applicable top-level axiom: use it to reduce
-reduce_top_fun_eq old_ev fsk ax_co rhs_ty
+-- 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
   , isTypeFamilyTyCon tc
   , tc_args `lengthIs` tyConArity tc    -- Short-cut
-  = shortCutReduction old_ev fsk ax_co tc tc_args
-       -- Try shortcut; see Note [Short cut for top-level reaction]
+  = -- 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
@@ -1406,50 +1426,36 @@ 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` tyCoVarsOfType rhs_ty)
-  = do { dischargeFmv old_ev fsk ax_co rhs_ty
+  | otherwise   -- So old_ev is Wanted (cannot be Derived)
+  = 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
        ; traceTcS "doTopReactFunEq" $
          vcat [ text "old_ev:" <+> ppr old_ev
               , nest 2 (text ":=") <+> ppr ax_co ]
        ; stopWith old_ev "Fun/Top (wanted)" }
 
-  | otherwise -- We must not assign ufsk := ...ufsk...!
-  = do { alpha_ty <- newFlexiTcSTy (tyVarKind fsk)
-       ; new_co <- case old_ev of
-           CtWanted {}  -> emitNewWantedEq loc Nominal alpha_ty rhs_ty
-           CtDerived {} -> do { ev <- newDerivedNC loc pred
-                              ; updWorkListTcS (extendWorkListDerived loc ev)
-                              ; return (ctEvCoercion ev) }  -- Coercion is bottom
-                        where pred = mkPrimEqPred alpha_ty rhs_ty
-           _ -> 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 new_co
-            --    ax_co :: fam_tc args ~ rhs_ty
-            --       ev :: alpha ~ rhs_ty
-            --     ufsk := alpha
-            -- final_co :: fam_tc args ~ alpha
-       ; dischargeFmv old_ev fsk final_co alpha_ty
-       ; traceTcS "doTopReactFunEq (occurs)" $
-         vcat [ text "old_ev:" <+> ppr old_ev
-              , nest 2 (text ":=") <+>
-                   if isDerived old_ev then text "(derived)"
-                   else ppr final_co
-              , text "new_co:" <+> ppr new_co ]
-       ; stopWith old_ev "Fun/Top (wanted)" }
   where
     loc = ctEvLoc old_ev
     deeper_loc = bumpCtLocDepth loc
 
-improveTopFunEqs :: CtLoc -> TyCon -> [TcType] -> TcTyVar -> TcS ()
-improveTopFunEqs loc fam_tc args fsk
-  = do { model <- getInertModel
+improveTopFunEqs :: CtEvidence -> TyCon -> [TcType] -> TcTyVar -> TcS ()
+-- See Note [FunDep and implicit parameter reactions]
+improveTopFunEqs ev fam_tc args fsk
+  | isGiven ev    -- See Note [No FunEq improvement for Givens]
+  = return ()
+
+  | otherwise
+  = do { ieqs <- getInertEqs
        ; fam_envs <- getFamInstEnvs
        ; eqns <- improve_top_fun_eqs fam_envs fam_tc args
-                                    (lookupFlattenTyVar model fsk)
+                                    (lookupFlattenTyVar ieqs fsk)
+       ; traceTcS "improveTopFunEqs" (vcat [ ppr fam_tc <+> ppr args <+> ppr fsk
+                                          , ppr eqns ])
        ; mapM_ (unifyDerived loc Nominal) eqns }
+  where
+    loc = ctEvLoc ev
 
 improve_top_fun_eqs :: FamInstEnvs
                     -> TyCon -> [TcType] -> TcType
@@ -1475,7 +1481,8 @@ improve_top_fun_eqs fam_envs fam_tc args rhs_ty
 
   | otherwise
   = return []
-     where
+
+  where
       buildImprovementData
           :: [a]                     -- axioms for a TF (FamInst or CoAxBranch)
           -> (a -> [Type])           -- get LHS of an axiom
@@ -1535,11 +1542,7 @@ shortCutReduction old_ev fsk ax_co fam_tc tc_args
                                         `mkTcTransCo` mkTcSymCo ax_co
                                         `mkTcTransCo` ctEvCoercion old_ev) )
 
-           Derived -> newDerivedNC deeper_loc $
-                      mkPrimEqPred (mkTyConApp fam_tc xis)
-                                   (mkTyVarTy fsk)
-
-           Wanted ->
+           Wanted {} ->
              do { (new_ev, new_co) <- newWantedEq deeper_loc Nominal
                                         (mkTyConApp fam_tc xis) (mkTyVarTy fsk)
                 ; setWantedEq (ctev_dest old_ev) $
@@ -1548,6 +1551,8 @@ shortCutReduction old_ev fsk ax_co fam_tc tc_args
                            `mkTcTransCo` new_co
                 ; return new_ev }
 
+           Derived -> pprPanic "shortCutReduction" (ppr old_ev)
+
        ; let new_ct = CFunEqCan { cc_ev = new_ev, cc_fun = fam_tc
                                 , cc_tyargs = xis, cc_fsk = fsk }
        ; updWorkListTcS (extendWorkListFunEq new_ct)
@@ -1559,19 +1564,21 @@ dischargeFmv :: CtEvidence -> TcTyVar -> TcCoercion -> TcType -> TcS ()
 -- (dischargeFmv x fmv co ty)
 --     [W] ev :: F tys ~ fmv
 --         co :: F tys ~ xi
--- Precondition: fmv is not filled, and fuv `notElem` xi
+-- Precondition: fmv is not filled, and fmv `notElem` xi
+--               ev is Wanted
 --
 -- Then set fmv := xi,
---      set ev := co
+--      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
+dischargeFmv ev@(CtWanted { ctev_dest = dest }) fmv co xi
   = ASSERT2( not (fmv `elemVarSet` tyCoVarsOfType xi), ppr ev $$ ppr fmv $$ ppr xi )
-    do { setEvBindIfWanted ev (EvCoercion co)
+    do { setWantedEvTerm dest (EvCoercion co)
        ; unflattenFmv fmv xi
        ; n_kicked <- kickOutAfterUnification fmv
        ; traceTcS "dischargeFmv" (ppr fmv <+> equals <+> ppr xi $$ ppr_kicked n_kicked) }
+dischargeFmv ev _ _ _ = pprPanic "dischargeFmv" (ppr ev)
 
 {- Note [Top-level reductions for type functions]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1585,15 +1592,14 @@ Here is what we do, in four cases:
     instantiate axiom: ax_co : F tys ~ rhs
 
    Then:
-      Discharge   fmv := alpha
+      Discharge   fmv := rhs
       Discharge   x := ax_co ; sym x2
-      New wanted  [W] x2 : alpha ~ rhs  (Non-canonical)
    This is *the* way that fmv's get unified; even though they are
    "untouchable".
 
-   NB: it can be the case that fmv appears in the (instantiated) rhs.
-   In that case the new Non-canonical wanted will be loopy, but that's
-   ok.  But it's good reason NOT to claim that it is canonical!
+   NB: Given Note [FunEq occurs-check principle], fmv does not appear
+   in tys, and hence does not appear in the instantiated RHS.  So
+   the unification can't make an infinite type.
 
 * Wanteds: short cut firing rule
   Applies when the RHS of the axiom is another type-function application
@@ -1625,6 +1631,36 @@ Here is what we do, in four cases:
      - Add new Canonical given
           [G] (sym (G flat_cos) ; co ; g) : G flat_tys ~ fsk   (CFunEqCan)
 
+Note [FunEq occurs-check principle]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+I have spent a lot of time finding a good way to deal with
+CFunEqCan constraints like
+    F (fuv, a) ~ fuv
+where flatten-skolem occurs on the LHS.  Now in principle we
+might may progress by doing a reduction, but in practice its
+hard to find examples where it is useful, and easy to find examples
+where we fall into an infinite reduction loop.  A rule that works
+very well is this:
+
+  *** FunEq occurs-check principle ***
+
+      Do not reduce a CFunEqCan
+          F tys ~ fsk
+      if fsk appears free in tys
+      Instead we treat it as stuck.
+
+Examples:
+
+* Trac #5837 has [G] a ~ TF (a,Int), with an instance
+    type instance TF (a,b) = (TF a, TF b)
+  This readily loops when solving givens.  But with the FunEq occurs
+  check principle, it rapidly gets stuck which is fine.
+
+* Trac #12444 is a good example, explained in comment:2.  We have
+    type instance F (Succ x) = Succ (F x)
+    [W] alpha ~ Succ (F alpha)
+  If we allow the reduction to happen, we get an infinite loop
+
 Note [Cached solved FunEqs]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
 When trying to solve, say (FunExpensive big-type ~ ty), it's important
@@ -1639,87 +1675,6 @@ When trying to match a dictionary (D tau) to a top-level instance, or a
 type family equation (F taus_1 ~ tau_2) to a top-level family instance,
 we do *not* need to expand type synonyms because the matcher will do that for us.
 
-
-Note [RHS-FAMILY-SYNONYMS]
-~~~~~~~~~~~~~~~~~~~~~~~~~~
-The RHS of a family instance is represented as yet another constructor which is
-like a type synonym for the real RHS the programmer declared. Eg:
-    type instance F (a,a) = [a]
-Becomes:
-    :R32 a = [a]      -- internal type synonym introduced
-    F (a,a) ~ :R32 a  -- instance
-
-When we react a family instance with a type family equation in the work list
-we keep the synonym-using RHS without expansion.
-
-Note [FunDep and implicit parameter reactions]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Currently, our story of interacting two dictionaries (or a dictionary
-and top-level instances) for functional dependencies, and implicit
-parameters, is that we simply produce new Derived equalities.  So for example
-
-        class D a b | a -> b where ...
-    Inert:
-        d1 :g D Int Bool
-    WorkItem:
-        d2 :w D Int alpha
-
-    We generate the extra work item
-        cv :d alpha ~ Bool
-    where 'cv' is currently unused.  However, this new item can perhaps be
-    spontaneously solved to become given and react with d2,
-    discharging it in favour of a new constraint d2' thus:
-        d2' :w D Int Bool
-        d2 := d2' |> D Int cv
-    Now d2' can be discharged from d1
-
-We could be more aggressive and try to *immediately* solve the dictionary
-using those extra equalities, but that requires those equalities to carry
-evidence and derived do not carry evidence.
-
-If that were the case with the same inert set and work item we might dischard
-d2 directly:
-
-        cv :w alpha ~ Bool
-        d2 := d1 |> D Int cv
-
-But in general it's a bit painful to figure out the necessary coercion,
-so we just take the first approach. Here is a better example. Consider:
-    class C a b c | a -> b
-And:
-     [Given]  d1 : C T Int Char
-     [Wanted] d2 : C T beta Int
-In this case, it's *not even possible* to solve the wanted immediately.
-So we should simply output the functional dependency and add this guy
-[but NOT its superclasses] back in the worklist. Even worse:
-     [Given] d1 : C T Int beta
-     [Wanted] d2: C T beta Int
-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 [Weird fundeps]
-~~~~~~~~~~~~~~~~~~~~
-Consider   class Het a b | a -> b where
-              het :: m (f c) -> a -> m b
-
-           class GHet (a :: * -> *) (b :: * -> *) | a -> b
-           instance            GHet (K a) (K [a])
-           instance Het a b => GHet (K a) (K b)
-
-The two instances don't actually conflict on their fundeps,
-although it's pretty strange.  So they are both accepted. Now
-try   [W] GHet (K Int) (K Bool)
-This triggers fundeps from both instance decls;
-      [D] K Bool ~ K [a]
-      [D] K Bool ~ K beta
-And there's a risk of complaining about Bool ~ [a].  But in fact
-the Wanted matches the second instance, so we never get as far
-as the fundeps.
-
-Trac #7875 is a case in point.
-
 Note [Improvement orientation]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 A very delicate point is the orientation of derived equalities
@@ -1756,10 +1711,170 @@ template.  But that's a bit tricky, esp when we remember that the
 kinds much match too; so it's easier to let the normal machinery
 handle it.  Instead we are careful to orient the new derived
 equality with the template on the left.  Delicate, but it works.
+
+Note [No FunEq improvement for Givens]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We don't do improvements (injectivity etc) for Givens. Why?
+
+* It generates Derived constraints on skolems, which don't do us
+  much good, except perhaps identify inaccessible branches.
+  (They'd be perfectly valid though.)
+
+* For type-nat stuff the derived constraints include type families;
+  e.g.  (a < b), (b < c) ==> a < c If we generate a Derived for this,
+  we'll generate a Derived/Wanted CFunEqCan; and, since the same
+  InertCans (after solving Givens) are used for each iteration, that
+  massively confused the unflattening step (TcFlatten.unflatten).
+
+  In fact it led to some infinite loops:
+     indexed-types/should_compile/T10806
+     indexed-types/should_compile/T10507
+     polykinds/T10742
+
+Note [Reduction for Derived CFunEqCans]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+You may wonder if it's important to use top-level instances to
+simplify [D] CFunEqCan's.  But it is.  Here's an example (T10226).
+
+   type instance F    Int = Int
+   type instance FInv Int = Int
+
+Suppose we have to solve
+    [WD] FInv (F alpha) ~ alpha
+    [WD] F alpha ~ Int
+
+  --> flatten
+    [WD] F alpha ~ fuv0
+    [WD] FInv fuv0 ~ fuv1  -- (A)
+    [WD] fuv1 ~ alpha
+    [WD] fuv0 ~ Int        -- (B)
+
+  --> Rewwrite (A) with (B), splitting it
+    [WD] F alpha ~ fuv0
+    [W] FInv fuv0 ~ fuv1
+    [D] FInv Int ~ fuv1    -- (C)
+    [WD] fuv1 ~ alpha
+    [WD] fuv0 ~ Int
+
+  --> Reduce (C) with top-level instance
+      **** This is the key step ***
+    [WD] F alpha ~ fuv0
+    [W] FInv fuv0 ~ fuv1
+    [D] fuv1 ~ Int        -- (D)
+    [WD] fuv1 ~ alpha     -- (E)
+    [WD] fuv0 ~ Int
+
+  --> Rewrite (D) with (E)
+    [WD] F alpha ~ fuv0
+    [W] FInv fuv0 ~ fuv1
+    [D] alpha ~ Int       -- (F)
+    [WD] fuv1 ~ alpha
+    [WD] fuv0 ~ Int
+
+  --> unify (F)  alpha := Int, and that solves it
+
+Another example is indexed-types/should_compile/T10634
 -}
 
 {- *******************************************************************
 *                                                                    *
+         Top-level reaction for class constraints (CDictCan)
+*                                                                    *
+**********************************************************************-}
+
+doTopReactDict :: InertSet -> Ct -> TcS (StopOrContinue Ct)
+-- Try to use type-class instance declarations to simplify the constraint
+doTopReactDict inerts work_item@(CDictCan { cc_ev = fl, cc_class = cls
+                                          , cc_tyargs = xis })
+  | isGiven fl
+  = do { try_fundep_improvement
+       ; continueWith work_item }
+
+  | Just ev <- lookupSolvedDict inerts cls xis   -- Cached
+  = do { setEvBindIfWanted fl (ctEvTerm ev)
+       ; stopWith fl "Dict/Top (cached)" }
+
+  | isDerived fl  -- Use type-class instances for Deriveds, in the hope
+                  -- of generating some improvements
+                  -- C.f. Example 3 of Note [The improvement story]
+                  -- It's easy because no evidence is involved
+   = do { dflags <- getDynFlags
+        ; lkup_inst_res <- matchClassInst dflags inerts cls xis dict_loc
+        ; case lkup_inst_res of
+               GenInst { lir_new_theta = preds
+                       , lir_safe_over = s } ->
+                 do { emitNewDeriveds dict_loc preds
+                    ; unless s $ insertSafeOverlapFailureTcS work_item
+                    ; stopWith fl "Dict/Top (solved)" }
+
+               NoInstance ->
+                 do { -- If there is no instance, try improvement
+                      try_fundep_improvement
+                    ; continueWith work_item } }
+
+  | otherwise  -- Wanted, but not cached
+   = do { dflags <- getDynFlags
+        ; lkup_inst_res <- matchClassInst dflags inerts cls xis dict_loc
+        ; case lkup_inst_res of
+               GenInst { lir_new_theta = theta
+                       , lir_mk_ev     = mk_ev
+                       , lir_safe_over = s } ->
+                 do { addSolvedDict fl cls xis
+                    ; unless s $ insertSafeOverlapFailureTcS work_item
+                    ; solve_from_instance theta mk_ev }
+               NoInstance ->
+                 do { try_fundep_improvement
+                    ; continueWith work_item } }
+   where
+     dict_pred   = mkClassPred cls xis
+     dict_loc    = ctEvLoc fl
+     dict_origin = ctLocOrigin dict_loc
+     deeper_loc  = zap_origin (bumpCtLocDepth dict_loc)
+
+     zap_origin loc  -- After applying an instance we can set ScOrigin to
+                     -- infinity, so that prohibitedSuperClassSolve never fires
+       | ScOrigin {} <- dict_origin
+       = setCtLocOrigin loc (ScOrigin infinity)
+       | otherwise
+       = loc
+
+     solve_from_instance :: [TcPredType]
+                         -> ([EvTerm] -> EvTerm) -> TcS (StopOrContinue Ct)
+      -- Precondition: evidence term matches the predicate workItem
+     solve_from_instance theta mk_ev
+        | null theta
+        = do { traceTcS "doTopReact/found nullary instance for" $ ppr fl
+             ; setWantedEvBind (ctEvId fl) (mk_ev [])
+             ; stopWith fl "Dict/Top (solved, no new work)" }
+        | otherwise
+        = do { checkReductionDepth deeper_loc dict_pred
+             ; traceTcS "doTopReact/found non-nullary instance for" $ ppr fl
+             ; evc_vars <- mapM (newWanted deeper_loc) theta
+             ; setWantedEvBind (ctEvId fl) (mk_ev (map getEvTerm evc_vars))
+             ; emitWorkNC (freshGoals evc_vars)
+             ; stopWith fl "Dict/Top (solved, more work)" }
+
+     -- 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)
+
+
+{- *******************************************************************
+*                                                                    *
                        Class lookup
 *                                                                    *
 **********************************************************************-}
index ff0ee9e..c200b4e 100644 (file)
@@ -43,7 +43,7 @@ module TcMType (
   --------------------------------
   -- Creating new evidence variables
   newEvVar, newEvVars, newDict,
-  newWanted, newWanteds,
+  newWanted, newWanteds, cloneWanted, cloneWC,
   emitWanted, emitWantedEq, emitWantedEvVar, emitWantedEvVars,
   newTcEvBinds, addTcEvBind,
 
@@ -170,11 +170,30 @@ newWanted orig t_or_k pty
                             else EvVarDest <$> newEvVar pty
        return $ CtWanted { ctev_dest = d
                          , ctev_pred = pty
+                         , ctev_nosh = WDeriv
                          , ctev_loc = loc }
 
 newWanteds :: CtOrigin -> ThetaType -> TcM [CtEvidence]
 newWanteds orig = mapM (newWanted orig Nothing)
 
+cloneWanted :: Ct -> TcM CtEvidence
+cloneWanted ct
+  = newWanted (ctEvOrigin ev) Nothing (ctEvPred ev)
+  where
+    ev = ctEvidence ct
+
+cloneWC :: WantedConstraints -> TcM WantedConstraints
+cloneWC wc@(WC { wc_simple = simples, wc_impl = implics })
+  = do { simples' <- mapBagM clone_one simples
+       ; implics' <- mapBagM clone_implic implics
+       ; return (wc { wc_simple = simples', wc_impl = implics' }) }
+  where
+    clone_one ct = do { ev <- cloneWanted ct; return (mkNonCanonical ev) }
+
+    clone_implic implic@(Implic { ic_wanted = inner_wanted })
+      = do { inner_wanted' <- cloneWC inner_wanted
+           ; return (implic { ic_wanted = inner_wanted' }) }
+
 -- | Emits a new Wanted. Deals with both equalities and non-equalities.
 emitWanted :: CtOrigin -> TcPredType -> TcM EvTerm
 emitWanted origin pty
@@ -188,7 +207,8 @@ emitWantedEq origin t_or_k role ty1 ty2
   = do { hole <- newCoercionHole
        ; loc <- getCtLocM origin (Just t_or_k)
        ; emitSimple $ mkNonCanonical $
-           CtWanted { ctev_pred = pty, ctev_dest = HoleDest hole, ctev_loc = loc }
+         CtWanted { ctev_pred = pty, ctev_dest = HoleDest hole
+                  , ctev_nosh = WDeriv, ctev_loc = loc }
        ; return (mkHoleCo hole role ty1 ty2) }
   where
     pty = mkPrimEqPredRole role ty1 ty2
@@ -201,6 +221,7 @@ emitWantedEvVar origin ty
        ; loc <- getCtLocM origin Nothing
        ; let ctev = CtWanted { ctev_dest = EvVarDest new_cv
                              , ctev_pred = ty
+                             , ctev_nosh = WDeriv
                              , ctev_loc  = loc }
        ; emitSimple $ mkNonCanonical ctev
        ; return new_cv }
index ce541c3..fd6d74c 100644 (file)
@@ -78,10 +78,8 @@ module TcRnTypes(
         ctEvTerm, ctEvCoercion, ctEvId,
         tyCoVarsOfCt, tyCoVarsOfCts,
         tyCoVarsOfCtList, tyCoVarsOfCtsList,
-        toDerivedCt,
 
         WantedConstraints(..), insolubleWC, emptyWC, isEmptyWC,
-        toDerivedWC,
         andWC, unionsWC, mkSimpleWC, mkImplicWC,
         addInsols, getInsolubles, addSimples, addImplics,
         tyCoVarsOfWC, dropDerivedWC, dropDerivedSimples, dropDerivedInsols,
@@ -107,7 +105,7 @@ module TcRnTypes(
 
         CtEvidence(..), TcEvDest(..),
         mkGivenLoc, mkKindLoc, toKindLoc,
-        isWanted, isGiven, isDerived,
+        isWanted, isGiven, isDerived, isGivenOrWDeriv,
         ctEvRole,
 
         -- Constraint solver plugins
@@ -115,10 +113,11 @@ module TcRnTypes(
         TcPluginM, runTcPluginM, unsafeTcPluginTcM,
         getEvBindsTcPluginM,
 
-        CtFlavour(..), ctEvFlavour,
+        CtFlavour(..), ShadowInfo(..), ctEvFlavour,
         CtFlavourRole, ctEvFlavourRole, ctFlavourRole,
-        eqCanRewrite, eqCanRewriteFR,  eqCanDischarge,
-        funEqCanDischarge, funEqCanDischargeFR,
+        eqCanRewriteFR, eqMayRewriteFR,
+        eqCanDischarge,
+        funEqCanDischarge, funEqCanDischargeF,
 
         -- Pretty printing
         pprEvVarTheta,
@@ -174,6 +173,7 @@ import ListSetOps
 import FastString
 import qualified GHC.LanguageExtensions as LangExt
 import Fingerprint
+import Util
 
 import Control.Monad (ap, liftM, msum)
 #if __GLASGOW_HASKELL__ > 710
@@ -1509,7 +1509,8 @@ data Ct
       cc_tyvar  :: TcTyVar,
       cc_rhs    :: TcType,     -- Not necessarily function-free (hence not Xi)
                                -- See invariants above
-      cc_eq_rel :: EqRel
+
+      cc_eq_rel :: EqRel       -- INVARIANT: cc_eq_rel = ctEvEqRel cc_ev
     }
 
   | CFunEqCan {  -- F xis ~ fsk
@@ -1625,16 +1626,6 @@ ctPred :: Ct -> PredType
 -- See Note [Ct/evidence invariant]
 ctPred ct = ctEvPred (cc_ev ct)
 
--- | Convert a Wanted to a Derived
-toDerivedCt :: Ct -> Ct
-toDerivedCt ct
-  = case ctEvidence ct of
-      CtWanted { ctev_pred = pred, ctev_loc = loc }
-        -> ct {cc_ev = CtDerived {ctev_pred = pred, ctev_loc = loc}}
-
-      CtDerived {} -> ct
-      CtGiven   {} -> pprPanic "to_derived" (ppr ct)
-
 -- | Makes a new equality predicate with the same role as the given
 -- evidence.
 mkTcEqPredLikeEv :: CtEvidence -> TcType -> TcType -> TcType
@@ -2074,16 +2065,6 @@ andWC (WC { wc_simple = f1, wc_impl = i1, wc_insol = n1 })
 unionsWC :: [WantedConstraints] -> WantedConstraints
 unionsWC = foldr andWC emptyWC
 
--- | Convert all Wanteds into Deriveds (ignoring insolubles)
-toDerivedWC :: WantedConstraints -> WantedConstraints
-toDerivedWC wc@(WC { wc_simple = simples, wc_impl = implics })
-  = wc { wc_simple = mapBag toDerivedCt simples
-       , wc_impl   = mapBag to_derived_implic implics }
-  where
-    to_derived_implic implic@(Implic { ic_wanted = inner_wanted })
-      = implic { ic_wanted = toDerivedWC inner_wanted }
-
-
 addSimples :: WantedConstraints -> Bag Ct -> WantedConstraints
 addSimples wc cts
   = wc { wc_simple = wc_simple wc `unionBags` cts }
@@ -2113,21 +2094,23 @@ isInsolubleStatus _            = False
 insolubleImplic :: Implication -> Bool
 insolubleImplic ic = isInsolubleStatus (ic_status ic)
 
-insolubleWC :: TcLevel -> WantedConstraints -> Bool
-insolubleWC tc_lvl (WC { wc_impl = implics, wc_insol = insols })
-  =  anyBag (trulyInsoluble tc_lvl) insols
+insolubleWC :: WantedConstraints -> Bool
+insolubleWC (WC { wc_impl = implics, wc_insol = insols })
+  =  anyBag trulyInsoluble insols
   || anyBag insolubleImplic implics
 
-trulyInsoluble :: TcLevel -> Ct -> Bool
+trulyInsoluble :: Ct -> Bool
 -- Constraints in the wc_insol set which ARE NOT
 -- treated as truly insoluble:
 --   a) type holes, arising from PartialTypeSignatures,
 --   b) "true" expression holes arising from TypedHoles
 --
--- Out-of-scope variables masquerading as expression holes
--- ARE treated as truly insoluble.
+-- A "expression hole" or "type hole" constraint isn't really an error
+-- at all; it's a report saying "_ :: Int" here.  But an out-of-scope
+-- variable masquerading as expression holes IS treated as truly
+-- insoluble, so that it trumps other errors during error reporting.
 -- Yuk!
-trulyInsoluble _tc_lvl insol
+trulyInsoluble insol
   | isHoleCt insol = isOutOfScopeCt insol
   | otherwise      = True
 
@@ -2342,22 +2325,25 @@ data TcEvDest
               -- See Note [Coercion holes] in TyCoRep
 
 data CtEvidence
-  = CtGiven { ctev_pred :: TcPredType      -- See Note [Ct/evidence invariant]
-            , ctev_evar :: EvVar           -- See Note [Evidence field of CtEvidence]
-            , ctev_loc  :: CtLoc }
-    -- Truly given, not depending on subgoals
-    -- NB: Spontaneous unifications belong here
-
-  | CtWanted { ctev_pred :: TcPredType     -- See Note [Ct/evidence invariant]
-             , ctev_dest :: TcEvDest
-             , ctev_loc  :: CtLoc }
-    -- Wanted goal
-
-  | CtDerived { ctev_pred :: TcPredType
-              , ctev_loc  :: CtLoc }
-    -- A goal that we don't really have to solve and can't immediately
-    -- rewrite anything other than a derived (there's no evidence!)
-    -- but if we do manage to solve it may help in solving other goals.
+  = CtGiven    -- Truly given, not depending on subgoals
+               -- NB: Spontaneous unifications belong here
+      { ctev_pred :: TcPredType      -- See Note [Ct/evidence invariant]
+      , ctev_evar :: EvVar           -- See Note [Evidence field of CtEvidence]
+      , ctev_loc  :: CtLoc }
+
+
+  | CtWanted   -- Wanted goal
+      { ctev_pred :: TcPredType     -- See Note [Ct/evidence invariant]
+      , ctev_dest :: TcEvDest
+      , ctev_nosh :: ShadowInfo     -- See Note [Constraint flavours]
+      , ctev_loc  :: CtLoc }
+
+  | CtDerived  -- A goal that we don't really have to solve and can't
+               -- immediately rewrite anything other than a derived
+               -- (there's no evidence!) but if we do manage to solve
+               -- it may help in solving other goals.
+      { ctev_pred :: TcPredType
+      , ctev_loc  :: CtLoc }
 
 ctEvPred :: CtEvidence -> TcPredType
 -- The predicate of a flavor
@@ -2399,11 +2385,12 @@ instance Outputable TcEvDest where
   ppr (EvVarDest ev) = ppr ev
 
 instance Outputable CtEvidence where
-  ppr fl = case fl of
-             CtGiven {}   -> text "[G]" <+> ppr (ctev_evar fl) <+> ppr_pty
-             CtWanted {}  -> text "[W]" <+> ppr (ctev_dest fl) <+> ppr_pty
-             CtDerived {} -> text "[D]" <+> text "_" <+> ppr_pty
-         where ppr_pty = dcolon <+> ppr (ctEvPred fl)
+  ppr ev = ppr (ctEvFlavour ev) <+> pp_ev <+> dcolon <+> ppr (ctEvPred ev)
+    where
+      pp_ev = case ev of
+             CtGiven { ctev_evar = v } -> ppr v
+             CtWanted {ctev_dest = d } -> ppr d
+             CtDerived {}              -> text "_"
 
 isWanted :: CtEvidence -> Bool
 isWanted (CtWanted {}) = True
@@ -2424,23 +2411,62 @@ isDerived _              = False
 %*                                                                      *
 %************************************************************************
 
-Just an enum type that tracks whether a constraint is wanted, derived,
-or given, when we need to separate that info from the constraint itself.
+Note [Constraint flavours]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+Constraints come in four flavours:
+
+* [G] Given: we have evidence
+
+* [W] Wanted WOnly: we want evidence
+
+* [D] Derived: any solution must satisfy this constraint, but
+      we don't need evidence for it.  Examples include:
+        - superclasses of [W] class constraints
+        - equalities arising from functional dependencies
+          or injectivity
 
+* [WD] Wanted WDeriv: a single constraint that represents
+                      both [W] and [D]
+  We keep them paired as one both for efficiency, and because
+  when we have a finite map  F tys -> CFunEqCan, it's inconvenient
+  to have two CFunEqCans in the range
+
+The ctev_nosh field of a Wanted distinguishes between [W] and [WD]
+
+Wanted constraints are born as [WD], but are split into [W] and its
+"shadow" [D] in TcSMonad.maybeEmitShadow.
+
+See Note [The improvement story and derived shadows] in TcSMonad
 -}
 
-data CtFlavour = Given | Wanted | Derived
+data CtFlavour  -- See Note [Constraint flavours]
+  = Given
+  | Wanted ShadowInfo
+  | Derived
   deriving Eq
 
+data ShadowInfo
+  = WDeriv   -- [WD] This Wanted constraint has no Derived shadow,
+             -- so it behaves like a pair of a Wanted and a Derived
+  | WOnly    -- [W] It has a separate derived shadow
+             -- See Note [Derived shadows]
+  deriving( Eq )
+
+isGivenOrWDeriv :: CtFlavour -> Bool
+isGivenOrWDeriv Given           = True
+isGivenOrWDeriv (Wanted WDeriv) = True
+isGivenOrWDeriv _               = False
+
 instance Outputable CtFlavour where
-  ppr Given   = text "[G]"
-  ppr Wanted  = text "[W]"
-  ppr Derived = text "[D]"
+  ppr Given           = text "[G]"
+  ppr (Wanted WDeriv) = text "[WD]"
+  ppr (Wanted WOnly)  = text "[W]"
+  ppr Derived         = text "[D]"
 
 ctEvFlavour :: CtEvidence -> CtFlavour
-ctEvFlavour (CtWanted {})  = Wanted
-ctEvFlavour (CtGiven {})   = Given
-ctEvFlavour (CtDerived {}) = Derived
+ctEvFlavour (CtWanted { ctev_nosh = nosh }) = Wanted nosh
+ctEvFlavour (CtGiven {})                    = Given
+ctEvFlavour (CtDerived {})                  = Derived
 
 -- | Whether or not one 'Ct' can rewrite another is determined by its
 -- flavour and its equality relation. See also
@@ -2456,7 +2482,7 @@ ctFlavourRole :: Ct -> CtFlavourRole
 ctFlavourRole = ctEvFlavourRole . cc_ev
 
 {- Note [eqCanRewrite]
-~~~~~~~~~~~~~~~~~~~
+~~~~~~~~~~~~~~~~~~~~~~
 (eqCanRewrite ct1 ct2) holds if the constraint ct1 (a CTyEqCan of form
 tv ~ ty) can be used to rewrite ct2.  It must satisfy the properties of
 a can-rewrite relation, see Definition [Can-rewrite relation] in
@@ -2498,9 +2524,31 @@ I thought maybe we could never get Derived ReprEq constraints, but
 we can; straight from the Wanteds during improvment. And from a Derived
 ReprEq we could conceivably get a Derived NomEq improvment (by decomposing
 a type constructor with Nomninal role), and hence unify.
+-}
 
-Note [funEqCanDischarge]
-~~~~~~~~~~~~~~~~~~~~~~~~~
+eqCanRewriteFR :: CtFlavourRole -> CtFlavourRole -> Bool
+-- Can fr1 actually rewrite fr2?
+-- Very important function!
+-- See Note [eqCanRewrite]
+-- See Note [Wanteds do not rewrite Wanteds]
+-- See Note [Deriveds do rewrite Deriveds]
+eqCanRewriteFR (Given, NomEq)         (_, _)           = True
+eqCanRewriteFR (Given, ReprEq)        (_, ReprEq)      = True
+eqCanRewriteFR (Wanted WDeriv, NomEq) (Derived, NomEq) = True
+eqCanRewriteFR (Derived,       NomEq) (Derived, NomEq) = True
+eqCanRewriteFR _                      _                = False
+
+eqMayRewriteFR :: CtFlavourRole -> CtFlavourRole -> Bool
+-- Is it /possible/ that fr1 can rewrite fr2?
+-- This is used when deciding which inerts to kick out,
+-- at which time a [WD] inert may be split into [W] and [D]
+eqMayRewriteFR (Wanted WDeriv, NomEq) (Wanted WDeriv, NomEq) = True
+eqMayRewriteFR (Derived,       NomEq) (Wanted WDeriv, NomEq) = True
+eqMayRewriteFR fr1 fr2 = eqCanRewriteFR fr1 fr2
+
+-----------------
+{- Note [funEqCanDischarge]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Suppose we have two CFunEqCans with the same LHS:
     (x1:F ts ~ f1) `funEqCanDischarge` (x2:F ts ~ f2)
 Can we drop x2 in favour of x1, either unifying
@@ -2508,12 +2556,37 @@ f2 (if it's a flatten meta-var) or adding a new Given
 (f1 ~ f2), if x2 is a Given?
 
 Answer: yes if funEqCanDischarge is true.
+-}
 
-Note [eqCanDischarge]
-~~~~~~~~~~~~~~~~~~~~~
-Suppose we have two identicla equality constraints
+funEqCanDischarge
+  :: CtEvidence -> CtEvidence
+  -> ( SwapFlag   -- NotSwapped => lhs can discharge rhs
+                  -- Swapped    => rhs can discharge lhs
+     , Bool)      -- True <=> upgrade non-discharded one
+                  --          from [W] to [WD]
+-- See Note [funEqCanDischarge]
+funEqCanDischarge ev1 ev2
+  = ASSERT2( ctEvEqRel ev1 == NomEq, ppr ev1 )
+    ASSERT2( ctEvEqRel ev2 == NomEq, ppr ev2 )
+    -- CFunEqCans are all Nominal, hence asserts
+    funEqCanDischargeF (ctEvFlavour ev1) (ctEvFlavour ev2)
+
+funEqCanDischargeF :: CtFlavour -> CtFlavour -> (SwapFlag, Bool)
+funEqCanDischargeF Given           _               = (NotSwapped, False)
+funEqCanDischargeF _               Given           = (IsSwapped,  False)
+funEqCanDischargeF (Wanted WDeriv) _               = (NotSwapped, False)
+funEqCanDischargeF _               (Wanted WDeriv) = (IsSwapped,  True)
+funEqCanDischargeF (Wanted WOnly)  (Wanted WOnly)  = (NotSwapped, False)
+funEqCanDischargeF (Wanted WOnly)  Derived         = (NotSwapped, True)
+funEqCanDischargeF Derived         (Wanted WOnly)  = (IsSwapped,  True)
+funEqCanDischargeF Derived         Derived         = (NotSwapped, False)
+
+
+{- Note [eqCanDischarge]
+~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose we have two identical CTyEqCan equality constraints
 (i.e. both LHS and RHS are the same)
-      (x1:s~t) `eqCanDischarge` (xs:s~t)
+      (x1:a~t) `eqCanDischarge` (xs:a~t)
 Can we just drop x2 in favour of x1?
 
 Answer: yes if eqCanDischarge is true.
@@ -2525,48 +2598,27 @@ other Deriveds in the model whereas the Wanted cannot.
 However a Wanted can certainly discharge an identical Wanted.  So
 eqCanDischarge does /not/ define a can-rewrite relation in the
 sense of Definition [Can-rewrite relation] in TcSMonad.
--}
 
------------------
-eqCanRewrite :: CtEvidence -> CtEvidence -> Bool
--- Very important function!
--- See Note [eqCanRewrite]
--- See Note [Wanteds do not rewrite Wanteds]
--- See Note [Deriveds do rewrite Deriveds]
-eqCanRewrite ev1 ev2 = eqCanRewriteFR (ctEvFlavourRole ev1)
-                                      (ctEvFlavourRole ev2)
+We /do/ say that a [W] can discharge a [WD].  In evidence terms it
+certainly can, and the /caller/ arranges that the otherwise-lost [D]
+is spat out as a new Derived.  -}
 
-eqCanRewriteFR :: CtFlavourRole -> CtFlavourRole -> Bool
-eqCanRewriteFR (Given, NomEq)   (_, _)           = True
-eqCanRewriteFR (Given, ReprEq)  (_, ReprEq)      = True
-eqCanRewriteFR (Derived, NomEq) (Derived, NomEq) = True
-eqCanRewriteFR _                _                = False
-
------------------
-funEqCanDischarge :: CtEvidence -> CtEvidence -> Bool
--- See Note [funEqCanDischarge]
-funEqCanDischarge ev1 ev2 = funEqCanDischargeFR (ctEvFlavourRole ev1)
-                                      (ctEvFlavourRole ev2)
-
-funEqCanDischargeFR :: CtFlavourRole -> CtFlavourRole -> Bool
-funEqCanDischargeFR (_, ReprEq)  (_, NomEq)   = False
-funEqCanDischargeFR (Given,   _) _            = True
-funEqCanDischargeFR (Wanted,  _) (Wanted,  _) = True
-funEqCanDischargeFR (Wanted,  _) (Derived, _) = True
-funEqCanDischargeFR (Derived, _) (Derived, _) = True
-funEqCanDischargeFR _            _            = False
-
------------------
 eqCanDischarge :: CtEvidence -> CtEvidence -> Bool
 -- See Note [eqCanDischarge]
 eqCanDischarge ev1 ev2 = eqCanDischargeFR (ctEvFlavourRole ev1)
                                           (ctEvFlavourRole ev2)
+
 eqCanDischargeFR :: CtFlavourRole -> CtFlavourRole -> Bool
-eqCanDischargeFR (_, ReprEq)  (_, NomEq)   = False
-eqCanDischargeFR (Given,   _) (Given,_)    = True
-eqCanDischargeFR (Wanted,  _) (Wanted,  _) = True
-eqCanDischargeFR (Derived, _) (Derived, _) = True
-eqCanDischargeFR _            _            = False
+eqCanDischargeFR (_, ReprEq) (_, NomEq) = False
+eqCanDischargeFR (f1,_)      (f2, _)    = eqCanDischargeF f1 f2
+
+eqCanDischargeF :: CtFlavour -> CtFlavour -> Bool
+eqCanDischargeF Given   _                  = True
+eqCanDischargeF (Wanted _)      (Wanted _) = True
+eqCanDischargeF (Wanted WDeriv) Derived    = True
+eqCanDischargeF Derived         Derived    = True
+eqCanDischargeF _               _          = False
+
 
 {-
 ************************************************************************
index 4cfccb6..2983ccb 100644 (file)
@@ -287,16 +287,14 @@ EvVar for the coercion, fill the hole with the invented EvVar, and
 then quantify over the EvVar. Not too tricky -- just some
 impedence matching, really.
 
-Note [Simplify *derived* constraints]
+Note [Simplify cloned constraints]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 At this stage, we're simplifying constraints only for insolubility
 and for unification. Note that all the evidence is quickly discarded.
-We make this explicit by working over derived constraints, for which
-there is no evidence. Using derived constraints also prevents solved
-equalities from being written to coercion holes. If we don't do this,
+We use a clone of the real constraint. If we don't do this,
 then RHS coercion-hole constraints get filled in, only to get filled
 in *again* when solving the implications emitted from tcRule. That's
-terrible, so we avoid the problem by using derived constraints.
+terrible, so we avoid the problem by cloning the constraints.
 
 -}
 
@@ -310,15 +308,16 @@ simplifyRule :: RuleName
 simplifyRule name lhs_wanted rhs_wanted
   = do {         -- We allow ourselves to unify environment
                  -- variables: runTcS runs with topTcLevel
-       ; tc_lvl    <- getTcLevel
+       ; lhs_clone <- cloneWC lhs_wanted
+       ; rhs_clone <- cloneWC rhs_wanted
        ; insoluble <- runTcSDeriveds $
              do { -- First solve the LHS and *then* solve the RHS
                   -- See Note [Solve order for RULES]
-                  -- See Note [Simplify *derived* constraints]
-                  lhs_resid <- solveWanteds $ toDerivedWC lhs_wanted
-                ; rhs_resid <- solveWanteds $ toDerivedWC rhs_wanted
-                ; return ( insolubleWC tc_lvl lhs_resid ||
-                           insolubleWC tc_lvl rhs_resid ) }
+                  -- See Note [Simplify cloned constraints]
+                  lhs_resid <- solveWanteds lhs_clone
+                ; rhs_resid <- solveWanteds rhs_clone
+                ; return ( insolubleWC lhs_resid ||
+                           insolubleWC rhs_resid ) }
 
 
        ; zonked_lhs_simples <- zonkSimples (wc_simple lhs_wanted)
index 0d20122..dd9a82b 100644 (file)
@@ -49,8 +49,9 @@ module TcSMonad (
     InertSet(..), InertCans(..),
     updInertTcS, updInertCans, updInertDicts, updInertIrreds,
     getNoGivenEqs, setInertCans,
-    getInertEqs, getInertCans, getInertModel, getInertGivens,
-    emptyInert, getTcSInerts, setTcSInerts, takeGivenInsolubles,
+    getInertEqs, getInertCans, getInertGivens,
+    getInertInsols,
+    emptyInert, getTcSInerts, setTcSInerts,
     matchableGivens, prohibitedSuperClassSolve,
     getUnsolvedInerts,
     removeInertCts, getPendingScDicts,
@@ -58,7 +59,7 @@ module TcSMonad (
     emitInsoluble, emitWorkNC, emitWork,
 
     -- The Model
-    InertModel, kickOutAfterUnification,
+    kickOutAfterUnification,
 
     -- Inert Safe Haskell safe-overlap failures
     addInertSafehask, insertSafeOverlapFailureTcS, updInertSafehask,
@@ -70,6 +71,7 @@ module TcSMonad (
 
     -- Inert CTyEqCans
     EqualCtList, findTyEqs, foldTyEqs, isInInertEqs,
+    lookupFlattenTyVar, lookupInertTyVar,
 
     -- Inert solved dictionaries
     addSolvedDict, lookupSolvedDict,
@@ -81,7 +83,7 @@ module TcSMonad (
     lookupFlatCache, extendFlatCache, newFlattenSkolem,            -- Flatten skolems
 
     -- Inert CFunEqCans
-    updInertFunEqs, findFunEq, sizeFunEqMap,
+    updInertFunEqs, findFunEq,
     findFunEqsByTyCon,
 
     instDFunType,                              -- Instantiation
@@ -341,8 +343,7 @@ selectNextWorkItem
        ; try (selectWorkItem wl) $
 
     do { ics <- getInertCans
-       ; solve_deriveds <- keepSolvingDeriveds
-       ; if inert_count ics == 0 && not solve_deriveds
+       ; if inert_count ics == 0
          then return Nothing
          else try (selectDerivedWorkItem wl) (return Nothing) } }
 
@@ -375,13 +376,14 @@ instance Outputable WorkList where
 
 data InertSet
   = IS { inert_cans :: InertCans
-              -- Canonical Given, Wanted, Derived (no Solved)
+              -- Canonical Given, Wanted, Derived
               -- Sometimes called "the inert set"
 
        , inert_flat_cache :: ExactFunEqMap (TcCoercion, TcType, CtFlavour)
               -- See Note [Type family equations]
-              -- If    F tys :-> (co, ty, ev),
-              -- then  co :: F tys ~ ty
+              -- If    F tys :-> (co, rhs, flav),
+              -- then  co :: F tys ~ rhs
+              --       flav is [G] or [WD]
               --
               -- Just a hash-cons cache for use when flattening only
               -- These include entirely un-processed goals, so don't use
@@ -410,8 +412,7 @@ emptyInert
                          , inert_safehask = emptyDicts
                          , inert_funeqs   = emptyFunEqs
                          , inert_irreds   = emptyCts
-                         , inert_insols   = emptyCts
-                         , inert_model    = emptyDVarEnv }
+                         , inert_insols   = emptyCts }
        , inert_flat_cache    = emptyExactFunEqs
        , inert_solved_dicts  = emptyDictMap }
 
@@ -584,26 +585,23 @@ Result
 ********************************************************************* -}
 
 data InertCans   -- See Note [Detailed InertCans Invariants] for more
-  = IC { inert_model :: InertModel
-              -- See Note [inert_model: the inert model]
-
-       , inert_eqs :: DTyVarEnv EqualCtList
+  = IC { inert_eqs :: InertEqs
               -- See Note [inert_eqs: the inert equalities]
-              -- All Given/Wanted CTyEqCans; index is the LHS tyvar
+              -- All CTyEqCans; index is the LHS tyvar
+              -- Domain = skolems and untouchables; a touchable would be unified
 
        , inert_funeqs :: FunEqMap Ct
               -- All CFunEqCans; index is the whole family head type.
               -- All Nominal (that's an invarint of all CFunEqCans)
               -- LHS is fully rewritten (modulo eqCanRewrite constraints)
-              --     wrt inert_eqs/inert_model
-              -- We can get Derived ones from e.g.
-              --   (a) flattening derived equalities
-              --   (b) emitDerivedShadows
+              --     wrt inert_eqs
+              -- Can include all flavours, [G], [W], [WD], [D]
+              -- See Note [Type family equations]
 
        , inert_dicts :: DictMap Ct
               -- Dictionaries only
               -- All fully rewritten (modulo flavour constraints)
-              --     wrt inert_eqs/inert_model
+              --     wrt inert_eqs
 
        , inert_safehask :: DictMap Ct
               -- Failed dictionary resolution due to Safe Haskell overlapping
@@ -627,15 +625,11 @@ data InertCans   -- See Note [Detailed InertCans Invariants] for more
               -- When non-zero, keep trying to solved
        }
 
-type InertModel  = DTyVarEnv Ct
-     -- If a -> ct, then ct is a
-     --    nominal, Derived, canonical CTyEqCan for [D] (a ~N rhs)
-     -- The index of the TyVarEnv is the 'a'
-     -- All saturated info for Given, Wanted, Derived is here
-
+type InertEqs    = DTyVarEnv EqualCtList
+type EqualCtList = [Ct]  -- See Note [EqualCtList invariants]
 
 {- Note [Detailed InertCans Invariants]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 The InertCans represents a collection of constraints with the following properties:
 
   * All canonical
@@ -657,69 +651,58 @@ The InertCans represents a collection of constraints with the following properti
   * CTyEqCan equalities: see Note [Applying the inert substitution]
                          in TcFlatten
 
+Note [EqualCtList invariants]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+    * All are equalities
+    * All these equalities have the same LHS
+    * The list is never empty
+    * No element of the list can rewrite any other
+    * Derived before Wanted
+
+From the fourth invariant it follows that the list is
+   - A single [G], or
+   - Zero or one [D] or [WD], followd by any number of [W]
+
+The Wanteds can't rewrite anything which is why we put them last
+
 Note [Type family equations]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Type-family equations, of form (ev : F tys ~ ty), live in three places
+Type-family equations, CFunEqCans, of form (ev : F tys ~ ty),
+live in three places
 
   * The work-list, of course
 
+  * The inert_funeqs are un-solved but fully processed, and in
+    the InertCans. They can be [G], [W], [WD], or [D].
+
   * The inert_flat_cache.  This is used when flattening, to get maximal
-    sharing.  It contains lots of things that are still in the work-list.
+    sharing. Everthing in the inert_flat_cache is [G] or [WD]
+
+    It contains lots of things that are still in the work-list.
     E.g Suppose we have (w1: F (G a) ~ Int), and (w2: H (G a) ~ Int) in the
         work list.  Then we flatten w1, dumping (w3: G a ~ f1) in the work
         list.  Now if we flatten w2 before we get to w3, we still want to
         share that (G a).
-
     Because it contains work-list things, DO NOT use the flat cache to solve
     a top-level goal.  Eg in the above example we don't want to solve w3
     using w3 itself!
 
-  * The inert_funeqs are un-solved but fully processed and in the InertCans.
+The CFunEqCan Ownership Invariant:
 
-Note [inert_model: the inert model]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-* Part of the inert set is the “model”
+  * Each [G/W/WD] CFunEqCan has a distinct fsk or fmv
+    It "owns" that fsk/fmv, in the sense that:
+      - reducing a [W/WD] CFunEqCan fills in the fmv
+      - unflattening a [W/WD] CFunEqCan fills in the fmv
+      (in both cases unless an occurs-check would result)
 
-   * The “Model” is an non-idempotent but no-occurs-check
-     substitution, reflecting *all* *Nominal* equalities (a ~N ty)
-     that are not immediately soluble by unification.
+  * In contrast a [D] CFunEqCan does not "own" its fmv:
+      - reducing a [D] CFunEqCan does not fill in the fmv;
+        it just generates an equality
+      - unflattening ignores [D] CFunEqCans altogether
 
-   * All the constraints in the model are Derived CTyEqCans
-     That is if (a -> ty) is in the model, then
-     we have an inert constraint [D] a ~N ty.
-
-   * There are two sources of constraints in the model:
-
-     - Derived constraints arising from functional dependencies, or
-       decomposing injective arguments of type functions, and
-       suchlike.
-
-     - A Derived "shadow copy" for every Wanted (a ~N ty) in
-       inert_eqs.  (Originally included every Given too; but
-       see Note [Add derived shadows only for Wanteds])
-
-   * The model is not subject to "kicking-out". Reason: we make a Derived
-     shadow copy of any Wanted (a ~ ty), and that Derived copy will
-     be fully rewritten by the model before it is added
-
-   * The principal reason for maintaining the model is to generate
-     equalities that tell us how to unify a variable: that is, what
-     Mark Jones calls "improvement". The same idea is sometimes also
-     called "saturation"; find all the equalities that must hold in
-     any solution.
-
-   * Domain of the model = skolems + untouchables.
-     A touchable unification variable would have been unified first.
-
-   * The inert_eqs are all Given/Wanted.  The Derived ones are in the
-     inert_model only.
-
-   * However inert_dicts, inert_funeqs, inert_irreds
-     may well contain derived constraints.
 
 Note [inert_eqs: the inert equalities]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
 Definition [Can-rewrite relation]
 A "can-rewrite" relation between flavours, written f1 >= f2, is a
 binary relation with the following properties
@@ -937,26 +920,6 @@ inerts whenever the tyvar of a work item is "exposed", where exposed means
 not under some proper data-type constructor, like [] or Maybe. See
 isTyVarExposed in TcType. This is encoded in (K3b).
 
-Note [Stability of flattening]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-The inert_eqs and inert_model, *considered separately* are each stable;
-that is, substituting using them will terminate.  Considered *together*
-they are not.  E.g.
-
-  Add: [G] a~[b] to inert set with model  [D] b~[a]
-
-  We add [G] a~[b] to inert_eqs, and emit [D] a~[b]. At this point
-  the combination of inert_eqs and inert_model is not stable.
-
-  Then we canonicalise [D] a~[b] to [D] a~[[a]], and add that to
-  insolubles as an occurs check.
-
-* When canonicalizing, the flattener respects flavours. In particular,
-  when flattening a type variable 'a':
-    * Derived:      look up 'a' in the inert_model
-    * Given/Wanted: look up 'a' in the inert_eqs
-
-
 Note [Flavours with roles]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~
 The system described in Note [inert_eqs: the inert equalities]
@@ -979,126 +942,10 @@ T Int Bool. The reason is that T's first parameter has a nominal role, and
 thus rewriting a to Int in T a b is wrong. Indeed, this non-congruence of
 substitution means that the proof in Note [The inert equalities] may need
 to be revisited, but we don't think that the end conclusion is wrong.
-
-Note [Examples of how the inert_model helps completeness]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
------------ Example 2 (indexed-types/should_fail/T4093a)
-  Ambiguity check for f: (Foo e ~ Maybe e) => Foo e
-
-  We get [G] Foo e ~ Maybe e
-         [W] Foo e ~ Foo ee      -- ee is a unification variable
-         [W] Foo ee ~ Maybe ee
-
-  Flatten: [G] Foo e ~ fsk
-           [G] fsk ~ Maybe e   -- (A)
-
-           [W] Foo ee ~ fmv
-           [W] fmv ~ fsk       -- (B) From Foo e ~ Foo ee
-           [W] fmv ~ Maybe ee
-
-  --> rewrite (B) with (A)
-           [W] Foo ee ~ fmv
-           [W] fmv ~ Maybe e
-           [W] fmv ~ Maybe ee
-
-  But now awe appear to be stuck, since we don't rewrite Wanteds with
-  Wanteds. But inert_model to the rescue.  In the model we first added
-           fmv -> Maybe e
-  Then when adding [W] fmv -> Maybe ee to the inert set, we noticed
-  that the model can rewrite the constraint, and so emit [D] fmv ~ Maybe ee.
-  That canonicalises to
-           [D] Maybe e ~ Maybe ee
-  and that soon yields ee := e, and all is well
-
------------ Example 3 (typecheck/should_compile/Improvement.hs)
-    type instance F Int = Bool
-    instance (b~Int) => C Bool b
-
-    [W] w1 : C (F alpha) alpha, [W] w2 : F alpha ~ Bool
-
-  If we rewrote wanteds with wanteds, we could rewrite w1 to
-  C Bool alpha, use the instance to get alpha ~ Int, and solve
-  the whole thing.
-
-  And that is exactly what happens, in the *Derived* constraints.
-  In effect we get
-
-    [D] F alpha ~ fmv
-    [D] C fmv alpha
-    [D] fmv ~ Bool
-
-  and now we can rewrite (C fmv alpha) with (fmv ~ Bool), ane
-  we are off to the races.
-
------------ Example 4 (Trac #10009, a nasty example):
-
-    f :: (UnF (F b) ~ b) => F b -> ()
-
-    g :: forall a. (UnF (F a) ~ a) => a -> ()
-    g _ = f (undefined :: F a)
-
-  For g we get [G] UnF (F a) ~ a
-               [W] UnF (F beta) ~ beta
-               [W] F a ~ F beta
-  Flatten:
-      [G] g1: F a ~ fsk1         fsk1 := F a
-      [G] g2: UnF fsk1 ~ fsk2    fsk2 := UnF fsk1
-      [G] g3: fsk2 ~ a
-
-      [W] w1: F beta ~ fmv1
-      [W] w2: UnF fmv1 ~ fmv2
-      [W] w3: beta ~ fmv2
-      [W] w5: fmv1 ~ fsk1   -- From F a ~ F beta using flat-cache
-                            -- and re-orient to put meta-var on left
-
-  Unify beta := fmv2
-      [W] w1: F fmv2 ~ fmv1
-      [W] w2: UnF fmv1 ~ fmv2
-      [W] w5: fmv1 ~ fsk1
-
-  In the model, we have the shadow Deriveds of w1 and w2
-  (I name them for convenience even though they are anonymous)
-      [D] d1: F fmv2 ~ fmv1d
-      [D] d2: fmv1d ~ fmv1
-      [D] d3: UnF fmv1 ~ fmv2d
-      [D] d4: fmv2d ~ fmv2
-
-  Now we can rewrite d3 with w5, and match with g2, to get
-      fmv2d := fsk2
-      [D] d1: F fmv2 ~ fmv1d
-      [D] d2: fmv1d ~ fmv1
-      [D] d4: fmv2 ~ fsk2
-
-  Use g2 to rewrite fsk2 to a.
-      [D] d1: F fmv2 ~ fmv1d
-      [D] d2: fmv1d ~ fmv1
-      [D] d4: fmv2 ~ a
-
-  Use d4 to rewrite d1, rewrite with g3,
-  match with g1, to get
-      fmv1d := fsk1
-      [D] d2: fmv1 ~ fsk1
-      [D] d4: fmv2 ~ a
-
-  At this point we are stuck so we unflatten this set:
-  See Note [Orientation of equalities with fmvs] in TcFlatten
-      [W] w1: F fmv2 ~ fmv1
-      [W] w2: UnF fmv1 ~ fmv2
-      [W] w5: fmv1 ~ fsk1
-      [D] d4: fmv2 ~ a
-
-  Unflattening will discharge w1: fmv1 := F fmv2
-  It can't discharge w2, so it is kept.  But we can
-  unify fmv2 := fsk2, and that is "progress". Result
-      [W] w2: UnF (F a) ~ a
-      [W] w5: F a ~ fsk1
-
-  And now both of these are easily proved in the next iteration.  Phew!
 -}
 
 instance Outputable InertCans where
-  ppr (IC { inert_model = model, inert_eqs = eqs
+  ppr (IC { inert_eqs = eqs
           , inert_funeqs = funeqs, inert_dicts = dicts
           , inert_safehask = safehask, inert_irreds = irreds
           , inert_insols = insols, inert_count = count })
@@ -1116,218 +963,160 @@ instance Outputable InertCans where
         text "Irreds =" <+> pprCts irreds
       , ppUnless (isEmptyCts insols) $
         text "Insolubles =" <+> pprCts insols
-      , ppUnless (isEmptyDVarEnv model) $
-        text "Model =" <+> pprCts (foldDVarEnv consCts emptyCts model)
       , text "Unsolved goals =" <+> int count
       ]
 
 {- *********************************************************************
 *                                                                      *
-                  Adding an inert
+             Shadow constraints and improvement
 *                                                                      *
 ************************************************************************
 
-Note [Adding an inert canonical constraint the InertCans]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-* Adding any constraint c *other* than a CTyEqCan (TcSMonad.addInertCan):
-
-    * If c can be rewritten by model, emit the shadow constraint [D] c
-      as NonCanonical.   See Note [Emitting shadow constraints]
-
-    * Reason for non-canonical: a CFunEqCan has a unique fmv on the RHS,
-      so we must not duplicate it.
-
-* Adding a *nominal* CTyEqCan (a ~N ty) to the inert set (TcSMonad.addInertEq).
-
-    (A) Always (G/W/D) kick out constraints that can be rewritten
-        (respecting flavours) by the new constraint. This is done
-        by kickOutRewritable.
-
-    (B) Applies only to nominal equalities: a ~ ty.  Four cases:
-
-        [Representational]   [G/W/D] a ~R ty:
-          Just add it to inert_eqs
-
-        [Derived Nominal]  [D] a ~N ty:
-          1. Add (a~ty) to the model
-             NB: 'a' cannot be in fv(ty), because the constraint is canonical.
-
-          2. (DShadow) Do emitDerivedShadows
-               For every inert [W] constraint c, st
-                (a) (a~ty) can rewrite c (see Note [Emitting shadow constraints]),
-                    and
-                (b) the model cannot rewrite c
-               kick out a Derived *copy*, leaving the original unchanged.
-               Reason for (b) if the model can rewrite c, then we have already
-               generated a shadow copy
-               See Note [Add derived shadows only for Wanteds]
-
-       [Given/Wanted Nominal]  [G/W] a ~N ty:
-          1. Add it to inert_eqs
-          2. For [W], Emit [D] a~ty
-             Step (2) is needed to allow the current model to fully
-             rewrite [D] a~ty before adding it using the [Derived Nominal]
-             steps above.
-             See Note [Add derived shadows only for Wanteds]
-
-* Unifying a:=ty, is like adding [G] a~ty, but we can't make a [D]
-  a~ty, as in step (1) of the [G/W] case above.  So instead, do
-  kickOutAfterUnification:
-    - Kick out from the model any equality (b~ty2) that mentions 'a'
-      (i.e. a=b or a in ty2).  Example:
-            [G] a ~ [b],    model [D] b ~ [a]
-
-Note [Emitting shadow constraints]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
- * Given a new model element [D] a ~ ty, we want to emit shadow
-   [D] constraints for any inert constraints 'c' that can be
-   rewritten [D] a-> ty
+Note [The improvement story and derived shadows]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Because Wanteds cannot rewrite Wanteds (see Note [Wanteds do not
+rewrite Wanteds] in TcRnTypes), we may miss some opportunities for
+solving.  Here's a classic example (indexed-types/should_fail/T4093a)
 
- * And similarly given a new Given/Wanted 'c', we want to emit a
-   shadow 'c' if the model can rewrite [D] c
+    Ambiguity check for f: (Foo e ~ Maybe e) => Foo e
 
-See modelCanRewrite.
+    We get [G] Foo e ~ Maybe e
+           [W] Foo e ~ Foo ee      -- ee is a unification variable
+           [W] Foo ee ~ Maybe ee
 
-NB the use of rewritableTyVars. You might wonder whether, given the new
-constraint [D] fmv ~ ty and the inert [W] F alpha ~ fmv, do we want to
-emit a shadow constraint [D] F alpha ~ fmv?  No, we don't, because
-it'll literally be a duplicate (since we do not rewrite the RHS of a
-CFunEqCan) and hence immediately eliminated again.  Insetad we simply
-want to *kick-out* the [W] F alpha ~ fmv, so that it is reconsidered
-from a fudep point of view.  See Note [Kicking out CFunEqCan for
-fundeps]
+    Flatten: [G] Foo e ~ fsk
+             [G] fsk ~ Maybe e   -- (A)
 
-Note [Kicking out CFunEqCan for fundeps]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider:
-   New:    [D] fmv1 ~ fmv2
-   Inert:  [W] F alpha ~ fmv1
-           [W] F beta  ~ fmv2
+             [W] Foo ee ~ fmv
+             [W] fmv ~ fsk       -- (B) From Foo e ~ Foo ee
+             [W] fmv ~ Maybe ee
 
-The new (derived) equality certainly can't rewrite the inerts. But we
-*must* kick out the first one, to get:
+    --> rewrite (B) with (A)
+             [W] Foo ee ~ fmv
+             [W] fmv ~ Maybe e
+             [W] fmv ~ Maybe ee
 
-   New:   [W] F alpha ~ fmv1
-   Inert: [W] F beta ~ fmv2
-   Model: [D] fmv1 ~ fmv2
+    But now we appear to be stuck, since we don't rewrite Wanteds with
+    Wanteds.  This is silly because we can see that ee := e is the
+    only solution.
 
-and now improvement will discover [D] alpha ~ beta. This is important;
-eg in Trac #9587.
--}
+The basic plan is
+  * generate Derived constraints that shadow Wanted constraints
+  * allow Derived to rewrite Derived
+  * in order to cause some unifications to take place
+  * that in turn solve the original Wanteds
 
-addInertEq :: Ct -> TcS ()
--- This is a key function, because of the kick-out stuff
--- Precondition: item /is/ canonical
-addInertEq ct@(CTyEqCan { cc_tyvar = tv })
-  = do { traceTcS "addInertEq {" $
-         text "Adding new inert equality:" <+> ppr ct
-       ; ics <- getInertCans
+The ONLY reason for all these Derived equalities is to tell us how to
+unify a variable: that is, what Mark Jones calls "improvement".
 
-       ; let (kicked_out, ics1) = kickOutRewritable (ctFlavourRole ct) tv ics
-       ; ics2 <- add_inert_eq ics1 ct
+The same idea is sometimes also called "saturation"; find all the
+equalities that must hold in any solution.
 
-       ; setInertCans ics2
+Or, equivalently, you can think of the derived shadows as implementing
+the "model": an non-idempotent but no-occurs-check substitution,
+reflecting *all* *Nominal* equalities (a ~N ty) that are not
+immediately soluble by unification.
 
-       ; unless (isEmptyWorkList kicked_out) $
-         do { updWorkListTcS (appendWorkList kicked_out)
-            ; csTraceTcS $
-               hang (text "Kick out, tv =" <+> ppr tv)
-                  2 (vcat [ text "n-kicked =" <+> int (workListSize kicked_out)
-                          , ppr kicked_out ]) }
+More specifically, here's how it works (Oct 16):
 
-       ; traceTcS "addInertEq }" $ empty }
-addInertEq ct = pprPanic "addInertEq" (ppr ct)
-
-add_inert_eq :: InertCans -> Ct -> TcS InertCans
-add_inert_eq ics@(IC { inert_count = n
-                     , inert_eqs = old_eqs
-                     , inert_model = old_model })
-             ct@(CTyEqCan { cc_ev = ev, cc_eq_rel = eq_rel, cc_tyvar = tv
-                          , cc_rhs = _rhs })
-  | ReprEq <- eq_rel
-  = return new_ics
-
-  | isDerived ev
-  = do { emitDerivedShadows ics tv
-       ; return (ics { inert_model = extendDVarEnv old_model tv ct }) }
-
-  | otherwise   -- Given/Wanted Nominal equality [W] tv ~N ty
-  = do { emitNewDerived loc pred
-       ; return new_ics }
-  where
-    loc     = ctEvLoc ev
-    pred    = ctEvPred ev
-    new_ics = ics { inert_eqs   = addTyEq old_eqs tv ct
-                  , inert_count = bumpUnsolvedCount ev n }
-
-add_inert_eq _ ct = pprPanic "addInertEq" (ppr ct)
-
-emitDerivedShadows :: InertCans -> TcTyVar -> TcS ()
-emitDerivedShadows IC { inert_eqs      = tv_eqs
-                      , inert_dicts    = dicts
-                      , inert_safehask = safehask
-                      , inert_funeqs   = funeqs
-                      , inert_irreds   = irreds
-                      , inert_model    = model } new_tv
-  | null shadows
-  = return ()
-  | otherwise
-  = do { traceTcS "Emit derived shadows:" $
-         vcat [ text "tyvar =" <+> ppr new_tv
-              , text "shadows =" <+> vcat (map ppr shadows) ]
-       ; emitWork shadows }
-  where
-    shadows = foldDicts  get_ct dicts    $
-              foldDicts  get_ct safehask $
-              foldFunEqs get_ct funeqs   $
-              foldIrreds get_ct irreds   $
-              foldTyEqs  get_ct tv_eqs []
-      -- Ignore insolubles
-
-    get_ct ct cts | want_shadow ct = mkShadowCt ct : cts
-                  | otherwise      = cts
-
-    want_shadow ct
-      =  isWantedCt ct                     -- See Note [Add shadows only for Wanteds]
-      && (new_tv `elemVarSet` rw_tvs)      -- New tv can rewrite ct, yielding a
-                                           -- different ct
-      && not (modelCanRewrite model rw_tvs)-- We have not already created a
-                                           -- shadow
-      where
-        rw_tvs = rewritableTyCoVars ct
-
-mkShadowCt :: Ct -> Ct
--- Produce a Derived shadow constraint from the input
--- If it is a CFunEqCan, make it NonCanonical, to avoid
---   duplicating the flatten-skolems
--- Otherwise keep the canonical shape.  This just saves work, but
--- is sometimes important; see Note [Keep CDictCan shadows as CDictCan]
-mkShadowCt ct
-  | CFunEqCan {} <- ct = CNonCanonical { cc_ev = derived_ev }
-  | otherwise          = ct { cc_ev = derived_ev }
-  where
-    ev = ctEvidence ct
-    derived_ev = CtDerived { ctev_pred = ctEvPred ev
-                           , ctev_loc  = ctEvLoc ev }
+* Wanted constraints are born as [WD]; this behaves like a
+  [W] and a [D] paired together.
 
-{- Note [Add derived shadows only for Wanteds]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-We now only add shadows for Wanted constraints.  Why add derived
-shadows for Givens?  After all, Givens can rewrite Deriveds.  But
-Deriveds can't rewrite Givens.  So in principle, if we created a
-Derived shadow of a Given, it could be rewritten by other Deriveds,
-and that could, conceivably, lead to a useful unification.
+* When we are about to add a [WD] to the inert set, if it can
+  be rewritten by a [D] a ~ ty, then we split it into [W] and [D],
+  putting the latter into the work list (see maybeEmitShadow).
+
+In the example above, we get to the point where we are stuck:
+    [WD] Foo ee ~ fmv
+    [WD] fmv ~ Maybe e
+    [WD] fmv ~ Maybe ee
+
+But now when [WD] fmv ~ Maybe ee is about to be added, we'll
+split it into [W] and [D], since the inert [WD] fmv ~ Maybe e
+can rewrite it.  Then:
+    work item: [D] fmv ~ Maybe ee
+    inert:     [W] fmv ~ Maybe ee
+               [WD] fmv ~ Maybe e   -- (C)
+               [WD] Foo ee ~ fmv
+
+Now the work item is rewritten by (C) and we soon get ee := e.
+
+Additional notes:
+
+  * The derived shadow equalities live in inert_eqs, along with
+    the Givens and Wanteds; see Note [EqualCtList invariants].
+
+  * We make Derived shadows only for Wanteds, not Givens.  So we
+    have only [G], not [GD] and [G] plus splitting.  See
+    Note [Add derived shadows only for Wanteds]
+
+  * We also get Derived equalities from functional dependencies
+    and type-function injectivity; see calls to unifyDerived.
+
+  * This splitting business applies to CFunEqCans too; and then
+    we do apply type-function reductions to the [D] CFunEqCan.
+    See Note [Reduction for Derived CFunEqCans]
+
+  * It's worth having [WD] rather than just [W] and [D] because
+    * efficiency: silly to process the same thing twice
+    * inert_funeqs, inert_dicts is a finite map keyed by
+      the type; it's inconvenient for it to map to TWO constraints
+
+Note [Examples of how Derived shadows helps completeness]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Trac #10009, a very nasty example:
+
+    f :: (UnF (F b) ~ b) => F b -> ()
+
+    g :: forall a. (UnF (F a) ~ a) => a -> ()
+    g _ = f (undefined :: F a)
+
+  For g we get [G] UnF (F a) ~ a
+               [WD] UnF (F beta) ~ beta
+               [WD] F a ~ F beta
+  Flatten:
+      [G] g1: F a ~ fsk1         fsk1 := F a
+      [G] g2: UnF fsk1 ~ fsk2    fsk2 := UnF fsk1
+      [G] g3: fsk2 ~ a
+
+      [WD] w1: F beta ~ fmv1
+      [WD] w2: UnF fmv1 ~ fmv2
+      [WD] w3: fmv2 ~ beta
+      [WD] w4: fmv1 ~ fsk1   -- From F a ~ F beta using flat-cache
+                             -- and re-orient to put meta-var on left
+
+Rewrite w2 with w4: [D] d1: UnF fsk1 ~ fmv2
+React that with g2: [D] d2: fmv2 ~ fsk2
+React that with w3: [D] beta ~ fsk2
+            and g3: [D] beta ~ a -- Hooray beta := a
+And that is enough to solve everything
+
+Note [Add derived shadows only for Wanteds]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We only add shadows for Wanted constraints. That is, we have
+[WD] but not [GD]; and maybeEmitShaodw looks only at [WD]
+constraints.
+
+It does just possibly make sense ot add a derived shadow for a
+Given. If we created a Derived shadow of a Given, it could be
+rewritten by other Deriveds, and that could, conceivably, lead to a
+useful unification.
 
 But (a) I have been unable to come up with an example of this
-happening and (b) see Trac #12660 for how adding the derived shadows
-of a Given led to an infinite loop.  For (b) there may be other
-ways to solve the loop, but simply reraining from adding
-derived shadows of Givens is particularly simple.  And it's more
-efficient too!
+        happening
+    (b) see Trac #12660 for how adding the derived shadows
+        of a Given led to an infinite loop.
+    (c) It's unlikely that rewriting derived Givens will lead
+        to a unification becuse Givens don't mention touchable
+        unification variables
+
+For (b) there may be other ways to solve the loop, but simply
+reraining from adding derived shadows of Givens is particularly
+simple.  And it's more efficient too!
 
 Still, here's one possible reason for adding derived shadows
 for Givens.  Consider
-           work-item [G] a ~ [b], model has [D] b ~ a.
+           work-item [G] a ~ [b], inerts has [D] b ~ a.
 If we added the derived shadow (into the work list)
          [D] a ~ [b]
 When we process it, we'll rewrite to a ~ [a] and get an
@@ -1358,36 +1147,178 @@ generating superclasses repeatedly will fail.
 See Trac #11379 for a case of this.
 -}
 
-modelCanRewrite :: InertModel -> TcTyCoVarSet -> Bool
--- See Note [Emitting shadow constraints]
--- True if there is any intersection between dom(model) and tvs
-modelCanRewrite model tvs = not (disjointUdfmUfm model tvs)
-     -- The low-level use of disjointUFM might e surprising.
-     -- InertModel = TyVarEnv Ct, and we want to see if its domain
-     -- is disjoint from that of a TcTyCoVarSet.  So we drop down
-     -- to the underlying UniqFM.  A bit yukky, but efficient.
+maybeEmitShadow :: InertCans -> Ct -> TcS Ct
+-- See Note [The improvement story and derived shadows]
+maybeEmitShadow ics ct
+  | let ev = ctEvidence ct
+  , CtWanted { ctev_pred = pred, ctev_loc = loc
+             , ctev_nosh = WDeriv } <- ev
+  , shouldSplitWD (inert_eqs ics) ct
+  = do { traceTcS "Emit derived shadow" (ppr ct)
+       ; let derived_ev = CtDerived { ctev_pred = pred
+                                    , ctev_loc  = loc }
+             shadow_ct = ct { cc_ev = derived_ev }
+               -- Te shadow constraint keeps the canonical shape.
+               -- This just saves work, but is sometimes important;
+               -- see Note [Keep CDictCan shadows as CDictCan]
+       ; emitWork [shadow_ct]
+
+       ; let ev' = ev { ctev_nosh = WOnly }
+             ct' = ct { cc_ev = ev' }
+                 -- Record that it now has a shadow
+                 -- This is /the/ place we set the flag to WOnly
+       ; return ct' }
+
+  | otherwise
+  = return ct
+
+shouldSplitWD :: InertEqs -> Ct -> Bool
+-- Precondition: 'ct' is [WD], and is inert
+-- True <=> we should split ct ito [W] and [D] because
+--          the inert_eqs can make progress on the [D]
+
+shouldSplitWD inert_eqs (CFunEqCan { cc_tyargs = tys })
+  = inert_eqs `intersects_with` rewritableTyVarsOfTypes tys
+    -- We don't need to split if the tv is the RHS fsk
+
+shouldSplitWD inert_eqs ct
+  = inert_eqs `intersects_with` rewritableTyVarsOfType (ctPred ct)
+    -- Otherwise split if the tv is mentioned at all
+
+intersects_with :: InertEqs -> TcTyVarSet -> Bool
+intersects_with inert_eqs free_vars
+  = not (disjointUdfmUfm inert_eqs free_vars)
+      -- Test whether the inert equalities could rewrite
+      -- a derived version of this constraint
+      -- The low-level use of disjointUFM might seem surprising.
+      -- InertEqs = TyVarEnv EqualCtList, and we want to see if its domain
+      -- is disjoint from that of a TcTyCoVarSet.  So we drop down
+      -- to the underlying UniqFM.  A bit yukky, but efficient.
+
+
+{- *********************************************************************
+*                                                                      *
+                   Inert equalities
+*                                                                      *
+********************************************************************* -}
+
+addTyEq :: InertEqs -> TcTyVar -> Ct -> InertEqs
+addTyEq old_eqs tv ct
+  = extendDVarEnv_C add_eq old_eqs tv [ct]
+  where
+    add_eq old_eqs _
+      | isWantedCt ct
+      , (eq1 : eqs) <- old_eqs
+      = eq1 : ct : eqs
+      | otherwise
+      = ct : old_eqs
+
+foldTyEqs :: (Ct -> b -> b) -> InertEqs -> b -> b
+foldTyEqs k eqs z
+  = foldDVarEnv (\cts z -> foldr k z cts) z eqs
+
+findTyEqs :: InertCans -> TyVar -> EqualCtList
+findTyEqs icans tv = lookupDVarEnv (inert_eqs icans) tv `orElse` []
+
+delTyEq :: InertEqs -> TcTyVar -> TcType -> InertEqs
+delTyEq m tv t = modifyDVarEnv (filter (not . isThisOne)) m tv
+  where isThisOne (CTyEqCan { cc_rhs = t1 }) = eqType t t1
+        isThisOne _                          = False
+
+lookupInertTyVar :: InertEqs -> TcTyVar -> Maybe TcType
+lookupInertTyVar ieqs tv
+  = case lookupDVarEnv ieqs tv of
+      Just (CTyEqCan { cc_rhs = rhs, cc_eq_rel = NomEq } : _ ) -> Just rhs
+      _                                                        -> Nothing
+
+lookupFlattenTyVar :: InertEqs -> TcTyVar -> TcType
+-- See Note [lookupFlattenTyVar]
+lookupFlattenTyVar ieqs ftv
+  = lookupInertTyVar ieqs ftv `orElse` mkTyVarTy ftv
+
+{- Note [lookupFlattenTyVar]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Supppose we have an injective function F and
+  inert_funeqs:   F t1 ~ fsk1
+                  F t2 ~ fsk2
+  inert_eqs:      fsk1 ~ fsk2
+
+We never rewrite the RHS (cc_fsk) of a CFunEqCan.  But we /do/ want to
+get the [D] t1 ~ t2 from the injectiveness of F.  So we look up the
+cc_fsk of CFunEqCans in the inert_eqs when trying to find derived
+equalities arising from injectivity.
+-}
+
 
-rewritableTyCoVars :: Ct -> TcTyVarSet
--- The tyvars of a Ct that can be rewritten
-rewritableTyCoVars (CFunEqCan { cc_tyargs = tys }) = tyCoVarsOfTypes tys
-rewritableTyCoVars ct                              = tyCoVarsOfType (ctPred ct)
+{- *********************************************************************
+*                                                                      *
+                  Adding an inert
+*                                                                      *
+************************************************************************
+
+Note [Adding an equality to the InertCans]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When adding an equality to the inerts:
+
+* Split [WD] into [W] and [D] if the inerts can rewrite the latter;
+  done by maybeEmitShadow.
+
+* Kick out any constraints that can be rewritten by the thing
+  we are adding.  Done by kickOutRewritable.
+
+* Note that unifying a:=ty, is like adding [G] a~ty; just use
+  kickOutRewritable with Nominal, Given.  See kickOutAfterUnification.
+
+Note [Kicking out CFunEqCan for fundeps]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider:
+   New:    [D] fmv1 ~ fmv2
+   Inert:  [W] F alpha ~ fmv1
+           [W] F beta  ~ fmv2
+
+where F is injective. The new (derived) equality certainly can't
+rewrite the inerts. But we *must* kick out the first one, to get:
+
+   New:   [W] F alpha ~ fmv1
+   Inert: [W] F beta ~ fmv2
+          [D] fmv1 ~ fmv2
+
+and now improvement will discover [D] alpha ~ beta. This is important;
+eg in Trac #9587.
+
+So in kickOutRewritable we look at all the tyvars of the
+CFunEqCan, including the fsk.
+-}
+
+addInertEq :: Ct -> TcS ()
+-- This is a key function, because of the kick-out stuff
+-- Precondition: item /is/ canonical
+-- See Note [Adding an equality to the InertCans]
+addInertEq ct
+  = do { traceTcS "addInertEq {" $
+         text "Adding new inert equality:" <+> ppr ct
+       ; ics <- getInertCans
+
+       ; ct@(CTyEqCan { cc_tyvar = tv, cc_ev = ev }) <- maybeEmitShadow ics ct
+
+       ; (_, ics1) <- kickOutRewritable (ctEvFlavourRole ev) tv ics
+
+       ; let ics2 = ics1 { inert_eqs   = addTyEq (inert_eqs ics1) tv ct
+                         , inert_count = bumpUnsolvedCount ev (inert_count ics1) }
+       ; setInertCans ics2
+
+       ; traceTcS "addInertEq }" $ empty }
 
 --------------
 addInertCan :: Ct -> TcS ()  -- Constraints *other than* equalities
 addInertCan ct
   = do { traceTcS "insertInertCan {" $
-         text "Trying to insert new inert item:" <+> ppr ct
+         text "Trying to insert new non-eq inert item:" <+> ppr ct
 
        ; ics <- getInertCans
+       ; ct <- maybeEmitShadow ics ct
        ; setInertCans (add_item ics ct)
 
-       -- Emit shadow derived if necessary
-       -- See Note [Emitting shadow constraints]
-       ; let rw_tvs = rewritableTyCoVars ct
-       ; when (isWantedCt ct && modelCanRewrite (inert_model ics) rw_tvs)
-              -- See Note [Add shadows only for Wanteds]
-              (emitWork [mkShadowCt ct])
-
        ; traceTcS "addInertCan }" $ empty }
 
 add_item :: InertCans -> Ct -> InertCans
@@ -1419,21 +1350,39 @@ bumpUnsolvedCount ev n | isWanted ev = n+1
 
 
 -----------------------------------------
-kickOutRewritable :: CtFlavourRole  -- Flavour/role of the equality that
-                                    -- is being added to the inert set
-                  -> TcTyVar        -- The new equality is tv ~ ty
-                  -> InertCans
-                  -> (WorkList, InertCans)
+kickOutRewritable  :: CtFlavourRole  -- Flavour/role of the equality that
+                                      -- is being added to the inert set
+                    -> TcTyVar        -- The new equality is tv ~ ty
+                    -> InertCans
+                    -> TcS (Int, InertCans)
+kickOutRewritable new_fr new_tv ics
+  = do { let (kicked_out, ics') = kick_out_rewritable new_fr new_tv ics
+             n_kicked = workListSize kicked_out
+
+       ; unless (n_kicked == 0) $
+         do { updWorkListTcS (appendWorkList kicked_out)
+            ; csTraceTcS $
+              hang (text "Kick out, tv =" <+> ppr new_tv)
+                 2 (vcat [ text "n-kicked =" <+> int n_kicked
+                         , text "kicked_out =" <+> ppr kicked_out
+                         , text "Residual inerts =" <+> ppr ics' ]) }
+
+       ; return (n_kicked, ics') }
+
+kick_out_rewritable :: CtFlavourRole  -- Flavour/role of the equality that
+                                      -- is being added to the inert set
+                    -> TcTyVar        -- The new equality is tv ~ ty
+                    -> InertCans
+                    -> (WorkList, InertCans)
 -- See Note [kickOutRewritable]
-kickOutRewritable new_fr new_tv ics@(IC { inert_eqs      = tv_eqs
+kick_out_rewritable new_fr new_tv ics@(IC { inert_eqs      = tv_eqs
                                         , inert_dicts    = dictmap
                                         , inert_safehask = safehask
                                         , inert_funeqs   = funeqmap
                                         , inert_irreds   = irreds
                                         , inert_insols   = insols
-                                        , inert_count    = n
-                                        , inert_model    = model })
-  | not (new_fr `eqCanRewriteFR` new_fr)
+                                        , inert_count    = n })
+  | not (new_fr `eqMayRewriteFR` new_fr)
   = (emptyWorkList, ics)
         -- If new_fr can't rewrite itself, it can't rewrite
         -- anything else, so no need to kick out anything.
@@ -1449,9 +1398,7 @@ kickOutRewritable new_fr new_tv ics@(IC { inert_eqs      = tv_eqs
                        , inert_funeqs   = feqs_in
                        , inert_irreds   = irs_in
                        , inert_insols   = insols_in
-                       , inert_count    = n - workListWantedCount kicked_out
-                       , inert_model    = model }
-                     -- Leave the model unchanged
+                       , inert_count    = n - workListWantedCount kicked_out }
 
     kicked_out = WL { wl_eqs    = tv_eqs_out
                     , wl_funeqs = feqs_out
@@ -1461,31 +1408,32 @@ kickOutRewritable new_fr new_tv ics@(IC { inert_eqs      = tv_eqs
                     , wl_implics = emptyBag }
 
     (tv_eqs_out, tv_eqs_in) = foldDVarEnv kick_out_eqs ([], emptyDVarEnv) tv_eqs
-    (feqs_out,   feqs_in)   = partitionFunEqs  kick_out_fe funeqmap
+    (feqs_out,   feqs_in)   = partitionFunEqs  kick_out_ct funeqmap
+           -- See Note [Kicking out CFunEqCan for fundeps]
     (dicts_out,  dicts_in)  = partitionDicts   kick_out_ct dictmap
     (irs_out,    irs_in)    = partitionBag     kick_out_ct irreds
     (insols_out, insols_in) = partitionBag     kick_out_ct insols
       -- Kick out even insolubles; see Note [Kick out insolubles]
 
-    fr_can_rewrite :: CtEvidence -> Bool
-    fr_can_rewrite ev = new_fr `eqCanRewriteFR` (ctEvFlavourRole ev)
+    fr_may_rewrite :: CtFlavourRole -> Bool
+    fr_may_rewrite fs = new_fr `eqMayRewriteFR` fs
+        -- Can the new item rewrite the inert item?
 
     kick_out_ct :: Ct -> Bool
     -- Kick it out if the new CTyEqCan can rewrite the inert
     -- one. See Note [kickOutRewritable]
-    kick_out_ct ct
-      = fr_can_rewrite ev
-        && new_tv `elemVarSet` tyCoVarsOfType (ctEvPred ev)
-      where
-        ev = ctEvidence ct
+    -- Or if it has no shadow and the shadow
+    kick_out_ct ct = kick_out_ev (ctEvidence ct)
 
-    kick_out_fe :: Ct -> Bool
-    kick_out_fe (CFunEqCan { cc_ev = ev, cc_tyargs = tys, cc_fsk = fsk })
-      = new_tv == fsk  -- If RHS is new_tvs, kick out /regardless of flavour/
-                       -- See Note [Kicking out CFunEqCan for fundeps]
-        || (fr_can_rewrite ev
-            && new_tv `elemVarSet` tyCoVarsOfTypes tys)
-    kick_out_fe ct = pprPanic "kick_out_fe" (ppr ct)
+    kick_out_ev :: CtEvidence -> Bool
+    -- Kick it out if the new CTyEqCan can rewrite the inert
+    -- one. See Note [kickOutRewritable]
+    kick_out_ev ev = fr_may_rewrite (ctEvFlavourRole ev)
+                  && new_tv `elemVarSet` rewritableTyVarsOfType (ctEvPred ev)
+                  -- NB: this includes the fsk of a CFunEqCan.  It can't
+                  --     actually be rewritten, but we need to kick it out
+                  --     so we get to take advantage of injectivity
+                  -- See Note [Kicking out CFunEqCan for fundeps]
 
     kick_out_eqs :: EqualCtList -> ([Ct], DTyVarEnv EqualCtList)
                  -> ([Ct], DTyVarEnv EqualCtList)
@@ -1500,19 +1448,19 @@ kickOutRewritable new_fr new_tv ics@(IC { inert_eqs      = tv_eqs
     keep_eq (CTyEqCan { cc_tyvar = tv, cc_rhs = rhs_ty, cc_ev = ev
                       , cc_eq_rel = eq_rel })
       | tv == new_tv
-      = not (fr_can_rewrite ev)  -- (K1)
+      = not (fr_may_rewrite fs)  -- (K1)
 
       | otherwise
       = check_k2 && check_k3
       where
         fs = ctEvFlavourRole ev
-        check_k2 = not (fs  `eqCanRewriteFR` fs)                   -- (K2a)
-                ||     (fs  `eqCanRewriteFR` new_fr)               -- (K2b)
-                || not (new_fr `eqCanRewriteFR` fs)                -- (K2c)
+        check_k2 = not (fs  `eqMayRewriteFR` fs)                   -- (K2a)
+                ||     (fs  `eqMayRewriteFR` new_fr)               -- (K2b)
+                || not (fr_may_rewrite  fs)                        -- (K2c)
                 || not (new_tv `elemVarSet` tyCoVarsOfType rhs_ty) -- (K2d)
 
         check_k3
-          | new_fr `eqCanRewriteFR` fs
+          | fr_may_rewrite fs
           = case eq_rel of
               NomEq  -> not (rhs_ty `eqType` mkTyVarTy new_tv)
               ReprEq -> not (isTyVarExposed new_tv rhs_ty)
@@ -1525,42 +1473,13 @@ kickOutRewritable new_fr new_tv ics@(IC { inert_eqs      = tv_eqs
 kickOutAfterUnification :: TcTyVar -> TcS Int
 kickOutAfterUnification new_tv
   = do { ics <- getInertCans
-       ; let (kicked_out1, ics1) = kickOutModel new_tv ics
-             (kicked_out2, ics2) = kickOutRewritable (Given,NomEq)
-                                                     new_tv ics1
+       ; (n_kicked, ics2) <- kickOutRewritable (Given,NomEq)
+                                                 new_tv ics
                      -- Given because the tv := xi is given; NomEq because
                      -- only nominal equalities are solved by unification
-             kicked_out = appendWorkList kicked_out1 kicked_out2
-       ; setInertCans ics2
-       ; updWorkListTcS (appendWorkList kicked_out)
-
-       ; unless (isEmptyWorkList kicked_out) $
-         csTraceTcS $
-         hang (text "Kick out (unify), tv =" <+> ppr new_tv)
-            2 (vcat [ text "n-kicked =" <+> int (workListSize kicked_out)
-                    , text "kicked_out =" <+> ppr kicked_out
-                    , text "Residual inerts =" <+> ppr ics2 ])
-       ; return (workListSize kicked_out) }
-
-kickOutModel :: TcTyVar -> InertCans -> (WorkList, InertCans)
-kickOutModel new_tv ics@(IC { inert_model = model, inert_eqs = eqs })
-  = (foldDVarEnv add emptyWorkList der_out, ics { inert_model = new_model })
-  where
-    (der_out, new_model) = partitionDVarEnv kick_out_der model
-
-    kick_out_der :: Ct -> Bool
-    kick_out_der (CTyEqCan { cc_tyvar = tv, cc_rhs = rhs })
-      = new_tv == tv || new_tv `elemVarSet` tyCoVarsOfType rhs
-    kick_out_der _ = False
-
-    add :: Ct -> WorkList -> WorkList
-    -- Don't kick out a Derived if there is a Given or Wanted with
-    -- the same predicate.  The model is just a shadow copy, and the
-    -- Given/Wanted will serve the purpose.
-    add (CTyEqCan { cc_ev = ev, cc_tyvar = tv, cc_rhs = rhs }) wl
-      | not (isInInertEqs eqs tv rhs) = extendWorkListDerived (ctEvLoc ev) ev wl
-    add _ wl                          = wl
 
+       ; setInertCans ics2
+       ; return n_kicked }
 
 {- Note [kickOutRewritable]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1582,13 +1501,8 @@ new equality, to maintain the inert-set invariants.
     kick out constraints that mention type variables whose kinds
     contain this variable!
 
-  - We do not need to kick anything out from the model; we only
-    add [D] constraints to the model (in effect) and they are
-    fully rewritten by the model, so (K2b) holds
-
-  - A Derived equality can kick out [D] constraints in inert_dicts,
-    inert_irreds etc.  Nothing in inert_eqs because there are no
-    Derived constraints in inert_eqs (they are in the model)
+  - A Derived equality can kick out [D] constraints in inert_eqs,
+    inert_dicts, inert_irreds etc.
 
   - We don't kick out constraints from inert_solved_dicts, and
     inert_solved_funeqs optimistically. But when we lookup we have to
@@ -1657,35 +1571,6 @@ getInertCans = do { inerts <- getTcSInerts; return (inert_cans inerts) }
 setInertCans :: InertCans -> TcS ()
 setInertCans ics = updInertTcS $ \ inerts -> inerts { inert_cans = ics }
 
-takeGivenInsolubles :: TcS Cts
--- See Note [The inert set after solving Givens]
-takeGivenInsolubles
-  = updRetInertCans $ \ cans ->
-    ( inert_insols cans
-    , cans { inert_insols = emptyBag
-           , inert_funeqs = filterFunEqs isGivenCt (inert_funeqs cans) } )
-
-{- Note [The inert set after solving Givens]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-After solving the Givens we take two things out of the inert set
-
-  a) The insolubles; we return these to report inaccessible code
-     We return these separately.  We don't want to leave them in
-     the inert set, lest we confuse them with insolubles arising from
-     solving wanteds
-
-  b) Any Derived CFunEqCans.  Derived CTyEqCans are in the
-     inert_model and do no harm.  In contrast, Derived CFunEqCans
-     get mixed up with the Wanteds later and confuse the
-     post-solve-wanted unflattening (Trac #10507).
-     E.g.  From   [G] 1 <= m, [G] m <= n
-           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 out not to
-     yield an insoluble, and hence have now done their work.
--}
-
 updRetInertCans :: (InertCans -> (a, InertCans)) -> TcS a
 -- Modify the inert set with the supplied function
 updRetInertCans upd_fn
@@ -1723,8 +1608,8 @@ updInertIrreds upd_fn
 getInertEqs :: TcS (DTyVarEnv EqualCtList)
 getInertEqs = do { inert <- getInertCans; return (inert_eqs inert) }
 
-getInertModel :: TcS InertModel
-getInertModel = do { inert <- getInertCans; return (inert_model inert) }
+getInertInsols :: TcS Cts
+getInertInsols = do { inert <- getInertCans; return (inert_insols inert) }
 
 getInertGivens :: TcS [Ct]
 -- Returns the Given constraints in the inert set,
@@ -1776,42 +1661,42 @@ getUnsolvedInerts
            , inert_irreds = irreds
            , inert_dicts  = idicts
            , inert_insols = insols
-           , inert_model  = model } <- getInertCans
-      ; keep_derived <- keepSolvingDeriveds
+           } <- getInertCans
 
-      ; let der_tv_eqs       = foldDVarEnv (add_der_eq keep_derived tv_eqs)
-                                          emptyCts model
-            unsolved_tv_eqs  = foldTyEqs add_if_unsolved tv_eqs der_tv_eqs
-            unsolved_fun_eqs = foldFunEqs add_if_unsolved fun_eqs emptyCts
+      ; let unsolved_tv_eqs  = foldTyEqs add_if_unsolved tv_eqs emptyCts
+            unsolved_fun_eqs = foldFunEqs add_if_wanted fun_eqs emptyCts
             unsolved_irreds  = Bag.filterBag is_unsolved irreds
             unsolved_dicts   = foldDicts add_if_unsolved idicts emptyCts
-            others           = unsolved_irreds `unionBags` unsolved_dicts
+            unsolved_others  = unsolved_irreds `unionBags` unsolved_dicts
+            unsolved_insols  = filterBag is_unsolved insols
 
       ; implics <- getWorkListImplics
 
       ; traceTcS "getUnsolvedInerts" $
         vcat [ text " tv eqs =" <+> ppr unsolved_tv_eqs
              , text "fun eqs =" <+> ppr unsolved_fun_eqs
-             , text "insols =" <+> ppr insols
-             , text "others =" <+> ppr others
+             , text "insols =" <+> ppr unsolved_insols
+             , text "others =" <+> ppr unsolved_others
              , text "implics =" <+> ppr implics ]
 
-      ; return ( implics, unsolved_tv_eqs, unsolved_fun_eqs, insols, others) }
-              -- Keep even the given insolubles
-              -- so that we can report dead GADT pattern match branches
+      ; return ( implics, unsolved_tv_eqs, unsolved_fun_eqs
+               , unsolved_insols, unsolved_others) }
   where
-    add_der_eq keep_derived tv_eqs ct cts
-       -- See Note [Unsolved Derived equalities]
-       | CTyEqCan { cc_tyvar = tv, cc_rhs = rhs } <- ct
-       , isMetaTyVar tv || keep_derived
-       , not (isInInertEqs tv_eqs tv rhs) = ct `consBag` cts
-       | otherwise                        = cts
     add_if_unsolved :: Ct -> Cts -> Cts
     add_if_unsolved ct cts | is_unsolved ct = ct `consCts` cts
                            | otherwise      = cts
 
     is_unsolved ct = not (isGivenCt ct)   -- Wanted or Derived
 
+    -- For CFunEqCans we ignore the Derived ones, and keep
+    -- only the Wanteds for flattening.  The Derived ones
+    -- share a unification variable with the corresponding
+    -- Wanted, so we definitely don't want to to participate
+    -- in unflattening
+    -- See Note [Type family equations]
+    add_if_wanted ct cts | isWantedCt ct = ct `consCts` cts
+                         | otherwise     = cts
+
 isInInertEqs :: DTyVarEnv EqualCtList -> TcTyVar -> TcType -> Bool
 -- True if (a ~N ty) is in the inert set, in either Given or Wanted
 isInInertEqs eqs tv rhs
@@ -1827,22 +1712,23 @@ isInInertEqs eqs tv rhs
 
 getNoGivenEqs :: TcLevel          -- TcLevel of this implication
                -> [TcTyVar]       -- Skolems of this implication
-               -> Cts             -- Given insolubles from solveGivens
-               -> TcS Bool        -- True <=> definitely no residual given equalities
+               -> TcS ( Bool      -- True <=> definitely no residual given equalities
+                      , Cts )     -- Insoluble constraints arising from givens
 -- See Note [When does an implication have given equalities?]
-getNoGivenEqs tclvl skol_tvs given_insols
+getNoGivenEqs tclvl skol_tvs
   = do { inerts@(IC { inert_eqs = ieqs, inert_irreds = iirreds
-                    , inert_funeqs = funeqs })
-             <- getInertCans
+                    , inert_funeqs = funeqs
+                    , inert_insols = insols })
+              <- getInertCans
        ; let local_fsks = foldFunEqs add_fsk funeqs emptyVarSet
 
              has_given_eqs = foldrBag ((||) . ev_given_here . ctEvidence) False
-                                      (iirreds `unionBags` given_insols)
+                                      (iirreds `unionBags` insols)
                           || anyDVarEnv (eqs_given_here local_fsks) ieqs
 
        ; traceTcS "getNoGivenEqs" (vcat [ ppr has_given_eqs, ppr inerts
-                                        , ppr given_insols])
-       ; return (not has_given_eqs) }
+                                        , ppr insols])
+       ; return (not has_given_eqs, insols) }
   where
     eqs_given_here :: VarSet -> EqualCtList -> Bool
     eqs_given_here local_fsks [CTyEqCan { cc_tyvar = tv, cc_ev = ev }]
@@ -1921,17 +1807,10 @@ prohibitedSuperClassSolve from_loc solve_loc
 
 {- Note [Unsolved Derived equalities]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-In getUnsolvedInerts, we return a derived equality from the model
-for two possible reasons:
-
-  * Because it is a candidate for floating out of this implication.
-    We only float equalities with a meta-tyvar on the left, so we only
-    pull those out here.
-
-  * If we are only solving derived constraints (i.e. tcs_need_derived
-    is true; see Note [Solving for Derived constraints]), then we
-    those Derived constraints are effectively unsolved, and we need
-    them!
+In getUnsolvedInerts, we return a derived equality from the inert_eqs
+because it is a candidate for floating out of this implication.  We
+only float equalities with a meta-tyvar on the left, so we only pull
+those out here.
 
 Note [When does an implication have given equalities?]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -2029,7 +1908,7 @@ lookupFlatCache fam_tc tys
     lookup_inerts inert_funeqs
       | Just (CFunEqCan { cc_ev = ctev, cc_fsk = fsk, cc_tyargs = xis })
            <- findFunEq inert_funeqs fam_tc tys
-      , tys `eqTypes` xis   -- the lookup might find a near-match; see
+      , tys `eqTypes` xis   -- The lookup might find a near-match; see
                             -- Note [Use loose types in inert set]
       = Just (ctEvCoercion ctev, mkTyVarTy fsk, ctEvFlavour ctev)
       | otherwise = Nothing
@@ -2076,42 +1955,6 @@ foldIrreds k irreds z = foldrBag k z irreds
 
 {- *********************************************************************
 *                                                                      *
-                   Type equalities
-*                                                                      *
-********************************************************************* -}
-
-type EqualCtList = [Ct]
-
-{- Note [EqualCtList invariants]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-    * All are equalities
-    * All these equalities have the same LHS
-    * The list is never empty
-    * No element of the list can rewrite any other
-
- From the fourth invariant it follows that the list is
-   - A single Given, or
-   - Any number of Wanteds and/or Deriveds
--}
-
-addTyEq :: DTyVarEnv EqualCtList -> TcTyVar -> Ct -> DTyVarEnv EqualCtList
-addTyEq old_list tv it = extendDVarEnv_C (\old_eqs _new_eqs -> it : old_eqs)
-                                        old_list tv [it]
-
-foldTyEqs :: (Ct -> b -> b) -> DTyVarEnv EqualCtList -> b -> b
-foldTyEqs k eqs z
-  = foldDVarEnv (\cts z -> foldr k z cts) z eqs
-
-findTyEqs :: InertCans -> TyVar -> EqualCtList
-findTyEqs icans tv = lookupDVarEnv (inert_eqs icans) tv `orElse` []
-
-delTyEq :: DTyVarEnv EqualCtList -> TcTyVar -> TcType -> DTyVarEnv EqualCtList
-delTyEq m tv t = modifyDVarEnv (filter (not . isThisOne)) m tv
-  where isThisOne (CTyEqCan { cc_rhs = t1 }) = eqType t t1
-        isThisOne _                          = False
-
-{- *********************************************************************
-*                                                                      *
                    TcAppMap
 *                                                                      *
 ************************************************************************
@@ -2245,9 +2088,6 @@ type FunEqMap a = TcAppMap a  -- A map whose key is a (TyCon, [Type]) pair
 emptyFunEqs :: TcAppMap a
 emptyFunEqs = emptyTcAppMap
 
-sizeFunEqMap :: FunEqMap a -> Int
-sizeFunEqMap m = foldFunEqs (\ _ x -> x+1) m 0
-
 findFunEq :: FunEqMap a -> TyCon -> [Type] -> Maybe a
 findFunEq m tc tys = findTcApp m (getUnique tc) tys
 
@@ -2269,8 +2109,8 @@ foldFunEqs = foldTcAppMap
 -- mapFunEqs :: (a -> b) -> FunEqMap a -> FunEqMap b
 -- mapFunEqs = mapTcApp
 
-filterFunEqs :: (Ct -> Bool) -> FunEqMap Ct -> FunEqMap Ct
-filterFunEqs = filterTcAppMap
+-- filterFunEqs :: (Ct -> Bool) -> FunEqMap Ct -> FunEqMap Ct
+-- filterFunEqs = filterTcAppMap
 
 insertFunEq :: FunEqMap a -> TyCon -> [Type] -> a -> FunEqMap a
 insertFunEq m tc tys val = insertTcApp m (getUnique tc) tys val
@@ -2324,16 +2164,6 @@ All you can do is
 Filling in a dictionary evidence variable means to create a binding
 for it, so TcS carries a mutable location where the binding can be
 added.  This is initialised from the innermost implication constraint.
-
-Note [Solving for Derived constraints]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Sometimes we invoke the solver on a bunch of Derived constraints, not to
-generate any evidence, but just to cause unification side effects or to
-produce a simpler set of constraints.  If that is what we are doing, we
-should do two things differently:
-  a) Don't stop when you've solved all the Wanteds; instead keep going
-     if there are any Deriveds in the work queue.
-  b) In getInertUnsolved, include Derived ones
 -}
 
 data TcSEnv
@@ -2350,11 +2180,7 @@ data TcSEnv
 
       -- The main work-list and the flattening worklist
       -- See Note [Work list priorities] and
-      tcs_worklist  :: IORef WorkList, -- Current worklist
-
-      tcs_need_deriveds :: Bool
-        -- Keep solving, even if all the unsolved constraints are Derived
-        -- See Note [Solving for Derived constraints]
+      tcs_worklist  :: IORef WorkList -- Current worklist
     }
 
 ---------------
@@ -2450,7 +2276,7 @@ runTcS :: TcS a                -- What to run
        -> TcM (a, EvBindMap)
 runTcS tcs
   = do { ev_binds_var <- TcM.newTcEvBinds
-       ; res <- runTcSWithEvBinds False ev_binds_var tcs
+       ; res <- runTcSWithEvBinds ev_binds_var tcs
        ; ev_binds <- TcM.getTcEvBindsMap ev_binds_var
        ; return (res, ev_binds) }
 
@@ -2460,19 +2286,18 @@ runTcS tcs
 runTcSDeriveds :: TcS a -> TcM a
 runTcSDeriveds tcs
   = do { ev_binds_var <- TcM.newTcEvBinds
-       ; runTcSWithEvBinds True ev_binds_var tcs }
+       ; runTcSWithEvBinds ev_binds_var tcs }
 
 -- | This can deal only with equality constraints.
 runTcSEqualities :: TcS a -> TcM a
 runTcSEqualities thing_inside
   = do { ev_binds_var <- TcM.newTcEvBinds
-       ; runTcSWithEvBinds False ev_binds_var thing_inside }
+       ; runTcSWithEvBinds ev_binds_var thing_inside }
 
-runTcSWithEvBinds :: Bool  -- ^ keep running even if only Deriveds are left?
-                  -> EvBindsVar
+runTcSWithEvBinds :: EvBindsVar
                   -> TcS a
                   -> TcM a
-runTcSWithEvBinds solve_deriveds ev_binds_var tcs
+runTcSWithEvBinds ev_binds_var tcs
   = do { unified_var <- TcM.newTcRef 0
        ; step_count <- TcM.newTcRef 0
        ; inert_var <- TcM.newTcRef emptyInert
@@ -2481,8 +2306,7 @@ runTcSWithEvBinds solve_deriveds ev_binds_var tcs
                           , tcs_unified       = unified_var
                           , tcs_count         = step_count
                           , tcs_inerts        = inert_var
-                          , tcs_worklist      = wl_var
-                          , tcs_need_deriveds = solve_deriveds }
+                          , tcs_worklist      = wl_var }
 
              -- Run the computation
        ; res <- unTcS tcs env
@@ -2536,7 +2360,6 @@ nestImplicTcS ref inner_tclvl (TcS thing_inside)
   = TcS $ \ TcSEnv { tcs_unified       = unified_var
                    , tcs_inerts        = old_inert_var
                    , tcs_count         = count
-                   , tcs_need_deriveds = solve_deriveds
                    } ->
     do { inerts <- TcM.readTcRef old_inert_var
        ; let nest_inert = inerts { inert_flat_cache = emptyExactFunEqs }
@@ -2547,8 +2370,7 @@ nestImplicTcS ref inner_tclvl (TcS thing_inside)
                                , tcs_unified       = unified_var
                                , tcs_count         = count
                                , tcs_inerts        = new_inert_var
-                               , tcs_worklist      = new_wl_var
-                               , tcs_need_deriveds = solve_deriveds }
+                               , tcs_worklist      = new_wl_var }
        ; res <- TcM.setTcLevel inner_tclvl $
                 thing_inside nest_env
 
@@ -2642,10 +2464,6 @@ updWorkListTcS f
        ; let new_work = f wl_curr
        ; wrapTcS (TcM.writeTcRef wl_var new_work) }
 
--- | Should we keep solving even only deriveds are left?
-keepSolvingDeriveds :: TcS Bool
-keepSolvingDeriveds = TcS (return . tcs_need_deriveds)
-
 emitWorkNC :: [CtEvidence] -> TcS ()
 emitWorkNC evs
   | null evs
@@ -2869,35 +2687,44 @@ which will result in two Deriveds to end up in the insoluble set:
 -- Flatten skolems
 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 newFlattenSkolem :: CtFlavour -> CtLoc
-                 -> TcType         -- F xis
-                 -> TcS (CtEvidence, Coercion, TcTyVar)    -- [W] x:: F xis ~ fsk
-newFlattenSkolem Given loc fam_ty
-  = do { fsk <- newFsk fam_ty
-       ; let co = mkNomReflCo fam_ty
-       ; ev  <- newGivenEvVar loc (mkPrimEqPred fam_ty (mkTyVarTy fsk),
-                                   EvCoercion co)
-       ; return (ev, co, fsk) }
-
-newFlattenSkolem Wanted loc fam_ty
-  = do { fmv <- newFmv fam_ty
-       ; (ev, hole_co) <- newWantedEq loc Nominal fam_ty (mkTyVarTy fmv)
-       ; return (ev, hole_co, fmv) }
-
-newFlattenSkolem Derived loc fam_ty
-  = do { fmv <- newFmv fam_ty
-       ; ev <- newDerivedNC loc (mkPrimEqPred fam_ty (mkTyVarTy fmv))
-       ; return (ev, pprPanic "newFlattenSkolem [D]" (ppr fam_ty), fmv) }
-
-newFsk, newFmv :: TcType -> TcS TcTyVar
-newFsk fam_ty = wrapTcS (TcM.newFskTyVar fam_ty)
-newFmv fam_ty = wrapTcS (TcM.newFmvTyVar fam_ty)
+                 -> TyCon -> [TcType]                    -- F xis
+                 -> TcS (CtEvidence, Coercion, TcTyVar)  -- [G/WD] x:: F xis ~ fsk
+newFlattenSkolem flav loc tc xis
+  = do { stuff@(ev, co, fsk) <- new_skolem
+       ; let fsk_ty = mkTyVarTy fsk
+       ; extendFlatCache tc xis (co, fsk_ty, ctEvFlavour ev)
+       ; return stuff }
+  where
+    fam_ty = mkTyConApp tc xis
+
+    new_skolem
+      | Given <- flav
+      = do { fsk <- wrapTcS (TcM.newFskTyVar fam_ty)
+           ; let co = mkNomReflCo fam_ty
+           ; ev  <- newGivenEvVar loc (mkPrimEqPred fam_ty (mkTyVarTy fsk),
+                                       EvCoercion co)
+           ; return (ev, co, fsk) }
+
+      | otherwise  -- Generate a [WD] for both Wanted and Derived
+                   -- See Note [No Derived CFunEqCans]
+      = do { fmv <- wrapTcS (TcM.newFmvTyVar fam_ty)
+           ; (ev, hole_co) <- newWantedEq loc Nominal fam_ty (mkTyVarTy fmv)
+           ; return (ev, hole_co, fmv) }
 
 extendFlatCache :: TyCon -> [Type] -> (TcCoercion, TcType, CtFlavour) -> TcS ()
-extendFlatCache tc xi_args stuff
+extendFlatCache tc xi_args stuff@(_, ty, fl)
+  | isGivenOrWDeriv fl  -- Maintain the invariant that inert_flat_cache
+                        -- only has [G] and [WD] CFunEqCans
   = do { dflags <- getDynFlags
        ; when (gopt Opt_FlatCache dflags) $
-         updInertTcS $ \ is@(IS { inert_flat_cache = fc }) ->
-            is { inert_flat_cache = insertExactFunEq fc tc xi_args stuff } }
+    do { traceTcS "extendFlatCache" (vcat [ ppr tc <+> ppr xi_args
+                                          , ppr fl, ppr ty ])
+            -- 'co' can be bottom, in the case of derived items
+       ; updInertTcS $ \ is@(IS { inert_flat_cache = fc }) ->
+            is { inert_flat_cache = insertExactFunEq fc tc xi_args stuff } } }
+
+  | otherwise
+  = return ()
 
 -- Instantiations
 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -3039,6 +2866,7 @@ newWantedEq loc role ty1 ty2
   = do { hole <- wrapTcS $ TcM.newCoercionHole
        ; traceTcS "Emitting new coercion hole" (ppr hole <+> dcolon <+> ppr pty)
        ; return ( CtWanted { ctev_pred = pty, ctev_dest = HoleDest hole
+                           , ctev_nosh = WDeriv
                            , ctev_loc = loc}
                 , mkHoleCo hole role ty1 ty2 ) }
   where
@@ -3048,11 +2876,11 @@ newWantedEq loc role ty1 ty2
 newWantedEvVarNC :: CtLoc -> TcPredType -> TcS CtEvidence
 -- Don't look up in the solved/inerts; we know it's not there
 newWantedEvVarNC loc pty
-  = do { -- checkReductionDepth loc pty
-       ; new_ev <- newEvVar pty
+  = do { new_ev <- newEvVar pty
        ; traceTcS "Emitting new wanted" (ppr new_ev <+> dcolon <+> ppr pty $$
                                          pprCtLoc loc)
        ; return (CtWanted { ctev_pred = pty, ctev_dest = EvVarDest new_ev
+                          , ctev_nosh = WDeriv
                           , ctev_loc = loc })}
 
 newWantedEvVar :: CtLoc -> TcPredType -> TcS MaybeNew
index c23b317..a9548f2 100644 (file)
@@ -413,8 +413,7 @@ simplifyAmbiguityCheck ty wanteds
        -- inaccessible code
        ; allow_ambiguous <- xoptM LangExt.AllowAmbiguousTypes
        ; traceTc "reportUnsolved(ambig) {" empty
-       ; tc_lvl <- TcM.getTcLevel
-       ; unless (allow_ambiguous && not (insolubleWC tc_lvl final_wc))
+       ; unless (allow_ambiguous && not (insolubleWC final_wc))
                 (discardResult (reportUnsolved final_wc))
        ; traceTc "reportUnsolved(ambig) }" empty
 
@@ -431,11 +430,8 @@ simplifyDefault :: ThetaType    -- Wanted; has no type variables in it
                 -> TcM ()       -- Succeeds if the constraint is soluble
 simplifyDefault theta
   = do { traceTc "simplifyDefault" empty
-       ; loc <- getCtLocM DefaultOrigin Nothing
-       ; let wanted = [ CtDerived { ctev_pred = pred
-                                  , ctev_loc  = loc }
-                      | pred <- theta ]
-       ; unsolved <- runTcSDeriveds (solveWanteds (mkSimpleWC wanted))
+       ; wanteds  <- newWanteds DefaultOrigin theta
+       ; unsolved <- runTcSDeriveds (solveWantedsAndDrop (mkSimpleWC wanteds))
        ; traceTc "reportUnsolved {" empty
        ; reportAllUnsolved unsolved
        ; traceTc "reportUnsolved }" empty
@@ -451,7 +447,8 @@ tcCheckSatisfiability given_ids
              do { traceTcS "checkSatisfiability {" (ppr given_ids)
                 ; let given_cts = mkGivens given_loc (bagToList given_ids)
                      -- See Note [Superclasses and satisfiability]
-                ; insols <- solveSimpleGivens given_cts
+                ; solveSimpleGivens given_cts
+                ; insols <- getInertInsols
                 ; insols <- try_harder insols
                 ; traceTcS "checkSatisfiability }" (ppr insols)
                 ; return (isEmptyBag insols) }
@@ -467,7 +464,8 @@ tcCheckSatisfiability given_ids
       | otherwise
       = do { pending_given <- getPendingScDicts
            ; new_given <- makeSuperClasses pending_given
-           ; solveSimpleGivens new_given }
+           ; solveSimpleGivens new_given
+           ; getInertInsols }
 
 {- Note [Superclasses and satisfiability]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -573,7 +571,7 @@ simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds
        ; psig_theta_vars <- mapM TcM.newEvVar psig_theta
        ; wanted_transformed_incl_derivs
             <- setTcLevel rhs_tclvl $
-               runTcSWithEvBinds False ev_binds_var $
+               runTcSWithEvBinds ev_binds_var $
                do { let loc = mkGivenLoc rhs_tclvl UnkSkol tc_lcl_env
                         psig_givens = mkGivens loc psig_theta_vars
                   ; _ <- solveSimpleGivens psig_givens
@@ -590,7 +588,7 @@ simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds
 
        ; let wanted_transformed = dropDerivedWC wanted_transformed_incl_derivs
        ; quant_pred_candidates   -- Fully zonked
-           <- if insolubleWC rhs_tclvl wanted_transformed_incl_derivs
+           <- if insolubleWC wanted_transformed_incl_derivs
               then return []   -- See Note [Quantification with errors]
                                -- NB: must include derived errors in this test,
                                --     hence "incl_derivs"
@@ -615,15 +613,11 @@ simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds
                       ; mapM_ def_tyvar meta_tvs
                       ; mapM_ (promoteTyVar rhs_tclvl) meta_tvs
 
+                      ; clone_wanteds <- mapM cloneWanted (bagToList quant_cand)
                       ; WC { wc_simple = simples }
                            <- setTcLevel rhs_tclvl $
-                              runTcSDeriveds       $
-                              solveSimpleWanteds   $
-                              mapBag toDerivedCt quant_cand
-                                -- NB: we don't want evidence,
-                                -- so use Derived constraints
-
-                      ; simples <- TcM.zonkSimples simples
+                              simplifyWantedsTcM clone_wanteds
+                              -- Discard evidence; result is zonked
 
                       ; return [ ctEvPred ev | ct <- bagToList simples
                                              , let ev = ctEvidence ct ] }
@@ -1074,7 +1068,7 @@ simplifyWantedsTcM :: [CtEvidence] -> TcM WantedConstraints
 -- Postcondition: fully zonked and unflattened constraints
 simplifyWantedsTcM wanted
   = do { traceTc "simplifyWantedsTcM {" (ppr wanted)
-       ; (result, _) <- runTcS (solveWantedsAndDrop $ mkSimpleWC wanted)
+       ; (result, _) <- runTcS (solveWantedsAndDrop (mkSimpleWC wanted))
        ; result <- TcM.zonkWC result
        ; traceTc "simplifyWantedsTcM }" (ppr result)
        ; return result }
@@ -1093,20 +1087,19 @@ solveWanteds :: WantedConstraints -> TcS WantedConstraints
 solveWanteds wc@(WC { wc_simple = simples, wc_insol = insols, wc_impl = implics })
   = do { traceTcS "solveWanteds {" (ppr wc)
 
-         -- Try the simple bit, including insolubles. Solving insolubles a
-         -- second time round is a bit of a waste; but the code is simple
-         -- and the program is wrong anyway, and we don't run the danger
-         -- of adding Derived insolubles twice; see
-         -- TcSMonad Note [Do not add duplicate derived insolubles]
        ; wc1 <- solveSimpleWanteds simples
-       ; (no_new_scs, wc1) <- expandSuperClasses wc1
        ; let WC { wc_simple = simples1, wc_insol = insols1, wc_impl = implics1 } = wc1
 
        ; (floated_eqs, implics2) <- solveNestedImplications (implics `unionBags` implics1)
+       ; (no_new_scs, simples2)  <- expandSuperClasses simples1
+
+       ; traceTcS "solveWanteds middle" $ vcat [ text "simples1 =" <+> ppr simples1
+                                               , text "simples2 =" <+> ppr simples2 ]
 
        ; dflags <- getDynFlags
-       ; final_wc <- simpl_loop 0 (solverIterations dflags) floated_eqs no_new_scs
-                                (WC { wc_simple = simples1, wc_impl = implics2
+       ; final_wc <- simpl_loop 0 (solverIterations dflags) floated_eqs
+                                no_new_scs
+                                (WC { wc_simple = simples2, wc_impl = implics2
                                     , wc_insol  = insols `unionBags` insols1 })
 
        ; bb <- TcS.getTcEvBindsMap
@@ -1119,9 +1112,9 @@ solveWanteds wc@(WC { wc_simple = simples, wc_insol = insols, wc_impl = implics
 simpl_loop :: Int -> IntWithInf -> Cts -> Bool
            -> WantedConstraints
            -> TcS WantedConstraints
-simpl_loop n limit floated_eqs no_new_scs
+simpl_loop n limit floated_eqs no_new_deriveds
            wc@(WC { wc_simple = simples, wc_insol = insols, wc_impl = implics })
-  | isEmptyBag floated_eqs && no_new_scs
+  | isEmptyBag floated_eqs && no_new_deriveds
   = return wc  -- Done!
 
   | n `intGtLimit` limit
@@ -1134,8 +1127,8 @@ simpl_loop n limit floated_eqs no_new_scs
                 2 (vcat [ text "Unsolved:" <+> ppr wc
                         , ppUnless (isEmptyBag floated_eqs) $
                           text "Floated equalities:" <+> ppr floated_eqs
-                        , ppUnless no_new_scs $
-                          text "New superclasses found"
+                        , ppUnless no_new_deriveds $
+                          text "New deriveds found"
                         , text "Set limit with -fconstraint-solver-iterations=n; n=0 for no limit"
                   ]))
        ; return wc }
@@ -1144,7 +1137,7 @@ simpl_loop n limit floated_eqs no_new_scs
   = do { let n_floated = lengthBag floated_eqs
        ; csTraceTcS $
          text "simpl_loop iteration=" <> int n
-         <+> (parens $ hsep [ text "no new scs =" <+> ppr no_new_scs <> comma
+         <+> (parens $ hsep [ text "no new deriveds =" <+> ppr no_new_deriveds <> comma
                             , int n_floated <+> text "floated eqs" <> comma
                             , int (lengthBag simples) <+> text "simples to solve" ])
 
@@ -1155,8 +1148,8 @@ simpl_loop n limit floated_eqs no_new_scs
                                -- NB: the floated_eqs may include /derived/ equalities
                                --     arising from fundeps inside an implication
 
-       ; (no_new_scs, wc1) <- expandSuperClasses wc1
        ; let WC { wc_simple = simples1, wc_insol = insols1, wc_impl = implics1 } = wc1
+       ; (no_new_scs, simples2) <- expandSuperClasses simples1
 
        -- We have already tried to solve the nested implications once
        -- Try again only if we have unified some meta-variables
@@ -1167,36 +1160,36 @@ simpl_loop n limit floated_eqs no_new_scs
                                      else solveNestedImplications (implics `unionBags` implics1)
 
        ; simpl_loop (n+1) limit floated_eqs2 no_new_scs
-                    (WC { wc_simple = simples1, wc_impl = implics2
+                    (WC { wc_simple = simples2, wc_impl = implics2
                         , wc_insol  = insols `unionBags` insols1 }) }
 
-expandSuperClasses :: WantedConstraints -> TcS (Bool, WantedConstraints)
--- If there are any unsolved wanteds, expand one step of superclasses for
--- unsolved wanteds or givens
+expandSuperClasses :: Cts -> TcS (Bool, Cts)
+-- If there are any unsolved wanteds, expand one step of
+-- superclasses for deriveds
+-- Returned Bool is True <=> no new superclass constraints added
 -- See Note [The superclass story] in TcCanonical
-expandSuperClasses wc@(WC { wc_simple = unsolved, wc_insol = insols })
+expandSuperClasses unsolved
   | not (anyBag superClassesMightHelp unsolved)
-  = return (True, wc)
+  = return (True, unsolved)
   | otherwise
   = do { traceTcS "expandSuperClasses {" empty
        ; let (pending_wanted, unsolved') = mapAccumBagL get [] unsolved
-             get acc ct = case isPendingScDict ct of
-                            Just ct' -> (ct':acc, ct')
-                            Nothing  -> (acc,     ct)
+             get acc ct | Just ct' <- isPendingScDict ct
+                        = (ct':acc, ct')
+                        | otherwise
+                        = (acc,     ct)
        ; pending_given <- getPendingScDicts
        ; if null pending_given && null pending_wanted
          then do { traceTcS "End expandSuperClasses no-op }" empty
-                 ; return (True, wc) }
+                 ; return (True, unsolved) }
          else
     do { new_given  <- makeSuperClasses pending_given
-       ; new_insols <- solveSimpleGivens new_given
+       ; solveSimpleGivens new_given
        ; new_wanted <- makeSuperClasses pending_wanted
        ; traceTcS "End expandSuperClasses }"
                   (vcat [ text "Given:" <+> ppr pending_given
-                        , text "Insols from given:" <+> ppr new_insols
                         , text "Wanted:" <+> ppr new_wanted ])
-       ; return (False, wc { wc_simple = unsolved' `unionBags` listToBag new_wanted
-                           , wc_insol = insols `unionBags` new_insols }) } }
+       ; return (False, unsolved' `unionBags` listToBag new_wanted) } }
 
 solveNestedImplications :: Bag Implication
                         -> TcS (Cts, Bag Implication)
@@ -1244,17 +1237,17 @@ solveImplication imp@(Implic { ic_tclvl  = tclvl
 
          -- Solve the nested constraints
        ; (no_given_eqs, given_insols, residual_wanted)
-             <- nestImplicTcS ev_binds_var tclvl $
+            <- nestImplicTcS ev_binds_var tclvl $
                do { let loc    = mkGivenLoc tclvl info env
                         givens = mkGivens loc given_ids
-                  ; given_insols <- solveSimpleGivens givens
+                  ; solveSimpleGivens givens
 
                   ; residual_wanted <- solveWanteds wanteds
                         -- solveWanteds, *not* solveWantedsAndDrop, because
                         -- we want to retain derived equalities so we can float
                         -- them out in floatEqualities
 
-                  ; no_eqs <- getNoGivenEqs tclvl skols given_insols
+                  ; (no_eqs, given_insols) <- getNoGivenEqs tclvl skols
                         -- Call getNoGivenEqs /after/ solveWanteds, because
                         -- solveWanteds can augment the givens, via expandSuperClasses,
                         -- to reveal given superclass equalities
@@ -1289,7 +1282,6 @@ setImplicationStatus :: Implication -> TcS (Maybe Implication)
 -- Return Nothing if we can discard the implication altogether
 setImplicationStatus implic@(Implic { ic_binds  = ev_binds_var
                                     , ic_info   = info
-                                    , ic_tclvl  = tc_lvl
                                     , ic_wanted = wc
                                     , ic_given  = givens })
  | some_insoluble
@@ -1299,10 +1291,13 @@ setImplicationStatus implic@(Implic { ic_binds  = ev_binds_var
                            , wc_insol  = pruned_insols } }
 
  | some_unsolved
- = return $ Just $
+ = do { traceTcS "setImplicationStatus" $
+        vcat [ppr givens $$ ppr simples $$ ppr insols $$ ppr mb_implic_needs]
+      ; return $ Just $
    implic { ic_status = IC_Unsolved
           , ic_wanted = wc { wc_simple = pruned_simples
                            , wc_insol  = pruned_insols } }
+      }
 
  | otherwise  -- Everything is solved; look at the implications
               -- See Note [Tracking redundant constraints]
@@ -1342,7 +1337,7 @@ setImplicationStatus implic@(Implic { ic_binds  = ev_binds_var
  where
    WC { wc_simple = simples, wc_impl = implics, wc_insol = insols } = wc
 
-   some_insoluble = insolubleWC tc_lvl wc
+   some_insoluble = insolubleWC wc
    some_unsolved = not (isEmptyBag simples && isEmptyBag insols)
                  || isNothing mb_implic_needs
 
@@ -1510,23 +1505,13 @@ works:
 
 ----- Shortcomings
 
-After I introduced -Wredundant-constraints there was extensive discussion
-about cases where it reported a redundant constraint but the programmer
-really wanted it.  See
+Consider (see Trac #9939)
+    f2 :: (Eq a, Ord a) => a -> a -> Bool
+    -- Ord a redundant, but Eq a is reported
+    f2 x y = (x == y)
 
-  * #11370 (removed it from -Wdefault)
-  * #10635 (removed it from -Wall as well)
-  * #12142
-  * #11474, #10100 (class not used, but its fundeps are)
-  * #11099 (redundant, but still desired)
-  * #10183 (constraint necessary to exclude omitted case)
-
-  * #9939:     f2 :: (Eq a, Ord a) => a -> a -> Bool
-               -- Ord a redundant, but Eq a is reported
-              f2 x y = (x == y)
-
-    We report (Eq a) as redundant, whereas actually (Ord a) is.
-    But it's really not easy to detect that!
+We report (Eq a) as redundant, whereas actually (Ord a) is.  But it's
+really not easy to detect that!
 
 
 Note [Cutting off simpl_loop]
@@ -1770,29 +1755,6 @@ beta! Concrete example is in indexed_types/should_fail/ExtraTcsUntch.hs:
         in (g1 '3', g2 undefined)
 
 
-Note [Solving Family Equations]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-After we are done with simplification we may be left with constraints of the form:
-     [Wanted] F xis ~ beta
-If 'beta' is a touchable unification variable not already bound in the TyBinds
-then we'd like to create a binding for it, effectively "defaulting" it to be 'F xis'.
-
-When is it ok to do so?
-    1) 'beta' must not already be defaulted to something. Example:
-
-           [Wanted] F Int  ~ beta   <~ Will default [beta := F Int]
-           [Wanted] F Char ~ beta   <~ Already defaulted, can't default again. We
-                                       have to report this as unsolved.
-
-    2) However, we must still do an occurs check when defaulting (F xis ~ beta), to
-       set [beta := F xis] only if beta is not among the free variables of xis.
-
-    3) Notice that 'beta' can't be bound in ty binds already because we rewrite RHS
-       of type family equations. See Inert Set invariants in TcInteract.
-
-This solving is now happening during zonking, see Note [Unflattening while zonking]
-in TcMType.
-
 
 *********************************************************************************
 *                                                                               *
index 99927aa..e2644c5 100644 (file)
@@ -102,6 +102,7 @@ module TcType (
   -- * Finding "exact" (non-dead) type variables
   exactTyCoVarsOfType, exactTyCoVarsOfTypes,
   splitDepVarsOfType, splitDepVarsOfTypes, TcDepVars(..), tcDepVarSet,
+  rewritableTyVarsOfTypes, rewritableTyVarsOfType,
 
   -- * Extracting bound variables
   allBoundVariables, allBoundVariabless,
@@ -835,6 +836,23 @@ exactTyCoVarsOfType ty
 exactTyCoVarsOfTypes :: [Type] -> TyVarSet
 exactTyCoVarsOfTypes tys = mapUnionVarSet exactTyCoVarsOfType tys
 
+rewritableTyVarsOfTypes :: [TcType] -> TcTyVarSet
+rewritableTyVarsOfTypes tys = mapUnionVarSet rewritableTyVarsOfType tys
+
+rewritableTyVarsOfType :: TcType -> TcTyVarSet
+rewritableTyVarsOfType ty
+  = go ty
+  where
+    go (TyVarTy tv)     = unitVarSet tv
+    go (LitTy {})       = emptyVarSet
+    go (TyConApp _ tys) = rewritableTyVarsOfTypes tys
+    go (AppTy fun arg)  = go fun `unionVarSet` go arg
+    go (FunTy arg res)  = go arg `unionVarSet` go res
+    go ty@(ForAllTy {}) = pprPanic "rewriteableTyVarOfType" (ppr ty)
+    go (CastTy ty _co)  = go ty
+    go (CoercionTy _co) = emptyVarSet
+
+
 {- *********************************************************************
 *                                                                      *
           Bound variables in a type
index d194321..566594f 100644 (file)
@@ -1509,8 +1509,10 @@ maybe_sym IsSwapped  = mkSymCo
 maybe_sym NotSwapped = id
 
 swapOverTyVars :: TcTyVar -> TcTyVar -> Bool
--- See Note [Canonical orientation for tyvar/tyvar equality constraints]
 swapOverTyVars tv1 tv2
+  | isFmvTyVar tv1 = False  -- See Note [Fmv Orientation Invariant]
+  | isFmvTyVar tv2 = True
+
   | Just lvl1 <- metaTyVarTcLevel_maybe tv1
       -- If tv1 is touchable, swap only if tv2 is also
       -- touchable and it's strictly better to update the latter
@@ -1565,7 +1567,46 @@ canSolveByUnification tclvl tv xi
                        FlatSkol {} -> False
                        RuntimeUnk  -> True
 
-{-
+{- Note [Fmv Orientation Invariant]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+   * We always orient a constraint
+        fmv ~ alpha
+     with fmv on the left, even if alpha is
+     a touchable unification variable
+
+Reason: doing it the other way round would unify alpha:=fmv, but that
+really doesn't add any info to alpha.  But a later constraint alpha ~
+Int might unlock everything.  Comment:9 of #12526 gives a detailed
+example.
+
+WARNING: I've gone to and fro on this one several times.
+I'm now pretty sure that unifying alpha:=fmv is a bad idea!
+So orienting with fmvs on the left is a good thing.
+
+This example comes from IndTypesPerfMerge. (Others include
+T10226, T10009.)
+    From the ambiguity check for
+      f :: (F a ~ a) => a
+    we get:
+          [G] F a ~ a
+          [WD] F alpha ~ alpha, alpha ~ a
+
+    From Givens we get
+          [G] F a ~ fsk, fsk ~ a
+
+    Now if we flatten we get
+          [WD] alpha ~ fmv, F alpha ~ fmv, alpha ~ a
+
+    Now, if we unified alpha := fmv, we'd get
+          [WD] F fmv ~ fmv, [WD] fmv ~ a
+    And now we are stuck.
+
+So instead the Fmv Orientation Invariant puts te fmv on the
+left, giving
+      [WD] fmv ~ alpha, [WD] F alpha ~ fmv, [WD] alpha ~ a
+
+    Now we get alpha:=a, and everything works out
+
 Note [Prevent unification with type families]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 We prevent unification with type families because of an uneasy compromise.
index 14d3a3e..77ce29a 100644 (file)
@@ -42,6 +42,30 @@ showFromF fa = undefined
 showFromF' :: (Show (FInv b), F (FInv b) ~ b) => b -> String
 showFromF' = showFromF
 
+{- [G] F (FInv b) ~ b
+   [W] FInv (F alpha) ~ alpha
+   [W] F alpha ~ b
+-->
+   [G] g1: FInv b ~ fsk1
+   [G] g2: F fsk1 ~ fsk2
+   [G} g3: fsk2 ~ b
+
+   [W] F alpha ~ fmv1
+   [W] FInv fmv1 ~ fmv2
+   [W] fmv2 ~ alpha
+   [W] fmv1 ~ b
+
+   [D] d1: F alpha ~ fmv1
+   [D] d2: FInv fmv1 ~ fmv2
+   [D] d3: fmv2 ~ alpha
+   [D] d4: fmv1 ~ b
+
+--> d2 + d4: [D] FInv b ~ fmv2
+       + g1: [D] fmv2 ~ b
+--> d3: b ~ alpha, and we are done
+
+-}
+
 {-------------------------------------------------------------------------------
   In 7.10 the definition of showFromF' is not accepted, but it gets stranger.
   In 7.10 we cannot _call_ showFromF at all, even at a concrete type. Below
@@ -57,3 +81,36 @@ type instance FInv Int = Int
 
 test :: String
 test = showFromF (0 :: Int)
+
+{-
+
+  [WD] FInv (F alpha) ~ alpha
+  [WD] F alpha ~ Int
+
+-->
+  [WD] F alpha ~ fuv0
+* [WD] FInv fuv0 ~ fuv1
+  [WD] fuv1 ~ alpha
+  [WD] fuv0 ~ Int
+
+-->
+  [WD] F alpha ~ fuv0
+  [W] FInv fuv0 ~ fuv1
+*  [D] FInv Int ~ fuv1
+  [WD] fuv1 ~ alpha
+  [WD] fuv0 ~ Int
+
+-->
+  [WD] F alpha ~ fuv0
+  [W] FInv fuv0 ~ fuv1
+* [D] fuv1 ~ Int
+  [WD] fuv1 ~ alpha
+  [WD] fuv0 ~ Int
+
+-->
+  [WD] F alpha ~ fuv0
+  [W] FInv fuv0 ~ fuv1
+  [D] alpha := Int
+  [WD] fuv1 ~ alpha
+  [WD] fuv0 ~ Int
+-}
index f02cf81..0b52ef5 100644 (file)
@@ -21,3 +21,18 @@ instance Convert Int32 where
 
 x :: Int8
 x = down 8
+
+{- From x = down 8
+
+[WD] Num alpha
+[WD] Convert alpha
+[WD] Down alpha ~ Int8
+
+--> superclasses
+[D] Up (Down alpha) ~ alpha
+
+--> substitute (Down alpha ~ Int8)
+[D] Up Int8 ~ alpha
+
+--> alpha := Int16
+-}
diff --git a/testsuite/tests/indexed-types/should_compile/T12526.hs b/testsuite/tests/indexed-types/should_compile/T12526.hs
new file mode 100644 (file)
index 0000000..35a653a
--- /dev/null
@@ -0,0 +1,69 @@
+{-# LANGUAGE TypeFamilies, MonoLocalBinds #-}
+module T12526 where
+
+type family P (s :: * -> *) :: * -> * -> *
+type instance P Signal = Causal
+
+type family S (p :: * -> * -> *) :: * -> *
+type instance S Causal = Signal
+
+class (P (S p) ~ p) => CP p
+instance CP Causal
+
+data Signal a = Signal
+data Causal a b = Causal
+
+shapeModOsci :: CP p => p Float Float
+shapeModOsci = undefined
+
+f :: Causal Float Float -> Bool
+f = undefined
+
+-- This fails
+ping :: Bool
+ping = let osci = shapeModOsci in  f osci
+
+
+-- This works
+-- ping :: Bool
+-- ping = f shapeModOsci
+
+
+{-
+
+    osci :: p Float Float
+    [W] CP p, [D] P (S p) ~ p
+-->
+    [W] CP p, [D] P fuv1 ~ fuv2, S p ~ fuv1, fuv2 ~ p
+-->
+    p := fuv2
+    [W] CP fuv2, [D] P fuv1 ~ fuv2, S fuv2 ~ fuv1
+
+-}
+
+-- P (S p) ~ p
+-- p Float Float ~ Causal Float Float
+
+
+{-
+  P (S p) ~ p
+  p Float Float ~ Causal Float Float
+
+--->
+  S p ~ fuv1    (FunEq)
+  P fuv1 ~ fuv2 (FunEq)
+  fuv2 ~ p
+  p F F ~ Causal F F
+
+--->
+  p := fuv2
+
+  fuv2 ~ Causal
+  S fuv2 ~ fuv1 (FunEq)
+  P fuv1 ~ fuv2 (FunEq)
+
+---> unflatten
+  fuv1 := S fuv2
+  fuv2 := Causal
+
+-}
diff --git a/testsuite/tests/indexed-types/should_compile/T12538.hs b/testsuite/tests/indexed-types/should_compile/T12538.hs
new file mode 100644 (file)
index 0000000..9aff36e
--- /dev/null
@@ -0,0 +1,40 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module T12538 where
+
+data Tagged t a = Tagged a
+
+type family Tag a where
+  Tag (Tagged t a) = Tagged t a
+  Tag a = Tagged Int a
+
+class (r ~ Tag a) => TagImpl a r | a -> r where
+  tag :: a -> r
+
+instance {-# OVERLAPPING #-} (r ~ Tag (Tagged t a)) => TagImpl (Tagged t a) r where
+  tag = id
+
+#ifdef WRONG
+instance {-# OVERLAPPING #-} (r ~ Tagged t a, r ~ Tag a) => TagImpl a r where
+#else
+instance {-# OVERLAPPING #-} (r ~ Tagged Int a, r ~ Tag a) => TagImpl a r where
+#endif
+  tag = Tagged @Int
+
+data family   DF x
+data instance DF (Tagged t a) = DF (Tagged t a)
+
+class ToDF a b | a -> b where
+  df :: a -> b
+
+instance (TagImpl a a', b ~ DF a') => ToDF a b where
+  df = DF . tag
+
+main :: IO ()
+main = pure ()
diff --git a/testsuite/tests/indexed-types/should_compile/T12538.stderr b/testsuite/tests/indexed-types/should_compile/T12538.stderr
new file mode 100644 (file)
index 0000000..ca10624
--- /dev/null
@@ -0,0 +1,13 @@
+
+T12538.hs:37:8: error:
+    • Could not deduce: a' ~ Tagged Int a
+      from the context: (TagImpl a a', b ~ DF a')
+        bound by the instance declaration at T12538.hs:36:10-46
+      ‘a'’ is a rigid type variable bound by
+        the instance declaration at T12538.hs:36:10-46
+      Expected type: a -> b
+        Actual type: a -> DF (Tagged Int a)
+    • In the expression: DF . tag
+      In an equation for ‘df’: df = DF . tag
+      In the instance declaration for ‘ToDF a b’
+    • Relevant bindings include df :: a -> b (bound at T12538.hs:37:3)
index 29877bf..b11c95e 100644 (file)
@@ -4,7 +4,7 @@ TYPE SIGNATURES
   emptyL :: forall a. ListColl a
   insert :: forall c. Coll c => Elem c -> c -> c
   test2 ::
-    forall a b c. (Elem c ~ (a, b), Coll c, Num a, Num b) => c -> c
+    forall a b c. (Elem c ~ (a, b), Num b, Num a, Coll c) => c -> c
 TYPE CONSTRUCTORS
   class Coll c where
     type family Elem c :: * open
index 6fa2ae8..64e224e 100644 (file)
@@ -17,7 +17,40 @@ instance Foo Char Int where
      tickle = (+1)
 
 test :: (Foo a b) => a -> a
-test = back . tickle . there
+test x = back (tickle (there x))
 
 main :: IO ()
 main = print $ test 'F'
+
+{-
+
+[G] Foo a b
+[G] There a ~ b
+[G] Back b ~ a
+
+[W] Foo a beta      -- from 'there'
+[W] Foo alpha beta  -- from tickle
+[W] Foo a beta      -- from back
+
+[D] There a ~ beta
+[D] Back beta ~ a
+
+[D] There alpha ~ beta
+[D] Back beta ~ alpha
+
+
+-- Hence beta = b
+--       alpha = a
+
+
+
+[W] Foo a (There t_a1jL)
+[W] Foo t_a1jL (There t_a1jL)
+[W] Back (There t_a1jL) ~ t_a1jL
+
+[D] There a ~ There t_a1jL
+     hence There t_a1jL ~ b
+[D] Back (There t_a1jL) ~ a
+[D] There t_a1jL ~ There t_a1jL
+[D] Back (There t_a1jL) ~ t_a1jL
+-}
index b093128..eb71a28 100644 (file)
@@ -278,3 +278,5 @@ test('T12175', normal, compile, [''])
 test('T12522', normal, compile, [''])
 test('T12522b', normal, compile, [''])
 test('T12676', normal, compile, [''])
+test('T12526', normal, compile, [''])
+test('T12538', normal, compile_fail, [''])
index 6375c8f..b943db2 100644 (file)
@@ -1,4 +1,16 @@
 
+T2544.hs:17:12: error:
+    • Couldn't match type ‘IxMap r’ with ‘IxMap i1’
+      Expected type: IxMap (l :|: r) [Int]
+        Actual type: BiApp (IxMap l) (IxMap i1) [Int]
+      NB: ‘IxMap’ is a type function, and may not be injective
+      The type variable ‘i1’ is ambiguous
+    • In the expression: BiApp empty empty
+      In an equation for ‘empty’: empty = BiApp empty empty
+      In the instance declaration for ‘Ix (l :|: r)’
+    • Relevant bindings include
+        empty :: IxMap (l :|: r) [Int] (bound at T2544.hs:17:4)
+
 T2544.hs:17:18: error:
     • Couldn't match type ‘IxMap i0’ with ‘IxMap l’
       Expected type: IxMap l [Int]
@@ -10,15 +22,3 @@ T2544.hs:17:18: error:
       In an equation for ‘empty’: empty = BiApp empty empty
     • Relevant bindings include
         empty :: IxMap (l :|: r) [Int] (bound at T2544.hs:17:4)
-
-T2544.hs:17:24: error:
-    • Couldn't match type ‘IxMap i1’ with ‘IxMap r’
-      Expected type: IxMap r [Int]
-        Actual type: IxMap i1 [Int]
-      NB: ‘IxMap’ is a type function, and may not be injective
-      The type variable ‘i1’ is ambiguous
-    • In the second argument of ‘BiApp’, namely ‘empty’
-      In the expression: BiApp empty empty
-      In an equation for ‘empty’: empty = BiApp empty empty
-    • Relevant bindings include
-        empty :: IxMap (l :|: r) [Int] (bound at T2544.hs:17:4)
index 11e1b8e..63f11b9 100644 (file)
@@ -1,9 +1,9 @@
 
 T2627b.hs:20:24: error:
     • Occurs check: cannot construct the infinite type:
-        t0 ~ Dual (Dual t0)
+        b0 ~ Dual (Dual b0)
         arising from a use of ‘conn’
-      The type variable ‘t0’ is ambiguous
+      The type variable ‘b0’ is ambiguous
     • In the expression: conn undefined undefined
       In an equation for ‘conn’:
           conn (Rd k) (Wr a r) = conn undefined undefined
index 8526c17..829bca1 100644 (file)
@@ -3,14 +3,14 @@ T3330c.hs:23:43: error:
     • Couldn't match kind ‘* -> *’ with ‘*’
       When matching types
         f1 :: * -> *
-        Der f1 x :: *
-      Expected type: Der ((->) x) (Der f1 x)
+        f1 x :: *
+      Expected type: Der ((->) x) (f1 x)
         Actual type: R f1
     • In the first argument of ‘plug’, namely ‘rf’
       In the first argument of ‘Inl’, namely ‘(plug rf df x)’
       In the expression: Inl (plug rf df x)
     • Relevant bindings include
         x :: x (bound at T3330c.hs:23:29)
-        df :: Der f1 x (bound at T3330c.hs:23:25)
+        df :: f1 x (bound at T3330c.hs:23:25)
         rf :: R f1 (bound at T3330c.hs:23:13)
         plug' :: R f -> Der f x -> x -> f x (bound at T3330c.hs:23:1)
index 91244c4..516bdf3 100644 (file)
@@ -1,13 +1,13 @@
 
 T4179.hs:26:16: error:
-    • Couldn't match type ‘A3 (x (A2 (FCon x) -> A3 (FCon x)))’
-                     with ‘A3 (FCon x)’
+    • Couldn't match type ‘A2 (x (A2 (FCon x) -> A3 (FCon x)))’
+                     with ‘A2 (FCon x)’
       Expected type: x (A2 (FCon x) -> A3 (FCon x))
                      -> A2 (FCon x) -> A3 (FCon x)
         Actual type: x (A2 (FCon x) -> A3 (FCon x))
                      -> A2 (x (A2 (FCon x) -> A3 (FCon x)))
                      -> A3 (x (A2 (FCon x) -> A3 (FCon x)))
-      NB: ‘A3’ is a type function, and may not be injective
+      NB: ‘A2’ is a type function, and may not be injective
     • In the first argument of ‘foldDoC’, namely ‘op’
       In the expression: foldDoC op
       In an equation for ‘fCon’: fCon = foldDoC op
index 3c77040..0ae1a5e 100644 (file)
@@ -1,9 +1,9 @@
 
 T6123.hs:10:14: error:
-    • Occurs check: cannot construct the infinite type: t0 ~ Id t0
+    • Occurs check: cannot construct the infinite type: a0 ~ Id a0
         arising from a use of ‘cid’
-      The type variable ‘t0’ is ambiguous
+      The type variable ‘a0’ is ambiguous
     • In the expression: cid undefined
       In an equation for ‘cundefined’: cundefined = cid undefined
     • Relevant bindings include
-        cundefined :: t0 (bound at T6123.hs:10:1)
+        cundefined :: a0 (bound at T6123.hs:10:1)
index 839a1fb..2a5c7f5 100644 (file)
@@ -55,17 +55,17 @@ type family Intersect (l :: Inventory a) (r :: Inventory a) :: Inventory a where
   Intersect l Empty = Empty
   Intersect (More ls l) r = InterAppend (Intersect ls r) r l
 
-type family InterAppend (l :: Inventory a) 
-                        (r :: Inventory a) 
-                        (one :: a) 
+type family InterAppend (l :: Inventory a)
+                        (r :: Inventory a)
+                        (one :: a)
             :: Inventory a where
   InterAppend acc Empty one = acc
   InterAppend acc (More rs one) one = More acc one
   InterAppend acc (More rs r) one = InterAppend acc rs one
 
-type family BuriedUnder (sub :: Inventory [KeySegment]) 
-                        (post :: [KeySegment]) 
-                        (inv :: Inventory [KeySegment]) 
+type family BuriedUnder (sub :: Inventory [KeySegment])
+                        (post :: [KeySegment])
+                        (inv :: Inventory [KeySegment])
             :: Inventory [KeySegment] where
   BuriedUnder Empty post inv = inv
   BuriedUnder (More ps p) post inv = More ((ps `BuriedUnder` post) inv) (p `Under` post)
@@ -82,9 +82,23 @@ foo :: Database inv
 foo db k sub = buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db
 -}
 
+foogle :: Database inv
+       -> Sing post
+       -> Database sub
+       -> Maybe (Sing (Intersect (BuriedUnder sub post 'Empty) inv))
+
+foogle db k sub = return (buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db)
+
+
 addSub :: Database inv -> Sing k -> Database sub -> Maybe (Database ((sub `BuriedUnder` k) inv))
-addSub db k sub = do Nil :: Sing xxx <- return (buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db)
+addSub db k sub = do Nil :: Sing xxx <- foogle db k sub
+                     return $ Sub db k sub
+
+{-
+addSub :: Database inv -> Sing k -> Database sub -> Maybe (Database ((sub `BuriedUnder` k) inv))
+addSub db k sub = do Nil :: Sing xxx <- foogle db sub k
                      -- Nil :: Sing ((sub `BuriedUnder` k) Empty `Intersect` inv) <- return (buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db)
                      -- Nil :: Sing Empty <- return (buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db)
                      -- Nil <- return (buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db)
                      return $ Sub db k sub
+-}
index ca3e9ec..8fdb49b 100644 (file)
@@ -1,29 +1,29 @@
 
-T7786.hs:86:49: error:
+T7786.hs:94:41: error:
     • Couldn't match type ‘xxx’
                      with ‘Intersect (BuriedUnder sub k 'Empty) inv’
-      Expected type: Sing xxx
-        Actual type: Sing (Intersect (BuriedUnder sub k 'Empty) inv)
-    • In the first argument of ‘return’, namely
-        ‘(buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db)’
-      In a stmt of a 'do' block:
-        Nil :: Sing xxx <- return
-                             (buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db)
+      Expected type: Maybe (Sing xxx)
+        Actual type: Maybe
+                       (Sing (Intersect (BuriedUnder sub k 'Empty) inv))
+    • In a stmt of a 'do' block: Nil :: Sing xxx <- foogle db k sub
       In the expression:
-        do { Nil :: Sing xxx <- return
-                                  (buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db);
+        do { Nil :: Sing xxx <- foogle db k sub;
              return $ Sub db k sub }
+      In an equation for ‘addSub’:
+          addSub db k sub
+            = do { Nil :: Sing xxx <- foogle db k sub;
+                   return $ Sub db k sub }
     • Relevant bindings include
-        sub :: Database sub (bound at T7786.hs:86:13)
-        k :: Sing k (bound at T7786.hs:86:11)
-        db :: Database inv (bound at T7786.hs:86:8)
+        sub :: Database sub (bound at T7786.hs:94:13)
+        k :: Sing k (bound at T7786.hs:94:11)
+        db :: Database inv (bound at T7786.hs:94:8)
         addSub :: Database inv
                   -> Sing k
                   -> Database sub
                   -> Maybe (Database (BuriedUnder sub k inv))
-          (bound at T7786.hs:86:1)
+          (bound at T7786.hs:94:1)
 
-T7786.hs:90:31: error:
+T7786.hs:95:31: error:
     • Could not deduce: Intersect (BuriedUnder sub k 'Empty) inv
                         ~
                         'Empty
@@ -32,19 +32,18 @@ T7786.hs:90:31: error:
         bound by a pattern with constructor: Nil :: forall a. Sing 'Empty,
                  in a pattern binding in
                       'do' block
-        at T7786.hs:86:22-24
+        at T7786.hs:94:22-24
     • In the second argument of ‘($)’, namely ‘Sub db k sub’
       In a stmt of a 'do' block: return $ Sub db k sub
       In the expression:
-        do { Nil :: Sing xxx <- return
-                                  (buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db);
+        do { Nil :: Sing xxx <- foogle db k sub;
              return $ Sub db k sub }
     • Relevant bindings include
-        sub :: Database sub (bound at T7786.hs:86:13)
-        k :: Sing k (bound at T7786.hs:86:11)
-        db :: Database inv (bound at T7786.hs:86:8)
+        sub :: Database sub (bound at T7786.hs:94:13)
+        k :: Sing k (bound at T7786.hs:94:11)
+        db :: Database inv (bound at T7786.hs:94:8)
         addSub :: Database inv
                   -> Sing k
                   -> Database sub
                   -> Maybe (Database (BuriedUnder sub k inv))
-          (bound at T7786.hs:86:1)
+          (bound at T7786.hs:94:1)
index 6dec5d0..88f4732 100644 (file)
@@ -1,10 +1,11 @@
 
-T8227.hs:16:44: error:
-    • Couldn't match expected type ‘Scalar (V (Scalar (V a)))’
-                  with actual type ‘Scalar (V a)’
-      NB: ‘Scalar’ is a type function, and may not be injective
-    • In the first argument of ‘arcLengthToParam’, namely ‘eps’
-      In the expression: arcLengthToParam eps eps
+T8227.hs:16:27: error:
+    • Couldn't match type ‘Scalar (V a)’
+                     with ‘Scalar (V a) -> Scalar (V a)’
+      Expected type: Scalar (V a)
+        Actual type: Scalar (V (Scalar (V a) -> Scalar (V a)))
+                     -> Scalar (V (Scalar (V a) -> Scalar (V a)))
+    • In the expression: arcLengthToParam eps eps
       In an equation for ‘absoluteToParam’:
           absoluteToParam eps seg = arcLengthToParam eps eps
     • Relevant bindings include
index 23c059e..0588c1b 100644 (file)
@@ -60,18 +60,3 @@ T10403.hs:28:8: warning: [-Wdeferred-type-errors (in -Wdefault)]
       In an equation for ‘app2’: app2 = h2 (H . I) (B ())
     • Relevant bindings include
         app2 :: H (B t) (bound at T10403.hs:28:1)
-
-T10403.hs:28:20: warning: [-Wdeferred-type-errors (in -Wdefault)]
-    • Couldn't match type ‘f0’ with ‘B t’
-        because type variable ‘t’ would escape its scope
-      This (rigid, skolem) type variable is bound by
-        the type signature for:
-          app2 :: H (B t)
-        at T10403.hs:27:1-15
-      Expected type: f0 ()
-        Actual type: B t ()
-    • In the second argument of ‘h2’, namely ‘(B ())’
-      In the expression: h2 (H . I) (B ())
-      In an equation for ‘app2’: app2 = h2 (H . I) (B ())
-    • Relevant bindings include
-        app2 :: H (B t) (bound at T10403.hs:28:1)
index 6ebbd65..0a500fb 100644 (file)
@@ -13,26 +13,35 @@ t = undefined
          [G] a ~ TF (a,Int)               -- a = a_am1
 -->
          [G] TF (a,Int) ~ fsk             -- fsk = fsk_am8
+
 inert    [G] fsk ~ a
 
---->
-    [G] fsk ~ (TF a, TF Int)
+---> reduce
+         [G] fsk ~ (TF a, TF Int)
+
 inert    [G] fsk ~ a
 
---->
-    a ~ (TF a, TF Int)
+---> substitute for fsk and flatten
+         [G] TF a ~ fsk1
+         [G] TF Int ~ fsk2
+
 inert    [G] fsk ~ a
+         [G] a ~ (fsk1, fsk2)
 
----> (attempting to flatten (TF a) so that it does not mention a
-         TF a ~ fsk2
-inert    a ~ (fsk2, TF Int)
-inert    fsk ~ (fsk2, TF Int)
+---> (substitute for a in first constraint)
+         TF (fsk1, fsk2) ~ fsk1     (C1)
+         TF Int ~ fsk2
 
----> (substitute for a)
-         TF (fsk2, TF Int) ~ fsk2
 inert    a ~ (fsk2, TF Int)
 inert    fsk ~ (fsk2, TF Int)
 
+
+------- At this point we are stuck because of
+--      the recursion in the first constraint C1
+--      Hooray
+
+-- Before, we reduced C1, which led to a loop
+
 ---> (top-level reduction, re-orient)
          fsk2 ~ (TF fsk2, TF Int)
 inert    a ~ (fsk2, TF Int)
@@ -50,4 +59,4 @@ inert    fsk2 ~ (fsk3, TF Int)
 inert    a   ~ ((fsk3, TF Int), TF Int)
 inert    fsk ~ ((fsk3, TF Int), TF Int)
 
--}
\ No newline at end of file
+-}
diff --git a/testsuite/tests/perf/compiler/T5837.stderr b/testsuite/tests/perf/compiler/T5837.stderr
deleted file mode 100644 (file)
index 324e817..0000000
+++ /dev/null
@@ -1,91 +0,0 @@
-
-T5837.hs:8:6: error:
-    Reduction stack overflow; size = 51
-    When simplifying the following type:
-      TF
-        (TF
-           (TF
-              (TF
-                 (TF
-                    (TF
-                       (TF
-                          (TF
-                             (TF
-                                (TF
-                                   (TF
-                                      (TF
-                                         (TF
-                                            (TF
-                                               (TF
-                                                  (TF
-                                                     (TF
-                                                        (TF
-                                                           (TF
-                                                              (TF
-                                                                 (TF
-                                                                    (TF
-                                                                       (TF
-                                                                          (TF
-                                                                             (TF
-                                                                                a))))))))))))))))))))))))
-      ~ (TF
-           (TF
-              (TF
-                 (TF
-                    (TF
-                       (TF
-                          (TF
-                             (TF
-                                (TF
-                                   (TF
-                                      (TF
-                                         (TF
-                                            (TF
-                                               (TF
-                                                  (TF
-                                                     (TF
-                                                        (TF
-                                                           (TF
-                                                              (TF
-                                                                 (TF
-                                                                    (TF
-                                                                       (TF
-                                                                          (TF
-                                                                             (TF
-                                                                                (TF
-                                                                                   (TF
-                                                                                      a))))))))))))))))))))))))),
-         TF
-           (TF
-              (TF
-                 (TF
-                    (TF
-                       (TF
-                          (TF
-                             (TF
-                                (TF
-                                   (TF
-                                      (TF
-                                         (TF
-                                            (TF
-                                               (TF
-                                                  (TF
-                                                     (TF
-                                                        (TF
-                                                           (TF
-                                                              (TF
-                                                                 (TF
-                                                                    (TF
-                                                                       (TF
-                                                                          (TF
-                                                                             (TF
-                                                                                (TF
-                                                                                   (TF
-                                                                                      Int))))))))))))))))))))))))))
-    Use -freduction-depth=0 to disable this check
-    (any upper bound you could choose might fail unpredictably with
-     minor updates to GHC, so disabling the check is recommended if
-     you're sure that type checking should terminate)
-    In the ambiguity check for ‘t’
-    In the type signature:
-      t :: (a ~ TF (a, Int)) => Int
index 72c58c7..7c8f55a 100644 (file)
@@ -594,7 +594,7 @@ test('T5837',
              # 2014-12-08: 115905208  Constraint solver perf improvements (esp kick-out)
              # 2016-04-06: 24199320  (x86/Linux, 64-bit machine) TypeInType
 
-           (wordsize(64), 41832056, 10)])
+           (wordsize(64), 52597024, 10)])
              # sample: 3926235424 (amd64/Linux, 15/2/2012)
              # 2012-10-02 81879216
              # 2012-09-20 87254264 amd64/Linux
@@ -615,8 +615,11 @@ test('T5837',
              #                           for other optimisations
              # 2016-09-15 42445672  Linux; fixing #12422
              # 2016-09-25 41832056  amd64/Linux, Rework handling of names (D2469)
+             # 2016-10-25 52597024  amd64/Linux, the test now passes (hooray), and so
+             #                          allocates more because it goes right down the
+             #                          compilation pipeline
       ],
-      compile_fail,['-freduction-depth=50'])
+      compile['-freduction-depth=50'])
 
 test('T6048',
      [ only_ways(['optasm']),
diff --git a/testsuite/tests/polykinds/T12444.hs b/testsuite/tests/polykinds/T12444.hs
new file mode 100644 (file)
index 0000000..746c644
--- /dev/null
@@ -0,0 +1,65 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+
+module T12444 where
+
+data Nat = Zero | Succ Nat
+
+data SNat (n :: Nat) where
+  SZero :: SNat Zero
+  SSucc :: SNat n -> SNat (Succ n)
+
+type family (:+:) (a :: Nat) (b :: Nat) :: Nat where
+  m :+: Zero = m
+  m :+: (Succ n) = Succ (m :+: n)
+
+foo :: SNat (Succ c) -> SNat b -> SNat (Succ (c :+: b))
+foo _ x = x
+
+
+{-
+sadd :: ((Succ n1 :+: n) ~ Succ (n1 :+: n), (Succ n1) ~ m)
+     => SNat m -> SNat n -> SNat (m :+: n)
+sadd SZero n = n
+-}
+
+{- [G]  a ~ Succ c
+        Succ c + b ~ Succ (c+b)
+        a ~ Zero
+
+-->
+        Zero ~ Succ c            TyEq
+        fsk1 ~ Succ fsk2         TyEq
+        fsk1 ~ (Succ c) + b      FunEq
+        fsk2 ~ c+b               FunEq
+----
+[W] b ~ a+b  --->   b ~ Succ (c+b)
+
+
+Derived
+       a ~ Succ c
+       fsk1 ~ Succ fsk2
+       b ~ Succ fsk2
+
+work   (Succ c) + b ~ fsk1
+       c+b ~ fsk2
+
+
+-}
+
+{-
+
+[G] a ~ [b]
+--> Derived shadow [D] a ~ [b]
+    When adding this to the model
+    don't kick out a derived shadow again!
+
+[G] (a ~ b)  --> sc   a ~~ b, a ~# b
+  Silly to then kick out (a~b) and (a~~b)
+  and rewrite them to (a~a) and (a~~a)
+
+Insoluble constraint does not halt solving;
+indeed derived version stays. somehow
+-}
diff --git a/testsuite/tests/polykinds/T12444.stderr b/testsuite/tests/polykinds/T12444.stderr
new file mode 100644 (file)
index 0000000..0ebd298
--- /dev/null
@@ -0,0 +1,16 @@
+
+T12444.hs:19:11: error:
+    • Couldn't match type ‘b’ with ‘'Succ (c :+: b)’
+      ‘b’ is a rigid type variable bound by
+        the type signature for:
+          foo :: forall (c :: Nat) (b :: Nat).
+                 SNat ('Succ c) -> SNat b -> SNat ('Succ (c :+: b))
+        at T12444.hs:18:1-55
+      Expected type: SNat ('Succ (c :+: b))
+        Actual type: SNat b
+    • In the expression: x
+      In an equation for ‘foo’: foo _ x = x
+    • Relevant bindings include
+        x :: SNat b (bound at T12444.hs:19:7)
+        foo :: SNat ('Succ c) -> SNat b -> SNat ('Succ (c :+: b))
+          (bound at T12444.hs:19:1)
index df97578..dc1b92c 100644 (file)
@@ -1,12 +1,12 @@
 
 T9222.hs:13:3: error:
-    • Couldn't match type ‘b0’ with ‘b
-        ‘b0’ is untouchable
+    • Couldn't match type ‘c0’ with ‘c
+        ‘c0’ is untouchable
           inside the constraints: a ~ '(b0, c0)
           bound by the type of the constructor ‘Want’:
                      a ~ '(b0, c0) => Proxy b0
           at T9222.hs:13:3
-      ‘b’ is a rigid type variable bound by
+      ‘c’ is a rigid type variable bound by
         the type of the constructor ‘Want’:
           forall i1 j1 (a :: (i1, j1)) (b :: i1) (c :: j1).
           (a ~ '(b, c) => Proxy b) -> Want a
index 6ec2a43..0e0d66a 100644 (file)
@@ -154,3 +154,4 @@ test('T12055a', normal, compile_fail, [''])
 test('T12593', normal, compile_fail, [''])
 test('T12668', normal, compile, [''])
 test('T12718', normal, compile, [''])
+test('T12444', normal, compile_fail, [''])
index e7e1190..8df81c2 100644 (file)
@@ -1,5 +1,15 @@
 {-# LANGUAGE TypeFamilies, FlexibleContexts, MultiParamTypeClasses, FlexibleInstances #-}
 {-# OPTIONS_GHC -fno-warn-redundant-constraints #-}
+
+-- This one relies on doing instance reduction
+-- on a /derived/ class
+--    [W] C (F a0) a0, F a0 ~ Bool
+-- Currently (Oct 16) I've disabled this because it seems like
+-- overkill.
+--
+-- See Note Note [No reduction for Derived class constraints]
+-- in TcInteract
+
 module Foo where
 
 type family F a
@@ -14,5 +24,5 @@ blug = error "Urk"
 
 foo :: Bool
 foo = blug undefined
--- [W] C (F a0) a0, F a0 ~ Bool
+
 
index 5fdb03b..91a67c5 100644 (file)
@@ -8,6 +8,38 @@
 
 module T6018 where
 
+{-
+barapp2 :: Int
+barapp2 = bar 1
+
+bar :: Bar a -> Bar a
+bar x = x
+
+type family Bar a = r | r -> a where
+    Bar Int  = Bool
+    Bar Bool = Int
+    Bar Bool = Char
+
+type family F a b c = (result :: k) | result -> a b c
+
+type family FClosed a b c = result | result -> a b c where
+    FClosed Int  Char Bool = Bool
+    FClosed Char Bool Int  = Int
+    FClosed Bool Int  Char = Char
+-}
+{-
+g6_use :: [Char]
+g6_use = g6_id "foo"
+
+g6_id :: G6 a -> G6 a
+g6_id x = x
+
+type family G6 a = r | r -> a
+type instance G6 [a]  = [Gi a]
+type family Gi a = r | r -> a
+type instance Gi Int = Char
+-}
+
 import T6018a -- defines G, identical to F
 
 type family F a b c = (result :: k) | result -> a b c
index 91d6b30..57eed50 100644 (file)
@@ -2,10 +2,10 @@
 [2 of 3] Compiling T6018a          (.hs -> .o)
 [3 of 3] Compiling T6018           (.hs -> .o)
 
-T6018.hs:75:5: warning:
+T6018.hs:107:5: warning:
     Type family instance equation is overlapped:
-      Foo Bool = Bool -- Defined at T6018.hs:75:5
+      Foo Bool = Bool -- Defined at T6018.hs:107:5
 
-T6018.hs:82:5: warning:
+T6018.hs:114:5: warning:
     Type family instance equation is overlapped:
-      Bar Bool = Char -- Defined at T6018.hs:82:5
+      Bar Bool = Char -- Defined at T6018.hs:114:5
index f3f93eb..d66103c 100644 (file)
@@ -5,6 +5,8 @@ module ContextStack2 where
 type family TF a :: *
 type instance TF (a,b) = (TF a, TF b)
 
+-- Succeeds with new approach to fuvs
+-- Aug 2016
 t :: (a ~ TF (a,Int)) => Int
 t = undefined
 
diff --git a/testsuite/tests/typecheck/should_fail/ContextStack2.stderr b/testsuite/tests/typecheck/should_fail/ContextStack2.stderr
deleted file mode 100644 (file)
index f76d1f4..0000000
+++ /dev/null
@@ -1,13 +0,0 @@
-
-ContextStack2.hs:8:6: error:
-    • Reduction stack overflow; size = 11
-      When simplifying the following type:
-        TF (TF (TF (TF (TF a))))
-        ~ (TF (TF (TF (TF (TF (TF a))))), TF (TF (TF (TF (TF (TF Int))))))
-      Use -freduction-depth=0 to disable this check
-      (any upper bound you could choose might fail unpredictably with
-       minor updates to GHC, so disabling the check is recommended if
-       you're sure that type checking should terminate)
-    • In the ambiguity check for ‘t’
-      In the type signature:
-        t :: (a ~ TF (a, Int)) => Int
index 9101fbd..f994435 100644 (file)
@@ -1,3 +1,8 @@
 TOP=../../..
 include $(TOP)/mk/boilerplate.mk
 include $(TOP)/mk/test.mk
+
+.PHONEY: foo
+
+foo:
+       echo hello
index 9d4e587..ad5c7e4 100644 (file)
@@ -1,12 +1,12 @@
 
-T5691.hs:15:24: error:
+T5691.hs:14:9: error:
     • Couldn't match type ‘p’ with ‘PrintRuleInterp’
       Expected type: PrintRuleInterp a
         Actual type: p a
-    • In the first argument of ‘printRule_’, namely ‘f’
-      In the second argument of ‘($)’, namely ‘printRule_ f’
-      In the expression: MkPRI $ printRule_ f
-    • Relevant bindings include f :: p a (bound at T5691.hs:14:9)
+    • When checking that the pattern signature: p a
+        fits the type of its context: PrintRuleInterp a
+      In the pattern: f :: p a
+      In an equation for ‘test’: test (f :: p a) = MkPRI $ printRule_ f
 
 T5691.hs:24:10: error:
     • No instance for (Alternative RecDecParser)
index 62385ea..719895a 100644 (file)
@@ -1,22 +1,22 @@
 
 T5853.hs:15:46: error:
-    • Could not deduce: Subst (Subst t2 t) t1 ~ Subst t2 t1
+    • Could not deduce: Subst (Subst fa a) b ~ Subst fa b
         arising from a use of ‘<$>’
-      from the context: (F t2,
-                         Elem t2 ~ Elem t2,
-                         Elem (Subst t2 t1) ~ t1,
-                         Subst t2 t1 ~ Subst t2 t1,
-                         Subst (Subst t2 t1) (Elem t2) ~ t2,
-                         F (Subst t2 t),
-                         Elem (Subst t2 t) ~ t,
-                         Elem t2 ~ Elem t2,
-                         Subst (Subst t2 t) (Elem t2) ~ t2,
-                         Subst t2 t ~ Subst t2 t)
+      from the context: (F fa,
+                         Elem fa ~ Elem fa,
+                         Elem (Subst fa b) ~ b,
+                         Subst fa b ~ Subst fa b,
+                         Subst (Subst fa b) (Elem fa) ~ fa,
+                         F (Subst fa a),
+                         Elem (Subst fa a) ~ a,
+                         Elem fa ~ Elem fa,
+                         Subst (Subst fa a) (Elem fa) ~ fa,
+                         Subst fa a ~ Subst fa a)
         bound by the RULE "map/map" at T5853.hs:15:2-57
       NB: ‘Subst’ is a type function, and may not be injective
     • In the expression: (f . g) <$> xs
       When checking the transformation rule "map/map"
     • Relevant bindings include
-        f :: Elem t2 -> t1 (bound at T5853.hs:15:19)
-        g :: t -> Elem t2 (bound at T5853.hs:15:21)
-        xs :: Subst t2 t (bound at T5853.hs:15:23)
+        f :: Elem fa -> b (bound at T5853.hs:15:19)
+        g :: a -> Elem fa (bound at T5853.hs:15:21)
+        xs :: Subst fa a (bound at T5853.hs:15:23)
index 8ba84a7..7503f4d 100644 (file)
@@ -1,11 +1,15 @@
 
-T8450.hs:8:7: error:
-    • Couldn't match expected type ‘a’ with actual type ‘()
+T8450.hs:8:20: error:
+    • Couldn't match type ‘a’ with ‘Bool
       ‘a’ is a rigid type variable bound by
         the type signature for:
           run :: forall a. a
         at T8450.hs:7:1-18
-    • In the expression: runEffect $ (undefined :: Either a ())
+      Expected type: Either Bool ()
+        Actual type: Either a ()
+    • In the second argument of ‘($)’, namely
+        ‘(undefined :: Either a ())’
+      In the expression: runEffect $ (undefined :: Either a ())
       In an equation for ‘run’:
           run = runEffect $ (undefined :: Either a ())
     • Relevant bindings include run :: a (bound at T8450.hs:8:1)
index 0773da2..f55f474 100644 (file)
@@ -1,7 +1,8 @@
 
-T9260.hs:12:8: error:
-    • Couldn't match type ‘2’ with ‘1’
-      Expected type: Fin 1
-        Actual type: Fin (1 + 1)
-    • In the expression: Fsucc Fzero
+T9260.hs:12:14: error:
+    • Couldn't match type ‘1’ with ‘0’
+      Expected type: Fin 0
+        Actual type: Fin (0 + 1)
+    • In the first argument of ‘Fsucc’, namely ‘Fzero’
+      In the expression: Fsucc Fzero
       In an equation for ‘test’: test = Fsucc Fzero
index 4d58d4f..6f99a94 100644 (file)
@@ -336,7 +336,7 @@ test('T8428', normal, compile_fail, [''])
 test('T8450', normal, compile_fail, [''])
 test('T8514', normal, compile_fail, [''])
 test('ContextStack1', normal, compile_fail, ['-freduction-depth=10'])
-test('ContextStack2', normal, compile_fail, ['-freduction-depth=10'])
+test('ContextStack2', normal, compile, [''])
 test('T8570', extra_clean(['T85570a.o', 'T8570a.hi','T85570b.o', 'T8570b.hi']),
      multimod_compile_fail, ['T8570', '-v0'])
 test('T8603', normal, compile_fail, [''])