Make a smart mkAppTyM
[ghc.git] / compiler / typecheck / TcUnify.hs
index ca33478..6af873e 100644 (file)
@@ -6,36 +6,39 @@
 Type subsumption and unification
 -}
 
-{-# LANGUAGE CPP, MultiWayIf, TupleSections #-}
+{-# LANGUAGE CPP, MultiWayIf, TupleSections, ScopedTypeVariables #-}
 
 module TcUnify (
   -- Full-blown subsumption
   tcWrapResult, tcWrapResultO, tcSkolemise, tcSkolemiseET,
-  tcSubTypeHR, tcSubType, tcSubTypeO, tcSubType_NC, tcSubTypeDS, tcSubTypeDS_O,
-  tcSubTypeDS_NC, tcSubTypeDS_NC_O, tcSubTypeET, tcSubTypeET_NC,
-  checkConstraints, buildImplicationFor,
+  tcSubTypeHR, tcSubTypeO, tcSubType_NC, tcSubTypeDS,
+  tcSubTypeDS_NC_O, tcSubTypeET,
+  checkConstraints, checkTvConstraints,
+  buildImplicationFor, emitResidualTvConstraint,
 
   -- Various unifications
-  unifyType, unifyTheta, unifyKind, noThing,
-  uType, unifyExpType,
+  unifyType, unifyKind,
+  uType, promoteTcType,
+  swapOverTyVars, canSolveByUnification,
 
   --------------------------------
   -- Holes
-  tcInfer,
+  tcInferInst, tcInferNoInst,
   matchExpectedListTy,
-  matchExpectedPArrTy,
   matchExpectedTyConApp,
   matchExpectedAppTy,
   matchExpectedFunTys,
   matchActualFunTys, matchActualFunTysPart,
   matchExpectedFunKind,
 
-  wrapFunResCoercion
+  metaTyVarUpdateOK, occCheckForErrors, OccCheckResult(..)
 
   ) where
 
 #include "HsVersions.h"
 
+import GhcPrelude
+
 import HsSyn
 import TyCoRep
 import TcMType
@@ -44,21 +47,21 @@ import TcType
 import Type
 import Coercion
 import TcEvidence
-import Name ( isSystemName )
+import Name( isSystemName )
 import Inst
 import TyCon
 import TysWiredIn
+import TysPrim( tYPE )
 import Var
 import VarSet
 import VarEnv
 import ErrUtils
 import DynFlags
 import BasicTypes
-import Name   ( Name )
 import Bag
 import Util
+import qualified GHC.LanguageExtensions as LangExt
 import Outputable
-import FastString
 
 import Control.Monad
 import Control.Arrow ( second )
@@ -92,6 +95,23 @@ This is used to construct a message of form
    The function 'f' is applied to two arguments
    but its type `Int -> Int' has only one
 
+When visible type applications (e.g., `f @Int 1 2`, as in #13902) enter the
+picture, we have a choice in deciding whether to count the type applications as
+proper arguments:
+
+   The function 'f' is applied to one visible type argument
+     and two value arguments
+   but its type `forall a. a -> a` has only one visible type argument
+     and one value argument
+
+Or whether to include the type applications as part of the herald itself:
+
+   The expression 'f @Int' is applied to two arguments
+   but its type `Int -> Int` has only one
+
+The latter is easier to implement and is arguably easier to understand, so we
+choose to implement that option.
+
 Note [matchExpectedFunTys]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~
 matchExpectedFunTys checks that a sigma has the form
@@ -111,14 +131,15 @@ passed in.
 -}
 
 -- Use this one when you have an "expected" type.
-matchExpectedFunTys :: SDoc   -- See Note [Herald for matchExpectedFunTys]
+matchExpectedFunTys :: forall a.
+                       SDoc   -- See Note [Herald for matchExpectedFunTys]
                     -> Arity
                     -> ExpRhoType  -- deeply skolemised
                     -> ([ExpSigmaType] -> ExpRhoType -> TcM a)
                           -- must fill in these ExpTypes here
                     -> TcM (a, HsWrapper)
 -- If    matchExpectedFunTys n ty = (_, wrap)
--- then  wrap : (t1 -> ... -> tn -> ty_r) "->" ty,
+-- then  wrap : (t1 -> ... -> tn -> ty_r) ~> ty,
 --   where [t1, ..., tn], ty_r are passed to the thing_inside
 matchExpectedFunTys herald arity orig_ty thing_inside
   = case orig_ty of
@@ -130,17 +151,20 @@ matchExpectedFunTys herald arity orig_ty thing_inside
            ; return (result, idHsWrapper) }
 
     go acc_arg_tys n ty
-      | Just ty' <- coreView ty = go acc_arg_tys n ty'
+      | Just ty' <- tcView ty = go acc_arg_tys n ty'
 
     go acc_arg_tys n (FunTy arg_ty res_ty)
       = ASSERT( not (isPredTy arg_ty) )
         do { (result, wrap_res) <- go (mkCheckExpType arg_ty : acc_arg_tys)
                                       (n-1) res_ty
            ; return ( result
-                    , mkWpFun idHsWrapper wrap_res arg_ty res_ty ) }
+                    , mkWpFun idHsWrapper wrap_res arg_ty res_ty doc ) }
+      where
+        doc = text "When inferring the argument type of a function with type" <+>
+              quotes (ppr orig_ty)
 
     go acc_arg_tys n ty@(TyVarTy tv)
-      | ASSERT( isTcTyVar tv) isMetaTyVar tv
+      | isMetaTyVar tv
       = do { cts <- readMetaTyVar tv
            ; case cts of
                Indirect ty' -> go acc_arg_tys n ty'
@@ -165,14 +189,16 @@ matchExpectedFunTys herald arity orig_ty thing_inside
                           defer acc_arg_tys n (mkCheckExpType ty)
 
     ------------
+    defer :: [ExpSigmaType] -> Arity -> ExpRhoType -> TcM (a, HsWrapper)
     defer acc_arg_tys n fun_ty
-      = do { more_arg_tys <- replicateM n newOpenInferExpType
-           ; res_ty       <- newOpenInferExpType
+      = do { more_arg_tys <- replicateM n newInferExpTypeNoInst
+           ; res_ty       <- newInferExpTypeInst
            ; result       <- thing_inside (reverse acc_arg_tys ++ more_arg_tys) res_ty
            ; more_arg_tys <- mapM readExpType more_arg_tys
            ; res_ty       <- readExpType res_ty
            ; let unif_fun_ty = mkFunTys more_arg_tys res_ty
-           ; wrap <- tcSubTypeDS GenSigCtxt noThing unif_fun_ty fun_ty
+           ; wrap <- tcSubTypeDS AppOrigin GenSigCtxt unif_fun_ty fun_ty
+                         -- Not a good origin at all :-(
            ; return (result, wrap) }
 
     ------------
@@ -189,24 +215,22 @@ matchExpectedFunTys herald arity orig_ty thing_inside
 
 -- Like 'matchExpectedFunTys', but used when you have an "actual" type,
 -- for example in function application
-matchActualFunTys :: Outputable a
-                  => SDoc   -- See Note [Herald for matchExpectedFunTys]
+matchActualFunTys :: SDoc   -- See Note [Herald for matchExpectedFunTys]
                   -> CtOrigin
-                  -> Maybe a   -- the thing with type TcSigmaType
+                  -> Maybe (HsExpr GhcRn)   -- the thing with type TcSigmaType
                   -> Arity
                   -> TcSigmaType
                   -> TcM (HsWrapper, [TcSigmaType], TcSigmaType)
 -- If    matchActualFunTys n ty = (wrap, [t1,..,tn], ty_r)
--- then  wrap : ty "->" (t1 -> ... -> tn -> ty_r)
+-- then  wrap : ty ~> (t1 -> ... -> tn -> ty_r)
 matchActualFunTys herald ct_orig mb_thing arity ty
   = matchActualFunTysPart herald ct_orig mb_thing arity ty [] arity
 
 -- | Variant of 'matchActualFunTys' that works when supplied only part
 -- (that is, to the right of some arrows) of the full function type
-matchActualFunTysPart :: Outputable a
-                      => SDoc -- See Note [Herald for matchExpectedFunTys]
+matchActualFunTysPart :: SDoc -- See Note [Herald for matchExpectedFunTys]
                       -> CtOrigin
-                      -> Maybe a  -- the thing with type TcSigmaType
+                      -> Maybe (HsExpr GhcRn)  -- the thing with type TcSigmaType
                       -> Arity
                       -> TcSigmaType
                       -> [TcSigmaType] -- reversed args. See (*) below.
@@ -256,16 +280,19 @@ matchActualFunTysPart herald ct_orig mb_thing arity orig_ty
         (tvs, theta, _) = tcSplitSigmaTy ty
 
     go n acc_args ty
-      | Just ty' <- coreView ty = go n acc_args ty'
+      | Just ty' <- tcView ty = go n acc_args ty'
 
     go n acc_args (FunTy arg_ty res_ty)
       = ASSERT( not (isPredTy arg_ty) )
         do { (wrap_res, tys, ty_r) <- go (n-1) (arg_ty : acc_args) res_ty
-           ; return ( mkWpFun idHsWrapper wrap_res arg_ty ty_r
+           ; return ( mkWpFun idHsWrapper wrap_res arg_ty ty_r doc
                     , arg_ty : tys, ty_r ) }
+      where
+        doc = text "When inferring the argument type of a function with type" <+>
+              quotes (ppr orig_ty)
 
     go n acc_args ty@(TyVarTy tv)
-      | ASSERT( isTcTyVar tv) isMetaTyVar tv
+      | isMetaTyVar tv
       = do { cts <- readMetaTyVar tv
            ; case cts of
                Indirect ty' -> go n acc_args ty'
@@ -332,13 +359,6 @@ matchExpectedListTy exp_ty
  = do { (co, [elt_ty]) <- matchExpectedTyConApp listTyCon exp_ty
       ; return (co, elt_ty) }
 
-----------------------
-matchExpectedPArrTy :: TcRhoType -> TcM (TcCoercionN, TcRhoType)
--- Special case for parrs
-matchExpectedPArrTy exp_ty
-  = do { (co, [elt_ty]) <- matchExpectedTyConApp parrTyCon exp_ty
-       ; return (co, elt_ty) }
-
 ---------------------
 matchExpectedTyConApp :: TyCon                -- T :: forall kv1 ... kvm. k1 -> ... -> kn -> *
                       -> TcRhoType            -- orig_ty
@@ -351,10 +371,10 @@ matchExpectedTyConApp :: TyCon                -- T :: forall kv1 ... kvm. k1 ->
 -- Postcondition: (T k1 k2 k3 a b c) is well-kinded
 
 matchExpectedTyConApp tc orig_ty
-  = go orig_ty
+  = ASSERT(tc /= funTyCon) go orig_ty
   where
     go ty
-       | Just ty' <- coreView ty
+       | Just ty' <- tcView ty
        = go ty'
 
     go ty@(TyConApp tycon args)
@@ -362,7 +382,7 @@ matchExpectedTyConApp tc orig_ty
        = return (mkTcNomReflCo ty, args)
 
     go (TyVarTy tv)
-       | ASSERT( isTcTyVar tv) isMetaTyVar tv
+       | isMetaTyVar tv
        = do { cts <- readMetaTyVar tv
             ; case cts of
                 Indirect ty -> go ty
@@ -376,16 +396,16 @@ matchExpectedTyConApp tc orig_ty
     -- kind-compatible with T.  For example, suppose we have
     --       matchExpectedTyConApp T (f Maybe)
     -- where data T a = MkT a
-    -- Then we don't want to instantate T's data constructors with
+    -- Then we don't want to instantiate T's data constructors with
     --    (a::*) ~ Maybe
     -- because that'll make types that are utterly ill-kinded.
     -- This happened in Trac #7368
     defer
       = do { (_, arg_tvs) <- newMetaTyVars (tyConTyVars tc)
-           ; traceTc "mtca" (ppr tc $$ ppr (tyConTyVars tc) $$ ppr arg_tvs)
+           ; traceTc "matchExpectedTyConApp" (ppr tc $$ ppr (tyConTyVars tc) $$ ppr arg_tvs)
            ; let args = mkTyVarTys arg_tvs
                  tc_template = mkTyConApp tc args
-           ; co <- unifyType noThing tc_template orig_ty
+           ; co <- unifyType Nothing tc_template orig_ty
            ; return (co, args) }
 
 ----------------------
@@ -399,13 +419,13 @@ matchExpectedAppTy orig_ty
   = go orig_ty
   where
     go ty
-      | Just ty' <- coreView ty = go ty'
+      | Just ty' <- tcView ty = go ty'
 
       | Just (fun_ty, arg_ty) <- tcSplitAppTy_maybe ty
       = return (mkTcNomReflCo orig_ty, (fun_ty, arg_ty))
 
     go (TyVarTy tv)
-      | ASSERT( isTcTyVar tv) isMetaTyVar tv
+      | isMetaTyVar tv
       = do { cts <- readMetaTyVar tv
            ; case cts of
                Indirect ty -> go ty
@@ -417,10 +437,10 @@ matchExpectedAppTy orig_ty
     defer
       = do { ty1 <- newFlexiTyVarTy kind1
            ; ty2 <- newFlexiTyVarTy kind2
-           ; co <- unifyType noThing (mkAppTy ty1 ty2) orig_ty
+           ; co <- unifyType Nothing (mkAppTy ty1 ty2) orig_ty
            ; return (co, (ty1, ty2)) }
 
-    orig_kind = typeKind orig_ty
+    orig_kind = tcTypeKind orig_ty
     kind1 = mkFunTy liftedTypeKind orig_kind
     kind2 = liftedTypeKind    -- m :: * -> k
                               -- arg type :: *
@@ -516,88 +536,48 @@ skolemising the type.
 
 -- | Call this variant when you are in a higher-rank situation and
 -- you know the right-hand type is deeply skolemised.
-tcSubTypeHR :: Outputable a
-            => CtOrigin    -- ^ of the actual type
-            -> Maybe a     -- ^ If present, it has type ty_actual
+tcSubTypeHR :: CtOrigin               -- ^ of the actual type
+            -> Maybe (HsExpr GhcRn)   -- ^ If present, it has type ty_actual
             -> TcSigmaType -> ExpRhoType -> TcM HsWrapper
 tcSubTypeHR orig = tcSubTypeDS_NC_O orig GenSigCtxt
 
-tcSubType :: Outputable a
-          => UserTypeCtxt -> Maybe a  -- ^ If present, it has type ty_actual
-          -> TcSigmaType -> ExpSigmaType -> TcM HsWrapper
--- Checks that actual <= expected
--- Returns HsWrapper :: actual ~ expected
-tcSubType ctxt maybe_thing ty_actual ty_expected
-  = tcSubTypeO origin ctxt ty_actual ty_expected
+------------------------
+tcSubTypeET :: CtOrigin -> UserTypeCtxt
+            -> ExpSigmaType -> TcSigmaType -> TcM HsWrapper
+-- If wrap = tc_sub_type_et t1 t2
+--    => wrap :: t1 ~> t2
+tcSubTypeET orig ctxt (Check ty_actual) ty_expected
+  = tc_sub_tc_type eq_orig orig ctxt ty_actual ty_expected
   where
-    origin = TypeEqOrigin { uo_actual   = ty_actual
-                          , uo_expected = ty_expected
-                          , uo_thing    = mkErrorThing <$> maybe_thing }
-
-
--- | This is like 'tcSubType' but accepts an 'ExpType' as the /actual/ type.
--- You probably want this only when looking at patterns, never expressions.
-tcSubTypeET :: CtOrigin -> ExpSigmaType -> TcSigmaType -> TcM HsWrapper
-tcSubTypeET orig ty_actual ty_expected
-  = uExpTypeX orig ty_expected ty_actual
-              (return . mkWpCastN . mkTcSymCo)
-              (\ty_a -> tcSubTypeO orig GenSigCtxt ty_a
-                                    (mkCheckExpType ty_expected))
-
--- | This is like 'tcSubType' but accepts an 'ExpType' as the /actual/ type.
--- You probably want this only when looking at patterns, never expressions.
--- Does not add context.
-tcSubTypeET_NC :: UserTypeCtxt -> ExpSigmaType -> TcSigmaType -> TcM HsWrapper
-tcSubTypeET_NC _ ty_actual@(Infer {}) ty_expected
-  = mkWpCastN . mkTcSymCo <$> unifyExpType noThing ty_expected ty_actual
-tcSubTypeET_NC ctxt (Check ty_actual) ty_expected
-  = tc_sub_type orig orig ctxt ty_actual ty_expected'
-  where
-    ty_expected' = mkCheckExpType ty_expected
-    orig = TypeEqOrigin { uo_actual   = ty_actual
-                        , uo_expected = ty_expected'
-                        , uo_thing    = Nothing }
-
+    eq_orig = TypeEqOrigin { uo_actual   = ty_expected
+                           , uo_expected = ty_actual
+                           , uo_thing    = Nothing
+                           , uo_visible  = True }
+
+tcSubTypeET _ _ (Infer inf_res) ty_expected
+  = ASSERT2( not (ir_inst inf_res), ppr inf_res $$ ppr ty_expected )
+      -- An (Infer inf_res) ExpSigmaType passed into tcSubTypeET never
+      -- has the ir_inst field set.  Reason: in patterns (which is what
+      -- tcSubTypeET is used for) do not aggressively instantiate
+    do { co <- fill_infer_result ty_expected inf_res
+               -- Since ir_inst is false, we can skip fillInferResult
+               -- and go straight to fill_infer_result
+
+       ; return (mkWpCastN (mkTcSymCo co)) }
+
+------------------------
 tcSubTypeO :: CtOrigin      -- ^ of the actual type
            -> UserTypeCtxt  -- ^ of the expected type
            -> TcSigmaType
-           -> ExpSigmaType
+           -> ExpRhoType
            -> TcM HsWrapper
-tcSubTypeO origin ctxt ty_actual ty_expected
-  = addSubTypeCtxt ty_actual ty_expected $
-    do { traceTc "tcSubType" (vcat [ pprCtOrigin origin
-                                   , pprUserTypeCtxt ctxt
-                                   , ppr ty_actual
-                                   , ppr ty_expected ])
-       ; tc_sub_type eq_orig origin ctxt ty_actual ty_expected }
-  where
-    eq_orig | TypeEqOrigin {} <- origin = origin
-            | otherwise
-            = TypeEqOrigin { uo_actual   = ty_actual
-                           , uo_expected = ty_expected
-                           , uo_thing    = Nothing }
-
-tcSubTypeDS :: Outputable a => UserTypeCtxt -> Maybe a  -- ^ has type ty_actual
-            -> TcSigmaType -> ExpRhoType -> TcM HsWrapper
--- Just like tcSubType, but with the additional precondition that
--- ty_expected is deeply skolemised (hence "DS")
-tcSubTypeDS ctxt m_expr ty_actual ty_expected
-  = addSubTypeCtxt ty_actual ty_expected $
-    tcSubTypeDS_NC ctxt m_expr ty_actual ty_expected
-
--- | Like 'tcSubTypeDS', but takes a 'CtOrigin' to use when instantiating
--- the "actual" type
-tcSubTypeDS_O :: Outputable a
-              => CtOrigin -> UserTypeCtxt
-              -> Maybe a -> TcSigmaType -> ExpRhoType
-              -> TcM HsWrapper
-tcSubTypeDS_O orig ctxt maybe_thing ty_actual ty_expected
+tcSubTypeO orig ctxt ty_actual ty_expected
   = addSubTypeCtxt ty_actual ty_expected $
     do { traceTc "tcSubTypeDS_O" (vcat [ pprCtOrigin orig
                                        , pprUserTypeCtxt ctxt
                                        , ppr ty_actual
                                        , ppr ty_expected ])
-       ; tcSubTypeDS_NC_O orig ctxt maybe_thing ty_actual ty_expected }
+       ; tcSubTypeDS_NC_O orig ctxt Nothing ty_actual ty_expected }
 
 addSubTypeCtxt :: TcType -> ExpType -> TcM a -> TcM a
 addSubTypeCtxt ty_actual ty_expected thing_inside
@@ -627,89 +607,135 @@ addSubTypeCtxt ty_actual ty_expected thing_inside
 -- The "_NC" variants do not add a typechecker-error context;
 -- the caller is assumed to do that
 
-tcSubType_NC :: UserTypeCtxt -> TcSigmaType -> ExpSigmaType -> TcM HsWrapper
+tcSubType_NC :: UserTypeCtxt -> TcSigmaType -> TcSigmaType -> TcM HsWrapper
+-- Checks that actual <= expected
+-- Returns HsWrapper :: actual ~ expected
 tcSubType_NC ctxt ty_actual ty_expected
   = do { traceTc "tcSubType_NC" (vcat [pprUserTypeCtxt ctxt, ppr ty_actual, ppr ty_expected])
-       ; tc_sub_type origin origin ctxt ty_actual ty_expected }
+       ; tc_sub_tc_type origin origin ctxt ty_actual ty_expected }
   where
     origin = TypeEqOrigin { uo_actual   = ty_actual
                           , uo_expected = ty_expected
-                          , uo_thing    = Nothing }
-
-tcSubTypeDS_NC :: Outputable a
-               => UserTypeCtxt
-               -> Maybe a  -- ^ If present, this has type ty_actual
-               -> TcSigmaType -> ExpRhoType -> TcM HsWrapper
-tcSubTypeDS_NC ctxt maybe_thing ty_actual ty_expected
-  = do { traceTc "tcSubTypeDS_NC" (vcat [pprUserTypeCtxt ctxt, ppr ty_actual, ppr ty_expected])
-       ; tcSubTypeDS_NC_O origin ctxt maybe_thing ty_actual ty_expected }
-  where
-    origin = TypeEqOrigin { uo_actual   = ty_actual
-                          , uo_expected = ty_expected
-                          , uo_thing    = mkErrorThing <$> maybe_thing }
+                          , uo_thing    = Nothing
+                          , uo_visible  = True }
+
+tcSubTypeDS :: CtOrigin -> UserTypeCtxt -> TcSigmaType -> ExpRhoType -> TcM HsWrapper
+-- Just like tcSubType, but with the additional precondition that
+-- ty_expected is deeply skolemised (hence "DS")
+tcSubTypeDS orig ctxt ty_actual ty_expected
+  = addSubTypeCtxt ty_actual ty_expected $
+    do { traceTc "tcSubTypeDS_NC" (vcat [pprUserTypeCtxt ctxt, ppr ty_actual, ppr ty_expected])
+       ; tcSubTypeDS_NC_O orig ctxt Nothing ty_actual ty_expected }
 
-tcSubTypeDS_NC_O :: Outputable a
-                 => CtOrigin   -- origin used for instantiation only
+tcSubTypeDS_NC_O :: CtOrigin   -- origin used for instantiation only
                  -> UserTypeCtxt
-                 -> Maybe a
+                 -> Maybe (HsExpr GhcRn)
                  -> TcSigmaType -> ExpRhoType -> TcM HsWrapper
 -- Just like tcSubType, but with the additional precondition that
 -- ty_expected is deeply skolemised
-tcSubTypeDS_NC_O inst_orig ctxt m_thing ty_actual et
-  = uExpTypeX eq_orig ty_actual et
-      (return . mkWpCastN)
-      (tc_sub_type_ds eq_orig inst_orig ctxt ty_actual)
-  where
-    eq_orig = TypeEqOrigin { uo_actual = ty_actual, uo_expected = et
-                           , uo_thing = mkErrorThing <$> m_thing }
+tcSubTypeDS_NC_O inst_orig ctxt m_thing ty_actual ty_expected
+  = case ty_expected of
+      Infer inf_res -> fillInferResult inst_orig ty_actual inf_res
+      Check ty      -> tc_sub_type_ds eq_orig inst_orig ctxt ty_actual ty
+         where
+           eq_orig = TypeEqOrigin { uo_actual = ty_actual, uo_expected = ty
+                                  , uo_thing  = ppr <$> m_thing
+                                  , uo_visible = True }
 
 ---------------
-tc_sub_type :: CtOrigin   -- origin used when calling uType
-            -> CtOrigin   -- origin used when instantiating
-            -> UserTypeCtxt -> TcSigmaType -> ExpSigmaType -> TcM HsWrapper
-tc_sub_type eq_orig inst_orig ctxt ty_actual et
-  = uExpTypeX eq_orig ty_actual et
-      (return . mkWpCastN)
-      (tc_sub_tc_type eq_orig inst_orig ctxt ty_actual)
-
 tc_sub_tc_type :: CtOrigin   -- used when calling uType
                -> CtOrigin   -- used when instantiating
                -> UserTypeCtxt -> TcSigmaType -> TcSigmaType -> TcM HsWrapper
+-- If wrap = tc_sub_type t1 t2
+--    => wrap :: t1 ~> t2
 tc_sub_tc_type eq_orig inst_orig ctxt ty_actual ty_expected
-  | Just tv_actual <- tcGetTyVar_maybe ty_actual -- See Note [Higher rank types]
-  = do { lookup_res <- lookupTcTyVar tv_actual
-       ; case lookup_res of
-           Filled ty_actual' -> tc_sub_tc_type eq_orig inst_orig
-                                               ctxt ty_actual' ty_expected
-
-             -- It's tempting to see if tv_actual can unify with a polytype
-             -- and, if so, call uType; otherwise, skolemise first. But this
-             -- is wrong, because skolemising will bump the TcLevel and the
-             -- unification will fail anyway.
-             -- It's also tempting to call uUnfilledVar directly, but calling
-             -- uType seems safer in the presence of possible refactoring
-             -- later.
-           Unfilled _        -> mkWpCastN <$>
-                                uType eq_orig TypeLevel ty_actual ty_expected }
-
-  | otherwise  -- See Note [Deep skolemisation]
-  = do { (sk_wrap, inner_wrap) <- tcSkolemise ctxt ty_expected $
-                                  \ _ sk_rho ->
+  | definitely_poly ty_expected      -- See Note [Don't skolemise unnecessarily]
+  , not (possibly_poly ty_actual)
+  = do { traceTc "tc_sub_tc_type (drop to equality)" $
+         vcat [ text "ty_actual   =" <+> ppr ty_actual
+              , text "ty_expected =" <+> ppr ty_expected ]
+       ; mkWpCastN <$>
+         uType TypeLevel eq_orig ty_actual ty_expected }
+
+  | otherwise   -- This is the general case
+  = do { traceTc "tc_sub_tc_type (general case)" $
+         vcat [ text "ty_actual   =" <+> ppr ty_actual
+              , text "ty_expected =" <+> ppr ty_expected ]
+       ; (sk_wrap, inner_wrap) <- tcSkolemise ctxt ty_expected $
+                                                   \ _ sk_rho ->
                                   tc_sub_type_ds eq_orig inst_orig ctxt
                                                  ty_actual sk_rho
        ; return (sk_wrap <.> inner_wrap) }
+  where
+    possibly_poly ty
+      | isForAllTy ty                        = True
+      | Just (_, res) <- splitFunTy_maybe ty = possibly_poly res
+      | otherwise                            = False
+      -- NB *not* tcSplitFunTy, because here we want
+      -- to decompose type-class arguments too
+
+    definitely_poly ty
+      | (tvs, theta, tau) <- tcSplitSigmaTy ty
+      , (tv:_) <- tvs
+      , null theta
+      , isInsolubleOccursCheck NomEq tv tau
+      = True
+      | otherwise
+      = False
+
+{- Note [Don't skolemise unnecessarily]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose we are trying to solve
+    (Char->Char) <= (forall a. a->a)
+We could skolemise the 'forall a', and then complain
+that (Char ~ a) is insoluble; but that's a pretty obscure
+error.  It's better to say that
+    (Char->Char) ~ (forall a. a->a)
+fails.
+
+So roughly:
+ * if the ty_expected has an outermost forall
+      (i.e. skolemisation is the next thing we'd do)
+ * and the ty_actual has no top-level polymorphism (but looking deeply)
+then we can revert to simple equality.  But we need to be careful.
+These examples are all fine:
+
+ * (Char -> forall a. a->a) <= (forall a. Char -> a -> a)
+      Polymorphism is buried in ty_actual
+
+ * (Char->Char) <= (forall a. Char -> Char)
+      ty_expected isn't really polymorphic
+
+ * (Char->Char) <= (forall a. (a~Char) => a -> a)
+      ty_expected isn't really polymorphic
+
+ * (Char->Char) <= (forall a. F [a] Char -> Char)
+                   where type instance F [x] t = t
+     ty_expected isn't really polymorphic
+
+If we prematurely go to equality we'll reject a program we should
+accept (e.g. Trac #13752).  So the test (which is only to improve
+error message) is very conservative:
+ * ty_actual is /definitely/ monomorphic
+ * ty_expected is /definitely/ polymorphic
+-}
 
 ---------------
 tc_sub_type_ds :: CtOrigin    -- used when calling uType
                -> CtOrigin    -- used when instantiating
                -> UserTypeCtxt -> TcSigmaType -> TcRhoType -> TcM HsWrapper
--- Just like tcSubType, but with the additional precondition that
--- ty_expected is deeply skolemised
+-- If wrap = tc_sub_type_ds t1 t2
+--    => wrap :: t1 ~> t2
+-- Here is where the work actually happens!
+-- Precondition: ty_expected is deeply skolemised
 tc_sub_type_ds eq_orig inst_orig ctxt ty_actual ty_expected
-  = go ty_actual ty_expected
+  = do { traceTc "tc_sub_type_ds" $
+         vcat [ text "ty_actual   =" <+> ppr ty_actual
+              , text "ty_expected =" <+> ppr ty_expected ]
+       ; go ty_actual ty_expected }
   where
-    go ty_a ty_e | Just ty_a' <- coreView ty_a = go ty_a' ty_e
-                 | Just ty_e' <- coreView ty_e = go ty_a  ty_e'
+    go ty_a ty_e | Just ty_a' <- tcView ty_a = go ty_a' ty_e
+                 | Just ty_e' <- tcView ty_e = go ty_a  ty_e'
 
     go (TyVarTy tv_a) ty_e
       = do { lookup_res <- lookupTcTyVar tv_a
@@ -720,40 +746,28 @@ tc_sub_type_ds eq_orig inst_orig ctxt ty_actual ty_expected
                     ; tc_sub_type_ds eq_orig inst_orig ctxt ty_a' ty_e }
                Unfilled _   -> unify }
 
-
-    go ty_a (TyVarTy tv_e)
-      = do { dflags <- getDynFlags
-           ; tclvl  <- getTcLevel
-           ; lookup_res <- lookupTcTyVar tv_e
-           ; case lookup_res of
-               Filled ty_e' ->
-                 do { traceTc "tcSubTypeDS_NC_O following filled exp meta-tyvar:"
-                        (ppr tv_e <+> text "-->" <+> ppr ty_e')
-                    ; tc_sub_tc_type eq_orig inst_orig ctxt ty_a ty_e' }
-               Unfilled details
-                 |  canUnifyWithPolyType dflags details
-                    && isTouchableMetaTyVar tclvl tv_e  -- don't want skolems here
-                 -> unify
-
-     -- We've avoided instantiating ty_actual just in case ty_expected is
-     -- polymorphic. But we've now assiduously determined that it is *not*
-     -- polymorphic. So instantiate away. This is needed for e.g. test
-     -- typecheck/should_compile/T4284.
-                 |  otherwise
-                 -> inst_and_unify }
+    -- Historical note (Sept 16): there was a case here for
+    --    go ty_a (TyVarTy alpha)
+    -- which, in the impredicative case unified  alpha := ty_a
+    -- where th_a is a polytype.  Not only is this probably bogus (we
+    -- simply do not have decent story for impredicative types), but it
+    -- caused Trac #12616 because (also bizarrely) 'deriving' code had
+    -- -XImpredicativeTypes on.  I deleted the entire case.
 
     go (FunTy act_arg act_res) (FunTy exp_arg exp_res)
       | not (isPredTy act_arg)
       , not (isPredTy exp_arg)
       = -- See Note [Co/contra-variance of subsumption checking]
-        do { res_wrap <- tc_sub_type_ds eq_orig inst_orig ctxt act_res exp_res
-           ; arg_wrap
-               <- tc_sub_tc_type eq_orig (GivenOrigin
-                                          (SigSkol GenSigCtxt exp_arg))
-                                 ctxt exp_arg act_arg
-           ; return (mkWpFun arg_wrap res_wrap exp_arg exp_res) }
-               -- arg_wrap :: exp_arg ~ act_arg
-               -- res_wrap :: act-res ~ exp_res
+        do { res_wrap <- tc_sub_type_ds eq_orig inst_orig  ctxt       act_res exp_res
+           ; arg_wrap <- tc_sub_tc_type eq_orig given_orig GenSigCtxt exp_arg act_arg
+                         -- GenSigCtxt: See Note [Setting the argument context]
+           ; return (mkWpFun arg_wrap res_wrap exp_arg exp_res doc) }
+               -- arg_wrap :: exp_arg ~> act_arg
+               -- res_wrap :: act-res ~> exp_res
+      where
+        given_orig = GivenOrigin (SigSkol GenSigCtxt exp_arg [])
+        doc = text "When checking that" <+> quotes (ppr ty_actual) <+>
+              text "is more polymorphic than" <+> quotes (ppr ty_expected)
 
     go ty_a ty_e
       | let (tvs, theta, _) = tcSplitSigmaTy ty_a
@@ -761,8 +775,7 @@ tc_sub_type_ds eq_orig inst_orig ctxt ty_actual ty_expected
       = do { (in_wrap, in_rho) <- topInstantiate inst_orig ty_a
            ; body_wrap <- tc_sub_type_ds
                             (eq_orig { uo_actual = in_rho
-                                     , uo_expected =
-                                         mkCheckExpType ty_expected })
+                                     , uo_expected = ty_expected })
                             inst_orig ctxt in_rho ty_e
            ; return (body_wrap <.> in_wrap) }
 
@@ -777,7 +790,7 @@ tc_sub_type_ds eq_orig inst_orig ctxt ty_actual ty_expected
 
     inst_and_unify = do { (wrap, rho_a) <- deeplyInstantiate inst_orig ty_actual
 
-                           -- if we haven't recurred through an arrow, then
+                           -- If we haven't recurred through an arrow, then
                            -- the eq_orig will list ty_actual. In this case,
                            -- we want to update the origin to reflect the
                            -- instantiation. If we *have* recurred through
@@ -789,63 +802,284 @@ tc_sub_type_ds eq_orig inst_orig ctxt ty_actual ty_expected
                                   -> eq_orig { uo_actual = rho_a }
                                 _ -> eq_orig
 
-                        ; cow <- uType eq_orig' TypeLevel rho_a ty_expected
+                        ; cow <- uType TypeLevel eq_orig' rho_a ty_expected
                         ; return (mkWpCastN cow <.> wrap) }
 
 
      -- use versions without synonyms expanded
-    unify = mkWpCastN <$> uType eq_orig TypeLevel ty_actual ty_expected
+    unify = mkWpCastN <$> uType TypeLevel eq_orig ty_actual ty_expected
+
+{- Note [Settting the argument context]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider we are doing the ambiguity check for the (bogus)
+  f :: (forall a b. C b => a -> a) -> Int
+
+We'll call
+   tcSubType ((forall a b. C b => a->a) -> Int )
+             ((forall a b. C b => a->a) -> Int )
+
+with a UserTypeCtxt of (FunSigCtxt "f").  Then we'll do the co/contra thing
+on the argument type of the (->) -- and at that point we want to switch
+to a UserTypeCtxt of GenSigCtxt.  Why?
+
+* Error messages.  If we stick with FunSigCtxt we get errors like
+     * Could not deduce: C b
+       from the context: C b0
+        bound by the type signature for:
+            f :: forall a b. C b => a->a
+  But of course f does not have that type signature!
+  Example tests: T10508, T7220a, Simple14
+
+* Implications. We may decide to build an implication for the whole
+  ambiguity check, but we don't need one for each level within it,
+  and TcUnify.alwaysBuildImplication checks the UserTypeCtxt.
+  See Note [When to build an implication]
+-}
 
 -----------------
 -- needs both un-type-checked (for origins) and type-checked (for wrapping)
 -- expressions
-tcWrapResult :: HsExpr Name -> HsExpr TcId -> TcSigmaType -> ExpRhoType
-             -> TcM (HsExpr TcId)
-tcWrapResult rn_expr = tcWrapResultO (exprCtOrigin rn_expr)
+tcWrapResult :: HsExpr GhcRn -> HsExpr GhcTcId -> TcSigmaType -> ExpRhoType
+             -> TcM (HsExpr GhcTcId)
+tcWrapResult rn_expr = tcWrapResultO (exprCtOrigin rn_expr) rn_expr
 
 -- | Sometimes we don't have a @HsExpr Name@ to hand, and this is more
 -- convenient.
-tcWrapResultO :: CtOrigin -> HsExpr TcId -> TcSigmaType -> ExpRhoType
-               -> TcM (HsExpr TcId)
-tcWrapResultO orig expr actual_ty res_ty
+tcWrapResultO :: CtOrigin -> HsExpr GhcRn -> HsExpr GhcTcId -> TcSigmaType -> ExpRhoType
+               -> TcM (HsExpr GhcTcId)
+tcWrapResultO orig rn_expr expr actual_ty res_ty
   = do { traceTc "tcWrapResult" (vcat [ text "Actual:  " <+> ppr actual_ty
                                       , text "Expected:" <+> ppr res_ty ])
        ; cow <- tcSubTypeDS_NC_O orig GenSigCtxt
-                                 (Just expr) actual_ty res_ty
+                                 (Just rn_expr) actual_ty res_ty
        ; return (mkHsWrap cow expr) }
 
------------------------------------
-wrapFunResCoercion
-        :: [TcType]        -- Type of args
-        -> HsWrapper       -- HsExpr a -> HsExpr b
-        -> TcM HsWrapper   -- HsExpr (arg_tys -> a) -> HsExpr (arg_tys -> b)
-wrapFunResCoercion arg_tys co_fn_res
-  | isIdHsWrapper co_fn_res
-  = return idHsWrapper
-  | null arg_tys
-  = return co_fn_res
-  | otherwise
-  = do  { arg_ids <- newSysLocalIds (fsLit "sub") arg_tys
-        ; return (mkWpLams arg_ids <.> co_fn_res <.> mkWpEvVarApps arg_ids) }
 
------------------------------------
+{- **********************************************************************
+%*                                                                      *
+            ExpType functions: tcInfer, fillInferResult
+%*                                                                      *
+%********************************************************************* -}
+
 -- | Infer a type using a fresh ExpType
 -- See also Note [ExpType] in TcMType
-tcInfer :: (ExpRhoType -> TcM a) -> TcM (a, TcType)
-tcInfer tc_check
-  = do { res_ty <- newOpenInferExpType
+-- Does not attempt to instantiate the inferred type
+tcInferNoInst :: (ExpSigmaType -> TcM a) -> TcM (a, TcSigmaType)
+tcInferNoInst = tcInfer False
+
+tcInferInst :: (ExpRhoType -> TcM a) -> TcM (a, TcRhoType)
+tcInferInst = tcInfer True
+
+tcInfer :: Bool -> (ExpSigmaType -> TcM a) -> TcM (a, TcSigmaType)
+tcInfer instantiate tc_check
+  = do { res_ty <- newInferExpType instantiate
        ; result <- tc_check res_ty
        ; res_ty <- readExpType res_ty
        ; return (result, res_ty) }
 
-{-
-************************************************************************
+fillInferResult :: CtOrigin -> TcType -> InferResult -> TcM HsWrapper
+-- If wrap = fillInferResult t1 t2
+--    => wrap :: t1 ~> t2
+-- See Note [Deep instantiation of InferResult]
+fillInferResult orig ty inf_res@(IR { ir_inst = instantiate_me })
+  | instantiate_me
+  = do { (wrap, rho) <- deeplyInstantiate orig ty
+       ; co <- fill_infer_result rho inf_res
+       ; return (mkWpCastN co <.> wrap) }
+
+  | otherwise
+  = do { co <- fill_infer_result ty inf_res
+       ; return (mkWpCastN co) }
+
+fill_infer_result :: TcType -> InferResult -> TcM TcCoercionN
+-- If wrap = fill_infer_result t1 t2
+--    => wrap :: t1 ~> t2
+fill_infer_result orig_ty (IR { ir_uniq = u, ir_lvl = res_lvl
+                            , ir_ref = ref })
+  = do { (ty_co, ty_to_fill_with) <- promoteTcType res_lvl orig_ty
+
+       ; traceTc "Filling ExpType" $
+         ppr u <+> text ":=" <+> ppr ty_to_fill_with
+
+       ; when debugIsOn (check_hole ty_to_fill_with)
+
+       ; writeTcRef ref (Just ty_to_fill_with)
+
+       ; return ty_co }
+  where
+    check_hole ty   -- Debug check only
+      = do { let ty_lvl = tcTypeLevel ty
+           ; MASSERT2( not (ty_lvl `strictlyDeeperThan` res_lvl),
+                       ppr u $$ ppr res_lvl $$ ppr ty_lvl $$
+                       ppr ty <+> dcolon <+> ppr (tcTypeKind ty) $$ ppr orig_ty )
+           ; cts <- readTcRef ref
+           ; case cts of
+               Just already_there -> pprPanic "writeExpType"
+                                       (vcat [ ppr u
+                                             , ppr ty
+                                             , ppr already_there ])
+               Nothing -> return () }
+
+{- Note [Deep instantiation of InferResult]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In some cases we want to deeply instantiate before filling in
+an InferResult, and in some cases not.  That's why InferReult
+has the ir_inst flag.
+
+* ir_inst = True: deeply instantiate
+
+  Consider
+    f x = (*)
+  We want to instantiate the type of (*) before returning, else we
+  will infer the type
+    f :: forall {a}. a -> forall b. Num b => b -> b -> b
+  This is surely confusing for users.
+
+  And worse, the monomorphism restriction won't work properly. The MR is
+  dealt with in simplifyInfer, and simplifyInfer has no way of
+  instantiating. This could perhaps be worked around, but it may be
+  hard to know even when instantiation should happen.
+
+  Another reason.  Consider
+       f :: (?x :: Int) => a -> a
+       g y = let ?x = 3::Int in f
+  Here want to instantiate f's type so that the ?x::Int constraint
+  gets discharged by the enclosing implicit-parameter binding.
+
+* ir_inst = False: do not instantiate
+
+  Consider this (which uses visible type application):
+
+    (let { f :: forall a. a -> a; f x = x } in f) @Int
+
+  We'll call TcExpr.tcInferFun to infer the type of the (let .. in f)
+  And we don't want to instantite the type of 'f' when we reach it,
+  else the outer visible type application won't work
+-}
+
+{- *********************************************************************
 *                                                                      *
-\subsection{Generalisation}
+              Promoting types
 *                                                                      *
-************************************************************************
+********************************************************************* -}
+
+promoteTcType :: TcLevel -> TcType -> TcM (TcCoercion, TcType)
+-- See Note [Promoting a type]
+-- promoteTcType level ty = (co, ty')
+--   * Returns ty'  whose max level is just 'level'
+--             and  whose kind is ~# to the kind of 'ty'
+--             and  whose kind has form TYPE rr
+--   * and co :: ty ~ ty'
+--   * and emits constraints to justify the coercion
+promoteTcType dest_lvl ty
+  = do { cur_lvl <- getTcLevel
+       ; if (cur_lvl `sameDepthAs` dest_lvl)
+         then dont_promote_it
+         else promote_it }
+  where
+    promote_it :: TcM (TcCoercion, TcType)
+    promote_it  -- Emit a constraint  (alpha :: TYPE rr) ~ ty
+                -- where alpha and rr are fresh and from level dest_lvl
+      = do { rr      <- newMetaTyVarTyAtLevel dest_lvl runtimeRepTy
+           ; prom_ty <- newMetaTyVarTyAtLevel dest_lvl (tYPE rr)
+           ; let eq_orig = TypeEqOrigin { uo_actual   = ty
+                                        , uo_expected = prom_ty
+                                        , uo_thing    = Nothing
+                                        , uo_visible  = False }
+
+           ; co <- emitWantedEq eq_orig TypeLevel Nominal ty prom_ty
+           ; return (co, prom_ty) }
+
+    dont_promote_it :: TcM (TcCoercion, TcType)
+    dont_promote_it  -- Check that ty :: TYPE rr, for some (fresh) rr
+      = do { res_kind <- newOpenTypeKind
+           ; let ty_kind = tcTypeKind ty
+                 kind_orig = TypeEqOrigin { uo_actual   = ty_kind
+                                          , uo_expected = res_kind
+                                          , uo_thing    = Nothing
+                                          , uo_visible  = False }
+           ; ki_co <- uType KindLevel kind_orig (tcTypeKind ty) res_kind
+           ; let co = mkTcGReflRightCo Nominal ty ki_co
+           ; return (co, ty `mkCastTy` ki_co) }
+
+{- Note [Promoting a type]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider (Trac #12427)
+
+  data T where
+    MkT :: (Int -> Int) -> a -> T
+
+  h y = case y of MkT v w -> v
+
+We'll infer the RHS type with an expected type ExpType of
+  (IR { ir_lvl = l, ir_ref = ref, ... )
+where 'l' is the TcLevel of the RHS of 'h'.  Then the MkT pattern
+match will increase the level, so we'll end up in tcSubType, trying to
+unify the type of v,
+  v :: Int -> Int
+with the expected type.  But this attempt takes place at level (l+1),
+rightly so, since v's type could have mentioned existential variables,
+(like w's does) and we want to catch that.
+
+So we
+  - create a new meta-var alpha[l+1]
+  - fill in the InferRes ref cell 'ref' with alpha
+  - emit an equality constraint, thus
+        [W] alpha[l+1] ~ (Int -> Int)
+
+That constraint will float outwards, as it should, unless v's
+type mentions a skolem-captured variable.
+
+This approach fails if v has a higher rank type; see
+Note [Promotion and higher rank types]
+
+
+Note [Promotion and higher rank types]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+If v had a higher-rank type, say v :: (forall a. a->a) -> Int,
+then we'd emit an equality
+        [W] alpha[l+1] ~ ((forall a. a->a) -> Int)
+which will sadly fail because we can't unify a unification variable
+with a polytype.  But there is nothing really wrong with the program
+here.
+
+We could just about solve this by "promote the type" of v, to expose
+its polymorphic "shape" while still leaving constraints that will
+prevent existential escape.  But we must be careful!  Exposing
+the "shape" of the type is precisely what we must NOT do under
+a GADT pattern match!  So in this case we might promote the type
+to
+        (forall a. a->a) -> alpha[l+1]
+and emit the constraint
+        [W] alpha[l+1] ~ Int
+Now the promoted type can fill the ref cell, while the emitted
+equality can float or not, according to the usual rules.
+
+But that's not quite right!  We are exposing the arrow! We could
+deal with that too:
+        (forall a. mu[l+1] a a) -> alpha[l+1]
+with constraints
+        [W] alpha[l+1] ~ Int
+        [W] mu[l+1] ~ (->)
+Here we abstract over the '->' inside the forall, in case that
+is subject to an equality constraint from a GADT match.
+
+Note that we kept the outer (->) because that's part of
+the polymorphic "shape".  And because of impredicativity,
+GADT matches can't give equalities that affect polymorphic
+shape.
+
+This reasoning just seems too complicated, so I decided not
+to do it.  These higher-rank notes are just here to record
+the thinking.
 -}
 
+{- *********************************************************************
+*                                                                      *
+                    Generalisation
+*                                                                      *
+********************************************************************* -}
+
 -- | Take an "expected type" and strip off quantifiers to expose the
 -- type underneath, binding the new skolems for the @thing_inside@.
 -- The returned 'HsWrapper' has type @specific_ty -> expected_ty@.
@@ -859,14 +1093,14 @@ tcSkolemise ctxt expected_ty thing_inside
    -- We expect expected_ty to be a forall-type
    -- If not, the call is a no-op
   = do  { traceTc "tcSkolemise" Outputable.empty
-        ; (wrap, tvs', given, rho') <- deeplySkolemise expected_ty
+        ; (wrap, tv_prs, given, rho') <- deeplySkolemise expected_ty
 
         ; lvl <- getTcLevel
         ; when debugIsOn $
               traceTc "tcSkolemise" $ vcat [
                 ppr lvl,
                 text "expected_ty" <+> ppr expected_ty,
-                text "inst tyvars" <+> ppr tvs',
+                text "inst tyvars" <+> ppr tv_prs,
                 text "given"       <+> ppr given,
                 text "inst type"   <+> ppr rho' ]
 
@@ -883,9 +1117,8 @@ tcSkolemise ctxt expected_ty thing_inside
         -- TcTyVars, all this is handled automatically with no need for
         -- extra faffing around
 
-        -- Use the *instantiated* type in the SkolemInfo
-        -- so that the names of displayed type variables line up
-        ; let skol_info = SigSkol ctxt (mkFunTys (map varType given) rho')
+        ; let tvs' = map snd tv_prs
+              skol_info = SigSkol ctxt expected_ty tv_prs
 
         ; (ev_binds, result) <- checkConstraints skol_info tvs' given $
                                 thing_inside tvs' rho'
@@ -910,35 +1143,88 @@ checkConstraints :: SkolemInfo
                  -> TcM (TcEvBinds, result)
 
 checkConstraints skol_info skol_tvs given thing_inside
-  = do { (implics, ev_binds, result)
-            <- buildImplication skol_info skol_tvs given thing_inside
-       ; emitImplications implics
-       ; return (ev_binds, result) }
-
-buildImplication :: SkolemInfo
-                 -> [TcTyVar]           -- Skolems
-                 -> [EvVar]             -- Given
-                 -> TcM result
-                 -> TcM (Bag Implication, TcEvBinds, result)
-buildImplication skol_info skol_tvs given thing_inside
-  = do { tc_lvl <- getTcLevel
-       ; deferred_type_errors <- goptM Opt_DeferTypeErrors <||>
-                                 goptM Opt_DeferTypedHoles
-       ; if null skol_tvs && null given && (not deferred_type_errors ||
-                                            not (isTopTcLevel tc_lvl))
-         then do { res <- thing_inside
-                 ; return (emptyBag, emptyTcEvBinds, res) }
-      -- Fast path.  We check every function argument with
-      -- tcPolyExpr, which uses tcSkolemise and hence checkConstraints.
-      -- But with the solver producing unlifted equalities, we need
-      -- to have an EvBindsVar for them when they might be deferred to
-      -- runtime. Otherwise, they end up as top-level unlifted bindings,
-      -- which are verboten. See also Note [Deferred errors for coercion holes]
-      -- in TcErrors.
+  = do { implication_needed <- implicationNeeded skol_info skol_tvs given
+
+       ; if implication_needed
+         then do { (tclvl, wanted, result) <- pushLevelAndCaptureConstraints thing_inside
+                 ; (implics, ev_binds) <- buildImplicationFor tclvl skol_info skol_tvs given wanted
+                 ; traceTc "checkConstraints" (ppr tclvl $$ ppr skol_tvs)
+                 ; emitImplications implics
+                 ; return (ev_binds, result) }
+
+         else -- Fast path.  We check every function argument with
+              -- tcPolyExpr, which uses tcSkolemise and hence checkConstraints.
+              -- So this fast path is well-exercised
+              do { res <- thing_inside
+                 ; return (emptyTcEvBinds, res) } }
+
+checkTvConstraints :: SkolemInfo
+                   -> Maybe SDoc  -- User-written telescope, if present
+                   -> TcM ([TcTyVar], result)
+                   -> TcM ([TcTyVar], result)
+
+checkTvConstraints skol_info m_telescope thing_inside
+  = do { (tclvl, wanted, (skol_tvs, result))
+             <- pushLevelAndCaptureConstraints thing_inside
+
+       ; emitResidualTvConstraint skol_info m_telescope
+                                  skol_tvs tclvl wanted
+
+       ; return (skol_tvs, result) }
+
+emitResidualTvConstraint :: SkolemInfo -> Maybe SDoc -> [TcTyVar]
+                         -> TcLevel -> WantedConstraints -> TcM ()
+emitResidualTvConstraint skol_info m_telescope skol_tvs tclvl wanted
+  | isEmptyWC wanted
+  = return ()
+  | otherwise
+  = do { ev_binds <- newNoTcEvBinds
+       ; implic   <- newImplication
+       ; emitImplication $
+         implic { ic_tclvl     = tclvl
+                , ic_skols     = skol_tvs
+                , ic_no_eqs    = True
+                , ic_telescope = m_telescope
+                , ic_wanted    = wanted
+                , ic_binds     = ev_binds
+                , ic_info      = skol_info } }
+
+implicationNeeded :: SkolemInfo -> [TcTyVar] -> [EvVar] -> TcM Bool
+-- See Note [When to build an implication]
+implicationNeeded skol_info skol_tvs given
+  | null skol_tvs
+  , null given
+  , not (alwaysBuildImplication skol_info)
+  = -- Empty skolems and givens
+    do { tc_lvl <- getTcLevel
+       ; if not (isTopTcLevel tc_lvl)  -- No implication needed if we are
+         then return False             -- already inside an implication
          else
-    do { (tclvl, wanted, result) <- pushLevelAndCaptureConstraints thing_inside
-       ; (implics, ev_binds) <- buildImplicationFor tclvl skol_info skol_tvs given wanted
-       ; return (implics, ev_binds, result) }}
+    do { dflags <- getDynFlags       -- If any deferral can happen,
+                                     -- we must build an implication
+       ; return (gopt Opt_DeferTypeErrors dflags ||
+                 gopt Opt_DeferTypedHoles dflags ||
+                 gopt Opt_DeferOutOfScopeVariables dflags) } }
+
+  | otherwise     -- Non-empty skolems or givens
+  = return True   -- Definitely need an implication
+
+alwaysBuildImplication :: SkolemInfo -> Bool
+-- See Note [When to build an implication]
+alwaysBuildImplication _ = False
+
+{-  Commmented out for now while I figure out about error messages.
+    See Trac #14185
+
+alwaysBuildImplication (SigSkol ctxt _ _)
+  = case ctxt of
+      FunSigCtxt {} -> True  -- RHS of a binding with a signature
+      _             -> False
+alwaysBuildImplication (RuleSkol {})      = True
+alwaysBuildImplication (InstSkol {})      = True
+alwaysBuildImplication (FamInstSkol {})   = True
+alwaysBuildImplication _                  = False
+-}
 
 buildImplicationFor :: TcLevel -> SkolemInfo -> [TcTyVar]
                    -> [EvVar] -> WantedConstraints
@@ -952,21 +1238,52 @@ buildImplicationFor tclvl skol_info skol_tvs given wanted
   = return (emptyBag, emptyTcEvBinds)
 
   | otherwise
-  = ASSERT2( all isTcTyVar skol_tvs, ppr skol_tvs )
-    ASSERT2( all isSkolemTyVar skol_tvs, ppr skol_tvs )
+  = ASSERT2( all (isSkolemTyVar <||> isTyVarTyVar) skol_tvs, ppr skol_tvs )
+      -- Why allow TyVarTvs? Because implicitly declared kind variables in
+      -- non-CUSK type declarations are TyVarTvs, and we need to bring them
+      -- into scope as a skolem in an implication. This is OK, though,
+      -- because TyVarTvs will always remain tyvars, even after unification.
     do { ev_binds_var <- newTcEvBinds
-       ; env <- getLclEnv
-       ; let implic = Implic { ic_tclvl = tclvl
-                             , ic_skols = skol_tvs
-                             , ic_no_eqs = False
-                             , ic_given = given
-                             , ic_wanted = wanted
-                             , ic_status  = IC_Unsolved
-                             , ic_binds = Just ev_binds_var
-                             , ic_env = env
-                             , ic_info = skol_info }
-
-       ; return (unitBag implic, TcEvBinds ev_binds_var) }
+       ; implic <- newImplication
+       ; let implic' = implic { ic_tclvl  = tclvl
+                              , ic_skols  = skol_tvs
+                              , ic_given  = given
+                              , ic_wanted = wanted
+                              , ic_binds  = ev_binds_var
+                              , ic_info   = skol_info }
+
+       ; return (unitBag implic', TcEvBinds ev_binds_var) }
+
+{- Note [When to build an implication]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose we have some 'skolems' and some 'givens', and we are
+considering whether to wrap the constraints in their scope into an
+implication.  We must /always/ so if either 'skolems' or 'givens' are
+non-empty.  But what if both are empty?  You might think we could
+always drop the implication.  Other things being equal, the fewer
+implications the better.  Less clutter and overhead.  But we must
+take care:
+
+* If we have an unsolved [W] g :: a ~# b, and -fdefer-type-errors,
+  we'll make a /term-level/ evidence binding for 'g = error "blah"'.
+  We must have an EvBindsVar those bindings!, otherwise they end up as
+  top-level unlifted bindings, which are verboten. This only matters
+  at top level, so we check for that
+  See also Note [Deferred errors for coercion holes] in TcErrors.
+  cf Trac #14149 for an example of what goes wrong.
+
+* If you have
+     f :: Int;  f = f_blah
+     g :: Bool; g = g_blah
+  If we don't build an implication for f or g (no tyvars, no givens),
+  the constraints for f_blah and g_blah are solved together.  And that
+  can yield /very/ confusing error messages, because we can get
+      [W] C Int b1    -- from f_blah
+      [W] C Int b2    -- from g_blan
+  and fundpes can yield [D] b1 ~ b2, even though the two functions have
+  literally nothing to do with each other.  Trac #14185 is an example.
+  Building an implication keeps them separage.
+-}
 
 {-
 ************************************************************************
@@ -979,49 +1296,25 @@ The exported functions are all defined as versions of some
 non-exported generic functions.
 -}
 
-unifyType :: Outputable a => Maybe a   -- ^ If present, has type 'ty1'
+unifyType :: Maybe (HsExpr GhcRn)   -- ^ If present, has type 'ty1'
           -> TcTauType -> TcTauType -> TcM TcCoercionN
 -- Actual and expected types
 -- Returns a coercion : ty1 ~ ty2
-unifyType thing ty1 ty2 = uType origin TypeLevel ty1 ty2
+unifyType thing ty1 ty2 = traceTc "utype" (ppr ty1 $$ ppr ty2 $$ ppr thing) >>
+                          uType TypeLevel origin ty1 ty2
   where
-    origin = TypeEqOrigin { uo_actual = ty1, uo_expected = mkCheckExpType ty2
-                          , uo_thing  = mkErrorThing <$> thing }
-
--- | Variant of 'unifyType' that takes an 'ExpType' as its second type
-unifyExpType :: Outputable a => Maybe a
-             -> TcTauType -> ExpType -> TcM TcCoercionN
-unifyExpType mb_thing ty1 ty2
-  = uExpType ty_orig ty1 ty2
-  where
-    ty_orig   = TypeEqOrigin { uo_actual   = ty1
-                             , uo_expected = ty2
-                             , uo_thing    = mkErrorThing <$> mb_thing }
-
--- | Use this instead of 'Nothing' when calling 'unifyType' without
--- a good "thing" (where the "thing" has the "actual" type passed in)
--- This has an 'Outputable' instance, avoiding amgiguity problems.
-noThing :: Maybe (HsExpr Name)
-noThing = Nothing
-
-unifyKind :: Outputable a => Maybe a -> TcKind -> TcKind -> TcM CoercionN
-unifyKind thing ty1 ty2 = uType origin KindLevel ty1 ty2
-  where origin = TypeEqOrigin { uo_actual = ty1, uo_expected = mkCheckExpType ty2
-                              , uo_thing  = mkErrorThing <$> thing }
+    origin = TypeEqOrigin { uo_actual = ty1, uo_expected = ty2
+                          , uo_thing  = ppr <$> thing
+                          , uo_visible = True } -- always called from a visible context
 
----------------
-unifyPred :: PredType -> PredType -> TcM TcCoercionN
--- Actual and expected types
-unifyPred = unifyType noThing
+unifyKind :: Maybe (HsType GhcRn) -> TcKind -> TcKind -> TcM CoercionN
+unifyKind thing ty1 ty2 = traceTc "ukind" (ppr ty1 $$ ppr ty2 $$ ppr thing) >>
+                          uType KindLevel origin ty1 ty2
+  where origin = TypeEqOrigin { uo_actual = ty1, uo_expected = ty2
+                              , uo_thing  = ppr <$> thing
+                              , uo_visible = True } -- also always from a visible context
 
 ---------------
-unifyTheta :: TcThetaType -> TcThetaType -> TcM [TcCoercionN]
--- Actual and expected types
-unifyTheta theta1 theta2
-  = do  { checkTc (equalLength theta1 theta2)
-                  (vcat [text "Contexts differ in length",
-                         nest 2 $ parens $ text "Use RelaxedPolyRec to allow this"])
-        ; zipWithM unifyPred theta1 theta2 }
 
 {-
 %************************************************************************
@@ -1033,67 +1326,37 @@ unifyTheta theta1 theta2
 uType is the heart of the unifier.
 -}
 
-uExpType :: CtOrigin -> TcType -> ExpType -> TcM CoercionN
-uExpType orig ty1 et
-  = uExpTypeX orig ty1 et return $
-    uType orig TypeLevel ty1
-
--- | Tries to unify with an ExpType. If the ExpType is filled in, calls the first
--- continuation with the produced coercion. Otherwise, calls the second
--- continuation. This can happen either with a Check or with an untouchable
--- ExpType that reverts to a tau-type. See Note [TcLevel of ExpType]
-uExpTypeX :: CtOrigin -> TcType -> ExpType
-          -> (TcCoercionN -> TcM a)   -- Infer case, co :: TcType ~N ExpType
-          -> (TcType -> TcM a)        -- Check / untouchable case
-          -> TcM a
-uExpTypeX orig ty1 et@(Infer _ tc_lvl ki _) coercion_cont type_cont
-  = do { cur_lvl <- getTcLevel
-       ; if cur_lvl `sameDepthAs` tc_lvl
-         then do { ki_co <- uType kind_orig KindLevel (typeKind ty1) ki
-                 ; writeExpType et (ty1 `mkCastTy` ki_co)
-                 ; coercion_cont $ mkTcNomReflCo ty1 `mkTcCoherenceRightCo` ki_co }
-         else do { traceTc "Preventing writing to untouchable ExpType" empty
-                 ; tau <- expTypeToType et -- See Note [TcLevel of ExpType]
-                 ; type_cont tau }}
-  where
-    kind_orig = KindEqOrigin ty1 Nothing orig (Just TypeLevel)
-uExpTypeX _ _ (Check ty2) _ type_cont
-  = type_cont ty2
-
-------------
 uType, uType_defer
-  :: CtOrigin
-  -> TypeOrKind
+  :: TypeOrKind
+  -> CtOrigin
   -> TcType    -- ty1 is the *actual* type
   -> TcType    -- ty2 is the *expected* type
-  -> TcM Coercion
+  -> TcM CoercionN
 
 --------------
 -- It is always safe to defer unification to the main constraint solver
 -- See Note [Deferred unification]
-uType_defer origin t_or_k ty1 ty2
-  = do { hole <- newCoercionHole
-       ; loc <- getCtLocM origin (Just t_or_k)
-       ; emitSimple $ mkNonCanonical $
-             CtWanted { ctev_dest = HoleDest hole
-                      , ctev_pred = mkPrimEqPred ty1 ty2
-                      , ctev_loc = loc }
+uType_defer t_or_k origin ty1 ty2
+  = do { co <- emitWantedEq origin t_or_k Nominal ty1 ty2
 
        -- Error trace only
-       -- NB. do *not* call mkErrInfo unless tracing is on, because
-       -- it is hugely expensive (#5631)
+       -- NB. do *not* call mkErrInfo unless tracing is on,
+       --     because it is hugely expensive (#5631)
        ; whenDOptM Opt_D_dump_tc_trace $ do
             { ctxt <- getErrCtxt
             ; doc <- mkErrInfo emptyTidyEnv ctxt
-            ; traceTc "utype_defer" (vcat [ppr hole, ppr ty1,
-                                           ppr ty2, pprCtOrigin origin, doc])
+            ; traceTc "utype_defer" (vcat [ debugPprType ty1
+                                          , debugPprType ty2
+                                          , pprCtOrigin origin
+                                          , doc])
+            ; traceTc "utype_defer2" (ppr co)
             }
-       ; return (mkHoleCo hole Nominal ty1 ty2) }
+       ; return co }
 
 --------------
-uType origin t_or_k orig_ty1 orig_ty2
+uType t_or_k origin orig_ty1 orig_ty2
   = do { tclvl <- getTcLevel
-       ; traceTc "u_tys " $ vcat
+       ; traceTc "u_tys" $ vcat
               [ text "tclvl" <+> ppr tclvl
               , sep [ ppr orig_ty1, text "~", ppr orig_ty2]
               , pprCtOrigin origin]
@@ -1103,10 +1366,21 @@ uType origin t_or_k orig_ty1 orig_ty2
             else traceTc "u_tys yields coercion:" (ppr co)
        ; return co }
   where
-    go :: TcType -> TcType -> TcM Coercion
+    go :: TcType -> TcType -> TcM CoercionN
         -- The arguments to 'go' are always semantically identical
         -- to orig_ty{1,2} except for looking through type synonyms
 
+     -- Unwrap casts before looking for variables. This way, we can easily
+     -- recognize (t |> co) ~ (t |> co), which is nice. Previously, we
+     -- didn't do it this way, and then the unification above was deferred.
+    go (CastTy t1 co1) t2
+      = do { co_tys <- uType t_or_k origin t1 t2
+           ; return (mkCoherenceLeftCo Nominal t1 co1 co_tys) }
+
+    go t1 (CastTy t2 co2)
+      = do { co_tys <- uType t_or_k origin t1 t2
+           ; return (mkCoherenceRightCo Nominal t2 co2 co_tys) }
+
         -- Variables; go for uVar
         -- Note that we pass in *original* (before synonym expansion),
         -- so that type variables tend to get filled in with
@@ -1116,18 +1390,18 @@ uType origin t_or_k orig_ty1 orig_ty2
            ; case lookup_res of
                Filled ty1   -> do { traceTc "found filled tyvar" (ppr tv1 <+> text ":->" <+> ppr ty1)
                                   ; go ty1 ty2 }
-               Unfilled ds1 -> uUnfilledVar origin t_or_k NotSwapped tv1 ds1 ty2 }
+               Unfilled _ -> uUnfilledVar origin t_or_k NotSwapped tv1 ty2 }
     go ty1 (TyVarTy tv2)
       = do { lookup_res <- lookupTcTyVar tv2
            ; case lookup_res of
                Filled ty2   -> do { traceTc "found filled tyvar" (ppr tv2 <+> text ":->" <+> ppr ty2)
                                   ; go ty1 ty2 }
-               Unfilled ds2 -> uUnfilledVar origin t_or_k IsSwapped tv2 ds2 ty1 }
+               Unfilled _ -> uUnfilledVar origin t_or_k IsSwapped tv2 ty1 }
 
       -- See Note [Expanding synonyms during unification]
     go ty1@(TyConApp tc1 []) (TyConApp tc2 [])
       | tc1 == tc2
-      = return $ mkReflCo Nominal ty1
+      = return $ mkNomReflCo ty1
 
         -- See Note [Expanding synonyms during unification]
         --
@@ -1138,21 +1412,13 @@ uType origin t_or_k orig_ty1 orig_ty2
         -- we'll end up saying "can't match Foo with Bool"
         -- rather than "can't match "Int with Bool".  See Trac #4535.
     go ty1 ty2
-      | Just ty1' <- coreView ty1 = go ty1' ty2
-      | Just ty2' <- coreView ty2 = go ty1  ty2'
-
-    go (CastTy t1 co1) t2
-      = do { co_tys <- go t1 t2
-           ; return (mkCoherenceLeftCo co_tys co1) }
-
-    go t1 (CastTy t2 co2)
-      = do { co_tys <- go t1 t2
-           ; return (mkCoherenceRightCo co_tys co2) }
+      | Just ty1' <- tcView ty1 = go ty1' ty2
+      | Just ty2' <- tcView ty2 = go ty1  ty2'
 
         -- Functions (or predicate functions) just check the two parts
     go (FunTy fun1 arg1) (FunTy fun2 arg2)
-      = do { co_l <- uType origin t_or_k fun1 fun2
-           ; co_r <- uType origin t_or_k arg1 arg2
+      = do { co_l <- uType t_or_k origin fun1 fun2
+           ; co_r <- uType t_or_k origin arg1 arg2
            ; return $ mkFunCo Nominal co_l co_r }
 
         -- Always defer if a type synonym family (type function)
@@ -1164,10 +1430,13 @@ uType origin t_or_k orig_ty1 orig_ty2
 
     go (TyConApp tc1 tys1) (TyConApp tc2 tys2)
       -- See Note [Mismatched type lists and application decomposition]
-      | tc1 == tc2, length tys1 == length tys2
+      | tc1 == tc2, equalLength tys1 tys2
       = ASSERT2( isGenerativeTyCon tc1 Nominal, ppr tc1 )
-        do { cos <- zipWithM (uType origin t_or_k) tys1 tys2
+        do { cos <- zipWith3M (uType t_or_k) origins' tys1 tys2
            ; return $ mkTyConAppCo Nominal tc1 cos }
+      where
+        origins' = map (\is_vis -> if is_vis then origin else toInvisibleOrigin origin)
+                       (tcTyConVisibilities tc1)
 
     go (LitTy m) ty@(LitTy n)
       | m == n
@@ -1177,24 +1446,24 @@ uType origin t_or_k orig_ty1 orig_ty2
         -- Do not decompose FunTy against App;
         -- it's often a type error, so leave it for the constraint solver
     go (AppTy s1 t1) (AppTy s2 t2)
-      = go_app s1 t1 s2 t2
+      = go_app (isNextArgVisible s1) s1 t1 s2 t2
 
     go (AppTy s1 t1) (TyConApp tc2 ts2)
       | Just (ts2', t2') <- snocView ts2
-      = ASSERT( mightBeUnsaturatedTyCon tc2 )
-        go_app s1 t1 (TyConApp tc2 ts2') t2'
+      = ASSERT( not (mustBeSaturated tc2) )
+        go_app (isNextTyConArgVisible tc2 ts2') s1 t1 (TyConApp tc2 ts2') t2'
 
     go (TyConApp tc1 ts1) (AppTy s2 t2)
       | Just (ts1', t1') <- snocView ts1
-      = ASSERT( mightBeUnsaturatedTyCon tc1 )
-        go_app (TyConApp tc1 ts1') t1' s2 t2
+      = ASSERT( not (mustBeSaturated tc1) )
+        go_app (isNextTyConArgVisible tc1 ts1') (TyConApp tc1 ts1') t1' s2 t2
 
     go (CoercionTy co1) (CoercionTy co2)
       = do { let ty1 = coercionType co1
                  ty2 = coercionType co2
-           ; kco <- uType (KindEqOrigin orig_ty1 (Just orig_ty2) origin
+           ; kco <- uType KindLevel
+                          (KindEqOrigin orig_ty1 (Just orig_ty2) origin
                                         (Just t_or_k))
-                          KindLevel
                           ty1 ty2
            ; return $ mkProofIrrelCo Nominal kco co1 co2 }
 
@@ -1205,12 +1474,15 @@ uType origin t_or_k orig_ty1 orig_ty2
     ------------------
     defer ty1 ty2   -- See Note [Check for equality before deferring]
       | ty1 `tcEqType` ty2 = return (mkNomReflCo ty1)
-      | otherwise          = uType_defer origin t_or_k ty1 ty2
+      | otherwise          = uType_defer t_or_k origin ty1 ty2
 
     ------------------
-    go_app s1 t1 s2 t2
-      = do { co_s <- uType origin t_or_k s1 s2
-           ; co_t <- uType origin t_or_k t1 t2
+    go_app vis s1 t1 s2 t2
+      = do { co_s <- uType t_or_k origin s1 s2
+           ; let arg_origin
+                   | vis       = origin
+                   | otherwise = toInvisibleOrigin origin
+           ; co_t <- uType t_or_k arg_origin t1 t2
            ; return $ mkAppCo co_s co_t }
 
 {- Note [Check for equality before deferring]
@@ -1257,6 +1529,9 @@ We expand synonyms during unification, but:
    more likely that the inferred types will mention type synonyms
    understandable to the user
 
+ * Similarly, we expand *after* the CastTy case, just in case the
+   CastTy wraps a variable.
+
  * We expand *before* the TyConApp case.  For example, if we have
       type Phantom a = Int
    and are unifying
@@ -1304,177 +1579,315 @@ of the substitution; rather, notice that @uVar@ (defined below) nips
 back into @uTys@ if it turns out that the variable is already bound.
 -}
 
+----------
 uUnfilledVar :: CtOrigin
              -> TypeOrKind
              -> SwapFlag
-             -> TcTyVar -> TcTyVarDetails       -- Tyvar 1
-             -> TcTauType                       -- Type 2
+             -> TcTyVar        -- Tyvar 1
+             -> TcTauType      -- Type 2
              -> TcM Coercion
 -- "Unfilled" means that the variable is definitely not a filled-in meta tyvar
 --            It might be a skolem, or untouchable, or meta
 
-uUnfilledVar origin t_or_k swapped tv1 details1 (TyVarTy tv2)
-  | tv1 == tv2  -- Same type variable => no-op
-  = return (mkNomReflCo (mkTyVarTy tv1))
-
-  | otherwise  -- Distinct type variables
-  = do  { lookup2 <- lookupTcTyVar tv2
-        ; case lookup2 of
-            Filled ty2'
-              -> uUnfilledVar origin t_or_k swapped tv1 details1 ty2'
-            Unfilled details2
-              -> uUnfilledVars origin t_or_k swapped tv1 details1 tv2 details2
-        }
-
-uUnfilledVar origin t_or_k swapped tv1 details1 non_var_ty2
--- ty2 is not a type variable
-  = case details1 of
-      MetaTv { mtv_ref = ref1 }
-        -> do { dflags <- getDynFlags
-              ; mb_ty2' <- checkTauTvUpdate dflags origin t_or_k tv1 non_var_ty2
-              ; case mb_ty2' of
-                  Just (ty2', co_k) -> maybe_sym swapped <$>
-                                       updateMeta tv1 ref1 ty2' co_k
-                  Nothing   -> do { traceTc "Occ/type-family defer"
-                                        (ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1)
-                                         $$ ppr non_var_ty2 $$ ppr (typeKind non_var_ty2))
-                                  ; defer }
-              }
-
-      _other -> do { traceTc "Skolem defer" (ppr tv1); defer }  -- Skolems of all sorts
+uUnfilledVar origin t_or_k swapped tv1 ty2
+  = do { ty2 <- zonkTcType ty2
+             -- Zonk to expose things to the
+             -- occurs check, and so that if ty2
+             -- looks like a type variable then it
+             -- /is/ a type variable
+       ; uUnfilledVar1 origin t_or_k swapped tv1 ty2 }
+
+----------
+uUnfilledVar1 :: CtOrigin
+              -> TypeOrKind
+              -> SwapFlag
+              -> TcTyVar        -- Tyvar 1
+              -> TcTauType      -- Type 2, zonked
+              -> TcM Coercion
+uUnfilledVar1 origin t_or_k swapped tv1 ty2
+  | Just tv2 <- tcGetTyVar_maybe ty2
+  = go tv2
+
+  | otherwise
+  = uUnfilledVar2 origin t_or_k swapped tv1 ty2
+
   where
-    defer = unSwap swapped (uType_defer origin t_or_k) (mkTyVarTy tv1) non_var_ty2
-               -- Occurs check or an untouchable: just defer
-               -- NB: occurs check isn't necessarily fatal:
-               --     eg tv1 occured in type family parameter
+    -- 'go' handles the case where both are
+    -- tyvars so we might want to swap
+    go tv2 | tv1 == tv2  -- Same type variable => no-op
+           = return (mkNomReflCo (mkTyVarTy tv1))
 
-----------------
-uUnfilledVars :: CtOrigin
+           | swapOverTyVars tv1 tv2   -- Distinct type variables
+           = uUnfilledVar2 origin t_or_k (flipSwap swapped)
+                           tv2 (mkTyVarTy tv1)
+
+           | otherwise
+           = uUnfilledVar2 origin t_or_k swapped tv1 ty2
+
+----------
+uUnfilledVar2 :: CtOrigin
               -> TypeOrKind
               -> SwapFlag
-              -> TcTyVar -> TcTyVarDetails      -- Tyvar 1
-              -> TcTyVar -> TcTyVarDetails      -- Tyvar 2
+              -> TcTyVar        -- Tyvar 1
+              -> TcTauType      -- Type 2, zonked
               -> TcM Coercion
--- Invarant: The type variables are distinct,
---           Neither is filled in yet
-
-uUnfilledVars origin t_or_k swapped tv1 details1 tv2 details2
-  = do { traceTc "uUnfilledVars for" (ppr tv1 <+> text "and" <+> ppr tv2)
-       ; traceTc "uUnfilledVars" (    text "trying to unify" <+> ppr k1
-                                  <+> text "with"            <+> ppr k2)
-       ; co_k <- uType kind_origin KindLevel k1 k2
-       ; let no_swap ref = maybe_sym swapped <$>
-                           updateMeta tv1 ref ty2 (mkSymCo co_k)
-             do_swap ref = maybe_sym (flipSwap swapped) <$>
-                           updateMeta tv2 ref ty1 co_k
-       ; case (details1, details2) of
-         { ( MetaTv { mtv_info = i1, mtv_ref = ref1 }
-           , MetaTv { mtv_info = i2, mtv_ref = ref2 } )
-             | nicer_to_update_tv1 tv1 i1 i2 -> no_swap ref1
-             | otherwise                     -> do_swap ref2
-         ; (MetaTv { mtv_ref = ref1 }, _) -> no_swap ref1
-         ; (_, MetaTv { mtv_ref = ref2 }) -> do_swap ref2
-
-           -- Can't do it in-place, so defer
-           -- This happens for skolems of all sorts
-         ; _ -> do { traceTc "deferring because I can't find a meta-tyvar:"
-                       (pprTcTyVarDetails details1 <+> pprTcTyVarDetails details2)
-                   ; unSwap swapped (uType_defer origin t_or_k) ty1 ty2 } } }
+uUnfilledVar2 origin t_or_k swapped tv1 ty2
+  = do { dflags  <- getDynFlags
+       ; cur_lvl <- getTcLevel
+       ; go dflags cur_lvl }
   where
-    k1  = tyVarKind tv1
-    k2  = tyVarKind tv2
+    go dflags cur_lvl
+      | canSolveByUnification cur_lvl tv1 ty2
+      , Just ty2' <- metaTyVarUpdateOK dflags tv1 ty2
+      = do { co_k <- uType KindLevel kind_origin (tcTypeKind ty2') (tyVarKind tv1)
+           ; traceTc "uUnfilledVar2 ok" $
+             vcat [ ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1)
+                  , ppr ty2 <+> dcolon <+> ppr (tcTypeKind  ty2)
+                  , ppr (isTcReflCo co_k), ppr co_k ]
+
+           ; if isTcReflCo co_k  -- only proceed if the kinds matched.
+
+             then do { writeMetaTyVar tv1 ty2'
+                     ; return (mkTcNomReflCo ty2') }
+
+             else defer } -- This cannot be solved now.  See TcCanonical
+                          -- Note [Equalities with incompatible kinds]
+
+      | otherwise
+      = do { traceTc "uUnfilledVar2 not ok" (ppr tv1 $$ ppr ty2)
+               -- Occurs check or an untouchable: just defer
+               -- NB: occurs check isn't necessarily fatal:
+               --     eg tv1 occured in type family parameter
+            ; defer }
+
     ty1 = mkTyVarTy tv1
-    ty2 = mkTyVarTy tv2
     kind_origin = KindEqOrigin ty1 (Just ty2) origin (Just t_or_k)
 
--- | apply sym iff swapped
-maybe_sym :: SwapFlag -> Coercion -> Coercion
-maybe_sym IsSwapped  = mkSymCo
-maybe_sym NotSwapped = id
+    defer = unSwap swapped (uType_defer t_or_k origin) ty1 ty2
 
-nicer_to_update_tv1 :: TcTyVar -> MetaInfo -> MetaInfo -> Bool
-nicer_to_update_tv1 _   _     SigTv = True
-nicer_to_update_tv1 _   SigTv _     = False
-        -- Try not to update SigTvs; and try to update sys-y type
-        -- variables in preference to ones gotten (say) by
-        -- instantiating a polymorphic function with a user-written
-        -- type sig
-nicer_to_update_tv1 tv1 _     _     = isSystemName (Var.varName tv1)
+swapOverTyVars :: TcTyVar -> TcTyVar -> Bool
+swapOverTyVars tv1 tv2
+  -- Level comparison: see Note [TyVar/TyVar orientation]
+  | lvl1 `strictlyDeeperThan` lvl2 = False
+  | lvl2 `strictlyDeeperThan` lvl1 = True
 
-----------------
-checkTauTvUpdate :: DynFlags
-                 -> CtOrigin
-                 -> TypeOrKind
-                 -> TcTyVar             -- tv :: k1
-                 -> TcType              -- ty :: k2
-                 -> TcM (Maybe ( TcType        -- possibly-expanded ty
-                               , Coercion )) -- :: k2 ~N k1
---    (checkTauTvUpdate tv ty)
--- We are about to update the TauTv tv with ty.
--- Check (a) that tv doesn't occur in ty (occurs check)
---       (b) that kind(ty) matches kind(tv)
---
--- We have two possible outcomes:
--- (1) Return the type to update the type variable with,
---        [we know the update is ok]
--- (2) Return Nothing,
---        [the update might be dodgy]
---
--- Note that "Nothing" does not mean "definite error".  For example
---   type family F a
---   type instance F Int = Int
--- consider
---   a ~ F a
--- This is perfectly reasonable, if we later get a ~ Int.  For now, though,
--- we return Nothing, leaving it to the later constraint simplifier to
--- sort matters out.
+  -- Priority: see Note [TyVar/TyVar orientation]
+  | pri1 > pri2 = False
+  | pri2 > pri1 = True
 
-checkTauTvUpdate dflags origin t_or_k tv ty
-  | SigTv <- info
-  = ASSERT( not (isTyVarTy ty) )
-    return Nothing
-  | otherwise
-  = do { ty   <- zonkTcType ty
-       ; co_k <- uType kind_origin KindLevel (typeKind ty) (tyVarKind tv)
-       ; if | defer_me ty ->  -- Quick test
-                -- Failed quick test so try harder
-                case occurCheckExpand dflags tv ty of
-                   OC_OK ty2 | defer_me ty2 -> return Nothing
-                             | otherwise    -> return (Just (ty2, co_k))
-                   _                        -> return Nothing
-            | otherwise   -> return (Just (ty, co_k)) }
+  -- Names: see Note [TyVar/TyVar orientation]
+  | isSystemName tv2_name, not (isSystemName tv1_name) = True
+
+  | otherwise = False
 
   where
-    kind_origin   = KindEqOrigin (mkTyVarTy tv) (Just ty) origin (Just t_or_k)
-    details       = tcTyVarDetails tv
-    info          = mtv_info details
-
-    impredicative = canUnifyWithPolyType dflags details
-
-    defer_me :: TcType -> Bool
-    -- Checks for (a) occurrence of tv
-    --            (b) type family applications
-    --            (c) foralls
-    -- See Note [Prevent unification with type families]
-    -- See Note [Refactoring hazard: checkTauTvUpdate]
-    defer_me (LitTy {})        = False
-    defer_me (TyVarTy tv')     = tv == tv' || defer_me (tyVarKind tv')
-    defer_me (TyConApp tc tys) = isTypeFamilyTyCon tc || any defer_me tys
-                                 || not (impredicative || isTauTyCon tc)
-    defer_me (ForAllTy bndr t) = defer_me (binderKind bndr) || defer_me t
-                                 || not impredicative
-    defer_me (FunTy fun arg)   = defer_me fun || defer_me arg
-    defer_me (AppTy fun arg)   = defer_me fun || defer_me arg
-    defer_me (CastTy ty co)    = defer_me ty || defer_me_co co
-    defer_me (CoercionTy co)   = defer_me_co co
-
-      -- We don't really care if there are type families in a coercion,
-      -- but we still can't have an occurs-check failure
-    defer_me_co co = tv `elemVarSet` tyCoVarsOfCo co
+    lvl1 = tcTyVarLevel tv1
+    lvl2 = tcTyVarLevel tv2
+    pri1 = lhsPriority tv1
+    pri2 = lhsPriority tv2
+    tv1_name = Var.varName tv1
+    tv2_name = Var.varName tv2
+
+
+lhsPriority :: TcTyVar -> Int
+-- Higher => more important to be on the LHS
+-- See Note [TyVar/TyVar orientation]
+lhsPriority tv
+  = ASSERT2( isTyVar tv, ppr tv)
+    case tcTyVarDetails tv of
+      RuntimeUnk  -> 0
+      SkolemTv {} -> 0
+      MetaTv { mtv_info = info } -> case info of
+                                     FlatSkolTv -> 1
+                                     TyVarTv    -> 2
+                                     TauTv      -> 3
+                                     FlatMetaTv -> 4
+{- Note [TyVar/TyVar orientation]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Given (a ~ b), should we orient the CTyEqCan as (a~b) or (b~a)?
+This is a surprisingly tricky question!
+
+First note: only swap if you have to!
+   See Note [Avoid unnecessary swaps]
+
+So we look for a positive reason to swap, using a three-step test:
+
+* Level comparison. If 'a' has deeper level than 'b',
+  put 'a' on the left.  See Note [Deeper level on the left]
+
+* Priority.  If the levels are the same, look at what kind of
+  type variable it is, using 'lhsPriority'
+
+  - FlatMetaTv: Always put on the left.
+    See Note [Fmv Orientation Invariant]
+    NB: FlatMetaTvs always have the current level, never an
+        outer one.  So nothing can be deeper than a FlatMetaTv
+
+
+  - TyVarTv/TauTv: if we have  tyv_tv ~ tau_tv, put tau_tv
+                   on the left because there are fewer
+                   restrictions on updating TauTvs
+
+  - TyVarTv/TauTv:  put on the left either
+     a) Because it's touchable and can be unified, or
+     b) Even if it's not touchable, TcSimplify.floatEqualities
+        looks for meta tyvars on the left
+
+  - FlatSkolTv: Put on the left in preference to a SkolemTv
+                See Note [Eliminate flat-skols]
+
+* Names. If the level and priority comparisons are all
+  equal, try to eliminate a TyVars with a System Name in
+  favour of ones with a Name derived from a user type signature
+
+* Age.  At one point in the past we tried to break any remaining
+  ties by eliminating the younger type variable, based on their
+  Uniques.  See Note [Eliminate younger unification variables]
+  (which also explains why we don't do this any more)
+
+Note [Deeper level on the left]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The most important thing is that we want to put tyvars with
+the deepest level on the left.  The reason to do so differs for
+Wanteds and Givens, but either way, deepest wins!  Simple.
+
+* Wanteds.  Putting the deepest variable on the left maximise the
+  chances that it's a touchable meta-tyvar which can be solved.
+
+* Givens. Suppose we have something like
+     forall a[2]. b[1] ~ a[2] => beta[1] ~ a[2]
+
+  If we orient the Given a[2] on the left, we'll rewrite the Wanted to
+  (beta[1] ~ b[1]), and that can float out of the implication.
+  Otherwise it can't.  By putting the deepest variable on the left
+  we maximise our changes of eliminating skolem capture.
+
+  See also TcSMonad Note [Let-bound skolems] for another reason
+  to orient with the deepest skolem on the left.
+
+  IMPORTANT NOTE: this test does a level-number comparison on
+  skolems, so it's important that skolems have (accurate) level
+  numbers.
+
+See Trac #15009 for an further analysis of why "deepest on the left"
+is a good plan.
+
+Note [Fmv Orientation Invariant]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+   * We always orient a constraint
+        fmv ~ alpha
+     with fmv on the left, even if alpha is
+     a touchable unification variable
+
+Reason: doing it the other way round would unify alpha:=fmv, but that
+really doesn't add any info to alpha.  But a later constraint alpha ~
+Int might unlock everything.  Comment:9 of #12526 gives a detailed
+example.
+
+WARNING: I've gone to and fro on this one several times.
+I'm now pretty sure that unifying alpha:=fmv is a bad idea!
+So orienting with fmvs on the left is a good thing.
+
+This example comes from IndTypesPerfMerge. (Others include
+T10226, T10009.)
+    From the ambiguity check for
+      f :: (F a ~ a) => a
+    we get:
+          [G] F a ~ a
+          [WD] F alpha ~ alpha, alpha ~ a
+
+    From Givens we get
+          [G] F a ~ fsk, fsk ~ a
 
-{-
-Note [Prevent unification with type families]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+    Now if we flatten we get
+          [WD] alpha ~ fmv, F alpha ~ fmv, alpha ~ a
+
+    Now, if we unified alpha := fmv, we'd get
+          [WD] F fmv ~ fmv, [WD] fmv ~ a
+    And now we are stuck.
+
+So instead the Fmv Orientation Invariant puts the fmv on the
+left, giving
+      [WD] fmv ~ alpha, [WD] F alpha ~ fmv, [WD] alpha ~ a
+
+    Now we get alpha:=a, and everything works out
+
+Note [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 instead 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 [Avoid unnecessary swaps]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+If we swap without actually improving matters, we can get an infinite loop.
+Consider
+    work item:  a ~ b
+   inert item:  b ~ c
+We canonicalise the work-item to (a ~ c).  If we then swap it before
+adding to the inert set, we'll add (c ~ a), and therefore kick out the
+inert guy, so we get
+   new work item:  b ~ c
+   inert item:     c ~ a
+And now the cycle just repeats
+
+Note [Eliminate younger unification variables]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Given a choice of unifying
+     alpha := beta   or   beta := alpha
+we try, if possible, to eliminate the "younger" one, as determined
+by `ltUnique`.  Reason: the younger one is less likely to appear free in
+an existing inert constraint, and hence we are less likely to be forced
+into kicking out and rewriting inert constraints.
+
+This is a performance optimisation only.  It turns out to fix
+Trac #14723 all by itself, but clearly not reliably so!
+
+It's simple to implement (see nicer_to_update_tv2 in swapOverTyVars).
+But, to my surprise, it didn't seem to make any significant difference
+to the compiler's performance, so I didn't take it any further.  Still
+it seemed to too nice to discard altogether, so I'm leaving these
+notes.  SLPJ Jan 18.
+-}
+
+-- @trySpontaneousSolve wi@ solves equalities where one side is a
+-- touchable unification variable.
+-- Returns True <=> spontaneous solve happened
+canSolveByUnification :: TcLevel -> TcTyVar -> TcType -> Bool
+canSolveByUnification tclvl tv xi
+  | isTouchableMetaTyVar tclvl tv
+  = case metaTyVarInfo tv of
+      TyVarTv -> is_tyvar xi
+      _       -> True
+
+  | otherwise    -- Untouchable
+  = False
+  where
+    is_tyvar xi
+      = case tcGetTyVar_maybe xi of
+          Nothing -> False
+          Just tv -> case tcTyVarDetails tv of
+                       MetaTv { mtv_info = info }
+                                   -> case info of
+                                        TyVarTv -> True
+                                        _       -> False
+                       SkolemTv {} -> True
+                       RuntimeUnk  -> True
+
+{- Note [Prevent unification with type families]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 We prevent unification with type families because of an uneasy compromise.
 It's perfectly sound to unify with type families, and it even improves the
 error messages in the testsuite. It also modestly improves performance, at
@@ -1508,14 +1921,15 @@ with type families].) So I checked the result of occurCheckExpand for any
 type family occurrences and deferred if there were any. This was done
 in commit e9bf7bb5cc9fb3f87dd05111aa23da76b86a8967 .
 
-This approach turned out not to be performant, because the expanded type
-was bigger than the original type, and tyConsOfType looks through type
-synonyms. So it then struck me that we could dispense with the defer_me
-check entirely. This simplified the code nicely, and it cut the allocations
-in T5030 by half. But, as documented in Note [Prevent unification with
-type families], this destroyed performance in T3064. Regardless, I missed this
-regression and the change was committed as
-3f5d1a13f112f34d992f6b74656d64d95a3f506d .
+This approach turned out not to be performant, because the expanded
+type was bigger than the original type, and tyConsOfType (needed to
+see if there are any type family occurrences) looks through type
+synonyms. So it then struck me that we could dispense with the
+defer_me check entirely. This simplified the code nicely, and it cut
+the allocations in T5030 by half. But, as documented in Note [Prevent
+unification with type families], this destroyed performance in
+T3064. Regardless, I missed this regression and the change was
+committed as 3f5d1a13f112f34d992f6b74656d64d95a3f506d .
 
 Bottom lines:
  * defer_me is back, but now fixed w.r.t. #11407.
@@ -1596,56 +2010,235 @@ lookupTcTyVar tyvar
   where
     details = tcTyVarDetails tyvar
 
--- | Fill in a meta-tyvar
-updateMeta :: TcTyVar            -- ^ tv to fill in, tv :: k1
-           -> TcRef MetaDetails  -- ^ ref to tv's metadetails
-           -> TcType             -- ^ ty2 :: k2
-           -> Coercion           -- ^ kind_co :: k2 ~N k1
-           -> TcM Coercion       -- ^ :: tv ~N ty2 (= ty2 |> kind_co ~N ty2)
-updateMeta tv1 ref1 ty2 kind_co
-  = do { let ty2_refl   = mkNomReflCo ty2
-             (ty2', co) = ( ty2 `mkCastTy` kind_co
-                          , mkCoherenceLeftCo ty2_refl kind_co )
-       ; writeMetaTyVarRef tv1 ref1 ty2'
-       ; return co }
-
 {-
 Note [Unifying untouchables]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 We treat an untouchable type variable as if it was a skolem.  That
-ensures it won't unify with anything.  It's a slight had, because
+ensures it won't unify with anything.  It's a slight hack, because
 we return a made-up TcTyVarDetails, but I think it works smoothly.
 -}
 
 -- | Breaks apart a function kind into its pieces.
-matchExpectedFunKind :: Arity           -- ^ # of args remaining, only for errors
-                     -> TcType          -- ^ type, only for errors
-                     -> TcKind          -- ^ function kind
-                     -> TcM (Coercion, TcKind, TcKind)
-                                  -- ^ co :: old_kind ~ arg -> res
-matchExpectedFunKind num_args_remaining ty = go
+matchExpectedFunKind
+  :: Outputable fun
+  => fun             -- ^ type, only for errors
+  -> Arity           -- ^ n: number of desired arrows
+  -> TcKind          -- ^ fun_ kind
+  -> TcM Coercion    -- ^ co :: fun_kind ~ (arg1 -> ... -> argn -> res)
+
+matchExpectedFunKind hs_ty n k = go n k
   where
-    go k | Just k' <- coreView k = go k'
+    go 0 k = return (mkNomReflCo k)
 
-    go k@(TyVarTy kvar)
-      | isTcTyVar kvar, isMetaTyVar kvar
+    go n k | Just k' <- tcView k = go n k'
+
+    go n k@(TyVarTy kvar)
+      | isMetaTyVar kvar
       = do { maybe_kind <- readMetaTyVar kvar
            ; case maybe_kind of
-                Indirect fun_kind -> go fun_kind
-                Flexi ->             defer k }
+                Indirect fun_kind -> go n fun_kind
+                Flexi ->             defer n k }
+
+    go n (FunTy arg res)
+      = do { co <- go (n-1) res
+           ; return (mkTcFunCo Nominal (mkTcNomReflCo arg) co) }
 
-    go k@(FunTy arg res) = return (mkNomReflCo k, arg, res)
-    go other             = defer other
+    go n other
+     = defer n other
 
-    defer k
-      = do { arg_kind <- newMetaKindVar
-           ; res_kind <- newMetaKindVar
-           ; let new_fun = mkFunTy arg_kind res_kind
-                 thing   = mkTypeErrorThingArgs ty num_args_remaining
+    defer n k
+      = do { arg_kinds <- newMetaKindVars n
+           ; res_kind  <- newMetaKindVar
+           ; let new_fun = mkFunTys arg_kinds res_kind
                  origin  = TypeEqOrigin { uo_actual   = k
-                                        , uo_expected = mkCheckExpType new_fun
-                                        , uo_thing    = Just thing
+                                        , uo_expected = new_fun
+                                        , uo_thing    = Just (ppr hs_ty)
+                                        , uo_visible  = True
                                         }
-           ; co <- uType origin KindLevel k new_fun
-           ; return (co, arg_kind, res_kind) }
-      where
+           ; uType KindLevel origin k new_fun }
+
+{- *********************************************************************
+*                                                                      *
+                 Occurrence checking
+*                                                                      *
+********************************************************************* -}
+
+
+{-  Note [Occurrence checking: look inside kinds]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose we are considering unifying
+   (alpha :: *)  ~  Int -> (beta :: alpha -> alpha)
+This may be an error (what is that alpha doing inside beta's kind?),
+but we must not make the mistake of actually unifying or we'll
+build an infinite data structure.  So when looking for occurrences
+of alpha in the rhs, we must look in the kinds of type variables
+that occur there.
+
+NB: we may be able to remove the problem via expansion; see
+    Note [Occurs check expansion].  So we have to try that.
+
+Note [Checking for foralls]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Unless we have -XImpredicativeTypes (which is a totally unsupported
+feature), we do not want to unify
+    alpha ~ (forall a. a->a) -> Int
+So we look for foralls hidden inside the type, and it's convenient
+to do that at the same time as the occurs check (which looks for
+occurrences of alpha).
+
+However, it's not just a question of looking for foralls /anywhere/!
+Consider
+   (alpha :: forall k. k->*)  ~  (beta :: forall k. k->*)
+This is legal; e.g. dependent/should_compile/T11635.
+
+We don't want to reject it because of the forall in beta's kind,
+but (see Note [Occurrence checking: look inside kinds]) we do
+need to look in beta's kind.  So we carry a flag saying if a 'forall'
+is OK, and sitch the flag on when stepping inside a kind.
+
+Why is it OK?  Why does it not count as impredicative polymorphism?
+The reason foralls are bad is because we reply on "seeing" foralls
+when doing implicit instantiation.  But the forall inside the kind is
+fine.  We'll generate a kind equality constraint
+  (forall k. k->*) ~ (forall k. k->*)
+to check that the kinds of lhs and rhs are compatible.  If alpha's
+kind had instead been
+  (alpha :: kappa)
+then this kind equality would rightly complain about unifying kappa
+with (forall k. k->*)
+
+-}
+
+data OccCheckResult a
+  = OC_OK a
+  | OC_Bad     -- Forall or type family
+  | OC_Occurs
+
+instance Functor OccCheckResult where
+      fmap = liftM
+
+instance Applicative OccCheckResult where
+      pure = OC_OK
+      (<*>) = ap
+
+instance Monad OccCheckResult where
+  OC_OK x    >>= k = k x
+  OC_Bad     >>= _ = OC_Bad
+  OC_Occurs  >>= _ = OC_Occurs
+
+occCheckForErrors :: DynFlags -> TcTyVar -> Type -> OccCheckResult ()
+-- Just for error-message generation; so we return OccCheckResult
+-- so the caller can report the right kind of error
+-- Check whether
+--   a) the given variable occurs in the given type.
+--   b) there is a forall in the type (unless we have -XImpredicativeTypes)
+occCheckForErrors dflags tv ty
+  = case preCheck dflags True tv ty of
+      OC_OK _   -> OC_OK ()
+      OC_Bad    -> OC_Bad
+      OC_Occurs -> case occCheckExpand [tv] ty of
+                     Nothing -> OC_Occurs
+                     Just _  -> OC_OK ()
+
+----------------
+metaTyVarUpdateOK :: DynFlags
+                  -> TcTyVar             -- tv :: k1
+                  -> TcType              -- ty :: k2
+                  -> Maybe TcType        -- possibly-expanded ty
+-- (metaTyFVarUpdateOK tv ty)
+-- We are about to update the meta-tyvar tv with ty
+-- Check (a) that tv doesn't occur in ty (occurs check)
+--       (b) that ty does not have any foralls
+--           (in the impredicative case), or type functions
+--
+-- We have two possible outcomes:
+-- (1) Return the type to update the type variable with,
+--        [we know the update is ok]
+-- (2) Return Nothing,
+--        [the update might be dodgy]
+--
+-- Note that "Nothing" does not mean "definite error".  For example
+--   type family F a
+--   type instance F Int = Int
+-- consider
+--   a ~ F a
+-- This is perfectly reasonable, if we later get a ~ Int.  For now, though,
+-- we return Nothing, leaving it to the later constraint simplifier to
+-- sort matters out.
+--
+-- See Note [Refactoring hazard: checkTauTvUpdate]
+
+metaTyVarUpdateOK dflags tv ty
+  = case preCheck dflags False tv ty of
+         -- False <=> type families not ok
+         -- See Note [Prevent unification with type families]
+      OC_OK _   -> Just ty
+      OC_Bad    -> Nothing  -- forall or type function
+      OC_Occurs -> occCheckExpand [tv] ty
+
+preCheck :: DynFlags -> Bool -> TcTyVar -> TcType -> OccCheckResult ()
+-- A quick check for
+--   (a) a forall type (unless -XImpredivativeTypes)
+--   (b) a type family
+--   (c) an occurrence of the type variable (occurs check)
+--
+-- For (a) and (b) we check only the top level of the type, NOT
+-- inside the kinds of variables it mentions.  But for (c) we do
+-- look in the kinds of course.
+
+preCheck dflags ty_fam_ok tv ty
+  = fast_check ty
+  where
+    details          = tcTyVarDetails tv
+    impredicative_ok = canUnifyWithPolyType dflags details
+
+    ok :: OccCheckResult ()
+    ok = OC_OK ()
+
+    fast_check :: TcType -> OccCheckResult ()
+    fast_check (TyVarTy tv')
+      | tv == tv' = OC_Occurs
+      | otherwise = fast_check_occ (tyVarKind tv')
+           -- See Note [Occurrence checking: look inside kinds]
+
+    fast_check (TyConApp tc tys)
+      | bad_tc tc              = OC_Bad
+      | otherwise              = mapM fast_check tys >> ok
+    fast_check (LitTy {})      = ok
+    fast_check (FunTy a r)     = fast_check a   >> fast_check r
+    fast_check (AppTy fun arg) = fast_check fun >> fast_check arg
+    fast_check (CastTy ty co)  = fast_check ty  >> fast_check_co co
+    fast_check (CoercionTy co) = fast_check_co co
+    fast_check (ForAllTy (Bndr tv' _) ty)
+       | not impredicative_ok = OC_Bad
+       | tv == tv'            = ok
+       | otherwise = do { fast_check_occ (tyVarKind tv')
+                        ; fast_check_occ ty }
+       -- Under a forall we look only for occurrences of
+       -- the type variable
+
+     -- For kinds, we only do an occurs check; we do not worry
+     -- about type families or foralls
+     -- See Note [Checking for foralls]
+    fast_check_occ k | tv `elemVarSet` tyCoVarsOfType k = OC_Occurs
+                     | otherwise                        = ok
+
+     -- For coercions, we are only doing an occurs check here;
+     -- no bother about impredicativity in coercions, as they're
+     -- inferred
+    fast_check_co co | tv `elemVarSet` tyCoVarsOfCo co = OC_Occurs
+                     | otherwise                       = ok
+
+    bad_tc :: TyCon -> Bool
+    bad_tc tc
+      | not (impredicative_ok || isTauTyCon tc)     = True
+      | not (ty_fam_ok        || isFamFreeTyCon tc) = True
+      | otherwise                                   = False
+
+canUnifyWithPolyType :: DynFlags -> TcTyVarDetails -> Bool
+canUnifyWithPolyType dflags details
+  = case details of
+      MetaTv { mtv_info = TyVarTv }    -> False
+      MetaTv { mtv_info = TauTv }      -> xopt LangExt.ImpredicativeTypes dflags
+      _other                           -> True
+          -- We can have non-meta tyvars in given constraints