Fix header locations
[ghc.git] / compiler / typecheck / TcSimplify.hs
index e2598b5..6b593d8 100644 (file)
@@ -5,11 +5,17 @@ module TcSimplify(
        growThetaTyVars,
        simplifyAmbiguityCheck,
        simplifyDefault,
-       simplifyTop, captureTopConstraints,
-       simplifyInteractive, solveEqualities,
+       simplifyTop, simplifyTopImplic, captureTopConstraints,
+       simplifyInteractive,
+       solveEqualities, solveLocalEqualities,
        simplifyWantedsTcM,
        tcCheckSatisfiability,
 
+       simpl_top,
+
+       promoteTyVar,
+       promoteTyVarSet,
+
        -- For Rules we need these
        solveWanteds, solveWantedsAndDrop,
        approximateWC, runTcSDeriveds
@@ -17,14 +23,16 @@ module TcSimplify(
 
 #include "HsVersions.h"
 
+import GhcPrelude
+
 import Bag
 import Class         ( Class, classKey, classTyCon )
 import DynFlags      ( WarningFlag ( Opt_WarnMonomorphism )
                      , WarnReason ( Reason )
                      , DynFlags( solverIterations ) )
+import Id            ( idType )
 import Inst
 import ListSetOps
-import Maybes
 import Name
 import Outputable
 import PrelInfo
@@ -32,7 +40,7 @@ import PrelNames
 import TcErrors
 import TcEvidence
 import TcInteract
-import TcCanonical   ( makeSuperClasses )
+import TcCanonical   ( makeSuperClasses, solveCallStack )
 import TcMType   as TcM
 import TcRnMonad as TcM
 import TcSMonad  as TcS
@@ -49,8 +57,11 @@ import BasicTypes    ( IntWithInf, intGtLimit )
 import ErrUtils      ( emptyMessages )
 import qualified GHC.LanguageExtensions as LangExt
 
-import Control.Monad ( when, unless )
-import Data.List     ( partition )
+import Control.Monad
+import Data.Foldable      ( toList )
+import Data.List          ( partition )
+import Data.List.NonEmpty ( NonEmpty(..) )
+import Maybes             ( isJust )
 
 {-
 *********************************************************************************
@@ -81,6 +92,15 @@ captureTopConstraints thing_inside
                 -- This call to reportUnsolved is the reason
                 -- this function is here instead of TcRnMonad
 
+simplifyTopImplic :: Bag Implication -> TcM ()
+simplifyTopImplic implics
+  = do { empty_binds <- simplifyTop (mkImplicWC implics)
+
+       -- Since all the inputs are implications the returned bindings will be empty
+       ; MASSERT2( isEmptyBag empty_binds, ppr empty_binds )
+
+       ; return () }
+
 simplifyTop :: WantedConstraints -> TcM (Bag EvBind)
 -- Simplify top-level constraints
 -- Usually these will be implications,
@@ -108,7 +128,6 @@ simplifyTop wanteds
            ; TcM.writeTcRef errs_var emptyMessages
 
            ; warnAllUnsolved $ WC { wc_simple = unsafe_ol
-                                  , wc_insol = emptyCts
                                   , wc_impl = emptyBag }
 
            ; whyUnsafe <- fst <$> TcM.readTcRef errs_var
@@ -119,14 +138,37 @@ simplifyTop wanteds
 
        ; return (evBindMapBinds binds1 `unionBags` binds2) }
 
+-- | Type-check a thing that emits only equality constraints, solving any
+-- constraints we can and re-emitting constraints that we can't. The thing_inside
+-- should generally bump the TcLevel to make sure that this run of the solver
+-- doesn't affect anything lying around.
+solveLocalEqualities :: TcM a -> TcM a
+solveLocalEqualities thing_inside
+  = do { traceTc "solveLocalEqualities {" empty
+
+       ; (result, wanted) <- captureConstraints thing_inside
+
+       ; traceTc "solveLocalEqualities: running solver {" (ppr wanted)
+       ; reduced_wanted <- runTcSEqualities (solveWanteds wanted)
+       ; traceTc "solveLocalEqualities: running solver }" (ppr reduced_wanted)
+
+       ; emitConstraints reduced_wanted
+
+       ; traceTc "solveLocalEqualities end }" empty
+       ; return result }
+
 -- | Type-check a thing that emits only equality constraints, then
 -- solve those constraints. Fails outright if there is trouble.
+-- Use this if you're not going to get another crack at solving
+-- (because, e.g., you're checking a datatype declaration)
 solveEqualities :: TcM a -> TcM a
 solveEqualities thing_inside
   = checkNoErrs $  -- See Note [Fail fast on kind errors]
     do { (result, wanted) <- captureConstraints thing_inside
        ; traceTc "solveEqualities {" $ text "wanted = " <+> ppr wanted
        ; final_wc <- runTcSEqualities $ simpl_top wanted
+          -- NB: Use simpl_top here so that we potentially default RuntimeRep
+          -- vars to LiftedRep. This is needed to avoid #14991.
        ; traceTc "End solveEqualities }" empty
 
        ; traceTc "reportAllUnsolved {" empty
@@ -134,6 +176,8 @@ solveEqualities thing_inside
        ; traceTc "reportAllUnsolved }" empty
        ; return result }
 
+-- | Simplify top-level constraints, but without reporting any unsolved
+-- constraints nor unsafe overlapping.
 simpl_top :: WantedConstraints -> TcS WantedConstraints
     -- See Note [Top-level Defaulting Plan]
 simpl_top wanteds
@@ -208,8 +252,9 @@ defaultCallStacks wanteds
          ; setImplicationStatus (implic { ic_wanted = wanteds }) }
 
   defaultCallStack ct
-    | Just _ <- isCallStackPred (ctPred ct)
-    = do { solveCallStack (cc_ev ct) EvCsEmpty
+    | ClassPred cls tys <- classifyPredType (ctPred ct)
+    , Just {} <- isCallStackPred cls tys
+    = do { solveCallStack (ctEvidence ct) EvCsEmpty
          ; return Nothing }
 
   defaultCallStack ct
@@ -492,7 +537,7 @@ tcCheckSatisfiability given_ids
       | not (isEmptyBag insols)   -- We've found that it's definitely unsatisfiable
       = return insols             -- Hurrah -- stop now.
       | otherwise
-      = do { pending_given <- getPendingScDicts
+      = do { pending_given <- getPendingGivenScs
            ; new_given <- makeSuperClasses pending_given
            ; solveSimpleGivens new_given
            ; getInertInsols }
@@ -567,14 +612,17 @@ simplifyInfer :: TcLevel               -- Used when generating the constraints
               -> WantedConstraints
               -> TcM ([TcTyVar],    -- Quantify over these type variables
                       [EvVar],      -- ... and these constraints (fully zonked)
-                      TcEvBinds)    -- ... binding these evidence variables
+                      TcEvBinds,    -- ... binding these evidence variables
+                      WantedConstraints, -- Redidual as-yet-unsolved constraints
+                      Bool)         -- True <=> the residual constraints are insoluble
+
 simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds
   | isEmptyWC wanteds
   = do { gbl_tvs <- tcGetGlobalTyCoVars
        ; dep_vars <- zonkTcTypesAndSplitDepVars (map snd name_taus)
-       ; qtkvs <- quantifyZonkedTyVars gbl_tvs dep_vars
+       ; qtkvs <- quantifyTyVars gbl_tvs dep_vars
        ; traceTc "simplifyInfer: empty WC" (ppr name_taus $$ ppr qtkvs)
-       ; return (qtkvs, [], emptyTcEvBinds) }
+       ; return (qtkvs, [], emptyTcEvBinds, emptyWC, False) }
 
   | otherwise
   = do { traceTc "simplifyInfer {"  $ vcat
@@ -596,18 +644,18 @@ simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds
        -- bindings, so we can't just revert to the input
        -- constraint.
 
-       ; tc_lcl_env      <- TcM.getLclEnv
+       ; tc_env          <- TcM.getEnv
        ; ev_binds_var    <- TcM.newTcEvBinds
        ; psig_theta_vars <- mapM TcM.newEvVar psig_theta
        ; wanted_transformed_incl_derivs
             <- setTcLevel rhs_tclvl $
                runTcSWithEvBinds ev_binds_var $
-               do { let loc = mkGivenLoc rhs_tclvl UnkSkol tc_lcl_env
+               do { let loc         = mkGivenLoc rhs_tclvl UnkSkol $
+                                      env_lcl tc_env
                         psig_givens = mkGivens loc psig_theta_vars
                   ; _ <- solveSimpleGivens psig_givens
                          -- See Note [Add signature contexts as givens]
                   ; solveWanteds wanteds }
-       ; wanted_transformed_incl_derivs <- TcM.zonkWC wanted_transformed_incl_derivs
 
        -- Find quant_pred_candidates, the predicates that
        -- we'll consider quantifying over
@@ -615,137 +663,131 @@ simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds
        --      the psig_theta; it's just the extra bit
        -- NB2: We do not do any defaulting when inferring a type, this can lead
        --      to less polymorphic types, see Note [Default while Inferring]
-
-       ; let wanted_transformed = dropDerivedWC wanted_transformed_incl_derivs
-       ; quant_pred_candidates   -- Fully zonked
-           <- if insolubleWC wanted_transformed_incl_derivs
-              then return []   -- See Note [Quantification with errors]
-                               -- NB: must include derived errors in this test,
-                               --     hence "incl_derivs"
-
-              else do { let quant_cand = approximateWC False wanted_transformed
-                            meta_tvs   = filter isMetaTyVar $
-                                         tyCoVarsOfCtsList quant_cand
-
-                      ; gbl_tvs <- tcGetGlobalTyCoVars
-                            -- Miminise quant_cand.  We are not interested in any evidence
-                            -- produced, because we are going to simplify wanted_transformed
-                            -- again later. All we want here are the predicates over which to
-                            -- quantify.
-                            --
-                            -- If any meta-tyvar unifications take place (unlikely),
-                            -- we'll pick that up later.
-
-                      -- See Note [Promote _and_ default when inferring]
-                      ; let def_tyvar tv
-                              = when (not $ tv `elemVarSet` gbl_tvs) $
-                                defaultTyVar tv
-                      ; 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 $
-                              simplifyWantedsTcM clone_wanteds
-                              -- Discard evidence; result is zonked
-
-                      ; return [ ctEvPred ev | ct <- bagToList simples
-                                             , let ev = ctEvidence ct ] }
-
-       -- NB: quant_pred_candidates is already fully zonked
+       ; wanted_transformed_incl_derivs <- TcM.zonkWC wanted_transformed_incl_derivs
+       ; let definite_error = insolubleWC wanted_transformed_incl_derivs
+                              -- See Note [Quantification with errors]
+                              -- NB: must include derived errors in this test,
+                              --     hence "incl_derivs"
+             wanted_transformed = dropDerivedWC wanted_transformed_incl_derivs
+             quant_pred_candidates
+               | definite_error = []
+               | otherwise      = ctsPreds (approximateWC False wanted_transformed)
 
        -- Decide what type variables and constraints to quantify
+       -- NB: quant_pred_candidates is already fully zonked
        -- NB: bound_theta are constraints we want to quantify over,
-       --     /apart from/ the psig_theta, which we always quantify over
-       ; (qtvs, bound_theta) <- decideQuantification infer_mode name_taus psig_theta
+       --     including the psig_theta, which we always quantify over
+       -- NB: bound_theta are fully zonked
+       ; (qtvs, bound_theta, co_vars) <- decideQuantification infer_mode rhs_tclvl
+                                                     name_taus partial_sigs
                                                      quant_pred_candidates
-
-         -- Promote any type variables that are free in the inferred type
-         -- of the function:
-         --    f :: forall qtvs. bound_theta => zonked_tau
-         -- These variables now become free in the envt, and hence will show
-         -- up whenever 'f' is called.  They may currently at rhs_tclvl, but
-         -- they had better be unifiable at the outer_tclvl!
-         -- Example:   envt mentions alpha[1]
-         --            tau_ty = beta[2] -> beta[2]
-         --            constraints = alpha ~ [beta]
-         -- we don't quantify over beta (since it is fixed by envt)
-         -- so we must promote it!  The inferred type is just
-         --   f :: beta -> beta
-       ; zonked_taus <- mapM (TcM.zonkTcType . snd) name_taus
-              -- decideQuantification turned some meta tyvars into
-              -- quantified skolems, so we have to zonk again
-
-       ; let phi_tkvs = tyCoVarsOfTypes bound_theta  -- Already zonked
-                        `unionVarSet` tyCoVarsOfTypes zonked_taus
-             promote_tkvs = closeOverKinds phi_tkvs `delVarSetList` qtvs
-
-       ; MASSERT2( closeOverKinds promote_tkvs `subVarSet` promote_tkvs
-                 , ppr phi_tkvs $$
-                   ppr (closeOverKinds phi_tkvs) $$
-                   ppr promote_tkvs $$
-                   ppr (closeOverKinds promote_tkvs) )
-           -- we really don't want a type to be promoted when its kind isn't!
-
-           -- promoteTyVar ignores coercion variables
-       ; outer_tclvl <- TcM.getTcLevel
-       ; mapM_ (promoteTyVar outer_tclvl) (nonDetEltsUniqSet promote_tkvs)
-           -- It's OK to use nonDetEltsUniqSet here because promoteTyVar is
-           -- commutative
-
-           -- Emit an implication constraint for the
-           -- remaining constraints from the RHS
-           -- extra_qtvs: see Note [Quantification and partial signatures]
        ; bound_theta_vars <- mapM TcM.newEvVar bound_theta
-       ; psig_theta_vars  <- mapM zonkId psig_theta_vars
-       ; all_qtvs         <- add_psig_tvs qtvs
-                             [ tv | sig <- partial_sigs
-                                  , (_,tv) <- sig_inst_skols sig ]
-
-       ; let full_theta      = psig_theta      ++ bound_theta
-             full_theta_vars = psig_theta_vars ++ bound_theta_vars
-             skol_info   = InferSkol [ (name, mkSigmaTy [] full_theta ty)
-                                     | (name, ty) <- name_taus ]
-                        -- Don't add the quantified variables here, because
-                        -- they are also bound in ic_skols and we want them
-                        -- to be tidied uniformly
-
-             implic = Implic { ic_tclvl    = rhs_tclvl
-                             , ic_skols    = all_qtvs
-                             , ic_no_eqs   = False
-                             , ic_given    = full_theta_vars
-                             , ic_wanted   = wanted_transformed
-                             , ic_status   = IC_Unsolved
-                             , ic_binds    = ev_binds_var
-                             , ic_info     = skol_info
-                             , ic_needed   = emptyVarSet
-                             , ic_env      = tc_lcl_env }
-       ; emitImplication implic
+
+       -- We must produce bindings for the psig_theta_vars, because we may have
+       -- used them in evidence bindings constructed by solveWanteds earlier
+       -- Easiest way to do this is to emit them as new Wanteds (Trac #14643)
+       ; ct_loc <- getCtLocM AnnOrigin Nothing
+       ; let psig_wanted = [ CtWanted { ctev_pred = idType psig_theta_var
+                                      , ctev_dest = EvVarDest psig_theta_var
+                                      , ctev_nosh = WDeriv
+                                      , ctev_loc  = ct_loc }
+                           | psig_theta_var <- psig_theta_vars ]
+
+       -- Now construct the residual constraint
+       ; residual_wanted <- mkResidualConstraints rhs_tclvl tc_env ev_binds_var
+                                 name_taus co_vars qtvs bound_theta_vars
+                                 (wanted_transformed `andWC` mkSimpleWC psig_wanted)
 
          -- All done!
        ; traceTc "} simplifyInfer/produced residual implication for quantification" $
          vcat [ text "quant_pred_candidates =" <+> ppr quant_pred_candidates
-              , text "promote_tvs=" <+> ppr promote_tkvs
               , text "psig_theta =" <+> ppr psig_theta
               , text "bound_theta =" <+> ppr bound_theta
-              , text "full_theta =" <+> ppr full_theta
-              , text "qtvs =" <+> ppr qtvs
-              , text "implic =" <+> ppr implic ]
+              , text "qtvs ="       <+> ppr qtvs
+              , text "definite_error =" <+> ppr definite_error ]
+
+       ; return ( qtvs, bound_theta_vars, TcEvBinds ev_binds_var
+                , residual_wanted, definite_error ) }
+         -- NB: bound_theta_vars must be fully zonked
+
+
+--------------------
+mkResidualConstraints :: TcLevel -> Env TcGblEnv TcLclEnv -> EvBindsVar
+                      -> [(Name, TcTauType)]
+                      -> VarSet -> [TcTyVar] -> [EvVar]
+                      -> WantedConstraints -> TcM WantedConstraints
+-- Emit the remaining constraints from the RHS.
+-- See Note [Emitting the residual implication in simplifyInfer]
+mkResidualConstraints rhs_tclvl tc_env ev_binds_var
+                        name_taus co_vars qtvs full_theta_vars wanteds
+  | isEmptyWC wanteds
+  = return wanteds
+
+  | otherwise
+  = do { wanted_simple <- TcM.zonkSimples (wc_simple wanteds)
+       ; let (outer_simple, inner_simple) = partitionBag is_mono wanted_simple
+             is_mono ct = isWantedCt ct && ctEvId ct `elemVarSet` co_vars
+
+        ; _ <- promoteTyVarSet (tyCoVarsOfCts outer_simple)
 
-       ; return ( qtvs, full_theta_vars, TcEvBinds ev_binds_var ) }
+        ; let inner_wanted = wanteds { wc_simple = inner_simple }
+        ; return (WC { wc_simple = outer_simple
+                     , wc_impl   = mk_implic inner_wanted })}
   where
-    add_psig_tvs qtvs [] = return qtvs
-    add_psig_tvs qtvs (tv:tvs)
-      = do { tv <- zonkTcTyVarToTyVar tv
-           ; if tv `elem` qtvs
-             then add_psig_tvs qtvs tvs
-             else do { mb_tv <- zonkQuantifiedTyVar False tv
-                     ; case mb_tv of
-                         Nothing -> add_psig_tvs qtvs      tvs
-                         Just tv -> add_psig_tvs (tv:qtvs) tvs } }
-
-{- Note [Add signature contexts as givens]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+    mk_implic inner_wanted
+      | isEmptyWC inner_wanted
+      = emptyBag
+      | otherwise
+      = unitBag (implicationPrototype { ic_tclvl  = rhs_tclvl
+                                      , ic_skols  = qtvs
+                                      , ic_telescope = Nothing
+                                      , ic_given  = full_theta_vars
+                                      , ic_wanted = inner_wanted
+                                      , ic_binds  = ev_binds_var
+                                      , ic_no_eqs = False
+                                      , ic_info   = skol_info
+                                      , ic_env    = tc_env })
+
+    full_theta = map idType full_theta_vars
+    skol_info  = InferSkol [ (name, mkSigmaTy [] full_theta ty)
+                           | (name, ty) <- name_taus ]
+                 -- Don't add the quantified variables here, because
+                 -- they are also bound in ic_skols and we want them
+                 -- to be tidied uniformly
+
+--------------------
+ctsPreds :: Cts -> [PredType]
+ctsPreds cts = [ ctEvPred ev | ct <- bagToList cts
+                             , let ev = ctEvidence ct ]
+
+{- Note [Emitting the residual implication in simplifyInfer]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+   f = e
+where f's type is inferred to be something like (a, Proxy k (Int |> co))
+and we have an as-yet-unsolved, or perhaps insoluble, constraint
+   [W] co :: Type ~ k
+We can't form types like (forall co. blah), so we can't generalise over
+the coercion variable, and hence we can't generalise over things free in
+its kind, in the case 'k'.  But we can still generalise over 'a'.  So
+we'll generalise to
+   f :: forall a. (a, Proxy k (Int |> co))
+Now we do NOT want to form the residual implication constraint
+   forall a. [W] co :: Type ~ k
+because then co's eventual binding (which will be a value binding if we
+use -fdefer-type-errors) won't scope over the entire binding for 'f' (whose
+type mentions 'co').  Instead, just as we don't generalise over 'co', we
+should not bury its constraint inside the implication.  Instead, we must
+put it outside.
+
+That is the reason for the partitionBag in emitResidualConstraints,
+which takes the CoVars free in the inferred type, and pulls their
+constraints out.  (NB: this set of CoVars should be closed-over-kinds.)
+
+All rather subtle; see Trac #14584.
+
+Note [Add signature contexts as givens]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Consider this (Trac #11016):
   f2 :: (?x :: Int) => _
   f2 = ?x
@@ -780,138 +822,329 @@ Note [Deciding quantification]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 If the monomorphism restriction does not apply, then we quantify as follows:
 
-  * Take the global tyvars, and "grow" them using the equality constraints
-    E.g.  if x:alpha is in the environment, and alpha ~ [beta] (which can
+* Step 1. Take the global tyvars, and "grow" them using the equality
+  constraints
+     E.g.  if x:alpha is in the environment, and alpha ~ [beta] (which can
           happen because alpha is untouchable here) then do not quantify over
           beta, because alpha fixes beta, and beta is effectively free in
           the environment too
-    These are the mono_tvs
 
-  * Take the free vars of the tau-type (zonked_tau_tvs) and "grow" them
-    using all the constraints.  These are tau_tvs_plus
+  We also account for the monomorphism restriction; if it applies,
+  add the free vars of all the constraints.
+
+  Result is mono_tvs; we will not quantify over these.
+
+* Step 2. Default any non-mono tyvars (i.e ones that are definitely
+  not going to become further constrained), and re-simplify the
+  candidate constraints.
+
+  Motivation for re-simplification (Trac #7857): imagine we have a
+  constraint (C (a->b)), where 'a :: TYPE l1' and 'b :: TYPE l2' are
+  not free in the envt, and instance forall (a::*) (b::*). (C a) => C
+  (a -> b) The instance doesn't match while l1,l2 are polymorphic, but
+  it will match when we default them to LiftedRep.
+
+  This is all very tiresome.
+
+* Step 3: decide which variables to quantify over, as follows:
 
-  * Use quantifyTyVars to quantify over (tau_tvs_plus - mono_tvs), being
+  - Take the free vars of the tau-type (zonked_tau_tvs) and "grow"
+    them using all the constraints.  These are tau_tvs_plus
+
+  - Use quantifyTyVars to quantify over (tau_tvs_plus - mono_tvs), being
     careful to close over kinds, and to skolemise the quantified tyvars.
     (This actually unifies each quantifies meta-tyvar with a fresh skolem.)
-    Result is qtvs.
 
-  * Filter the constraints using pickQuantifiablePreds and the qtvs.
-    We have to zonk the constraints first, so they "see" the freshly
-    created skolems.
+  Result is qtvs.
 
-If the MR does apply, mono_tvs includes all the constrained tyvars --
-including all covars -- and the quantified constraints are empty/insoluble.
+* Step 4: Filter the constraints using pickQuantifiablePreds and the
+  qtvs. We have to zonk the constraints first, so they "see" the
+  freshly created skolems.
 
 -}
 
 decideQuantification
   :: InferMode
+  -> TcLevel
   -> [(Name, TcTauType)]   -- Variables to be generalised
-  -> [PredType]            -- All annotated constraints from signatures
+  -> [TcIdSigInst]         -- Partial type signatures (if any)
   -> [PredType]            -- Candidate theta; already zonked
   -> TcM ( [TcTyVar]       -- Quantify over these (skolems)
-         , [PredType] )    -- and this context (fully zonked)
+         , [PredType]      -- and this context (fully zonked)
+         , VarSet)
 -- See Note [Deciding quantification]
-decideQuantification infer_mode name_taus psig_theta candidates
-  = do { ovl_strings <- xoptM LangExt.OverloadedStrings
-       ; gbl_tvs     <- tcGetGlobalTyCoVars
-       ; let (gbl_cand, quant_cand)    -- gbl_cand   = do not quantify me
-                = case infer_mode of   -- quant_cand = try to quantify me
-                    ApplyMR         -> (candidates, [])
-                    NoRestrictions  -> ([], candidates)
-                    EagerDefaulting -> partition is_interactive_ct candidates
-                      where
-                        is_interactive_ct ct
-                          | Just (cls, _) <- getClassPredTys_maybe ct
-                          = isInteractiveClass ovl_strings cls
-                          | otherwise
-                          = False
-
-             eq_constraints  = filter isEqPred quant_cand
-             constrained_tvs = tyCoVarsOfTypes gbl_cand
-             mono_tvs        = growThetaTyVars eq_constraints $
-                               gbl_tvs `unionVarSet` constrained_tvs
-
-       ; zonked_taus <- mapM TcM.zonkTcType (psig_theta ++ taus)
-                        -- psig_theta: see Note [Quantification and partial signatures]
-
-       ; let -- The candidate tyvars are the ones free in
-             -- either quant_cand or zonked_taus.
-             DV {dv_kvs = cand_kvs, dv_tvs = cand_tvs}
-                = candidateQTyVarsOfTypes (quant_cand ++ zonked_taus)
-
-               -- Now keep only the ones reachable
-               -- (via growThetaTyVars) from zonked_taus.
-             grown_tvs = growThetaTyVars quant_cand (tyCoVarsOfTypes zonked_taus)
-             pick      = filterDVarSet (`elemVarSet` grown_tvs)
-             dvs_plus  = DV { dv_kvs = pick cand_kvs, dv_tvs = pick cand_tvs }
-
-       ; qtvs <- quantifyZonkedTyVars mono_tvs dvs_plus
-          -- We don't grow the kvs, as there's no real need to. Recall
-          -- that quantifyTyVars uses the separation between kvs and tvs
-          -- only for defaulting, and we don't want (ever) to default a tv
-          -- to *. So, don't grow the kvs.
-
-       ; quant_cand <- TcM.zonkTcTypes quant_cand
-                 -- quantifyTyVars turned some meta tyvars into
-                 -- quantified skolems, so we have to zonk again
-
-       ; let qtv_set   = mkVarSet qtvs
-             theta     = pickQuantifiablePreds qtv_set quant_cand
-             min_theta = mkMinimalBySCs theta
-               -- See Note [Minimize by Superclasses]
+decideQuantification infer_mode rhs_tclvl name_taus psigs candidates
+  = do { -- Step 1: find the mono_tvs
+       ; (mono_tvs, candidates, co_vars) <- decideMonoTyVars infer_mode
+                                              name_taus psigs candidates
+
+       -- Step 2: default any non-mono tyvars, and re-simplify
+       -- This step may do some unification, but result candidates is zonked
+       ; candidates <- defaultTyVarsAndSimplify rhs_tclvl mono_tvs candidates
+
+       -- Step 3: decide which kind/type variables to quantify over
+       ; qtvs <- decideQuantifiedTyVars mono_tvs name_taus psigs candidates
+
+       -- Step 4: choose which of the remaining candidate
+       --         predicates to actually quantify over
+       -- NB: decideQuantifiedTyVars turned some meta tyvars
+       -- into quantified skolems, so we have to zonk again
+       ; candidates <- TcM.zonkTcTypes candidates
+       ; psig_theta <- TcM.zonkTcTypes (concatMap sig_inst_theta psigs)
+       ; let quantifiable_candidates
+               = pickQuantifiablePreds (mkVarSet qtvs) candidates
+             -- NB: do /not/ run pickQuantifiablePreds over psig_theta,
+             -- because we always want to quantify over psig_theta, and not
+             -- drop any of them; e.g. CallStack constraints.  c.f Trac #14658
+
+             theta = mkMinimalBySCs id $  -- See Note [Minimize by Superclasses]
+                     (psig_theta ++ quantifiable_candidates)
+
+       ; traceTc "decideQuantification"
+           (vcat [ text "infer_mode:" <+> ppr infer_mode
+                 , text "candidates:" <+> ppr candidates
+                 , text "psig_theta:" <+> ppr psig_theta
+                 , text "mono_tvs:"   <+> ppr mono_tvs
+                 , text "co_vars:"    <+> ppr co_vars
+                 , text "qtvs:"       <+> ppr qtvs
+                 , text "theta:"      <+> ppr theta ])
+       ; return (qtvs, theta, co_vars) }
+
+------------------
+decideMonoTyVars :: InferMode
+                 -> [(Name,TcType)]
+                 -> [TcIdSigInst]
+                 -> [PredType]
+                 -> TcM (TcTyCoVarSet, [PredType], CoVarSet)
+-- Decide which tyvars and covars cannot be generalised:
+--   (a) Free in the environment
+--   (b) Mentioned in a constraint we can't generalise
+--   (c) Connected by an equality to (a) or (b)
+-- Also return CoVars that appear free in the final quatified types
+--   we can't quantify over these, and we must make sure they are in scope
+decideMonoTyVars infer_mode name_taus psigs candidates
+  = do { (no_quant, maybe_quant) <- pick infer_mode candidates
+
+       -- If possible, we quantify over partial-sig qtvs, so they are
+       -- not mono. Need to zonk them because they are meta-tyvar SigTvs
+       ; psig_qtvs <- mapM zonkTcTyVarToTyVar $
+                      concatMap (map snd . sig_inst_skols) psigs
+
+       ; psig_theta <- mapM TcM.zonkTcType $
+                       concatMap sig_inst_theta psigs
+
+       ; taus <- mapM (TcM.zonkTcType . snd) name_taus
+
+       ; mono_tvs0 <- tcGetGlobalTyCoVars
+       ; let psig_tys = mkTyVarTys psig_qtvs ++ psig_theta
+
+             co_vars = coVarsOfTypes (psig_tys ++ taus)
+             co_var_tvs = closeOverKinds co_vars
+               -- The co_var_tvs are tvs mentioned in the types of covars or
+               -- coercion holes. We can't quantify over these covars, so we
+               -- must include the variable in their types in the mono_tvs.
+               -- E.g.  If we can't quantify over co :: k~Type, then we can't
+               --       quantify over k either!  Hence closeOverKinds
+
+             mono_tvs1 = mono_tvs0 `unionVarSet` co_var_tvs
+
+             eq_constraints = filter isEqPred candidates
+             mono_tvs2      = growThetaTyVars eq_constraints mono_tvs1
+
+             constrained_tvs = (growThetaTyVars eq_constraints
+                                               (tyCoVarsOfTypes no_quant)
+                                `minusVarSet` mono_tvs2)
+                               `delVarSetList` psig_qtvs
+             -- constrained_tvs: the tyvars that we are not going to
+             -- quantify solely because of the moonomorphism restriction
+             --
+             -- (`minusVarSet` mono_tvs1`): a type variable is only
+             --   "constrained" (so that the MR bites) if it is not
+             --   free in the environment (Trac #13785)
+             --
+             -- (`delVarSetList` psig_qtvs): if the user has explicitly
+             --   asked for quantification, then that request "wins"
+             --   over the MR.  Note: do /not/ delete psig_qtvs from
+             --   mono_tvs1, because mono_tvs1 cannot under any circumstances
+             --   be quantified (Trac #14479); see
+             --   Note [Quantification and partial signatures], Wrinkle 3, 4
+
+             mono_tvs = mono_tvs2 `unionVarSet` constrained_tvs
 
            -- Warn about the monomorphism restriction
        ; warn_mono <- woptM Opt_WarnMonomorphism
-       ; let mr_bites | ApplyMR <- infer_mode
-                      = constrained_tvs `intersectsVarSet` grown_tvs
-                      | otherwise
-                      = False
-       ; warnTc (Reason Opt_WarnMonomorphism) (warn_mono && mr_bites) $
-         hang (text "The Monomorphism Restriction applies to the binding"
-               <> plural bndrs <+> text "for" <+> pp_bndrs)
-             2 (text "Consider giving a type signature for"
-                <+> if isSingleton bndrs then pp_bndrs
-                                         else text "these binders")
+       ; when (case infer_mode of { ApplyMR -> warn_mono; _ -> False}) $
+         warnTc (Reason Opt_WarnMonomorphism)
+                (constrained_tvs `intersectsVarSet` tyCoVarsOfTypes taus)
+                mr_msg
+
+       ; traceTc "decideMonoTyVars" $ vcat
+           [ text "mono_tvs0 =" <+> ppr mono_tvs0
+           , text "mono_tvs1 =" <+> ppr mono_tvs1
+           , text "no_quant =" <+> ppr no_quant
+           , text "maybe_quant =" <+> ppr maybe_quant
+           , text "eq_constraints =" <+> ppr eq_constraints
+           , text "mono_tvs =" <+> ppr mono_tvs
+           , text "co_vars =" <+> ppr co_vars ]
+
+       ; return (mono_tvs, maybe_quant, co_vars) }
+  where
+    pick :: InferMode -> [PredType] -> TcM ([PredType], [PredType])
+    -- Split the candidates into ones we definitely
+    -- won't quantify, and ones that we might
+    pick NoRestrictions  cand = return ([], cand)
+    pick ApplyMR         cand = return (cand, [])
+    pick EagerDefaulting cand = do { os <- xoptM LangExt.OverloadedStrings
+                                   ; return (partition (is_int_ct os) cand) }
+
+    -- For EagerDefaulting, do not quantify over
+    -- over any interactive class constraint
+    is_int_ct ovl_strings pred
+      | Just (cls, _) <- getClassPredTys_maybe pred
+      = isInteractiveClass ovl_strings cls
+      | otherwise
+      = False
 
-       ; traceTc "decideQuantification"
-           (vcat [ text "infer_mode:"   <+> ppr infer_mode
-                 , text "gbl_cand:"     <+> ppr gbl_cand
-                 , text "quant_cand:"   <+> ppr quant_cand
-                 , text "gbl_tvs:"      <+> ppr gbl_tvs
-                 , text "mono_tvs:"     <+> ppr mono_tvs
-                 , text "cand_tvs"      <+> ppr cand_tvs
-                 , text "grown_tvs:"    <+> ppr grown_tvs
-                 , text "qtvs:"         <+> ppr qtvs
-                 , text "min_theta:"    <+> ppr min_theta ])
-       ; return (qtvs, min_theta) }
+    pp_bndrs = pprWithCommas (quotes . ppr . fst) name_taus
+    mr_msg =
+         hang (sep [ text "The Monomorphism Restriction applies to the binding"
+                     <> plural name_taus
+                   , text "for" <+> pp_bndrs ])
+            2 (hsep [ text "Consider giving"
+                    , text (if isSingleton name_taus then "it" else "them")
+                    , text "a type signature"])
+
+-------------------
+defaultTyVarsAndSimplify :: TcLevel
+                         -> TyCoVarSet
+                         -> [PredType]          -- Assumed zonked
+                         -> TcM [PredType]      -- Guaranteed zonked
+-- Default any tyvar free in the constraints,
+-- and re-simplify in case the defaulting allows further simplification
+defaultTyVarsAndSimplify rhs_tclvl mono_tvs candidates
+  = do {  -- Promote any tyvars that we cannot generalise
+          -- See Note [Promote momomorphic tyvars]
+       ; traceTc "decideMonoTyVars: promotion:" (ppr mono_tvs)
+       ; prom <- promoteTyVarSet mono_tvs
+
+       -- Default any kind/levity vars
+       ; let DV {dv_kvs = cand_kvs, dv_tvs = cand_tvs}
+                = candidateQTyVarsOfTypes candidates
+       ; poly_kinds  <- xoptM LangExt.PolyKinds
+       ; default_kvs <- mapM (default_one poly_kinds True)
+                             (dVarSetElems cand_kvs)
+       ; default_tvs <- mapM (default_one poly_kinds False)
+                             (dVarSetElems (cand_tvs `minusDVarSet` cand_kvs))
+       ; let some_default = or default_kvs || or default_tvs
+
+       ; case () of
+           _ | some_default -> simplify_cand candidates
+             | prom         -> mapM TcM.zonkTcType candidates
+             | otherwise    -> return candidates
+       }
   where
-    pp_bndrs = pprWithCommas (quotes . ppr) bndrs
-    (bndrs, taus) = unzip name_taus
+    default_one poly_kinds is_kind_var tv
+      | not (isMetaTyVar tv)
+      = return False
+      | tv `elemVarSet` mono_tvs
+      = return False
+      | otherwise
+      = defaultTyVar (not poly_kinds && is_kind_var) tv
+
+    simplify_cand candidates
+      = do { clone_wanteds <- newWanteds DefaultOrigin candidates
+           ; WC { wc_simple = simples } <- setTcLevel rhs_tclvl $
+                                           simplifyWantedsTcM clone_wanteds
+              -- Discard evidence; simples is fully zonked
+
+           ; let new_candidates = ctsPreds simples
+           ; traceTc "Simplified after defaulting" $
+                      vcat [ text "Before:" <+> ppr candidates
+                           , text "After:"  <+> ppr new_candidates ]
+           ; return new_candidates }
+
+------------------
+decideQuantifiedTyVars
+   :: TyCoVarSet        -- Monomorphic tyvars
+   -> [(Name,TcType)]   -- Annotated theta and (name,tau) pairs
+   -> [TcIdSigInst]     -- Partial signatures
+   -> [PredType]        -- Candidates, zonked
+   -> TcM [TyVar]
+-- Fix what tyvars we are going to quantify over, and quantify them
+decideQuantifiedTyVars mono_tvs name_taus psigs candidates
+  = do {     -- Why psig_tys? We try to quantify over everything free in here
+             -- See Note [Quantification and partial signatures]
+             --     Wrinkles 2 and 3
+       ; psig_tv_tys <- mapM TcM.zonkTcTyVar [ tv | sig <- psigs
+                                                  , (_,tv) <- sig_inst_skols sig ]
+       ; psig_theta <- mapM TcM.zonkTcType [ pred | sig <- psigs
+                                                  , pred <- sig_inst_theta sig ]
+       ; tau_tys  <- mapM (TcM.zonkTcType . snd) name_taus
+       ; mono_tvs <- TcM.zonkTyCoVarsAndFV mono_tvs
+
+       ; let -- Try to quantify over variables free in these types
+             psig_tys = psig_tv_tys ++ psig_theta
+             seed_tys = psig_tys ++ tau_tys
+
+             -- Now "grow" those seeds to find ones reachable via 'candidates'
+             grown_tcvs = growThetaTyVars candidates (tyCoVarsOfTypes seed_tys)
+
+       -- Now we have to classify them into kind variables and type variables
+       -- (sigh) just for the benefit of -XNoPolyKinds; see quantifyTyVars
+       --
+       -- Keep the psig_tys first, so that candidateQTyVarsOfTypes produces
+       -- them in that order, so that the final qtvs quantifies in the same
+       -- order as the partial signatures do (Trac #13524)
+       ; let DV {dv_kvs = cand_kvs, dv_tvs = cand_tvs}
+                      = candidateQTyVarsOfTypes $
+                        psig_tys ++ candidates ++ tau_tys
+             pick     = (`dVarSetIntersectVarSet` grown_tcvs)
+             dvs_plus = DV { dv_kvs = pick cand_kvs, dv_tvs = pick cand_tvs }
+
+       ; traceTc "decideQuantifiedTyVars" (vcat
+           [ text "seed_tys =" <+> ppr seed_tys
+           , text "seed_tcvs =" <+> ppr (tyCoVarsOfTypes seed_tys)
+           , text "grown_tcvs =" <+> ppr grown_tcvs])
+
+       ; quantifyTyVars mono_tvs dvs_plus }
 
 ------------------
-growThetaTyVars :: ThetaType -> TyCoVarSet -> TyVarSet
+growThetaTyVars :: ThetaType -> TyCoVarSet -> TyCoVarSet
 -- See Note [Growing the tau-tvs using constraints]
--- NB: only returns tyvars, never covars
-growThetaTyVars theta tvs
-  | null theta = tvs_only
-  | otherwise  = filterVarSet isTyVar $
-                 transCloVarSet mk_next seed_tvs
+growThetaTyVars theta tcvs
+  | null theta = tcvs
+  | otherwise  = transCloVarSet mk_next seed_tcvs
   where
-    tvs_only = filterVarSet isTyVar tvs
-    seed_tvs = tvs `unionVarSet` tyCoVarsOfTypes ips
+    seed_tcvs = tcvs `unionVarSet` tyCoVarsOfTypes ips
     (ips, non_ips) = partition isIPPred theta
                          -- See Note [Inheriting implicit parameters] in TcType
 
     mk_next :: VarSet -> VarSet -- Maps current set to newly-grown ones
     mk_next so_far = foldr (grow_one so_far) emptyVarSet non_ips
-    grow_one so_far pred tvs
-       | pred_tvs `intersectsVarSet` so_far = tvs `unionVarSet` pred_tvs
-       | otherwise                          = tvs
+    grow_one so_far pred tcvs
+       | pred_tcvs `intersectsVarSet` so_far = tcvs `unionVarSet` pred_tcvs
+       | otherwise                           = tcvs
        where
-         pred_tvs = tyCoVarsOfType pred
+         pred_tcvs = tyCoVarsOfType pred
+
 
-{- Note [Quantification and partial signatures]
+{- Note [Promote momomorphic tyvars]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Promote any type variables that are free in the environment.  Eg
+   f :: forall qtvs. bound_theta => zonked_tau
+The free vars of f's type become free in the envt, and hence will show
+up whenever 'f' is called.  They may currently at rhs_tclvl, but they
+had better be unifiable at the outer_tclvl!  Example: envt mentions
+alpha[1]
+           tau_ty = beta[2] -> beta[2]
+           constraints = alpha ~ [beta]
+we don't quantify over beta (since it is fixed by envt)
+so we must promote it!  The inferred type is just
+  f :: beta -> beta
+
+NB: promoteTyVar ignores coercion variables
+
+Note [Quantification and partial signatures]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 When choosing type variables to quantify, the basic plan is to
 quantify over all type variables that are
@@ -925,24 +1158,19 @@ However, in the case of a partial type signature, be doing inference
    f x = ...
 or
    g :: (Eq _a) => _b -> _b
-In both cases we use plan InferGen, and hence call simplifyInfer.
-But those 'a' variables are skolems, and we should be sure to quantify
-over them, for two reasons
+In both cases we use plan InferGen, and hence call simplifyInfer.  But
+those 'a' variables are skolems (actually SigTvs), and we should be
+sure to quantify over them.  This leads to several wrinkles:
 
-* In the case of a type error
+* Wrinkle 1.  In the case of a type error
      f :: _ -> Maybe a
      f x = True && x
   The inferred type of 'f' is f :: Bool -> Bool, but there's a
   left-over error of form (HoleCan (Maybe a ~ Bool)).  The error-reporting
   machine expects to find a binding site for the skolem 'a', so we
-  add it to the ic_skols of the residual implication.
-
-  Note that we /only/ do this to the residual implication. We don't
-  complicate the quantified type variables of 'f' for downstream code;
-  it's just a device to make the error message generator know what to
-  report.
+  add it to the quantified tyvars.
 
-* Consider the partial type signature
+* Wrinkle 2.  Consider the partial type signature
      f :: (Eq _) => Int -> Int
      f x = x
   In normal cases that makes sense; e.g.
@@ -955,9 +1183,29 @@ over them, for two reasons
   (thereby correctly triggering an ambiguity error later).  If we don't
   we'll end up with a strange open type
      f :: Eq alpha => Int -> Int
-  which isn't ambiguous but is still very wrong.  That's why include
-  psig_theta in the variables to quantify over, passed to
-  decideQuantification.
+  which isn't ambiguous but is still very wrong.
+
+  Bottom line: Try to quantify over any variable free in psig_theta,
+  just like the tau-part of the type.
+
+* Wrinkle 3 (Trac #13482). Also consider
+    f :: forall a. _ => Int -> Int
+    f x = if (undefined :: a) == undefined then x else 0
+  Here we get an (Eq a) constraint, but it's not mentioned in the
+  psig_theta nor the type of 'f'.  But we still want to quantify
+  over 'a' even if the monomorphism restriction is on.
+
+* Wrinkle 4 (Trac #14479)
+    foo :: Num a => a -> a
+    foo xxx = g xxx
+      where
+        g :: forall b. Num b => _ -> b
+        g y = xxx + y
+
+  In the signature for 'g', we cannot quantify over 'b' because it turns out to
+  get unified with 'a', which is free in g's environment.  So we carefully
+  refrain from bogusly quantifying, in TcSimplify.decideMonoTyVars.  We
+  report the error later, in TcBinds.chooseInferredQuantifiers.
 
 Note [Quantifying over equality constraints]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -987,13 +1235,33 @@ Notice that
 Note [Quantification with errors]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 If we find that the RHS of the definition has some absolutely-insoluble
-constraints, we abandon all attempts to find a context to quantify
-over, and instead make the function fully-polymorphic in whatever
-type we have found.  For two reasons
-  a) Minimise downstream errors
-  b) Avoid spurious errors from this function
-
-But NB that we must include *derived* errors in the check. Example:
+constraints (including especially "variable not in scope"), we
+
+* Abandon all attempts to find a context to quantify over,
+  and instead make the function fully-polymorphic in whatever
+  type we have found
+
+* Return a flag from simplifyInfer, indicating that we found an
+  insoluble constraint.  This flag is used to suppress the ambiguity
+  check for the inferred type, which may well be bogus, and which
+  tends to obscure the real error.  This fix feels a bit clunky,
+  but I failed to come up with anything better.
+
+Reasons:
+    - Avoid downstream errors
+    - Do not perform an ambiguity test on a bogus type, which might well
+      fail spuriously, thereby obfuscating the original insoluble error.
+      Trac #14000 is an example
+
+I tried an alternative approach: simply failM, after emitting the
+residual implication constraint; the exception will be caught in
+TcBinds.tcPolyBinds, which gives all the binders in the group the type
+(forall a. a).  But that didn't work with -fdefer-type-errors, because
+the recovery from failM emits no code at all, so there is no function
+to run!   But -fdefer-type-errors aspires to produce a runnable program.
+
+NB that we must include *derived* errors in the check for insolubles.
+Example:
     (a::*) ~ Int#
 We get an insoluble derived error *~#, and we don't want to discard
 it before doing the isInsolubleWC test!  (Trac #8262)
@@ -1099,39 +1367,31 @@ solveWantedsAndDrop wanted
 solveWanteds :: WantedConstraints -> TcS WantedConstraints
 -- so that the inert set doesn't mindlessly propagate.
 -- NB: wc_simples may be wanted /or/ derived now
-solveWanteds wc@(WC { wc_simple = simples, wc_insol = insols, wc_impl = implics })
+solveWanteds wc@(WC { wc_simple = simples, wc_impl = implics })
   = do { traceTcS "solveWanteds {" (ppr wc)
 
        ; wc1 <- solveSimpleWanteds simples
-       ; 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
+                -- Any insoluble constraints are in 'simples' and so get rewritten
+                -- See Note [Rewrite insolubles] in TcSMonad
 
-       ; traceTcS "solveWanteds middle" $ vcat [ text "simples1 =" <+> ppr simples1
-                                               , text "simples2 =" <+> ppr simples2 ]
+       ; (floated_eqs, implics2) <- solveNestedImplications $
+                                    implics `unionBags` wc_impl wc1
 
-       ; dflags <- getDynFlags
+       ; dflags   <- getDynFlags
        ; final_wc <- simpl_loop 0 (solverIterations dflags) floated_eqs
-                                no_new_scs
-                                (WC { wc_simple = simples2, wc_impl = implics2
-                                    , wc_insol  = insols `unionBags` insols1 })
+                                (wc1 { wc_impl = implics2 })
 
-       ; bb <- TcS.getTcEvBindsMap
+       ; ev_binds_var <- getTcEvBindsVar
+       ; bb <- TcS.getTcEvBindsMap ev_binds_var
        ; traceTcS "solveWanteds }" $
                  vcat [ text "final wc =" <+> ppr final_wc
                       , text "current evbinds  =" <+> ppr (evBindMapBinds bb) ]
 
        ; return final_wc }
 
-simpl_loop :: Int -> IntWithInf -> Cts -> Bool
-           -> WantedConstraints
-           -> TcS WantedConstraints
-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_deriveds
-  = return wc  -- Done!
-
+simpl_loop :: Int -> IntWithInf -> Cts
+           -> WantedConstraints -> TcS WantedConstraints
+simpl_loop n limit floated_eqs wc@(WC { wc_simple = simples })
   | n `intGtLimit` limit
   = do { -- Add an error (not a warning) if we blow the limit,
          -- Typically if we blow the limit we are going to report some other error
@@ -1142,69 +1402,67 @@ simpl_loop n limit floated_eqs no_new_deriveds
                 2 (vcat [ text "Unsolved:" <+> ppr wc
                         , ppUnless (isEmptyBag floated_eqs) $
                           text "Floated equalities:" <+> ppr floated_eqs
-                        , ppUnless no_new_deriveds $
-                          text "New deriveds found"
                         , text "Set limit with -fconstraint-solver-iterations=n; n=0 for no limit"
                   ]))
        ; return wc }
 
+  | not (isEmptyBag floated_eqs)
+  = simplify_again n limit True (wc { wc_simple = floated_eqs `unionBags` simples })
+            -- Put floated_eqs first so they get solved first
+            -- NB: the floated_eqs may include /derived/ equalities
+            -- arising from fundeps inside an implication
+
+  | superClassesMightHelp wc
+  = -- We still have unsolved goals, and apparently no way to solve them,
+    -- so try expanding superclasses at this level, both Given and Wanted
+    do { pending_given <- getPendingGivenScs
+       ; let (pending_wanted, simples1) = getPendingWantedScs simples
+       ; if null pending_given && null pending_wanted
+           then return wc  -- After all, superclasses did not help
+           else
+    do { new_given  <- makeSuperClasses pending_given
+       ; new_wanted <- makeSuperClasses pending_wanted
+       ; solveSimpleGivens new_given -- Add the new Givens to the inert set
+       ; simplify_again n limit (null pending_given)
+         wc { wc_simple = simples1 `unionBags` listToBag new_wanted } } }
+
   | otherwise
-  = do { let n_floated = lengthBag floated_eqs
-       ; csTraceTcS $
+  = return wc
+
+simplify_again :: Int -> IntWithInf -> Bool
+               -> WantedConstraints -> TcS WantedConstraints
+-- We have definitely decided to have another go at solving
+-- the wanted constraints (we have tried at least once already
+simplify_again n limit no_new_given_scs
+               wc@(WC { wc_simple = simples, wc_impl = implics })
+  = do { csTraceTcS $
          text "simpl_loop iteration=" <> int n
-         <+> (parens $ hsep [ text "no new deriveds =" <+> ppr no_new_deriveds <> comma
-                            , int n_floated <+> text "floated eqs" <> comma
+         <+> (parens $ hsep [ text "no new given superclasses =" <+> ppr no_new_given_scs <> comma
                             , int (lengthBag simples) <+> text "simples to solve" ])
+       ; traceTcS "simpl_loop: wc =" (ppr wc)
 
-       -- solveSimples may make progress if either float_eqs hold
        ; (unifs1, wc1) <- reportUnifications $
-                          solveSimpleWanteds (floated_eqs `unionBags` simples)
-                               -- Put floated_eqs first so they get solved first
-                               -- NB: the floated_eqs may include /derived/ equalities
-                               --     arising from fundeps inside an implication
-
-       ; let WC { wc_simple = simples1, wc_insol = insols1, wc_impl = implics1 } = wc1
-       ; (no_new_scs, simples2) <- expandSuperClasses simples1
+                          solveSimpleWanteds $
+                          simples
 
+       -- See Note [Cutting off simpl_loop]
        -- We have already tried to solve the nested implications once
        -- Try again only if we have unified some meta-variables
-       -- (which is a bit like adding more givens
-       -- See Note [Cutting off simpl_loop]
-       ; (floated_eqs2, implics2) <- if unifs1 == 0 && isEmptyBag implics1
-                                     then return (emptyBag, implics)
-                                     else solveNestedImplications (implics `unionBags` implics1)
-
-       ; simpl_loop (n+1) limit floated_eqs2 no_new_scs
-                    (WC { wc_simple = simples2, wc_impl = implics2
-                        , wc_insol  = insols `unionBags` insols1 }) }
-
-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 unsolved
-  | not (anyBag superClassesMightHelp unsolved)
-  = return (True, unsolved)
-  | otherwise
-  = do { traceTcS "expandSuperClasses {" empty
-       ; let (pending_wanted, unsolved') = mapAccumBagL get [] unsolved
-             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, unsolved) }
-         else
-    do { new_given  <- makeSuperClasses pending_given
-       ; solveSimpleGivens new_given
-       ; new_wanted <- makeSuperClasses pending_wanted
-       ; traceTcS "End expandSuperClasses }"
-                  (vcat [ text "Given:" <+> ppr pending_given
-                        , text "Wanted:" <+> ppr new_wanted ])
-       ; return (False, unsolved' `unionBags` listToBag new_wanted) } }
+       -- (which is a bit like adding more givens), or we have some
+       -- new Given superclasses
+       ; let new_implics = wc_impl wc1
+       ; if unifs1 == 0       &&
+            no_new_given_scs  &&
+            isEmptyBag new_implics
+
+           then -- Do not even try to solve the implications
+                simpl_loop (n+1) limit emptyBag (wc1 { wc_impl = implics })
+
+           else -- Try to solve the implications
+                do { (floated_eqs2, implics2) <- solveNestedImplications $
+                                                 implics `unionBags` new_implics
+                   ; simpl_loop (n+1) limit floated_eqs2 (wc1 { wc_impl = implics2 })
+    } }
 
 solveNestedImplications :: Bag Implication
                         -> TcS (Cts, Bag Implication)
@@ -1238,8 +1496,7 @@ solveImplication imp@(Implic { ic_tclvl  = tclvl
                              , ic_given  = given_ids
                              , ic_wanted = wanteds
                              , ic_info   = info
-                             , ic_status = status
-                             , ic_env    = env })
+                             , ic_status = status })
   | isSolvedStatus status
   = return (emptyCts, Just imp)  -- Do nothing
 
@@ -1250,10 +1507,12 @@ solveImplication imp@(Implic { ic_tclvl  = tclvl
   = do { inerts <- getTcSInerts
        ; traceTcS "solveImplication {" (ppr imp $$ text "Inerts" <+> ppr inerts)
 
+       ; when debugIsOn check_tc_level
+
          -- Solve the nested constraints
        ; (no_given_eqs, given_insols, residual_wanted)
             <- nestImplicTcS ev_binds_var tclvl $
-               do { let loc    = mkGivenLoc tclvl info env
+               do { let loc    = mkGivenLoc tclvl info (implicLclEnv imp)
                         givens = mkGivens loc given_ids
                   ; solveSimpleGivens givens
 
@@ -1270,16 +1529,20 @@ solveImplication imp@(Implic { ic_tclvl  = tclvl
                   ; return (no_eqs, given_insols, residual_wanted) }
 
        ; (floated_eqs, residual_wanted)
-             <- floatEqualities skols no_given_eqs residual_wanted
+             <- floatEqualities skols given_ids ev_binds_var
+                                no_given_eqs residual_wanted
 
        ; traceTcS "solveImplication 2"
            (ppr given_insols $$ ppr residual_wanted)
        ; let final_wanted = residual_wanted `addInsols` given_insols
+             -- Don't lose track of the insoluble givens,
+             -- which signal unreachable code; put them in ic_wanted
 
        ; res_implic <- setImplicationStatus (imp { ic_no_eqs = no_given_eqs
                                                  , ic_wanted = final_wanted })
 
-       ; (evbinds, tcvs) <- TcS.getTcEvBindsAndTCVs ev_binds_var
+       ; evbinds <- TcS.getTcEvBindsMap ev_binds_var
+       ; tcvs    <- TcS.getTcEvTyCoVars ev_binds_var
        ; traceTcS "solveImplication end }" $ vcat
              [ text "no_given_eqs =" <+> ppr no_given_eqs
              , text "floated_eqs =" <+> ppr floated_eqs
@@ -1289,6 +1552,15 @@ solveImplication imp@(Implic { ic_tclvl  = tclvl
 
        ; return (floated_eqs, res_implic) }
 
+  where
+    -- TcLevels must be strictly increasing (see (ImplicInv) in
+    -- Note [TcLevel and untouchable type variables] in TcType),
+    -- and in fact I thinkthey should always increase one level at a time.
+    check_tc_level = do { cur_lvl <- TcS.getTcLevel
+                        ; MASSERT2( tclvl == pushTcLevel cur_lvl
+                                  , text "Cur lvl =" <+> ppr cur_lvl $$
+                                    text "Imp lvl =" <+> ppr tclvl ) }
+
 ----------------------
 setImplicationStatus :: Implication -> TcS (Maybe Implication)
 -- Finalise the implication returned from solveImplication:
@@ -1296,99 +1568,101 @@ setImplicationStatus :: Implication -> TcS (Maybe Implication)
 --    * Trim the ic_wanted field to remove Derived constraints
 -- Precondition: the ic_status field is not already IC_Solved
 -- Return Nothing if we can discard the implication altogether
-setImplicationStatus implic@(Implic { ic_binds  = ev_binds_var
-                                    , ic_status = status
-                                    , ic_info   = info
-                                    , ic_wanted = wc
-                                    , ic_needed = old_discarded_needs
-                                    , ic_given  = givens })
+setImplicationStatus implic@(Implic { ic_status     = status
+                                    , ic_info       = info
+                                    , ic_wanted     = wc
+                                    , ic_given      = givens })
  | ASSERT2( not (isSolvedStatus status ), ppr info )
    -- Precondition: we only set the status if it is not already solved
-   some_insoluble
- = return $ Just $
-   implic { ic_status = IC_Insoluble
-          , ic_needed = new_discarded_needs
-          , ic_wanted = pruned_wc }
-
- | some_unsolved
- = do { traceTcS "setImplicationStatus" $
-        vcat [ppr givens $$ ppr simples $$ ppr insols $$ ppr mb_implic_needs]
-      ; return $ Just $
-        implic { ic_status = IC_Unsolved
-               , ic_needed = new_discarded_needs
-               , ic_wanted = pruned_wc }
-   }
-
- | otherwise  -- Everything is solved; look at the implications
+   not (isSolvedWC pruned_wc)
+ = do { traceTcS "setImplicationStatus(not-all-solved) {" (ppr implic)
+
+      ; implic <- neededEvVars implic
+
+      ; let new_status | insolubleWC pruned_wc = IC_Insoluble
+                       | otherwise             = IC_Unsolved
+            new_implic = implic { ic_status = new_status
+                                , ic_wanted = pruned_wc }
+
+      ; traceTcS "setImplicationStatus(not-all-solved) }" (ppr new_implic)
+
+      ; return $ Just new_implic }
+
+ | otherwise  -- Everything is solved
+              -- Set status to IC_Solved,
+              -- and compute the dead givens and outer needs
               -- See Note [Tracking redundant constraints]
- = do { ev_binds <- TcS.getTcEvBindsAndTCVs ev_binds_var
-      ; let all_needs = neededEvVars ev_binds $
-                        solved_implic_needs `unionVarSet` new_discarded_needs
+ = do { traceTcS "setImplicationStatus(all-solved) {" (ppr implic)
 
-            dead_givens | warnRedundantGivens info
-                        = filterOut (`elemVarSet` all_needs) givens
-                        | otherwise = []   -- None to report
+      ; implic@(Implic { ic_need_inner = need_inner
+                       , ic_need_outer = need_outer }) <- neededEvVars implic
+
+      ; bad_telescope <- checkBadTelescope implic
 
-            final_needs = all_needs `delVarSetList` givens
+      ; let dead_givens | warnRedundantGivens info
+                        = filterOut (`elemVarSet` need_inner) givens
+                        | otherwise = []   -- None to report
 
             discard_entire_implication  -- Can we discard the entire implication?
               =  null dead_givens           -- No warning from this implication
-              && isEmptyBag pruned_implics  -- No live children
-              && isEmptyVarSet final_needs  -- No needed vars to pass up to parent
+              && not bad_telescope
+              && isEmptyWC pruned_wc        -- No live children
+              && isEmptyVarSet need_outer   -- No needed vars to pass up to parent
 
-            final_status = IC_Solved { ics_need = final_needs
-                                     , ics_dead = dead_givens }
+            final_status
+              | bad_telescope = IC_BadTelescope
+              | otherwise     = IC_Solved { ics_dead = dead_givens }
             final_implic = implic { ic_status = final_status
-                                  , ic_needed = emptyVarSet -- Irrelevant for IC_Solved
                                   , ic_wanted = pruned_wc }
 
-        -- Check that there are no term-level evidence bindings
-        -- in the cases where we have no place to put them
-      ; MASSERT2( termEvidenceAllowed info || isEmptyEvBindMap (fst ev_binds)
-                , ppr info $$ ppr ev_binds )
+      ; traceTcS "setImplicationStatus(all-solved) }" $
+        vcat [ text "discard:" <+> ppr discard_entire_implication
+             , text "new_implic:" <+> ppr final_implic ]
 
-      ; traceTcS "setImplicationStatus 2" $
-        vcat [ppr givens $$ ppr ev_binds $$ ppr all_needs]
       ; return $ if discard_entire_implication
                  then Nothing
                  else Just final_implic }
  where
-   WC { wc_simple = simples, wc_impl = implics, wc_insol = insols } = wc
-
-   some_insoluble = insolubleWC wc
-   some_unsolved = not (isEmptyBag simples && isEmptyBag insols)
-                 || isNothing mb_implic_needs
+   WC { wc_simple = simples, wc_impl = implics } = wc
 
    pruned_simples = dropDerivedSimples simples
-   pruned_insols  = dropDerivedInsols insols
-   (pruned_implics, discarded_needs) = partitionBagWith discard_me implics
-   pruned_wc = wc { wc_simple = pruned_simples
-                  , wc_insol  = pruned_insols
+   pruned_implics = filterBag keep_me implics
+   pruned_wc = WC { wc_simple = pruned_simples
                   , wc_impl   = pruned_implics }
-   new_discarded_needs = foldrBag unionVarSet old_discarded_needs discarded_needs
-
-   mb_implic_needs :: Maybe VarSet
-        -- Just vs => all implics are IC_Solved, with 'vs' needed
-        -- Nothing => at least one implic is not IC_Solved
-   mb_implic_needs   = foldrBag add_implic (Just emptyVarSet) pruned_implics
-   Just solved_implic_needs = mb_implic_needs
-
-   add_implic implic acc
-      | Just vs_acc <- acc
-      , IC_Solved { ics_need = vs } <- ic_status implic
-      = Just (vs `unionVarSet` vs_acc)
-      | otherwise = Nothing
-
-   discard_me :: Implication -> Either Implication VarSet
-   discard_me ic
-     | IC_Solved { ics_dead = dead_givens, ics_need = needed } <- ic_status ic
+
+   keep_me :: Implication -> Bool
+   keep_me ic
+     | IC_Solved { ics_dead = dead_givens } <- ic_status ic
                           -- Fully solved
      , null dead_givens   -- No redundant givens to report
      , isEmptyBag (wc_impl (ic_wanted ic))
            -- And no children that might have things to report
-     = Right needed
+     = False       -- Tnen we don't need to keep it
      | otherwise
-     = Left ic
+     = True        -- Otherwise, keep it
+
+checkBadTelescope :: Implication -> TcS Bool
+-- True <=> the skolems form a bad telescope
+-- See Note [Keeping scoped variables in order: Explicit] in TcHsType
+checkBadTelescope (Implic { ic_telescope  = m_telescope
+                          , ic_skols      = skols })
+  | isJust m_telescope
+  = do{ skols <- mapM TcS.zonkTcTyCoVarBndr skols
+      ; return (go emptyVarSet (reverse skols))}
+
+  | otherwise
+  = return False
+
+  where
+    go :: TyVarSet   -- skolems that appear *later* than the current ones
+       -> [TcTyVar]  -- ordered skolems, in reverse order
+       -> Bool       -- True <=> there is an out-of-order skolem
+    go _ [] = False
+    go later_skols (one_skol : earlier_skols)
+      | tyCoVarsOfType (tyVarKind one_skol) `intersectsVarSet` later_skols
+      = True
+      | otherwise
+      = go (later_skols `extendVarSet` one_skol) earlier_skols
 
 warnRedundantGivens :: SkolemInfo -> Bool
 warnRedundantGivens (SigSkol ctxt _ _)
@@ -1402,41 +1676,109 @@ warnRedundantGivens (SigSkol ctxt _ _)
 warnRedundantGivens (InstSkol {}) = True
 warnRedundantGivens _             = False
 
-neededEvVars :: (EvBindMap, TcTyVarSet) -> VarSet -> VarSet
+neededEvVars :: Implication -> TcS Implication
 -- Find all the evidence variables that are "needed",
---    and then delete all those bound by the evidence bindings
--- See Note [Tracking redundant constraints]
-neededEvVars (ev_binds, tcvs) initial_seeds
- = (needed `unionVarSet` tcvs) `minusVarSet` bndrs
+-- and delete dead evidence bindings
+--   See Note [Tracking redundant constraints]
+--   See Note [Delete dead Given evidence bindings]
+--
+--   - Start from initial_seeds (from nested implications)
+--
+--   - Add free vars of RHS of all Wanted evidence bindings
+--     and coercion variables accumulated in tcvs (all Wanted)
+--
+--   - Generate 'needed', the needed set of EvVars, by doing transitive
+--     closure through Given bindings
+--     e.g.   Needed {a,b}
+--            Given  a = sc_sel a2
+--            Then a2 is needed too
+--
+--   - Prune out all Given bindings that are not needed
+--
+--   - From the 'needed' set, delete ev_bndrs, the binders of the
+--     evidence bindings, to give the final needed variables
+--
+neededEvVars implic@(Implic { ic_given = givens
+                            , ic_binds = ev_binds_var
+                            , ic_wanted = WC { wc_impl = implics }
+                            , ic_need_inner = old_needs })
+ = do { ev_binds <- TcS.getTcEvBindsMap ev_binds_var
+      ; tcvs     <- TcS.getTcEvTyCoVars ev_binds_var
+
+      ; let seeds1        = foldrBag add_implic_seeds old_needs implics
+            seeds2        = foldEvBindMap add_wanted seeds1 ev_binds
+            seeds3        = seeds2 `unionVarSet` tcvs
+            need_inner    = findNeededEvVars ev_binds seeds3
+            live_ev_binds = filterEvBindMap (needed_ev_bind need_inner) ev_binds
+            need_outer    = foldEvBindMap del_ev_bndr need_inner live_ev_binds
+                            `delVarSetList` givens
+
+      ; TcS.setTcEvBindsMap ev_binds_var live_ev_binds
+           -- See Note [Delete dead Given evidence bindings]
+
+      ; traceTcS "neededEvVars" $
+        vcat [ text "old_needs:" <+> ppr old_needs
+             , text "seeds3:" <+> ppr seeds3
+             , text "ev_binds:" <+> ppr ev_binds
+             , text "live_ev_binds:" <+> ppr live_ev_binds ]
+
+      ; return (implic { ic_need_inner = need_inner
+                       , ic_need_outer = need_outer }) }
  where
-   seeds  = foldEvBindMap add_wanted initial_seeds ev_binds
-   needed = transCloVarSet also_needs seeds
-   bndrs  = foldEvBindMap add_bndr emptyVarSet ev_binds
+   add_implic_seeds (Implic { ic_need_outer = needs, ic_given = givens }) acc
+      = (needs `delVarSetList` givens) `unionVarSet` acc
+
+   needed_ev_bind needed (EvBind { eb_lhs = ev_var
+                                 , eb_is_given = is_given })
+     | is_given  = ev_var `elemVarSet` needed
+     | otherwise = True   -- Keep all wanted bindings
+
+   del_ev_bndr :: EvBind -> VarSet -> VarSet
+   del_ev_bndr (EvBind { eb_lhs = v }) needs = delVarSet needs v
 
    add_wanted :: EvBind -> VarSet -> VarSet
    add_wanted (EvBind { eb_is_given = is_given, eb_rhs = rhs }) needs
      | is_given  = needs  -- Add the rhs vars of the Wanted bindings only
      | otherwise = evVarsOfTerm rhs `unionVarSet` needs
 
-   also_needs :: VarSet -> VarSet
-   also_needs needs
-     = nonDetFoldUniqSet add emptyVarSet needs
-     -- It's OK to use nonDetFoldUFM here because we immediately forget
-     -- about the ordering by creating a set
-     where
-       add v needs
-        | Just ev_bind <- lookupEvBind ev_binds v
-        , EvBind { eb_is_given = is_given, eb_rhs = rhs } <- ev_bind
-        , is_given
-        = evVarsOfTerm rhs `unionVarSet` needs
-        | otherwise
-        = needs
 
-   add_bndr :: EvBind -> VarSet -> VarSet
-   add_bndr (EvBind { eb_lhs = v }) vs = extendVarSet vs v
+{- Note [Delete dead Given evidence bindings]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+As a result of superclass expansion, we speculatively
+generate evidence bindings for Givens. E.g.
+   f :: (a ~ b) => a -> b -> Bool
+   f x y = ...
+We'll have
+   [G] d1 :: (a~b)
+and we'll specuatively generate the evidence binding
+   [G] d2 :: (a ~# b) = sc_sel d
 
+Now d2 is available for solving.  But it may not be needed!  Usually
+such dead superclass selections will eventually be dropped as dead
+code, but:
+
+ * It won't always be dropped (Trac #13032).  In the case of an
+   unlifted-equality superclass like d2 above, we generate
+       case heq_sc d1 of d2 -> ...
+   and we can't (in general) drop that case exrpession in case
+   d1 is bottom.  So it's technically unsound to have added it
+   in the first place.
+
+ * Simply generating all those extra superclasses can generate lots of
+   code that has to be zonked, only to be discarded later.  Better not
+   to generate it in the first place.
+
+   Moreover, if we simplify this implication more than once
+   (e.g. because we can't solve it completely on the first iteration
+   of simpl_looop), we'll generate all the same bindings AGAIN!
+
+Easy solution: take advantage of the work we are doing to track dead
+(unused) Givens, and use it to prune the Given bindings too.  This is
+all done by neededEvVars.
+
+This led to a remarkable 25% overall compiler allocation decrease in
+test T12227.
 
-{-
 Note [Tracking redundant constraints]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 With Opt_WarnRedundantConstraints, GHC can report which
@@ -1473,18 +1815,16 @@ works:
 
 ----- How tracking works
 
+* The ic_need fields of an Implic records in-scope (given) evidence
+  variables bound by the context, that were needed to solve this
+  implication (so far).  See the declaration of Implication.
+
 * When the constraint solver finishes solving all the wanteds in
   an implication, it sets its status to IC_Solved
 
   - The ics_dead field, of IC_Solved, records the subset of this
     implication's ic_given that are redundant (not needed).
 
-  - The ics_need field of IC_Solved then records all the
-    in-scope (given) evidence variables bound by the context, that
-    were needed to solve this implication, including all its nested
-    implications.  (We remove the ic_given of this implication from
-    the set, of course.)
-
 * We compute which evidence variables are needed by an implication
   in setImplicationStatus.  A variable is needed if
     a) it is free in the RHS of a Wanted EvBind,
@@ -1567,47 +1907,46 @@ we'll get more Givens (a unification is like adding a Given) to
 allow the implication to make progress.
 -}
 
-promoteTyVar :: TcLevel -> TcTyVar  -> TcM ()
+promoteTyVar :: TcTyVar -> TcM Bool
 -- When we float a constraint out of an implication we must restore
--- invariant (MetaTvInv) in Note [TcLevel and untouchable type variables] in TcType
+-- invariant (WantedInv) in Note [TcLevel and untouchable type variables] in TcType
+-- Return True <=> we did some promotion
 -- See Note [Promoting unification variables]
-promoteTyVar tclvl tv
-  | isFloatedTouchableMetaTyVar tclvl tv
-  = do { cloned_tv <- TcM.cloneMetaTyVar tv
-       ; let rhs_tv = setMetaTyVarTcLevel cloned_tv tclvl
-       ; TcM.writeMetaTyVar tv (mkTyVarTy rhs_tv) }
-  | otherwise
-  = return ()
-
-promoteTyVarTcS :: TcLevel -> TcTyVar  -> TcS ()
+promoteTyVar tv
+  = do { tclvl <- TcM.getTcLevel
+       ; if (isFloatedTouchableMetaTyVar tclvl tv)
+         then do { cloned_tv <- TcM.cloneMetaTyVar tv
+                 ; let rhs_tv = setMetaTyVarTcLevel cloned_tv tclvl
+                 ; TcM.writeMetaTyVar tv (mkTyVarTy rhs_tv)
+                 ; return True }
+         else return False }
+
+-- Returns whether or not *any* tyvar is defaulted
+promoteTyVarSet :: TcTyVarSet -> TcM Bool
+promoteTyVarSet tvs
+  = or <$> mapM promoteTyVar (nonDetEltsUniqSet tvs)
+    -- non-determinism is OK because order of promotion doesn't matter
+
+promoteTyVarTcS :: TcTyVar  -> TcS ()
 -- When we float a constraint out of an implication we must restore
--- invariant (MetaTvInv) in Note [TcLevel and untouchable type variables] in TcType
+-- invariant (WantedInv) in Note [TcLevel and untouchable type variables] in TcType
 -- See Note [Promoting unification variables]
 -- We don't just call promoteTyVar because we want to use unifyTyVar,
 -- not writeMetaTyVar
-promoteTyVarTcS tclvl tv
-  | isFloatedTouchableMetaTyVar tclvl tv
-  = do { cloned_tv <- TcS.cloneMetaTyVar tv
-       ; let rhs_tv = setMetaTyVarTcLevel cloned_tv tclvl
-       ; unifyTyVar tv (mkTyVarTy rhs_tv) }
-  | otherwise
-  = return ()
-
--- | If the tyvar is a RuntimeRep var, set it to LiftedRep.
-defaultTyVar :: TcTyVar -> TcM ()
--- Precondition: MetaTyVars only
--- See Note [DefaultTyVar]
-defaultTyVar the_tv
-  | isRuntimeRepVar the_tv
-  = do { traceTc "defaultTyVar RuntimeRep" (ppr the_tv)
-       ; writeMetaTyVar the_tv liftedRepTy }
-
-  | otherwise = return ()    -- The common case
+promoteTyVarTcS tv
+  = do { tclvl <- TcS.getTcLevel
+       ; when (isFloatedTouchableMetaTyVar tclvl tv) $
+         do { cloned_tv <- TcS.cloneMetaTyVar tv
+            ; let rhs_tv = setMetaTyVarTcLevel cloned_tv tclvl
+            ; unifyTyVar tv (mkTyVarTy rhs_tv) } }
 
 -- | Like 'defaultTyVar', but in the TcS monad.
 defaultTyVarTcS :: TcTyVar -> TcS Bool
 defaultTyVarTcS the_tv
   | isRuntimeRepVar the_tv
+  , not (isSigTyVar the_tv)  -- SigTvs should only be unified with a tyvar
+                             -- never with a type; c.f. TcMType.defaultTyVar
+                             -- See Note [Kind generalisation and SigTvs]
   = do { traceTcS "defaultTyVarTcS RuntimeRep" (ppr the_tv)
        ; unifyTyVar the_tv liftedRepTy
        ; return True }
@@ -1622,10 +1961,9 @@ approximateWC float_past_equalities wc
   where
     float_wc :: TcTyCoVarSet -> WantedConstraints -> Cts
     float_wc trapping_tvs (WC { wc_simple = simples, wc_impl = implics })
-      = filterBag is_floatable simples `unionBags`
+      = filterBag (is_floatable trapping_tvs) simples `unionBags`
         do_bag (float_implic trapping_tvs) implics
       where
-        is_floatable ct = tyCoVarsOfCt ct `disjointVarSet` trapping_tvs
 
     float_implic :: TcTyCoVarSet -> Implication -> Cts
     float_implic trapping_tvs imp
@@ -1635,9 +1973,16 @@ approximateWC float_past_equalities wc
       = emptyCts    -- See (1) under Note [ApproximateWC]
       where
         new_trapping_tvs = trapping_tvs `extendVarSetList` ic_skols imp
+
     do_bag :: (a -> Bag c) -> Bag a -> Bag c
     do_bag f = foldrBag (unionBags.f) emptyBag
 
+    is_floatable skol_tvs ct
+       | isGivenCt ct     = False
+       | isHoleCt ct      = False
+       | insolubleEqCt ct = False
+       | otherwise        = tyCoVarsOfCt ct `disjointVarSet` skol_tvs
+
 {- Note [ApproximateWC]
 ~~~~~~~~~~~~~~~~~~~~~~~
 approximateWC takes a constraint, typically arising from the RHS of a
@@ -1726,7 +2071,7 @@ When we are inferring a type, we simplify the constraint, and then use
 approximateWC to produce a list of candidate constraints.  Then we MUST
 
   a) Promote any meta-tyvars that have been floated out by
-     approximateWC, to restore invariant (MetaTvInv) described in
+     approximateWC, to restore invariant (WantedInv) described in
      Note [TcLevel and untouchable type variables] in TcType.
 
   b) Default the kind of any meta-tyvars that are not mentioned in
@@ -1743,8 +2088,8 @@ Note [Promoting unification variables]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 When we float an equality out of an implication we must "promote" free
 unification variables of the equality, in order to maintain Invariant
-(MetaTvInv) from Note [TcLevel and untouchable type variables] in TcType.  for the
-leftover implication.
+(WantedInv) from Note [TcLevel and untouchable type variables] in
+TcType.  for the leftover implication.
 
 This is absolutely necessary. Consider the following example. We start
 with two implications and a class with a functional dependency.
@@ -1834,7 +2179,7 @@ no evidence for a fundep equality), but equality superclasses do matter (since
 they carry evidence).
 -}
 
-floatEqualities :: [TcTyVar] -> Bool
+floatEqualities :: [TcTyVar] -> [EvId] -> EvBindsVar -> Bool
                 -> WantedConstraints
                 -> TcS (Cts, WantedConstraints)
 -- Main idea: see Note [Float Equalities out of Implications]
@@ -1851,37 +2196,69 @@ floatEqualities :: [TcTyVar] -> Bool
 --
 -- Subtleties: Note [Float equalities from under a skolem binding]
 --             Note [Skolem escape]
-floatEqualities skols no_given_eqs
+--             Note [What prevents a constraint from floating]
+floatEqualities skols given_ids ev_binds_var no_given_eqs
                 wanteds@(WC { wc_simple = simples })
   | not no_given_eqs  -- There are some given equalities, so don't float
   = return (emptyBag, wanteds)   -- Note [Float Equalities out of Implications]
+
   | otherwise
-  = do { outer_tclvl <- TcS.getTcLevel
-       ; mapM_ (promoteTyVarTcS outer_tclvl)
-               (tyCoVarsOfCtsList float_eqs)
-           -- See Note [Promoting unification variables]
+  = do { -- First zonk: the inert set (from whence they came) is fully
+         -- zonked, but unflattening may have filled in unification
+         -- variables, and we /must/ see them.  Otherwise we may float
+         -- constraints that mention the skolems!
+         simples <- TcS.zonkSimples simples
+       ; binds   <- TcS.getTcEvBindsMap ev_binds_var
+
+       -- Now we can pick the ones to float
+       -- The constraints are un-flattened and de-canonicalised
+       ; let seed_skols = mkVarSet skols     `unionVarSet`
+                          mkVarSet given_ids `unionVarSet`
+                          foldEvBindMap add_one emptyVarSet binds
+             add_one bind acc = extendVarSet acc (evBindVar bind)
+             -- seed_skols: See Note [What prevents a constraint from floating] (1,2,3)
+
+             (eqs, non_eqs)        = partitionBag is_eq_ct simples
+             extended_skols        = transCloVarSet (extra_skols eqs) seed_skols
+             (flt_eqs, no_flt_eqs) = partitionBag (is_floatable extended_skols) eqs
+             remaining_simples = non_eqs `andCts` no_flt_eqs
+             -- extended_skols: See Note [What prevents a constraint from floating] (3)
+
+       -- Promote any unification variables mentioned in the floated equalities
+       -- See Note [Promoting unification variables]
+       ; mapM_ promoteTyVarTcS (tyCoVarsOfCtsList flt_eqs)
 
        ; traceTcS "floatEqualities" (vcat [ text "Skols =" <+> ppr skols
+                                          , text "Extended skols =" <+> ppr extended_skols
                                           , text "Simples =" <+> ppr simples
-                                          , text "Floated eqs =" <+> ppr float_eqs])
-       ; return ( float_eqs
-                , wanteds { wc_simple = remaining_simples } ) }
-  where
-    skol_set = mkVarSet skols
-    (float_eqs, remaining_simples) = partitionBag (usefulToFloat skol_set) simples
+                                          , text "Eqs =" <+> ppr eqs
+                                          , text "Floated eqs =" <+> ppr flt_eqs])
+       ; return ( flt_eqs, wanteds { wc_simple = remaining_simples } ) }
 
-usefulToFloat :: VarSet -> Ct -> Bool
-usefulToFloat skol_set ct   -- The constraint is un-flattened and de-canonicalised
-  = is_meta_var_eq pred &&
-    (tyCoVarsOfType pred `disjointVarSet` skol_set)
   where
-    pred = ctPred ct
+    is_floatable :: VarSet -> Ct -> Bool
+    is_floatable skols ct
+      | isDerivedCt ct = not (tyCoVarsOfCt ct `intersectsVarSet` skols)
+      | otherwise      = not (ctEvId ct `elemVarSet` skols)
+
+    is_eq_ct ct | CTyEqCan {} <- ct      = True
+                | is_homo_eq (ctPred ct) = True
+                | otherwise              = False
+
+    extra_skols :: Cts -> VarSet -> VarSet
+    extra_skols eqs skols = foldrBag extra_skol emptyVarSet eqs
+       where
+         extra_skol ct acc
+           | isDerivedCt ct                           = acc
+           | tyCoVarsOfCt ct `intersectsVarSet` skols = extendVarSet acc (ctEvId ct)
+           | otherwise                                = acc
 
       -- Float out alpha ~ ty, or ty ~ alpha
       -- which might be unified outside
       -- See Note [Which equalities to float]
-    is_meta_var_eq pred
+    is_homo_eq pred
       | EqPred NomEq ty1 ty2 <- classifyPredType pred
+      , typeKind ty1 `tcEqType` typeKind ty2
       = case (tcGetTyVar_maybe ty1, tcGetTyVar_maybe ty2) of
           (Just tv1, _) -> float_tv_eq tv1 ty2
           (_, Just tv2) -> float_tv_eq tv2 ty1
@@ -1893,6 +2270,7 @@ usefulToFloat skol_set ct   -- The constraint is un-flattened and de-canonicalis
       =  isMetaTyVar tv1
       && (not (isSigTyVar tv1) || isTyVarTy ty2)
 
+
 {- Note [Float equalities from under a skolem binding]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Which of the simple equalities can we float out?  Obviously, only
@@ -1922,7 +2300,7 @@ Which equalities should we float?  We want to float ones where there
 is a decent chance that floating outwards will allow unification to
 happen.  In particular:
 
-   Float out equalities of form (alpha ~ ty) or (ty ~ alpha), where
+   Float out homogeneous equalities of form (alpha ~ ty) or (ty ~ alpha), where
 
    * alpha is a meta-tyvar.
 
@@ -1930,6 +2308,15 @@ happen.  In particular:
      case, floating out won't help either, and it may affect grouping
      of error messages.
 
+Why homogeneous (i.e., the kinds of the types are the same)? Because heterogeneous
+equalities have derived kind equalities. See Note [Equalities with incompatible kinds]
+in TcCanonical. If we float out a hetero equality, then it will spit out the
+same derived kind equality again, which might create duplicate error messages.
+Instead, we do float out the kind equality (if it's worth floating out, as
+above). If/when we solve it, we'll be able to rewrite the original hetero equality
+to be homogeneous, and then perhaps make progress / float it out. The duplicate
+error message was spotted in typecheck/should_fail/T7368.
+
 Note [Skolem escape]
 ~~~~~~~~~~~~~~~~~~~~
 You might worry about skolem escape with all this floating.
@@ -1946,6 +2333,37 @@ skolem has escaped!
 But it's ok: when we float (Maybe beta[2] ~ gamma[1]), we promote beta[2]
 to beta[1], and that means the (a ~ beta[1]) will be stuck, as it should be.
 
+Note [What prevents a constraint from floating]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+What /prevents/ a constraint from floating?  If it mentions one of the
+"bound variables of the implication".  What are they?
+
+The "bound variables of the implication" are
+
+  1. The skolem type variables `ic_skols`
+
+  2. The "given" evidence variables `ic_given`.  Example:
+         forall a. (co :: t1 ~# t2) =>  [W] co : (a ~# b |> co)
+
+  3. The binders of all evidence bindings in `ic_binds`. Example
+         forall a. (d :: t1 ~ t2)
+            EvBinds { (co :: t1 ~# t2) = superclass-sel d }
+            => [W] co2 : (a ~# b |> co)
+     Here `co` is gotten by superclass selection from `d`, and the
+     wanted constraint co2 must not float.
+
+  4. And the evidence variable of any equality constraint (incl
+     Wanted ones) whose type mentions a bound variable.  Example:
+        forall k. [W] co1 :: t1 ~# t2 |> co2
+                  [W] co2 :: k ~# *
+     Here, since `k` is bound, so is `co2` and hence so is `co1`.
+
+Here (1,2,3) are handled by the "seed_skols" calculation, and
+(4) is done by the transCloVarSet call.
+
+The possible dependence on givens, and evidence bindings, is more
+subtle than we'd realised at first.  See Trac #14584.
+
 
 *********************************************************************************
 *                                                                               *
@@ -1988,7 +2406,8 @@ findDefaultableGroups (default_tys, (ovl_strings, extended_defaults)) wanteds
   = []
   | otherwise
   = [ (tv, map fstOf3 group)
-    | group@((_,_,tv):_) <- unary_groups
+    | group'@((_,_,tv) :| _) <- unary_groups
+    , let group = toList group'
     , defaultable_tyvar tv
     , defaultable_classes (map sndOf3 group) ]
   where
@@ -1996,9 +2415,9 @@ findDefaultableGroups (default_tys, (ovl_strings, extended_defaults)) wanteds
     (unaries, non_unaries) = partitionWith find_unary (bagToList simples)
     unary_groups           = equivClasses cmp_tv unaries
 
-    unary_groups :: [[(Ct, Class, TcTyVar)]]  -- (C tv) constraints
-    unaries      ::  [(Ct, Class, TcTyVar)]   -- (C tv) constraints
-    non_unaries  :: [Ct]                      -- and *other* constraints
+    unary_groups :: [NonEmpty (Ct, Class, TcTyVar)] -- (C tv) constraints
+    unaries      :: [(Ct, Class, TcTyVar)]          -- (C tv) constraints
+    non_unaries  :: [Ct]                            -- and *other* constraints
 
         -- Finds unary type-class constraints
         -- But take account of polykinded classes like Typeable,
@@ -2064,10 +2483,8 @@ disambigGroup (default_ty:default_tys) group@(the_tv, wanteds)
     try_group
       | Just subst <- mb_subst
       = do { lcl_env <- TcS.getLclEnv
-           ; let loc = CtLoc { ctl_origin = GivenOrigin UnkSkol
-                             , ctl_env    = lcl_env
-                             , ctl_t_or_k = Nothing
-                             , ctl_depth  = initialSubGoalDepth }
+           ; tc_lvl <- TcS.getTcLevel
+           ; let loc = mkGivenLoc tc_lvl UnkSkol lcl_env
            ; wanted_evs <- mapM (newWantedEvVarNC loc . substTy subst . ctPred)
                                 wanteds
            ; fmap isEmptyWC $