Make a smart mkAppTyM
[ghc.git] / compiler / typecheck / TcCanonical.hs
index dc85fe2..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]
@@ -270,6 +289,15 @@ So here's the plan:
    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.
 
@@ -424,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]
+
+  | 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 -> TcS [Ct]
+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
@@ -459,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
@@ -515,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
@@ -533,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
@@ -617,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]
@@ -630,11 +886,14 @@ 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
+
+  | 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
@@ -657,7 +916,7 @@ can_eq_nc' True _rdr_env _envs ev eq_rel ty1 ps_ty1 (TyVarTy tv2) ps_ty2
 -- 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
@@ -676,11 +935,13 @@ 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
@@ -690,9 +951,22 @@ can_eq_nc' False rdr_env envs ev eq_rel _ ps_ty1 _ ps_ty2
        ; 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
@@ -709,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
@@ -727,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" } }
 
@@ -763,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.
@@ -900,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
@@ -976,8 +1276,8 @@ can_eq_newtype_nc ev swapped ty1 ((gres, co), 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)
@@ -985,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" }
@@ -1025,8 +1319,8 @@ can_eq_app ev NomEq s1 t1 s2 t2
        ; canEqNC evar_s NomEq s1 s2 }
 
   where
-    s1k = typeKind s1
-    s2k = typeKind s2
+    s1k = tcTypeKind s1
+    s2k = tcTypeKind s2
 
     k1 `mismatches` k2
       =  isForAllTy k1 && not (isForAllTy k2)
@@ -1047,7 +1341,7 @@ canEqCast flat ev eq_rel swapped ty1 co1 ty2 ps_ty2
                                            , ppr ty1 <+> text "|>" <+> ppr co1
                                            , ppr ps_ty2 ])
        ; new_ev <- rewriteEqEvidence ev swapped ty1 ps_ty2
-                                     (mkTcReflCo role ty1 `mkTcCoherenceRightCo` co1)
+                                     (mkTcGReflRightCo role ty1 co1)
                                      (mkTcReflCo role ps_ty2)
        ; can_eq_nc flat new_ev eq_rel ty1 ty1 ty2 ps_ty2 }
   where
@@ -1282,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) }
 
@@ -1302,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.
@@ -1461,6 +1767,11 @@ 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
@@ -1474,33 +1785,40 @@ canCFunEqCan :: CtEvidence
 canCFunEqCan ev fn tys fsk
   = 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'
 
              flav    = ctEvFlavour ev
        ; (ev', fsk')
-              -- See Note [canCFunEqCan]
-           <- if isTcReflCo kind_co
-              then do { let fsk_ty = mkTyVarTy 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 { (ev', new_co, new_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'
-                      ; case flav of
-                          Given -> return () -- nothing more to do.
-                                             -- NB: new_co is stored within ev',
-                                             -- and will be put in the flat_cache below
-                          _     -> do { let xi = mkTyVarTy new_fsk `mkCastTy` kind_co
-                                               -- sym lhs_co :: F tys ~ F tys'
-                                               -- new_co     :: F tys' ~ new_fsk
-                                               -- co         :: F tys ~ (new_fsk |> kind_co)
-                                            co = mkTcSymCo lhs_co `mkTcTransCo`
-                                                 (new_co `mkTcCoherenceRightCo` kind_co)
-
-                                      ; traceTcS "Discharging fmv due to hetero flattening" empty
-                                      ; dischargeFmv ev fsk co xi }
+                      ; let xi = mkTyVarTy new_fsk `mkCastTy` kind_co
+                               -- sym lhs_co :: F tys ~ F tys'
+                               -- new_co     :: F tys' ~ new_fsk
+                               -- co         :: F tys ~ (new_fsk |> kind_co)
+                            co = mkTcSymCo lhs_co `mkTcTransCo`
+                                 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')
@@ -1518,10 +1836,11 @@ 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
 
-         -- 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.
+  -- 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)
@@ -1534,7 +1853,7 @@ canEqTyVar ev eq_rel swapped tv1 ps_ty1 xi2 ps_xi2
                         , ppr flat_k2
                         , ppr k2_co ])
 
-         -- we know the LHS is a tyvar. So let's dump all the coercions on the RHS
+         -- 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)
@@ -1548,7 +1867,7 @@ canEqTyVar ev eq_rel swapped tv1 ps_ty1 xi2 ps_xi2
 
                        new_rhs     = xi2 `mkCastTy` rhs_kind_co
                        ps_rhs      = ps_xi2 `mkCastTy` rhs_kind_co
