Make a smart mkAppTyM
[ghc.git] / compiler / typecheck / TcCanonical.hs
index 1e1fa39..09ef93a 100644 (file)
@@ -24,10 +24,13 @@ import Class
 import TyCon
 import TyCoRep   -- cleverly decomposes types, good for completeness checking
 import Coercion
+import CoreSyn
+import Id( idType, mkTemplateLocals )
 import FamInstEnv ( FamInstEnvs )
 import FamInst ( tcTopNormaliseNewTypeTF_maybe )
 import Var
 import VarEnv( mkInScopeSet )
+import VarSet( delVarSetList )
 import Outputable
 import DynFlags( DynFlags )
 import NameSet
@@ -40,7 +43,7 @@ import Bag
 import MonadUtils
 import Control.Monad
 import Data.Maybe ( isJust )
-import Data.List  ( zip4, foldl' )
+import Data.List  ( zip4 )
 import BasicTypes
 
 import Data.Bifunctor ( bimap )
@@ -81,15 +84,31 @@ last time through, so we can skip the classification step.
 canonicalize :: Ct -> TcS (StopOrContinue Ct)
 canonicalize (CNonCanonical { cc_ev = ev })
   = {-# SCC "canNC" #-}
-    case classifyPredType (ctEvPred ev) of
+    case classifyPredType pred of
       ClassPred cls tys     -> do traceTcS "canEvNC:cls" (ppr cls <+> ppr tys)
                                   canClassNC ev cls tys
       EqPred eq_rel ty1 ty2 -> do traceTcS "canEvNC:eq" (ppr ty1 $$ ppr ty2)
                                   canEqNC    ev eq_rel ty1 ty2
-      IrredPred {}          -> do traceTcS "canEvNC:irred" (ppr (ctEvPred ev))
+      IrredPred {}          -> do traceTcS "canEvNC:irred" (ppr pred)
                                   canIrred ev
+      ForAllPred _ _ pred   -> do traceTcS "canEvNC:forall" (ppr pred)
+                                  canForAll ev (isClassPred pred)
+  where
+    pred = ctEvPred ev
+
+canonicalize (CQuantCan (QCI { qci_ev = ev, qci_pend_sc = pend_sc }))
+  = canForAll ev pend_sc
 
 canonicalize (CIrredCan { cc_ev = ev })
+  | EqPred eq_rel ty1 ty2 <- classifyPredType (ctEvPred ev)
+  = -- For insolubles (all of which are equalities, do /not/ flatten the arguments
+    -- In Trac #14350 doing so led entire-unnecessary and ridiculously large
+    -- type function expansion.  Instead, canEqNC just applies
+    -- the substitution to the predicate, and may do decomposition;
+    --    e.g. a ~ [a], where [G] a ~ [Int], can decompose
+    canEqNC ev eq_rel ty1 ty2
+
+  | otherwise
   = canIrred ev
 
 canonicalize (CDictCan { cc_ev = ev, cc_class  = cls
@@ -130,7 +149,7 @@ canClassNC :: CtEvidence -> Class -> [Type] -> TcS (StopOrContinue Ct)
 -- Precondition: EvVar is class evidence
 canClassNC ev cls tys
   | isGiven ev  -- See Note [Eagerly expand given superclasses]
-  = do { sc_cts <- mkStrictSuperClasses ev cls tys
+  = do { sc_cts <- mkStrictSuperClasses ev [] [] cls tys
        ; emitWork sc_cts
        ; canClass ev cls tys False }
 
@@ -174,7 +193,7 @@ solveCallStack ev ev_cs = do
   -- `IP ip CallStack`. See Note [Overview of implicit CallStacks]
   cs_tm <- evCallStack ev_cs
   let ev_tm = mkEvCast cs_tm (wrapIP (ctEvPred ev))
-  setWantedEvBind (ctEvEvId ev) (EvExpr ev_tm)
+  setEvBindIfWanted ev ev_tm
 
 canClass :: CtEvidence
          -> Class -> [Type]
@@ -185,8 +204,9 @@ canClass :: CtEvidence
 canClass ev cls tys pend_sc
   =   -- all classes do *nominal* matching
     ASSERT2( ctEvRole ev == Nominal, ppr ev $$ ppr cls $$ ppr tys )
-    do { (xis, cos) <- flattenManyNom ev tys
-       ; let co = mkTcTyConAppCo Nominal (classTyCon cls) cos
+    do { (xis, cos, _kind_co) <- flattenArgsNom ev cls_tc tys
+       ; MASSERT( isTcReflCo _kind_co )
+       ; let co = mkTcTyConAppCo Nominal cls_tc cos
              xi = mkClassPred cls xis
              mk_ct new_ev = CDictCan { cc_ev = new_ev
                                      , cc_tyargs = xis
@@ -196,6 +216,8 @@ canClass ev cls tys pend_sc
        ; traceTcS "canClass" (vcat [ ppr ev
                                    , ppr xi, ppr mb ])
        ; return (fmap mk_ct mb) }
+  where
+    cls_tc = classTyCon cls
 
 {- Note [The superclass story]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -241,19 +263,19 @@ So here's the plan:
 
 1. Eagerly generate superclasses for given (but not wanted)
    constraints; see Note [Eagerly expand given superclasses].
-   This is done in canClassNC, when we take a non-canonical constraint
-   and cannonicalise it.
+   This is done using mkStrictSuperClasses in canClassNC, when
+   we take a non-canonical Given constraint and cannonicalise it.
 
    However stop if you encounter the same class twice.  That is,
-   expand eagerly, but have a conservative termination condition: see
-   Note [Expanding superclasses] in TcType.
+   mkStrictSuperClasses expands eagerly, but has a conservative
+   termination condition: see Note [Expanding superclasses] in TcType.
 
 2. Solve the wanteds as usual, but do no further expansion of
    superclasses for canonical CDictCans in solveSimpleGivens or
    solveSimpleWanteds; Note [Danger of adding superclasses during solving]
 
-   However, /do/ continue to eagerly expand superlasses for /given/
-   non-canonical constraints (canClassNC does this).  As Trac #12175
+   However, /do/ continue to eagerly expand superlasses for new /given/
+   /non-canonical/ constraints (canClassNC does this).  As Trac #12175
    showed, a type-family application can expand to a class constraint,
    and we want to see its superclasses for just the same reason as
    Note [Eagerly expand given superclasses].
@@ -261,9 +283,20 @@ So here's the plan:
 3. If we have any remaining unsolved wanteds
         (see Note [When superclasses help] in TcRnTypes)
    try harder: take both the Givens and Wanteds, and expand
-   superclasses again.  This may succeed in generating (a finite
-   number of) extra Givens, and extra Deriveds. Both may help the
-   proof.  This is done in TcSimplify.expandSuperClasses.
+   superclasses again.  See the calls to expandSuperClasses in
+   TcSimplify.simpl_loop and solveWanteds.
+
+   This may succeed in generating (a finite number of) extra Givens,
+   and extra Deriveds. Both may help the proof.
+
+3a An important wrinkle: only expand Givens from the current level.
+   Two reasons:
+      - We only want to expand it once, and that is best done at
+        the level it is bound, rather than repeatedly at the leaves
+        of the implication tree
+      - We may be inside a type where we can't create term-level
+        evidence anyway, so we can't superclass-expand, say,
+        (a ~ b) to get (a ~# b).  This happened in Trac #15290.
 
 4. Go round to (2) again.  This loop (2,3,4) is implemented
    in TcSimplify.simpl_loop.
@@ -285,10 +318,31 @@ Why do we do this?  Two reasons:
 When we take a CNonCanonical or CIrredCan, but end up classifying it
 as a CDictCan, we set the cc_pend_sc flag to False.
 
+Note [Superclass loops]
+~~~~~~~~~~~~~~~~~~~~~~~
+Suppose we have
+  class C a => D a
+  class D a => C a
+
+Then, when we expand superclasses, we'll get back to the self-same
+predicate, so we have reached a fixpoint in expansion and there is no
+point in fruitlessly expanding further.  This case just falls out from
+our strategy.  Consider
+  f :: C a => a -> Bool
+  f x = x==x
+Then canClassNC gets the [G] d1: C a constraint, and eager emits superclasses
+G] d2: D a, [G] d3: C a (psc).  (The "psc" means it has its sc_pend flag set.)
+When processing d3 we find a match with d1 in the inert set, and we always
+keep the inert item (d1) if possible: see Note [Replacement vs keeping] in
+TcInteract.  So d3 dies a quick, happy death.
+
 Note [Eagerly expand given superclasses]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 In step (1) of Note [The superclass story], why do we eagerly expand
-Given superclasses by one layer?  Mainly because of some very obscure
+Given superclasses by one layer?  (By "one layer" we mean expand transitively
+until you meet the same class again -- the conservative criterion embodied
+in expandSuperClasses.  So a "layer" might be a whole stack of superclasses.)
+We do this eagerly for Givens mainly because of some very obscure
 cases like this:
 
    instance Bad a => Eq (T a)
@@ -398,34 +452,115 @@ makeSuperClasses :: [Ct] -> TcS [Ct]
 makeSuperClasses cts = concatMapM go cts
   where
     go (CDictCan { cc_ev = ev, cc_class = cls, cc_tyargs = tys })
-          = mkStrictSuperClasses ev cls tys
+      = mkStrictSuperClasses ev [] [] cls tys
+    go (CQuantCan (QCI { qci_pred = pred, qci_ev = ev }))
+      = ASSERT2( isClassPred pred, ppr pred )  -- The cts should all have
+                                               -- class pred heads
+        mkStrictSuperClasses ev tvs theta cls tys
+      where
+        (tvs, theta, cls, tys) = tcSplitDFunTy (ctEvPred ev)
     go ct = pprPanic "makeSuperClasses" (ppr ct)
 
-mkStrictSuperClasses :: CtEvidence -> Class -> [Type] -> TcS [Ct]
--- Return constraints for the strict superclasses of (c tys)
-mkStrictSuperClasses ev cls tys
-  = mk_strict_superclasses (unitNameSet (className cls)) ev cls tys
+mkStrictSuperClasses
+    :: CtEvidence
+    -> [TyVar] -> ThetaType  -- These two args are non-empty only when taking
+                             -- superclasses of a /quantified/ constraint
+    -> Class -> [Type] -> TcS [Ct]
+-- Return constraints for the strict superclasses of
+--   ev :: forall as. theta => cls tys
+mkStrictSuperClasses ev tvs theta cls tys
+  = mk_strict_superclasses (unitNameSet (className cls))
+                           ev tvs theta cls tys
+
+mk_strict_superclasses :: NameSet -> CtEvidence
+                       -> [TyVar] -> ThetaType
+                       -> Class -> [Type] -> TcS [Ct]
+-- Always return the immediate superclasses of (cls tys);
+-- and expand their superclasses, provided none of them are in rec_clss
+-- nor are repeated
+mk_strict_superclasses rec_clss ev tvs theta cls tys
+  | CtGiven { ctev_evar = evar, ctev_loc = loc } <- ev
+  = concatMapM (do_one_given evar (mk_given_loc loc)) $
+    classSCSelIds cls
+  where
+    dict_ids  = mkTemplateLocals theta
+    size      = sizeTypes tys
+
+    do_one_given evar given_loc sel_id
+      | isUnliftedType sc_pred
+      , not (null tvs && null theta)
+      = -- See Note [Equality superclasses in quantified constraints]
+        return []
+      | otherwise
+      = do { given_ev <- newGivenEvVar given_loc $
+                         (given_ty, mk_sc_sel evar sel_id)
+           ; mk_superclasses rec_clss given_ev tvs theta sc_pred }
+      where
+        sc_pred  = funResultTy (piResultTys (idType sel_id) tys)
+        given_ty = mkInfSigmaTy tvs theta sc_pred
+
+    mk_sc_sel evar sel_id
+      = EvExpr $ mkLams tvs $ mkLams dict_ids $
+        Var sel_id `mkTyApps` tys `App`
+        (evId evar `mkTyApps` mkTyVarTys tvs `mkVarApps` dict_ids)
+
+    mk_given_loc loc
+       | isCTupleClass cls
+       = loc   -- For tuple predicates, just take them apart, without
+               -- adding their (large) size into the chain.  When we
+               -- get down to a base predicate, we'll include its size.
+               -- Trac #10335
+
+       | GivenOrigin skol_info <- ctLocOrigin loc
+         -- See Note [Solving superclass constraints] in TcInstDcls
+         -- for explantation of this transformation for givens
+       = case skol_info of
+            InstSkol -> loc { ctl_origin = GivenOrigin (InstSC size) }
+            InstSC n -> loc { ctl_origin = GivenOrigin (InstSC (n `max` size)) }
+            _        -> loc
+
+       | otherwise  -- Probably doesn't happen, since this function
+       = loc        -- is only used for Givens, but does no harm
+
+mk_strict_superclasses rec_clss ev tvs theta cls tys
+  | all noFreeVarsOfType tys
+  = return [] -- Wanteds with no variables yield no deriveds.
+              -- See Note [Improvement from Ground Wanteds]
 
-mk_superclasses :: NameSet -> CtEvidence -> TcS [Ct]
+  | otherwise -- Wanted/Derived case, just add Derived superclasses
+              -- that can lead to improvement.
+  = ASSERT2( null tvs && null theta, ppr tvs $$ ppr theta )
+    concatMapM do_one_derived (immSuperClasses cls tys)
+  where
+    loc = ctEvLoc ev
+
+    do_one_derived sc_pred
+      = do { sc_ev <- newDerivedNC loc sc_pred
+           ; mk_superclasses rec_clss sc_ev [] [] sc_pred }
+
+mk_superclasses :: NameSet -> CtEvidence
+                -> [TyVar] -> ThetaType -> PredType -> TcS [Ct]
 -- Return this constraint, plus its superclasses, if any
-mk_superclasses rec_clss ev
-  | ClassPred cls tys <- classifyPredType (ctEvPred ev)
-  = mk_superclasses_of rec_clss ev cls tys
+mk_superclasses rec_clss ev tvs theta pred
+  | ClassPred cls tys <- classifyPredType pred
+  = mk_superclasses_of rec_clss ev tvs theta cls tys
 
   | otherwise   -- Superclass is not a class predicate
   = return [mkNonCanonical ev]
 
-mk_superclasses_of :: NameSet -> CtEvidence -> Class -> [Type] -> TcS [Ct]
+mk_superclasses_of :: NameSet -> CtEvidence
+                   -> [TyVar] -> ThetaType -> Class -> [Type]
+                   -> TcS [Ct]
 -- Always return this class constraint,
 -- and expand its superclasses
-mk_superclasses_of rec_clss ev cls tys
+mk_superclasses_of rec_clss ev tvs theta cls tys
   | loop_found = do { traceTcS "mk_superclasses_of: loop" (ppr cls <+> ppr tys)
                     ; return [this_ct] }  -- cc_pend_sc of this_ct = True
   | otherwise  = do { traceTcS "mk_superclasses_of" (vcat [ ppr cls <+> ppr tys
                                                           , ppr (isCTupleClass cls)
                                                           , ppr rec_clss
                                                           ])
-                    ; sc_cts <- mk_strict_superclasses rec_clss' ev cls tys
+                    ; sc_cts <- mk_strict_superclasses rec_clss' ev tvs theta cls tys
                     ; return (this_ct : sc_cts) }
                                    -- cc_pend_sc of this_ct = False
   where
@@ -433,52 +568,55 @@ mk_superclasses_of rec_clss ev cls tys
     loop_found = not (isCTupleClass cls) && cls_nm `elemNameSet` rec_clss
                  -- Tuples never contribute to recursion, and can be nested
     rec_clss'  = rec_clss `extendNameSet` cls_nm
-    this_ct    = CDictCan { cc_ev = ev, cc_class = cls, cc_tyargs = tys
-                          , cc_pend_sc = loop_found }
+
+    this_ct | null tvs, null theta
+            = CDictCan { cc_ev = ev, cc_class = cls, cc_tyargs = tys
+                       , cc_pend_sc = loop_found }
                  -- NB: If there is a loop, we cut off, so we have not
                  --     added the superclasses, hence cc_pend_sc = True
+            | otherwise
+            = CQuantCan (QCI { qci_tvs = tvs, qci_pred = mkClassPred cls tys
+                             , qci_ev = ev
+                             , qci_pend_sc = loop_found })
 
-mk_strict_superclasses :: NameSet -> CtEvidence -> Class -> [Type] -> TcS [Ct]
--- Always return the immediate superclasses of (cls tys);
--- and expand their superclasses, provided none of them are in rec_clss
--- nor are repeated
-mk_strict_superclasses rec_clss ev cls tys
-  | CtGiven { ctev_evar = evar, ctev_loc = loc } <- ev
-  = do { sc_evs <- newGivenEvVars (mk_given_loc loc)
-                                  (mkEvScSelectors (evId evar) cls tys)
-       ; concatMapM (mk_superclasses rec_clss) sc_evs }
 
-  | all noFreeVarsOfType tys
-  = return [] -- Wanteds with no variables yield no deriveds.
-              -- See Note [Improvement from Ground Wanteds]
+{- Note [Equality superclasses in quantified constraints]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider (Trac #15359, #15593, #15625)
+  f :: (forall a. theta => a ~ b) => stuff
 
-  | otherwise -- Wanted/Derived case, just add Derived superclasses
-              -- that can lead to improvement.
-  = do { let loc = ctEvLoc ev
-       ; sc_evs <- mapM (newDerivedNC loc) (immSuperClasses cls tys)
-       ; concatMapM (mk_superclasses rec_clss) sc_evs }
-  where
-    size = sizeTypes tys
-    mk_given_loc loc
-       | isCTupleClass cls
-       = loc   -- For tuple predicates, just take them apart, without
-               -- adding their (large) size into the chain.  When we
-               -- get down to a base predicate, we'll include its size.
-               -- Trac #10335
+It's a bit odd to have a local, quantified constraint for `(a~b)`,
+but some people want such a thing (see the tickets). And for
+Coercible it is definitely useful
+  f :: forall m. (forall p q. Coercible p q => Coercible (m p) (m q)))
+                 => stuff
 
-       | GivenOrigin skol_info <- ctLocOrigin loc
-         -- See Note [Solving superclass constraints] in TcInstDcls
-         -- for explantation of this transformation for givens
-       = case skol_info of
-            InstSkol -> loc { ctl_origin = GivenOrigin (InstSC size) }
-            InstSC n -> loc { ctl_origin = GivenOrigin (InstSC (n `max` size)) }
-            _        -> loc
+Moreover it's not hard to arrange; we just need to look up /equality/
+constraints in the quantified-constraint environment, which we do in
+TcInteract.doTopReactOther.
 
-       | otherwise  -- Probably doesn't happen, since this function
-       = loc        -- is only used for Givens, but does no harm
+There is a wrinkle though, in the case where 'theta' is empty, so
+we have
+  f :: (forall a. a~b) => stuff
+
+Now, potentially, the superclass machinery kicks in, in
+makeSuperClasses, giving us a a second quantified constrait
+       (forall a. a ~# b)
+BUT this is an unboxed value!  And nothing has prepared us for
+dictionary "functions" that are unboxed.  Actually it does just
+about work, but the simplier ends up with stuff like
+   case (/\a. eq_sel d) of df -> ...(df @Int)...
+and fails to simplify that any further.  And it doesn't satisfy
+isPredTy any more.
+
+So for now we simply decline to take superclasses in the quantified
+case.  Instead we have a special case in TcInteract.doTopReactOther,
+which looks for primitive equalities specially in the quantified
+constraints.
+
+See also Note [Evidence for quantified constraints] in Type.
 
 
-{-
 ************************************************************************
 *                                                                      *
 *                      Irreducibles canonicalization
@@ -489,16 +627,8 @@ mk_strict_superclasses rec_clss ev cls tys
 canIrred :: CtEvidence -> TcS (StopOrContinue Ct)
 -- Precondition: ty not a tuple and no other evidence form
 canIrred ev
-  | EqPred eq_rel ty1 ty2 <- classifyPredType pred
-  = -- For insolubles (all of which are equalities, do /not/ flatten the arguments
-    -- In Trac #14350 doing so led entire-unnecessary and ridiculously large
-    -- type function expansion.  Instead, canEqNC just applies
-    -- the substitution to the predicate, and may do decomposition;
-    --    e.g. a ~ [a], where [G] a ~ [Int], can decompose
-    canEqNC ev eq_rel ty1 ty2
-
-  | otherwise
-  = do { traceTcS "can_pred" (text "IrredPred = " <+> ppr pred)
+  = do { let pred = ctEvPred ev
+       ; traceTcS "can_pred" (text "IrredPred = " <+> ppr pred)
        ; (xi,co) <- flatten FM_FlattenAll ev pred -- co :: xi ~ pred
        ; rewriteEvidence ev xi co `andWhenContinue` \ new_ev ->
     do { -- Re-classify, in case flattening has improved its shape
@@ -507,19 +637,171 @@ canIrred ev
            EqPred eq_rel ty1 ty2 -> canEqNC new_ev eq_rel ty1 ty2
            _                     -> continueWith $
                                     mkIrredCt new_ev } }
-  where
-    pred = ctEvPred ev
 
 canHole :: CtEvidence -> Hole -> TcS (StopOrContinue Ct)
 canHole ev hole
-  = do { let ty = ctEvPred ev
-       ; (xi,co) <- flatten FM_SubstOnly ev ty -- co :: xi ~ ty
+  = do { let pred = ctEvPred ev
+       ; (xi,co) <- flatten FM_SubstOnly ev pred -- co :: xi ~ pred
        ; rewriteEvidence ev xi co `andWhenContinue` \ new_ev ->
     do { updInertIrreds (`snocCts` (CHoleCan { cc_ev = new_ev
                                              , cc_hole = hole }))
        ; stopWith new_ev "Emit insoluble hole" } }
 
-{-
+
+{- *********************************************************************
+*                                                                      *
+*                      Quantified predicates
+*                                                                      *
+********************************************************************* -}
+
+{- Note [Quantified constraints]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The -XQuantifiedConstraints extension allows type-class contexts like this:
+
+  data Rose f x = Rose x (f (Rose f x))
+
+  instance (Eq a, forall b. Eq b => Eq (f b))
+        => Eq (Rose f a)  where
+    (Rose x1 rs1) == (Rose x2 rs2) = x1==x2 && rs1 == rs2
+
+Note the (forall b. Eq b => Eq (f b)) in the instance contexts.
+This quantified constraint is needed to solve the
+ [W] (Eq (f (Rose f x)))
+constraint which arises form the (==) definition.
+
+The wiki page is
+  https://ghc.haskell.org/trac/ghc/wiki/QuantifiedConstraints
+which in turn contains a link to the GHC Proposal where the change
+is specified, and a Haskell Symposium paper about it.
+
+We implement two main extensions to the design in the paper:
+
+ 1. We allow a variable in the instance head, e.g.
+      f :: forall m a. (forall b. m b) => D (m a)
+    Notice the 'm' in the head of the quantified constraint, not
+    a class.
+
+ 2. We suport superclasses to quantified constraints.
+    For example (contrived):
+      f :: (Ord b, forall b. Ord b => Ord (m b)) => m a -> m a -> Bool
+      f x y = x==y
+    Here we need (Eq (m a)); but the quantifed constraint deals only
+    with Ord.  But we can make it work by using its superclass.
+
+Here are the moving parts
+  * Language extension {-# LANGUAGE QuantifiedConstraints #-}
+    and add it to ghc-boot-th:GHC.LanguageExtensions.Type.Extension
+
+  * A new form of evidence, EvDFun, that is used to discharge
+    such wanted constraints
+
+  * checkValidType gets some changes to accept forall-constraints
+    only in the right places.
+
+  * Type.PredTree gets a new constructor ForAllPred, and
+    and classifyPredType analyses a PredType to decompose
+    the new forall-constraints
+
+  * TcSMonad.InertCans gets an extra field, inert_insts,
+    which holds all the Given forall-constraints.  In effect,
+    such Given constraints are like local instance decls.
+
+  * When trying to solve a class constraint, via
+    TcInteract.matchInstEnv, use the InstEnv from inert_insts
+    so that we include the local Given forall-constraints
+    in the lookup.  (See TcSMonad.getInstEnvs.)
+
+  * TcCanonical.canForAll deals with solving a
+    forall-constraint.  See
+       Note [Solving a Wanted forall-constraint]
+
+  * We augment the kick-out code to kick out an inert
+    forall constraint if it can be rewritten by a new
+    type equality; see TcSMonad.kick_out_rewritable
+
+Note that a quantified constraint is never /inferred/
+(by TcSimplify.simplifyInfer).  A function can only have a
+quantified constraint in its type if it is given an explicit
+type signature.
+
+Note that we implement
+-}
+
+canForAll :: CtEvidence -> Bool -> TcS (StopOrContinue Ct)
+-- We have a constraint (forall as. blah => C tys)
+canForAll ev pend_sc
+  = do { -- First rewrite it to apply the current substitution
+         -- Do not bother with type-family reductions; we can't
+         -- do them under a forall anyway (c.f. Flatten.flatten_one
+         -- on a forall type)
+         let pred = ctEvPred ev
+       ; (xi,co) <- flatten FM_SubstOnly ev pred -- co :: xi ~ pred
+       ; rewriteEvidence ev xi co `andWhenContinue` \ new_ev ->
+
+    do { -- Now decompose into its pieces and solve it
+         -- (It takes a lot less code to flatten before decomposing.)
+       ; case classifyPredType (ctEvPred new_ev) of
+           ForAllPred tv_bndrs theta pred
+              -> solveForAll new_ev tv_bndrs theta pred pend_sc
+           _  -> pprPanic "canForAll" (ppr new_ev)
+    } }
+
+solveForAll :: CtEvidence -> [TyVarBinder] -> TcThetaType -> PredType -> Bool
+            -> TcS (StopOrContinue Ct)
+solveForAll ev tv_bndrs theta pred pend_sc
+  | CtWanted { ctev_dest = dest } <- ev
+  = -- See Note [Solving a Wanted forall-constraint]
+    do { let skol_info = QuantCtxtSkol
+             empty_subst = mkEmptyTCvSubst $ mkInScopeSet $
+                           tyCoVarsOfTypes (pred:theta) `delVarSetList` tvs
+       ; (subst, skol_tvs) <- tcInstSkolTyVarsX empty_subst tvs
+       ; given_ev_vars <- mapM newEvVar (substTheta subst theta)
+
+       ; (w_id, ev_binds)
+             <- checkConstraintsTcS skol_info skol_tvs given_ev_vars $
+                do { wanted_ev <- newWantedEvVarNC loc $
+                                  substTy subst pred
+                   ; return ( ctEvEvId wanted_ev
+                            , unitBag (mkNonCanonical wanted_ev)) }
+
+      ; setWantedEvTerm dest $
+        EvFun { et_tvs = skol_tvs, et_given = given_ev_vars
+              , et_binds = ev_binds, et_body = w_id }
+
+      ; stopWith ev "Wanted forall-constraint" }
+
+  | isGiven ev   -- See Note [Solving a Given forall-constraint]
+  = do { addInertForAll qci
+       ; stopWith ev "Given forall-constraint" }
+
+  | otherwise
+  = stopWith ev "Derived forall-constraint"
+  where
+    loc = ctEvLoc ev
+    tvs = binderVars tv_bndrs
+    qci = QCI { qci_ev = ev, qci_tvs = tvs
+              , qci_pred = pred, qci_pend_sc = pend_sc }
+
+{- Note [Solving a Wanted forall-constraint]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Solving a wanted forall (quantified) constraint
+  [W] df :: forall ab. (Eq a, Ord b) => C x a b
+is delightfully easy.   Just build an implication constraint
+    forall ab. (g1::Eq a, g2::Ord b) => [W] d :: C x a
+and discharge df thus:
+    df = /\ab. \g1 g2. let <binds> in d
+where <binds> is filled in by solving the implication constraint.
+All the machinery is to hand; there is little to do.
+
+Note [Solving a Given forall-constraint]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+For a Given constraint
+  [G] df :: forall ab. (Eq a, Ord b) => C x a b
+we just add it to TcS's local InstEnv of known instances,
+via addInertForall.  Then, if we look up (C x Int Bool), say,
+we'll find a match in the InstEnv.
+
+
 ************************************************************************
 *                                                                      *
 *        Equalities
@@ -591,9 +873,9 @@ can_eq_nc'
    -> TcS (StopOrContinue Ct)
 
 -- Expand synonyms first; see Note [Type synonyms and canonicalization]
-can_eq_nc' flat _rdr_env _envs ev eq_rel ty1 ps_ty1 ty2 ps_ty2
-  | Just ty1' <- tcView ty1 = can_eq_nc flat ev eq_rel ty1' ps_ty1 ty2  ps_ty2
-  | Just ty2' <- tcView ty2 = can_eq_nc flat ev eq_rel ty1  ps_ty1 ty2' ps_ty2
+can_eq_nc' flat rdr_env envs ev eq_rel ty1 ps_ty1 ty2 ps_ty2
+  | Just ty1' <- tcView ty1 = can_eq_nc' flat rdr_env envs ev eq_rel ty1' ps_ty1 ty2  ps_ty2
+  | Just ty2' <- tcView ty2 = can_eq_nc' flat rdr_env envs ev eq_rel ty1  ps_ty1 ty2' ps_ty2
 
 -- need to check for reflexivity in the ReprEq case.
 -- See Note [Eager reflexivity check]
@@ -604,28 +886,15 @@ can_eq_nc' True _rdr_env _envs ev ReprEq ty1 _ ty2 _
   = canEqReflexive ev ReprEq ty1
 
 -- When working with ReprEq, unwrap newtypes.
-can_eq_nc' _flat rdr_env envs ev ReprEq ty1 _ ty2 ps_ty2
-  | Just stuff1 <- tcTopNormaliseNewTypeTF_maybe envs rdr_env ty1
+-- See Note [Unwrap newtypes first]
+can_eq_nc' _flat rdr_env envs ev eq_rel ty1 ps_ty1 ty2 ps_ty2
+  | ReprEq <- eq_rel
+  , Just stuff1 <- tcTopNormaliseNewTypeTF_maybe envs rdr_env ty1
   = can_eq_newtype_nc ev NotSwapped ty1 stuff1 ty2 ps_ty2
-can_eq_nc' _flat rdr_env envs ev ReprEq ty1 ps_ty1 ty2 _
-  | Just stuff2 <- tcTopNormaliseNewTypeTF_maybe envs rdr_env ty2
-  = can_eq_newtype_nc ev IsSwapped  ty2 stuff2 ty1 ps_ty1
 
--- Now, check for tyvars. This must happen before CastTy because we need
--- to catch casted tyvars, as the flattener might produce these,
--- due to the fact that flattened types have flattened kinds.
--- See Note [Flattening].
--- Note that there can be only one cast on the tyvar because this will
--- run after the "get rid of casts" case of can_eq_nc' function on the
--- not-yet-flattened types.
--- NB: pattern match on True: we want only flat types sent to canEqTyVar.
--- See also Note [No top-level newtypes on RHS of representational equalities]
-can_eq_nc' True _rdr_env _envs ev eq_rel ty1 ps_ty1 ty2 ps_ty2
-  | Just (tv1, co1) <- getCastedTyVar_maybe ty1
-  = canEqTyVar ev eq_rel NotSwapped tv1 co1 ps_ty1 ty2 ps_ty2
-can_eq_nc' True _rdr_env _envs ev eq_rel ty1 ps_ty1 ty2 ps_ty2
-  | Just (tv2, co2) <- getCastedTyVar_maybe ty2
-  = canEqTyVar ev eq_rel IsSwapped tv2 co2 ps_ty2 ty1 ps_ty1
+  | ReprEq <- eq_rel
+  , Just stuff2 <- tcTopNormaliseNewTypeTF_maybe envs rdr_env ty2
+  = can_eq_newtype_nc ev IsSwapped  ty2 stuff2 ty1 ps_ty1
 
 -- Then, get rid of casts
 can_eq_nc' flat _rdr_env _envs ev eq_rel (CastTy ty1 co1) _ ty2 ps_ty2
@@ -633,6 +902,13 @@ can_eq_nc' flat _rdr_env _envs ev eq_rel (CastTy ty1 co1) _ ty2 ps_ty2
 can_eq_nc' flat _rdr_env _envs ev eq_rel ty1 ps_ty1 (CastTy ty2 co2) _
   = canEqCast flat ev eq_rel IsSwapped ty2 co2 ty1 ps_ty1
 
+-- NB: pattern match on True: we want only flat types sent to canEqTyVar.
+-- See also Note [No top-level newtypes on RHS of representational equalities]
+can_eq_nc' True _rdr_env _envs ev eq_rel (TyVarTy tv1) ps_ty1 ty2 ps_ty2
+  = canEqTyVar ev eq_rel NotSwapped tv1 ps_ty1 ty2 ps_ty2
+can_eq_nc' True _rdr_env _envs ev eq_rel ty1 ps_ty1 (TyVarTy tv2) ps_ty2
+  = canEqTyVar ev eq_rel IsSwapped tv2 ps_ty2 ty1 ps_ty1
+
 ----------------------
 -- Otherwise try to decompose
 ----------------------
@@ -640,7 +916,7 @@ can_eq_nc' flat _rdr_env _envs ev eq_rel ty1 ps_ty1 (CastTy ty2 co2) _
 -- Literals
 can_eq_nc' _flat _rdr_env _envs ev eq_rel ty1@(LitTy l1) _ (LitTy l2) _
  | l1 == l2
-  = do { setEqIfWanted ev (mkReflCo (eqRelRole eq_rel) ty1)
+  = do { setEvBindIfWanted ev (evCoercion $ mkReflCo (eqRelRole eq_rel) ty1)
        ; stopWith ev "Equal LitTy" }
 
 -- Try to decompose type constructor applications
@@ -659,24 +935,38 @@ can_eq_nc' _flat _rdr_env _envs ev eq_rel
 
 -- See Note [Canonicalising type applications] about why we require flat types
 can_eq_nc' True _rdr_env _envs ev eq_rel (AppTy t1 s1) _ ty2 _
-  | Just (t2, s2) <- tcSplitAppTy_maybe ty2
-  = can_eq_app ev eq_rel t1 s1 t2 s2
+  | NomEq <- eq_rel
+  , Just (t2, s2) <- tcSplitAppTy_maybe ty2
+  = can_eq_app ev t1 s1 t2 s2
 can_eq_nc' True _rdr_env _envs ev eq_rel ty1 _ (AppTy t2 s2) _
-  | Just (t1, s1) <- tcSplitAppTy_maybe ty1
-  = can_eq_app ev eq_rel t1 s1 t2 s2
+  | NomEq <- eq_rel
+  , Just (t1, s1) <- tcSplitAppTy_maybe ty1
+  = can_eq_app ev t1 s1 t2 s2
 
 -- No similarity in type structure detected. Flatten and try again.
 can_eq_nc' False rdr_env envs ev eq_rel _ ps_ty1 _ ps_ty2
   = do { (xi1, co1) <- flatten FM_FlattenAll ev ps_ty1
        ; (xi2, co2) <- flatten FM_FlattenAll ev ps_ty2
-       ; rewriteEqEvidence ev NotSwapped xi1 xi2 co1 co2
-         `andWhenContinue` \ new_ev ->
-         can_eq_nc' True rdr_env envs new_ev eq_rel xi1 xi1 xi2 xi2 }
+       ; new_ev <- rewriteEqEvidence ev NotSwapped xi1 xi2 co1 co2
+       ; can_eq_nc' True rdr_env envs new_ev eq_rel xi1 xi1 xi2 xi2 }
 
 -- We've flattened and the types don't match. Give up.
-can_eq_nc' True _rdr_env _envs ev _eq_rel _ ps_ty1 _ ps_ty2
+can_eq_nc' True _rdr_env _envs ev eq_rel _ ps_ty1 _ ps_ty2
   = do { traceTcS "can_eq_nc' catch-all case" (ppr ps_ty1 $$ ppr ps_ty2)
-       ; canEqHardFailure ev ps_ty1 ps_ty2 }
+       ; case eq_rel of -- See Note [Unsolved equalities]
+            ReprEq -> continueWith (mkIrredCt ev)
+            NomEq  -> continueWith (mkInsolubleCt ev) }
+          -- No need to call canEqFailure/canEqHardFailure because they
+          -- flatten, and the types involved here are already flat
+
+{- Note [Unsolved equalities]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+If we have an unsolved equality like
+  (a b ~R# Int)
+that is not necessarily insoluble!  Maybe 'a' will turn out to be a newtype.
+So we want to make it a potentially-soluble Irred not an insoluble one.
+Missing this point is what caused Trac #15431
+-}
 
 ---------------------------------
 can_eq_nc_forall :: CtEvidence -> EqRel
@@ -693,8 +983,8 @@ can_eq_nc_forall :: CtEvidence -> EqRel
 can_eq_nc_forall ev eq_rel s1 s2
  | CtWanted { ctev_loc = loc, ctev_dest = orig_dest } <- ev
  = do { let free_tvs       = tyCoVarsOfTypes [s1,s2]
-            (bndrs1, phi1) = tcSplitForAllTyVarBndrs s1
-            (bndrs2, phi2) = tcSplitForAllTyVarBndrs s2
+            (bndrs1, phi1) = tcSplitForAllVarBndrs s1
+            (bndrs2, phi2) = tcSplitForAllVarBndrs s2
       ; if not (equalLength bndrs1 bndrs2)
         then do { traceTcS "Forall failure" $
                      vcat [ ppr s1, ppr s2, ppr bndrs1, ppr bndrs2
@@ -711,34 +1001,30 @@ can_eq_nc_forall ev eq_rel s1 s2
             phi1' = substTy subst1 phi1
 
             -- Unify the kinds, extend the substitution
+            go :: [TcTyVar] -> TCvSubst -> [TyVarBinder]
+               -> TcS (TcCoercion, Cts)
             go (skol_tv:skol_tvs) subst (bndr2:bndrs2)
               = do { let tv2 = binderVar bndr2
-                   ; kind_co <- unifyWanted loc Nominal
-                                            (tyVarKind skol_tv)
-                                            (substTy subst (tyVarKind tv2))
+                   ; (kind_co, wanteds1) <- unify loc Nominal (tyVarKind skol_tv)
+                                                  (substTy subst (tyVarKind tv2))
                    ; let subst' = extendTvSubst subst tv2
                                        (mkCastTy (mkTyVarTy skol_tv) kind_co)
-                   ; co <- go skol_tvs subst' bndrs2
-                   ; return (mkForAllCo skol_tv kind_co co) }
+                   ; (co, wanteds2) <- go skol_tvs subst' bndrs2
+                   ; return ( mkTcForAllCo skol_tv kind_co co
+                            , wanteds1 `unionBags` wanteds2 ) }
 
             -- Done: unify phi1 ~ phi2
             go [] subst bndrs2
               = ASSERT( null bndrs2 )
-                unifyWanted loc (eqRelRole eq_rel)
-                            phi1' (substTy subst phi2)
+                unify loc (eqRelRole eq_rel) phi1' (substTy subst phi2)
 
             go _ _ _ = panic "cna_eq_nc_forall"  -- case (s:ss) []
 
             empty_subst2 = mkEmptyTCvSubst (getTCvInScope subst1)
 
-      ; (implic, _ev_binds, all_co) <- buildImplication skol_info skol_tvs [] $
-                                       go skol_tvs empty_subst2 bndrs2
-           -- We have nowhere to put these bindings
-           -- but TcSimplify.setImplicationStatus
-           -- checks that we don't actually use them
-           -- when skol_info = UnifyForAllSkol
+      ; all_co <- checkTvConstraintsTcS skol_info skol_tvs $
+                  go skol_tvs empty_subst2 bndrs2
 
-      ; updWorkListTcS (extendWorkListImplic implic)
       ; setWantedEq orig_dest all_co
       ; stopWith ev "Deferred polytype equality" } }
 
@@ -747,11 +1033,22 @@ can_eq_nc_forall ev eq_rel s1 s2
         pprEq s1 s2    -- See Note [Do not decompose given polytype equalities]
       ; stopWith ev "Discard given polytype equality" }
 
+ where
+    unify :: CtLoc -> Role -> TcType -> TcType -> TcS (TcCoercion, Cts)
+    -- This version returns the wanted constraint rather
+    -- than putting it in the work list
+    unify loc role ty1 ty2
+      | ty1 `tcEqType` ty2
+      = return (mkTcReflCo role ty1, emptyBag)
+      | otherwise
+      = do { (wanted, co) <- newWantedEq loc role ty1 ty2
+           ; return (co, unitBag (mkNonCanonical wanted)) }
+
 ---------------------------------
 -- | Compare types for equality, while zonking as necessary. Gives up
 -- as soon as it finds that two types are not equal.
 -- This is quite handy when some unification has made two
--- types in an inert wanted to be equal. We can discover the equality without
+-- types in an inert Wanted to be equal. We can discover the equality without
 -- flattening, which is sometimes very expensive (in the case of type functions).
 -- In particular, this function makes a ~20% improvement in test case
 -- perf/compiler/T5030.
@@ -884,7 +1181,26 @@ zonk_eq_types = go
     combine_rev f (Right tys) (Left elt) = Left (f <$> elt     <*> pure tys)
     combine_rev f (Right tys) (Right ty) = Right (f ty tys)
 
-{-
+{- See Note [Unwrap newtypes first]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+  newtype N m a = MkN (m a)
+Then N will get a conservative, Nominal role for its second parameter 'a',
+because it appears as an argument to the unknown 'm'. Now consider
+  [W] N Maybe a  ~R#  N Maybe b
+
+If we decompose, we'll get
+  [W] a ~N# b
+
+But if instead we unwrap we'll get
+  [W] Maybe a ~R# Maybe b
+which in turn gives us
+  [W] a ~R# b
+which is easier to satisfy.
+
+Bottom line: unwrap newtypes before decomposing them!
+c.f. Trac #9123 comment:52,53 for a compelling example.
+
 Note [Newtypes can blow the stack]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Suppose we have
@@ -953,16 +1269,15 @@ can_eq_newtype_nc ev swapped ty1 ((gres, co), ty1') ty2 ps_ty2
            -- we have actually used the newtype constructor here, so
            -- make sure we don't warn about importing it!
 
-       ; rewriteEqEvidence ev swapped ty1' ps_ty2
-                           (mkTcSymCo co) (mkTcReflCo Representational ps_ty2)
-         `andWhenContinue` \ new_ev ->
-         can_eq_nc False new_ev ReprEq ty1' ty1' ty2 ps_ty2 }
+       ; new_ev <- rewriteEqEvidence ev swapped ty1' ps_ty2
+                                     (mkTcSymCo co) (mkTcReflCo Representational ps_ty2)
+       ; can_eq_nc False new_ev ReprEq ty1' ty1' ty2 ps_ty2 }
 
 ---------
 -- ^ Decompose a type application.
 -- All input types must be flat. See Note [Canonicalising type applications]
-can_eq_app :: CtEvidence       -- :: s1 t1 ~r s2 t2
-           -> EqRel            -- r
+-- Nominal equality only!
+can_eq_app :: CtEvidence       -- :: s1 t1 ~N s2 t2
            -> Xi -> Xi         -- s1 t1
            -> Xi -> Xi         -- s2 t2
            -> TcS (StopOrContinue Ct)
@@ -970,13 +1285,7 @@ can_eq_app :: CtEvidence       -- :: s1 t1 ~r s2 t2
 -- AppTys only decompose for nominal equality, so this case just leads
 -- to an irreducible constraint; see typecheck/should_compile/T10494
 -- See Note [Decomposing equality], note {4}
-can_eq_app ev ReprEq _ _ _ _
-  = do { traceTcS "failing to decompose representational AppTy equality" (ppr ev)
-       ; continueWith (mkIrredCt ev) }
-          -- no need to call canEqFailure, because that flattens, and the
-          -- types involved here are already flat
-
-can_eq_app ev NomEq s1 t1 s2 t2
+can_eq_app ev s1 t1 s2 t2
   | CtDerived { ctev_loc = loc } <- ev
   = do { unifyDeriveds loc [Nominal, Nominal] [s1, t1] [s2, t2]
        ; stopWith ev "Decomposed [D] AppTy" }
@@ -989,6 +1298,15 @@ can_eq_app ev NomEq s1 t1 s2 t2
        ; let co = mkAppCo co_s co_t
        ; setWantedEq dest co
        ; stopWith ev "Decomposed [W] AppTy" }
+
+    -- If there is a ForAll/(->) mismatch, the use of the Left coercion
+    -- below is ill-typed, potentially leading to a panic in splitTyConApp
+    -- Test case: typecheck/should_run/Typeable1
+    -- We could also include this mismatch check above (for W and D), but it's slow
+    -- and we'll get a better error message not doing it
+  | s1k `mismatches` s2k
+  = canEqHardFailure ev (s1 `mkAppTy` t1) (s2 `mkAppTy` t2)
+
   | CtGiven { ctev_evar = evar, ctev_loc = loc } <- ev
   = do { let co   = mkTcCoVarCo evar
              co_s = mkTcLRCo CLeft  co
@@ -999,8 +1317,14 @@ can_eq_app ev NomEq s1 t1 s2 t2
                                      , evCoercion co_t )
        ; emitWorkNC [evar_t]
        ; canEqNC evar_s NomEq s1 s2 }
-  | otherwise  -- Can't happen
-  = error "can_eq_app"
+
+  where
+    s1k = tcTypeKind s1
+    s2k = tcTypeKind s2
+
+    k1 `mismatches` k2
+      =  isForAllTy k1 && not (isForAllTy k2)
+      || not (isForAllTy k1) && isForAllTy k2
 
 -----------------------
 -- | Break apart an equality over a casted type
@@ -1016,12 +1340,10 @@ canEqCast flat ev eq_rel swapped ty1 co1 ty2 ps_ty2
   = do { traceTcS "Decomposing cast" (vcat [ ppr ev
                                            , ppr ty1 <+> text "|>" <+> ppr co1
                                            , ppr ps_ty2 ])
-       ; rewriteEqEvidence ev swapped ty1 ps_ty2
-                           (mkTcReflCo role ty1
-                              `mkTcCoherenceRightCo` co1)
-                           (mkTcReflCo role ps_ty2)
-         `andWhenContinue` \ new_ev ->
-         can_eq_nc flat new_ev eq_rel ty1 ty1 ty2 ps_ty2 }
+       ; new_ev <- rewriteEqEvidence ev swapped ty1 ps_ty2
+                                     (mkTcGReflRightCo role ty1 co1)
+                                     (mkTcReflCo role ps_ty2)
+       ; can_eq_nc flat new_ev eq_rel ty1 ty1 ty2 ps_ty2 }
   where
     role = eqRelRole eq_rel
 
@@ -1254,11 +1576,15 @@ canDecomposableTyConAppOK :: CtEvidence -> EqRel
                           -> TcS ()
 -- Precondition: tys1 and tys2 are the same length, hence "OK"
 canDecomposableTyConAppOK ev eq_rel tc tys1 tys2
-  = case ev of
+  = ASSERT( tys1 `equalLength` tys2 )
+    case ev of
      CtDerived {}
         -> unifyDeriveds loc tc_roles tys1 tys2
 
      CtWanted { ctev_dest = dest }
+                   -- new_locs and tc_roles are both infinite, so
+                   -- we are guaranteed that cos has the same length
+                   -- as tys1 and tys2
         -> do { cos <- zipWith4M unifyWanted new_locs tc_roles tys1 tys2
               ; setWantedEq dest (mkTyConAppCo role tc cos) }
 
@@ -1266,7 +1592,7 @@ canDecomposableTyConAppOK ev eq_rel tc tys1 tys2
         -> do { let ev_co = mkCoVarCo evar
               ; given_evs <- newGivenEvVars loc $
                              [ ( mkPrimEqPredRole r ty1 ty2
-                               , evCoercion $ mkNthCo i ev_co )
+                               , evCoercion $ mkNthCo i ev_co )
                              | (r, ty1, ty2, i) <- zip4 tc_roles tys1 tys2 [0..]
                              , r /= Phantom
                              , not (isCoercionTy ty1) && not (isCoercionTy ty2) ]
@@ -1274,21 +1600,29 @@ canDecomposableTyConAppOK ev eq_rel tc tys1 tys2
   where
     loc        = ctEvLoc ev
     role       = eqRelRole eq_rel
-    tc_roles   = tyConRolesX role tc
-
-      -- the following makes a better distinction between "kind" and "type"
-      -- in error messages
-    bndrs      = tyConBinders tc
-    is_kinds   = map isNamedTyConBinder bndrs
-    is_viss    = map isVisibleTyConBinder bndrs
 
-    kind_xforms = map (\is_kind -> if is_kind then toKindLoc else id) is_kinds
-    vis_xforms  = map (\is_vis  -> if is_vis  then id
-                                   else flip updateCtLocOrigin toInvisibleOrigin)
-                      is_viss
+      -- infinite, as tyConRolesX returns an infinite tail of Nominal
+    tc_roles   = tyConRolesX role tc
 
-    -- zipWith3 (.) composes its first two arguments and applies it to the third
-    new_locs = zipWith3 (.) kind_xforms vis_xforms (repeat loc)
+      -- Add nuances to the location during decomposition:
+      --  * if the argument is a kind argument, remember this, so that error
+      --    messages say "kind", not "type". This is determined based on whether
+      --    the corresponding tyConBinder is named (that is, dependent)
+      --  * if the argument is invisible, note this as well, again by
+      --    looking at the corresponding binder
+      -- For oversaturated tycons, we need the (repeat loc) tail, which doesn't
+      -- do either of these changes. (Forgetting to do so led to #16188)
+      --
+      -- NB: infinite in length
+    new_locs = [ new_loc
+               | bndr <- tyConBinders tc
+               , let new_loc0 | isNamedTyConBinder bndr = toKindLoc loc
+                              | otherwise               = loc
+                     new_loc  | isVisibleTyConBinder bndr
+                              = updateCtLocOrigin new_loc0 toInvisibleOrigin
+                              | otherwise
+                              = new_loc0 ]
+               ++ repeat loc
 
 -- | Call when canonicalizing an equality fails, but if the equality is
 -- representational, there is some hope for the future.
@@ -1305,9 +1639,8 @@ canEqFailure ev ReprEq ty1 ty2
             -- new equalities become available
        ; traceTcS "canEqFailure with ReprEq" $
          vcat [ ppr ev, ppr ty1, ppr ty2, ppr xi1, ppr xi2 ]
-       ; rewriteEqEvidence ev NotSwapped xi1 xi2 co1 co2
-         `andWhenContinue` \ new_ev ->
-         continueWith (mkIrredCt new_ev) }
+       ; new_ev <- rewriteEqEvidence ev NotSwapped xi1 xi2 co1 co2
+       ; continueWith (mkIrredCt new_ev) }
 
 -- | Call when canonicalizing an equality fails with utterly no hope.
 canEqHardFailure :: CtEvidence
@@ -1316,9 +1649,8 @@ canEqHardFailure :: CtEvidence
 canEqHardFailure ev ty1 ty2
   = do { (s1, co1) <- flatten FM_SubstOnly ev ty1
        ; (s2, co2) <- flatten FM_SubstOnly ev ty2
-       ; rewriteEqEvidence ev NotSwapped s1 s2 co1 co2
-         `andWhenContinue` \ new_ev ->
-         continueWith (mkInsolubleCt new_ev) }
+       ; new_ev <- rewriteEqEvidence ev NotSwapped s1 s2 co1 co2
+       ; continueWith (mkInsolubleCt new_ev) }
 
 {-
 Note [Decomposing TyConApps]
@@ -1421,6 +1753,25 @@ isInsolubleOccursCheck does.
 
 See also #10715, which induced this addition.
 
+Note [canCFunEqCan]
+~~~~~~~~~~~~~~~~~~~
+Flattening the arguments to a type family can change the kind of the type
+family application. As an easy example, consider (Any k) where (k ~ Type)
+is in the inert set. The original (Any k :: k) becomes (Any Type :: Type).
+The problem here is that the fsk in the CFunEqCan will have the old kind.
+
+The solution is to come up with a new fsk/fmv of the right kind. For
+givens, this is easy: just introduce a new fsk and update the flat-cache
+with the new one. For wanteds, we want to solve the old one if favor of
+the new one, so we use dischargeFmv. This also kicks out constraints
+from the inert set; this behavior is correct, as the kind-change may
+allow more constraints to be solved.
+
+We use `isTcReflexiveCo`, to ensure that we only use the hetero-kinded case
+if we really need to.  Of course `flattenArgsNom` should return `Refl`
+whenever possible, but Trac #15577 was an infinite loop because even
+though the coercion was homo-kinded, `kind_co` was not `Refl`, so we
+made a new (identical) CFunEqCan, and then the entire process repeated.
 -}
 
 canCFunEqCan :: CtEvidence
@@ -1432,107 +1783,210 @@ canCFunEqCan :: CtEvidence
 -- and the RHS is a fsk, which we must *not* substitute.
 -- So just substitute in the LHS
 canCFunEqCan ev fn tys fsk
-  = do { (tys', cos) <- flattenManyNom ev tys
+  = do { (tys', cos, kind_co) <- flattenArgsNom ev fn tys
                         -- cos :: tys' ~ tys
+
        ; let lhs_co  = mkTcTyConAppCo Nominal fn cos
                         -- :: F tys' ~ F tys
              new_lhs = mkTyConApp fn tys'
-             fsk_ty  = mkTyVarTy fsk
-       ; rewriteEqEvidence ev NotSwapped new_lhs fsk_ty
-                           lhs_co (mkTcNomReflCo fsk_ty)
-         `andWhenContinue` \ ev' ->
-    do { extendFlatCache fn tys' (ctEvCoercion ev', fsk_ty, ctEvFlavour ev')
+
+             flav    = ctEvFlavour ev
+       ; (ev', fsk')
+           <- if isTcReflexiveCo kind_co   -- See Note [canCFunEqCan]
+              then do { traceTcS "canCFunEqCan: refl" (ppr new_lhs)
+                      ; let fsk_ty = mkTyVarTy fsk
+                      ; ev' <- rewriteEqEvidence ev NotSwapped new_lhs fsk_ty
+                                                 lhs_co (mkTcNomReflCo fsk_ty)
+                      ; return (ev', fsk) }
+              else do { traceTcS "canCFunEqCan: non-refl" $
+                        vcat [ text "Kind co:" <+> ppr kind_co
+                             , text "RHS:" <+> ppr fsk <+> dcolon <+> ppr (tyVarKind fsk)
+                             , text "LHS:" <+> hang (ppr (mkTyConApp fn tys))
+                                                  2 (dcolon <+> ppr (tcTypeKind (mkTyConApp fn tys)))
+                             , text "New LHS" <+> hang (ppr new_lhs)
+                                                     2 (dcolon <+> ppr (tcTypeKind new_lhs)) ]
+                      ; (ev', new_co, new_fsk)
+                          <- newFlattenSkolem flav (ctEvLoc ev) fn tys'
+                      ; let xi = mkTyVarTy new_fsk `mkCastTy` kind_co
+                               -- sym lhs_co :: F tys ~ F tys'
+                               -- new_co     :: F tys' ~ new_fsk
+                               -- co         :: F tys ~ (new_fsk |> kind_co)
+                            co = mkTcSymCo lhs_co `mkTcTransCo`
+                                 mkTcCoherenceRightCo Nominal
+                                                      (mkTyVarTy new_fsk)
+                                                      kind_co
+                                                      new_co
+
+                      ; traceTcS "Discharging fmv/fsk due to hetero flattening" (ppr ev)
+                      ; dischargeFunEq ev fsk co xi
+                      ; return (ev', new_fsk) }
+
+       ; extendFlatCache fn tys' (ctEvCoercion ev', mkTyVarTy fsk', ctEvFlavour ev')
        ; continueWith (CFunEqCan { cc_ev = ev', cc_fun = fn
-                                 , cc_tyargs = tys', cc_fsk = fsk }) } }
+                                 , cc_tyargs = tys', cc_fsk = fsk' }) }
 
 ---------------------
 canEqTyVar :: CtEvidence          -- ev :: lhs ~ rhs
            -> EqRel -> SwapFlag
-           -> TcTyVar -> CoercionN  -- tv1 |> co1
+           -> TcTyVar               -- tv1
            -> TcType                -- lhs: pretty lhs, already flat
            -> TcType -> TcType      -- rhs: already flat
            -> TcS (StopOrContinue Ct)
-canEqTyVar ev eq_rel swapped tv1 co1 ps_ty1 xi2 ps_xi2
-  | k1 `eqType` k2
-  = canEqTyVarHomo ev eq_rel swapped tv1 co1 ps_ty1 xi2 ps_xi2
+canEqTyVar ev eq_rel swapped tv1 ps_ty1 xi2 ps_xi2
+  | k1 `tcEqType` k2
+  = canEqTyVarHomo ev eq_rel swapped tv1 ps_ty1 xi2 ps_xi2
+
+  -- So the LHS and RHS don't have equal kinds
+  -- Note [Flattening] in TcFlatten gives us (F2), which says that
+  -- flattening is always homogeneous (doesn't change kinds). But
+  -- perhaps by flattening the kinds of the two sides of the equality
+  -- at hand makes them equal. So let's try that.
+  | otherwise
+  = do { (flat_k1, k1_co) <- flattenKind loc flav k1  -- k1_co :: flat_k1 ~N kind(xi1)
+       ; (flat_k2, k2_co) <- flattenKind loc flav k2  -- k2_co :: flat_k2 ~N kind(xi2)
+       ; traceTcS "canEqTyVar tried flattening kinds"
+                  (vcat [ sep [ parens (ppr tv1 <+> dcolon <+> ppr k1)
+                              , text "~"
+                              , parens (ppr xi2 <+> dcolon <+> ppr k2) ]
+                        , ppr flat_k1
+                        , ppr k1_co
+                        , ppr flat_k2
+                        , ppr k2_co ])
+
+         -- We know the LHS is a tyvar. So let's dump all the coercions on the RHS
+         -- If flat_k1 == flat_k2, let's dump all the coercions on the RHS and
+         -- then call canEqTyVarHomo. If they don't equal, just rewriteEqEvidence
+         -- (as an optimization, so that we don't have to flatten the kinds again)
+         -- and then emit a kind equality in canEqTyVarHetero.
+         -- See Note [Equalities with incompatible kinds]
+
+       ; let role = eqRelRole eq_rel
+       ; if flat_k1 `tcEqType` flat_k2
+         then do { let rhs_kind_co = mkTcSymCo k2_co `mkTcTransCo` k1_co
+                         -- :: kind(xi2) ~N kind(xi1)
+
+                       new_rhs     = xi2 `mkCastTy` rhs_kind_co
+                       ps_rhs      = ps_xi2 `mkCastTy` rhs_kind_co
+                       rhs_co      = mkTcGReflLeftCo role xi2 rhs_kind_co
+
+                 ; new_ev <- rewriteEqEvidence ev swapped xi1 new_rhs
+                                               (mkTcReflCo role xi1) rhs_co
+                       -- NB: rewriteEqEvidence executes a swap, if any, so we're
+                       -- NotSwapped now.
+                 ; canEqTyVarHomo new_ev eq_rel NotSwapped tv1 ps_ty1 new_rhs ps_rhs }
+         else
+    do { let sym_k1_co = mkTcSymCo k1_co  -- :: kind(xi1) ~N flat_k1
+             sym_k2_co = mkTcSymCo k2_co  -- :: kind(xi2) ~N flat_k2
+
+             new_lhs = xi1 `mkCastTy` sym_k1_co  -- :: flat_k1
+             new_rhs = xi2 `mkCastTy` sym_k2_co  -- :: flat_k2
+             ps_rhs  = ps_xi2 `mkCastTy` sym_k2_co
+
+             lhs_co = mkTcGReflLeftCo role xi1 sym_k1_co
+             rhs_co = mkTcGReflLeftCo role xi2 sym_k2_co
+               -- lhs_co :: (xi1 |> sym k1_co) ~ xi1
+               -- rhs_co :: (xi2 |> sym k2_co) ~ xi2
+
+       ; new_ev <- rewriteEqEvidence ev swapped new_lhs new_rhs lhs_co rhs_co
+         -- no longer swapped, due to rewriteEqEvidence
+       ; canEqTyVarHetero new_ev eq_rel tv1 sym_k1_co flat_k1 ps_ty1
+                                        new_rhs flat_k2 ps_rhs } }
+  where
+    xi1 = mkTyVarTy tv1
+
+    k1 = tyVarKind tv1
+    k2 = tcTypeKind xi2
 
+    loc  = ctEvLoc ev
+    flav = ctEvFlavour ev
+
+canEqTyVarHetero :: CtEvidence   -- :: (tv1 |> co1 :: ki1) ~ (xi2 :: ki2)
+                 -> EqRel
+                 -> TcTyVar -> TcCoercionN -> TcKind  -- tv1 |> co1 :: ki1
+                 -> TcType            -- pretty tv1 (*without* the coercion)
+                 -> TcType -> TcKind  -- xi2 :: ki2
+                 -> TcType            -- pretty xi2
+                 -> TcS (StopOrContinue Ct)
+canEqTyVarHetero ev eq_rel tv1 co1 ki1 ps_tv1 xi2 ki2 ps_xi2
   -- See Note [Equalities with incompatible kinds]
   | CtGiven { ctev_evar = evar } <- ev
-    -- unswapped: tm :: (lhs :: k1) ~ (rhs :: k2)
-    -- swapped  : tm :: (rhs :: k2) ~ (lhs :: k1)
-  = do { kind_ev_id <- newBoundEvVarId kind_pty
-                                       (evCoercion $
-                                        if isSwapped swapped
-                                        then mkTcSymCo $ mkTcKindCo $ mkTcCoVarCo evar
-                                        else             mkTcKindCo $ mkTcCoVarCo evar)
-           -- kind_ev_id :: (k1 :: *) ~ (k2 :: *)   (whether swapped or not)
-       ; let kind_ev = CtGiven { ctev_pred = kind_pty
-                               , ctev_evar = kind_ev_id
-                               , ctev_loc  = kind_loc }
-             homo_co = mkSymCo $ mkCoVarCo kind_ev_id
-             rhs'    = mkCastTy xi2 homo_co
-             ps_rhs' = mkCastTy ps_xi2 homo_co
+    -- unswapped: tm :: (lhs :: ki1) ~ (rhs :: ki2)
+    -- swapped  : tm :: (rhs :: ki2) ~ (lhs :: ki1)
+  = do { let kind_co = mkTcKindCo (mkTcCoVarCo evar)
+       ; kind_ev <- newGivenEvVar kind_loc (kind_pty, evCoercion kind_co)
+       ; let  -- kind_ev :: (ki1 :: *) ~ (ki2 :: *)   (whether swapped or not)
+              -- co1     :: kind(tv1) ~N ki1
+              -- homo_co :: ki2 ~N kind(tv1)
+             homo_co = mkTcSymCo (ctEvCoercion kind_ev) `mkTcTransCo` mkTcSymCo co1
+             rhs'    = mkCastTy xi2 homo_co     -- :: kind(tv1)
+             ps_rhs' = mkCastTy ps_xi2 homo_co  -- :: kind(tv1)
+             rhs_co  = mkTcGReflLeftCo role xi2 homo_co
+               -- rhs_co :: (xi2 |> homo_co :: kind(tv1)) ~ xi2
+
+             lhs'   = mkTyVarTy tv1       -- :: kind(tv1)
+             lhs_co = mkTcGReflRightCo role lhs' co1
+               -- lhs_co :: (tv1 :: kind(tv1)) ~ (tv1 |> co1 :: ki1)
+
        ; traceTcS "Hetero equality gives rise to given kind equality"
-           (ppr kind_ev_id <+> dcolon <+> ppr kind_pty)
+           (ppr kind_ev <+> dcolon <+> ppr kind_pty)
        ; emitWorkNC [kind_ev]
-       ; type_ev <- newGivenEvVar loc $
-                    if isSwapped swapped
-                    then ( mkTcEqPredLikeEv ev rhs' lhs
-                         , evCoercion $
-                           mkTcCoherenceLeftCo (mkTcCoVarCo evar) homo_co )
-                    else ( mkTcEqPredLikeEv ev lhs rhs'
-                         , evCoercion $
-                           mkTcCoherenceRightCo (mkTcCoVarCo evar) homo_co )
-          -- unswapped: type_ev :: (lhs :: k1) ~ ((rhs |> sym kind_ev_id) :: k1)
-          -- swapped  : type_ev :: ((rhs |> sym kind_ev_id) :: k1) ~ (lhs :: k1)
-       ; canEqTyVarHomo type_ev eq_rel swapped tv1 co1 ps_ty1 rhs' ps_rhs' }
+       ; type_ev <- rewriteEqEvidence ev NotSwapped lhs' rhs' lhs_co rhs_co
+       ; canEqTyVarHomo type_ev eq_rel NotSwapped tv1 ps_tv1 rhs' ps_rhs' }
 
   -- See Note [Equalities with incompatible kinds]
   | otherwise   -- Wanted and Derived
-                  -- NB: all kind equalities are Nominal
-  = do { emitNewDerivedEq kind_loc Nominal k1 k2
-             -- kind_ev :: (k1 :: *) ~ (k2 :: *)
+                -- NB: all kind equalities are Nominal
+  = do { emitNewDerivedEq kind_loc Nominal ki1 ki2
+             -- kind_ev :: (ki1 :: *) ~ (ki2 :: *)
        ; traceTcS "Hetero equality gives rise to derived kind equality" $
            ppr ev
        ; continueWith (mkIrredCt ev) }
 
   where
-    lhs = mkTyVarTy tv1 `mkCastTy` co1
-
-    Pair _ k1 = coercionKind co1
-    k2        = typeKind xi2
-
-    kind_pty = mkHeteroPrimEqPred liftedTypeKind liftedTypeKind k1 k2
-    kind_loc = mkKindLoc lhs xi2 loc
+    kind_pty = mkHeteroPrimEqPred liftedTypeKind liftedTypeKind ki1 ki2
+    kind_loc = mkKindLoc (mkTyVarTy tv1 `mkCastTy` co1) xi2 loc
 
     loc  = ctev_loc ev
+    role = eqRelRole eq_rel
 
--- guaranteed that typeKind lhs == typeKind rhs
+-- guaranteed that tcTypeKind lhs == tcTypeKind rhs
 canEqTyVarHomo :: CtEvidence
                -> EqRel -> SwapFlag
-               -> TcTyVar -> CoercionN   -- lhs: tv1 |> co1
+               -> TcTyVar                -- lhs: tv1
                -> TcType                 -- pretty lhs
                -> TcType -> TcType       -- rhs (might not be flat)
                -> TcS (StopOrContinue Ct)
-canEqTyVarHomo ev eq_rel swapped tv1 co1 ps_ty1 ty2 _
+canEqTyVarHomo ev eq_rel swapped tv1 ps_ty1 ty2 _
   | Just (tv2, _) <- tcGetCastedTyVar_maybe ty2
   , tv1 == tv2
-  = canEqReflexive ev eq_rel (mkTyVarTy tv1 `mkCastTy` co1)
-    -- we don't need to check co2 because its type must match co1
+  = canEqReflexive ev eq_rel (mkTyVarTy tv1)
+    -- we don't need to check co because it must be reflexive
 
   | Just (tv2, co2) <- tcGetCastedTyVar_maybe ty2
   , swapOverTyVars tv1 tv2
-  = do { traceTcS "canEqTyVar" (ppr tv1 $$ ppr tv2 $$ ppr swapped)
+  = do { traceTcS "canEqTyVar swapOver" (ppr tv1 $$ ppr tv2 $$ ppr swapped)
          -- FM_Avoid commented out: see Note [Lazy flattening] in TcFlatten
          -- let fmode = FE { fe_ev = ev, fe_mode = FM_Avoid tv1' True }
          -- Flatten the RHS less vigorously, to avoid gratuitous flattening
          -- True <=> xi2 should not itself be a type-function application
+
+       ; let role    = eqRelRole eq_rel
+             sym_co2 = mkTcSymCo co2
+             ty1     = mkTyVarTy tv1
+             new_lhs = ty1 `mkCastTy` sym_co2
+             lhs_co  = mkTcGReflLeftCo role ty1 sym_co2
+
+             new_rhs = mkTyVarTy tv2
+             rhs_co  = mkTcGReflRightCo role new_rhs co2
+
+       ; new_ev <- rewriteEqEvidence ev swapped new_lhs new_rhs lhs_co rhs_co
+
        ; dflags <- getDynFlags
-       ; canEqTyVar2 dflags ev eq_rel (flipSwap swapped) tv2 co2 ps_ty1 }
+       ; canEqTyVar2 dflags new_ev eq_rel IsSwapped tv2 (ps_ty1 `mkCastTy` sym_co2) }
 
-canEqTyVarHomo ev eq_rel swapped tv1 co1 _ _ ps_ty2
+canEqTyVarHomo ev eq_rel swapped tv1 _ _ ps_ty2
   = do { dflags <- getDynFlags
-       ; canEqTyVar2 dflags ev eq_rel swapped tv1 co1 ps_ty2 }
+       ; canEqTyVar2 dflags ev eq_rel swapped tv1 ps_ty2 }
 
 -- The RHS here is either not a casted tyvar, or it's a tyvar but we want
 -- to rewrite the LHS to the RHS (as per swapOverTyVars)
@@ -1540,28 +1994,26 @@ canEqTyVar2 :: DynFlags
             -> CtEvidence   -- lhs ~ rhs (or, if swapped, orhs ~ olhs)
             -> EqRel
             -> SwapFlag
-            -> TcTyVar -> CoercionN     -- lhs = tv |> co, flat
+            -> TcTyVar                  -- lhs = tv, flat
             -> TcType                   -- rhs
             -> TcS (StopOrContinue Ct)
 -- LHS is an inert type variable,
 -- and RHS is fully rewritten, but with type synonyms
 -- preserved as much as possible
-canEqTyVar2 dflags ev eq_rel swapped tv1 co1 orhs
-  | Just nrhs' <- metaTyVarUpdateOK dflags tv1 nrhs  -- No occurs check
+canEqTyVar2 dflags ev eq_rel swapped tv1 rhs
+  | Just rhs' <- metaTyVarUpdateOK dflags tv1 rhs  -- No occurs check
      -- Must do the occurs check even on tyvar/tyvar
      -- equalities, in case have  x ~ (y :: ..x...)
      -- Trac #12593
-  = rewriteEqEvidence ev swapped nlhs nrhs' rewrite_co1 rewrite_co2
-    `andWhenContinue` \ new_ev ->
-    continueWith (CTyEqCan { cc_ev = new_ev, cc_tyvar = tv1
-                           , cc_rhs = nrhs', cc_eq_rel = eq_rel })
+  = do { new_ev <- rewriteEqEvidence ev swapped lhs rhs' rewrite_co1 rewrite_co2
+       ; continueWith (CTyEqCan { cc_ev = new_ev, cc_tyvar = tv1
+                                , cc_rhs = rhs', cc_eq_rel = eq_rel }) }
 
   | otherwise  -- For some reason (occurs check, or forall) we can't unify
                -- We must not use it for further rewriting!
-  = do { traceTcS "canEqTyVar2 can't unify" (ppr tv1 $$ ppr nrhs)
-       ; rewriteEqEvidence ev swapped nlhs nrhs rewrite_co1 rewrite_co2
-         `andWhenContinue` \ new_ev ->
-         if isInsolubleOccursCheck eq_rel tv1 nrhs
+  = do { traceTcS "canEqTyVar2 can't unify" (ppr tv1 $$ ppr rhs)
+       ; new_ev <- rewriteEqEvidence ev swapped lhs rhs rewrite_co1 rewrite_co2
+       ; if isInsolubleOccursCheck eq_rel tv1 rhs
          then continueWith (mkInsolubleCt new_ev)
              -- If we have a ~ [a], it is not canonical, and in particular
              -- we don't want to rewrite existing inerts with it, otherwise
@@ -1577,13 +2029,10 @@ canEqTyVar2 dflags ev eq_rel swapped tv1 co1 orhs
   where
     role = eqRelRole eq_rel
 
-    nlhs = mkTyVarTy tv1
-    nrhs = orhs `mkCastTy` mkTcSymCo co1
+    lhs = mkTyVarTy tv1
 
-    -- rewrite_co1 :: tv1 ~ (tv1 |> co1)
-    -- rewrite_co2 :: (rhs |> sym co1) ~ rhs
-    rewrite_co1  = mkTcReflCo role nlhs `mkTcCoherenceRightCo` co1
-    rewrite_co2  = mkTcReflCo role orhs `mkTcCoherenceLeftCo`  mkTcSymCo co1
+    rewrite_co1  = mkTcReflCo role lhs
+    rewrite_co2  = mkTcReflCo role rhs
 
 -- | Solve a reflexive equality constraint
 canEqReflexive :: CtEvidence    -- ty ~ ty
@@ -1611,36 +2060,18 @@ canEqTyVarTyVar, are these
    number) on the left, so there is the best chance of unifying it
         alpha[3] ~ beta[2]
 
- * If both are meta-tyvars and both at the same level, put a SigTv
+ * If both are meta-tyvars and both at the same level, put a TyVarTv
    on the right if possible
         alpha[2] ~ beta[2](sig-tv)
-   That way, when we unify alpha := beta, we don't lose the SigTv flag.
+   That way, when we unify alpha := beta, we don't lose the TyVarTv flag.
 
  * Put a meta-tv with a System Name on the left if possible so it
    gets eliminated (improves error messages)
 
  * If one is a flatten-skolem, put it on the left so that it is
-   substituted out  Note [Elminate flat-skols]
+   substituted out  Note [Eliminate flat-skols] in TcUinfy
         fsk ~ a
 
-Note [Eliminate flat-skols]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Suppose we have  [G] Num (F [a])
-then we flatten to
-     [G] Num fsk
-     [G] F [a] ~ fsk
-where fsk is a flatten-skolem (FlatSkolTv). Suppose we have
-      type instance F [a] = a
-then we'll reduce the second constraint to
-     [G] a ~ fsk
-and then replace all uses of 'a' with fsk.  That's bad because
-in error messages intead of saying 'a' we'll say (F [a]).  In all
-places, including those where the programmer wrote 'a' in the first
-place.  Very confusing!  See Trac #7862.
-
-Solution: re-orient a~fsk to fsk~a, so that we preferentially eliminate
-the fsk.
-
 Note [Equalities with incompatible kinds]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 What do we do when we have an equality
@@ -1677,11 +2108,16 @@ is embarrassing. See #11198 for more tales of destruction.
 
 The reason for this odd behavior is much the same as
 Note [Wanteds do not rewrite Wanteds] in TcRnTypes: note that the
-new `co` is a Wanted. The solution is then not to use `co` to "rewrite"
--- that is, cast -- `w`, but instead to keep `w` heterogeneous and irreducible.
-Given that we're not using `co`, there is no reason to collect evidence
-for it, so `co` is born a Derived. When the Derived is solved (by unification),
-the original wanted (`w`) will get kicked out.
+new `co` is a Wanted.
+
+   The solution is then not to use `co` to "rewrite" -- that is, cast
+   -- `w`, but instead to keep `w` heterogeneous and
+   irreducible. Given that we're not using `co`, there is no reason to
+   collect evidence for it, so `co` is born a Derived, with a CtOrigin
+   of KindEqOrigin.
+
+When the Derived is solved (by unification), the original wanted (`w`)
+will get kicked out.
 
 Note that, if we had [G] co1 :: k ~ Type available, then none of this code would
 trigger, because flattening would have rewritten k to Type. That is,
@@ -1854,8 +2290,8 @@ rewriteEvidence ev@(CtWanted { ctev_dest = dest
   = do { mb_new_ev <- newWanted loc new_pred
        ; MASSERT( tcCoercionRole co == ctEvRole ev )
        ; setWantedEvTerm dest
-            (EvExpr $ mkEvCast (getEvExpr mb_new_ev)
-                               (tcDowngradeRole Representational (ctEvRole ev) co))
+            (mkEvCast (getEvExpr mb_new_ev)
+                      (tcDowngradeRole Representational (ctEvRole ev) co))
        ; case mb_new_ev of
             Fresh  new_ev -> continueWith new_ev
             Cached _      -> stopWith ev "Cached wanted" }
@@ -1865,10 +2301,10 @@ rewriteEqEvidence :: CtEvidence         -- Old evidence :: olhs ~ orhs (not swap
                                         --              or orhs ~ olhs (swapped)
                   -> SwapFlag
                   -> TcType -> TcType   -- New predicate  nlhs ~ nrhs
-                                        -- Should be zonked, because we use typeKind on nlhs/nrhs
+                                        -- Should be zonked, because we use tcTypeKind on nlhs/nrhs
                   -> TcCoercion         -- lhs_co, of type :: nlhs ~ olhs
                   -> TcCoercion         -- rhs_co, of type :: nrhs ~ orhs
-                  -> TcS (StopOrContinue CtEvidence)  -- Of type nlhs ~ nrhs
+                  -> TcS CtEvidence     -- Of type nlhs ~ nrhs
 -- For (rewriteEqEvidence (Given g olhs orhs) False nlhs nrhs lhs_co rhs_co)
 -- we generate
 -- If not swapped
@@ -1886,19 +2322,18 @@ rewriteEqEvidence :: CtEvidence         -- Old evidence :: olhs ~ orhs (not swap
 -- It's all a form of rewwriteEvidence, specialised for equalities
 rewriteEqEvidence old_ev swapped nlhs nrhs lhs_co rhs_co
   | CtDerived {} <- old_ev  -- Don't force the evidence for a Derived
-  = continueWith (old_ev { ctev_pred = new_pred })
+  = return (old_ev { ctev_pred = new_pred })
 
   | NotSwapped <- swapped
   , isTcReflCo lhs_co      -- See Note [Rewriting with Refl]
   , isTcReflCo rhs_co
-  = continueWith (old_ev { ctev_pred = new_pred })
+  = return (old_ev { ctev_pred = new_pred })
 
   | CtGiven { ctev_evar = old_evar } <- old_ev
   = do { let new_tm = evCoercion (lhs_co
                                   `mkTcTransCo` maybeSym swapped (mkTcCoVarCo old_evar)
                                   `mkTcTransCo` mkTcSymCo rhs_co)
-       ; new_ev <- newGivenEvVar loc' (new_pred, new_tm)
-       ; continueWith new_ev }
+       ; newGivenEvVar loc' (new_pred, new_tm) }
 
   | CtWanted { ctev_dest = dest } <- old_ev
   = do { (new_ev, hole_co) <- newWantedEq loc' (ctEvRole old_ev) nlhs nrhs
@@ -1908,7 +2343,7 @@ rewriteEqEvidence old_ev swapped nlhs nrhs lhs_co rhs_co
                   `mkTransCo` rhs_co
        ; setWantedEq dest co
        ; traceTcS "rewriteEqEvidence" (vcat [ppr old_ev, ppr nlhs, ppr nrhs, ppr co])
-       ; continueWith new_ev }
+       ; return new_ev }
 
   | otherwise
   = panic "rewriteEvidence"
@@ -1928,7 +2363,7 @@ When decomposing equalities we often create new wanted constraints for
 Similar remarks apply for Derived.
 
 Rather than making an equality test (which traverses the structure of the
-type, perhaps fruitlessly, unifyWanted traverses the common structure, and
+type, perhaps fruitlessly), unifyWanted traverses the common structure, and
 bales out when it finds a difference by creating a new Wanted constraint.
 But where it succeeds in finding common structure, it just builds a coercion
 to reflect it.
@@ -1942,7 +2377,7 @@ unifyWanted :: CtLoc -> Role
 -- See Note [unifyWanted and unifyDerived]
 -- The returned coercion's role matches the input parameter
 unifyWanted loc Phantom ty1 ty2
-  = do { kind_co <- unifyWanted loc Nominal (typeKind ty1) (typeKind ty2)
+  = do { kind_co <- unifyWanted loc Nominal (tcTypeKind ty1) (tcTypeKind ty2)
        ; return (mkPhantomCo kind_co ty1 ty2) }
 
 unifyWanted loc role orig_ty1 orig_ty2