-                       rhs_co      = mkTcReflCo role xi2 `mkTcCoherenceLeftCo` rhs_kind_co
+                       rhs_co      = mkTcGReflLeftCo role xi2 rhs_kind_co
 
                  ; new_ev <- rewriteEqEvidence ev swapped xi1 new_rhs
                                                (mkTcReflCo role xi1) rhs_co
@@ -1563,8 +1882,8 @@ canEqTyVar ev eq_rel swapped tv1 ps_ty1 xi2 ps_xi2
              new_rhs = xi2 `mkCastTy` sym_k2_co  -- :: flat_k2
              ps_rhs  = ps_xi2 `mkCastTy` sym_k2_co
 
-             lhs_co = mkReflCo role xi1 `mkTcCoherenceLeftCo` sym_k1_co
-             rhs_co = mkReflCo role xi2 `mkTcCoherenceLeftCo` 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
 
@@ -1576,7 +1895,7 @@ canEqTyVar ev eq_rel swapped tv1 ps_ty1 xi2 ps_xi2
     xi1 = mkTyVarTy tv1
 
     k1 = tyVarKind tv1
-    k2 = typeKind xi2
+    k2 = tcTypeKind xi2
 
     loc  = ctEvLoc ev
     flav = ctEvFlavour ev
@@ -1593,34 +1912,30 @@ canEqTyVarHetero ev eq_rel tv1 co1 ki1 ps_tv1 xi2 ki2 ps_xi2
   | CtGiven { ctev_evar = evar } <- ev
     -- unswapped: tm :: (lhs :: ki1) ~ (rhs :: ki2)
     -- swapped  : tm :: (rhs :: ki2) ~ (lhs :: ki1)
-  = do { kind_ev_id <- newBoundEvVarId kind_pty
-                                       (evCoercion $ mkTcKindCo $ mkTcCoVarCo evar)
-           -- kind_ev_id :: (ki1 :: *) ~ (ki2 :: *)   (whether swapped or not)
-       ; let kind_ev = CtGiven { ctev_pred = kind_pty
-                               , ctev_evar = kind_ev_id
-                               , ctev_loc  = kind_loc }
+  = do { let kind_co = mkTcKindCo (mkTcCoVarCo evar)
+       ; kind_ev <- newGivenEvVar kind_loc (kind_pty, evCoercion kind_co)
+       ; let  -- kind_ev :: (ki1 :: *) ~ (ki2 :: *)   (whether swapped or not)
               -- co1     :: kind(tv1) ~N ki1
               -- homo_co :: ki2 ~N kind(tv1)
-             homo_co = mkTcSymCo (mkCoVarCo kind_ev_id) `mkTcTransCo` mkTcSymCo co1
-
+             homo_co = mkTcSymCo (ctEvCoercion kind_ev) `mkTcTransCo` mkTcSymCo co1
              rhs'    = mkCastTy xi2 homo_co     -- :: kind(tv1)
              ps_rhs' = mkCastTy ps_xi2 homo_co  -- :: kind(tv1)
-             rhs_co  = mkReflCo role xi2 `mkTcCoherenceLeftCo` homo_co
+             rhs_co  = mkTcGReflLeftCo role xi2 homo_co
                -- rhs_co :: (xi2 |> homo_co :: kind(tv1)) ~ xi2
 
              lhs'   = mkTyVarTy tv1       -- :: kind(tv1)
-             lhs_co = mkReflCo role lhs' `mkTcCoherenceRightCo` co1
+             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 <- 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
+                -- 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" $
@@ -1634,7 +1949,7 @@ canEqTyVarHetero ev eq_rel tv1 co1 ki1 ps_tv1 xi2 ki2 ps_xi2
     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                -- lhs: tv1
@@ -1659,10 +1974,10 @@ canEqTyVarHomo ev eq_rel swapped tv1 ps_ty1 ty2 _
              sym_co2 = mkTcSymCo co2
              ty1     = mkTyVarTy tv1
              new_lhs = ty1 `mkCastTy` sym_co2
-             lhs_co  = mkReflCo role ty1 `mkTcCoherenceLeftCo` sym_co2
+             lhs_co  = mkTcGReflLeftCo role ty1 sym_co2
 
              new_rhs = mkTyVarTy tv2
-             rhs_co  = mkReflCo role new_rhs `mkTcCoherenceRightCo` co2
+             rhs_co  = mkTcGReflRightCo role new_rhs co2
 
        ; new_ev <- rewriteEqEvidence ev swapped new_lhs new_rhs lhs_co rhs_co
 
@@ -1745,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
@@ -1993,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" }
@@ -2004,7 +2301,7 @@ 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 CtEvidence     -- Of type nlhs ~ nrhs
@@ -2080,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