Allow multiple case branches to have a higher rank type

As #18412 points out, it should be OK for multiple case alternatives
to have a higher rank type, provided they are all the same.

This patch implements that change.  It sweeps away
GHC.Tc.Gen.Match.tauifyMultipleBranches, and friends, replacing it
with an enhanced version of fillInferResult.

The basic change to fillInferResult is to permit the case in which
another case alternative has already filled in the result; and in
that case simply unify.  It's very simple actually.

See the new Note [fillInferResult] in TcMType

Other refactoring:

- Move all the InferResult code to one place, in GHC.Tc.Utils.TcMType
  (previously some of it was in Unify)

- Move tcInstType and friends from TcMType to Instantiate, where it
  more properly belongs.  (TCMType was getting very long.)

21 files changed, 638 insertions, 610 deletions

diff --git a/compiler/GHC/Core/TyCo/Rep.hs b/compiler/GHC/Core/TyCo/Rep.hs
index 98c47aa767..61a374b38e 100644
--- a/compiler/GHC/Core/TyCo/Rep.hs
+++ b/compiler/GHC/Core/TyCo/Rep.hs
@@ -19,7 +19,7 @@ Note [The Type-related module hierarchy]
 
 -- We expose the relevant stuff from this module via the Type module
 {-# OPTIONS_HADDOCK not-home #-}
-{-# LANGUAGE CPP, DeriveDataTypeable, MultiWayIf, PatternSynonyms, BangPatterns #-}
+{-# LANGUAGE CPP, MultiWayIf, PatternSynonyms, BangPatterns, DeriveDataTypeable #-}
 
 module GHC.Core.TyCo.Rep (
         TyThing(..), tyThingCategory, pprTyThingCategory, pprShortTyThing,
@@ -2025,6 +2025,12 @@ GHC.Core.Multiplicity above this module.
 -- | A shorthand for data with an attached 'Mult' element (the multiplicity).
 data Scaled a = Scaled Mult a
   deriving (Data.Data)
+  -- You might think that this would be a natural candiate for
+  -- Functor, Traversable but Krzysztof says (!3674) "it was too easy
+  -- to accidentally lift functions (substitutions, zonking etc.) from
+  -- Type -> Type to Scaled Type -> Scaled Type, ignoring
+  -- multiplicities and causing bugs".  So we don't.
+
 
 instance (Outputable a) => Outputable (Scaled a) where
    ppr (Scaled _cnt t) = ppr t
diff --git a/compiler/GHC/Core/Type.hs b/compiler/GHC/Core/Type.hs
index 5bb11a9ee7..a0865b1820 100644
--- a/compiler/GHC/Core/Type.hs
+++ b/compiler/GHC/Core/Type.hs
@@ -48,7 +48,7 @@ module GHC.Core.Type (
         mkSpecForAllTy, mkSpecForAllTys,
         mkVisForAllTys, mkTyCoInvForAllTy,
         mkInfForAllTy, mkInfForAllTys,
-        splitForAllTys, splitSomeForAllTys,
+        splitForAllTys,
         splitForAllTysReq, splitForAllTysInvis,
         splitForAllVarBndrs,
         splitForAllTy_maybe, splitForAllTy,
@@ -284,7 +284,7 @@ import GHC.Data.List.SetOps
 import GHC.Types.Unique ( nonDetCmpUnique )
 
 import GHC.Data.Maybe   ( orElse, expectJust )
-import Data.Maybe       ( isJust, mapMaybe )
+import Data.Maybe       ( isJust )
 import Control.Monad    ( guard )
 
 -- $type_classification
@@ -1526,46 +1526,34 @@ splitForAllTys ty = split ty ty []
     split orig_ty ty tvs | Just ty' <- coreView ty = split orig_ty ty' tvs
     split orig_ty _                            tvs = (reverse tvs, orig_ty)
 
--- | Like 'splitForAllTys', but only splits a 'ForAllTy' if @argf_pred argf@
--- is 'True', where @argf@ is the visibility of the @ForAllTy@'s binder and
--- @argf_pred@ is a predicate over visibilities provided as an argument to this
--- function. Furthermore, each returned tyvar is annotated with its @argf@.
-splitSomeForAllTys :: (ArgFlag -> Bool) -> Type -> ([TyCoVarBinder], Type)
+-- | Splits the longest initial sequence of ForAllTys' that satisfy
+-- @argf_pred@, returning the binders transformed by @argf_pred@
+splitSomeForAllTys :: (ArgFlag -> Maybe af) -> Type -> ([VarBndr TyCoVar af], Type)
 splitSomeForAllTys argf_pred ty = split ty ty []
   where
-    split _       (ForAllTy tvb@(Bndr _ argf) ty) tvs
-      | argf_pred argf                             = split ty ty (tvb:tvs)
+    split _ (ForAllTy (Bndr tcv argf) ty) tvs
+      | Just argf' <- argf_pred argf               = split ty ty (Bndr tcv argf' : tvs)
     split orig_ty ty tvs | Just ty' <- coreView ty = split orig_ty ty' tvs
     split orig_ty _                            tvs = (reverse tvs, orig_ty)
 
 -- | Like 'splitForAllTys', but only splits 'ForAllTy's with 'Required' type
 -- variable binders. Furthermore, each returned tyvar is annotated with '()'.
 splitForAllTysReq :: Type -> ([ReqTVBinder], Type)
-splitForAllTysReq ty =
-  let (all_bndrs, body) = splitSomeForAllTys isVisibleArgFlag ty
-      req_bndrs         = mapMaybe mk_req_bndr_maybe all_bndrs in
-  ASSERT( req_bndrs `equalLength` all_bndrs )
-  (req_bndrs, body)
+splitForAllTysReq ty = splitSomeForAllTys argf_pred ty
   where
-    mk_req_bndr_maybe :: TyCoVarBinder -> Maybe ReqTVBinder
-    mk_req_bndr_maybe (Bndr tv argf) = case argf of
-      Required    -> Just $ Bndr tv ()
-      Invisible _ -> Nothing
+    argf_pred :: ArgFlag -> Maybe ()
+    argf_pred Required       = Just ()
+    argf_pred (Invisible {}) = Nothing
 
 -- | Like 'splitForAllTys', but only splits 'ForAllTy's with 'Invisible' type
 -- variable binders. Furthermore, each returned tyvar is annotated with its
 -- 'Specificity'.
 splitForAllTysInvis :: Type -> ([InvisTVBinder], Type)
-splitForAllTysInvis ty =
-  let (all_bndrs, body) = splitSomeForAllTys isInvisibleArgFlag ty
-      inv_bndrs         = mapMaybe mk_inv_bndr_maybe all_bndrs in
-  ASSERT( inv_bndrs `equalLength` all_bndrs )
-  (inv_bndrs, body)
+splitForAllTysInvis ty = splitSomeForAllTys argf_pred ty
   where
-    mk_inv_bndr_maybe :: TyCoVarBinder -> Maybe InvisTVBinder
-    mk_inv_bndr_maybe (Bndr tv argf) = case argf of
-      Invisible s -> Just $ Bndr tv s
-      Required    -> Nothing
+    argf_pred :: ArgFlag -> Maybe Specificity
+    argf_pred Required         = Nothing
+    argf_pred (Invisible spec) = Just spec
 
 -- | Like splitForAllTys, but split only for tyvars.
 -- This always succeeds, even if it returns only an empty list. Note that the
diff --git a/compiler/GHC/Core/UsageEnv.hs b/compiler/GHC/Core/UsageEnv.hs
index a03343ee9f..867b9533f0 100644
--- a/compiler/GHC/Core/UsageEnv.hs
+++ b/compiler/GHC/Core/UsageEnv.hs
@@ -1,7 +1,7 @@
 {-# LANGUAGE ViewPatterns #-}
 module GHC.Core.UsageEnv (UsageEnv, addUsage, scaleUsage, zeroUE,
                           lookupUE, scaleUE, deleteUE, addUE, Usage(..), unitUE,
-                          supUE, supUEs) where
+                          bottomUE, supUE, supUEs) where
 
 import Data.Foldable
 import GHC.Prelude
diff --git a/compiler/GHC/Tc/Gen/Expr.hs b/compiler/GHC/Tc/Gen/Expr.hs
index d5ecbcbe45..e8954914e3 100644
--- a/compiler/GHC/Tc/Gen/Expr.hs
+++ b/compiler/GHC/Tc/Gen/Expr.hs
@@ -599,22 +599,13 @@ tcExpr (HsCase x scrut matches) res_ty
 
 tcExpr (HsIf x pred b1 b2) res_ty
   = do { pred' <- tcLExpr pred (mkCheckExpType boolTy)
-       ; res_ty <- tauifyExpType res_ty
-           -- Just like Note [Case branches must never infer a non-tau type]
-           -- in GHC.Tc.Gen.Match (See #10619)
        ; (u1,b1') <- tcCollectingUsage $ tcLExpr b1 res_ty
        ; (u2,b2') <- tcCollectingUsage $ tcLExpr b2 res_ty
        ; tcEmitBindingUsage (supUE u1 u2)
        ; return (HsIf x pred' b1' b2') }
 
 tcExpr (HsMultiIf _ alts) res_ty
-  = do { res_ty <- if isSingleton alts
-                   then return res_ty
-                   else tauifyExpType res_ty
-             -- Just like GHC.Tc.Gen.Match
-             -- Note [Case branches must never infer a non-tau type]
-
-       ; alts' <- mapM (wrapLocM $ tcGRHS match_ctxt res_ty) alts
+  = do { alts' <- mapM (wrapLocM $ tcGRHS match_ctxt res_ty) alts
        ; res_ty <- readExpType res_ty
        ; return (HsMultiIf res_ty alts') }
   where match_ctxt = MC { mc_what = IfAlt, mc_body = tcBody }
diff --git a/compiler/GHC/Tc/Gen/Match.hs b/compiler/GHC/Tc/Gen/Match.hs
index 39dae3bf95..ee428cbc42 100644
--- a/compiler/GHC/Tc/Gen/Match.hs
+++ b/compiler/GHC/Tc/Gen/Match.hs
@@ -164,80 +164,47 @@ tcGRHSsPat grhss res_ty = tcGRHSs match_ctxt grhss (mkCheckExpType res_ty)
     match_ctxt = MC { mc_what = PatBindRhs,
                       mc_body = tcBody }
 
-{-
-************************************************************************
+{- *********************************************************************
 *                                                                      *
-\subsection{tcMatch}
+                tcMatch
 *                                                                      *
-************************************************************************
-
-Note [Case branches must never infer a non-tau type]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider
-
-  case ... of
-    ... -> \(x :: forall a. a -> a) -> x
-    ... -> \y -> y
-
-Should that type-check? The problem is that, if we check the second branch
-first, then we'll get a type (b -> b) for the branches, which won't unify
-with the polytype in the first branch. If we check the first branch first,
-then everything is OK. This order-dependency is terrible. So we want only
-proper tau-types in branches (unless a sigma-type is pushed down).
-This is what expTypeToType ensures: it replaces an Infer with a fresh
-tau-type.
-
-An even trickier case looks like
-
-  f x True  = x undefined
-  f x False = x ()
-
-Here, we see that the arguments must also be non-Infer. Thus, we must
-use expTypeToType on the output of matchExpectedFunTys, not the input.
-
-But we make a special case for a one-branch case. This is so that
-
-  f = \(x :: forall a. a -> a) -> x
-
-still gets assigned a polytype.
--}
+********************************************************************* -}
 
--- | When the MatchGroup has multiple RHSs, convert an Infer ExpType in the
--- expected type into TauTvs.
--- See Note [Case branches must never infer a non-tau type]
-tauifyMultipleMatches :: [LMatch id body]
-                      -> [Scaled ExpType] -> TcM [Scaled ExpType]
-tauifyMultipleMatches group exp_tys
-  | isSingletonMatchGroup group = return exp_tys
-  | otherwise                   = mapM (\(Scaled m t) ->
-                                       fmap (Scaled m) (tauifyExpType t)) exp_tys
-  -- NB: In the empty-match case, this ensures we fill in the ExpType
+data TcMatchCtxt body   -- c.f. TcStmtCtxt, also in this module
+  = MC { mc_what :: HsMatchContext GhcRn,  -- What kind of thing this is
+         mc_body :: Located (body GhcRn)   -- Type checker for a body of
+                                           -- an alternative
+                 -> ExpRhoType
+                 -> TcM (Located (body GhcTc)) }
 
 -- | Type-check a MatchGroup.
 tcMatches :: (Outputable (body GhcRn)) => TcMatchCtxt body
           -> [Scaled ExpSigmaType]      -- Expected pattern types
-          -> ExpRhoType          -- Expected result-type of the Match.
+          -> ExpRhoType                 -- Expected result-type of the Match.
           -> MatchGroup GhcRn (Located (body GhcRn))
           -> TcM (MatchGroup GhcTc (Located (body GhcTc)))
 
-data TcMatchCtxt body   -- c.f. TcStmtCtxt, also in this module
-  = MC { mc_what :: HsMatchContext GhcRn,  -- What kind of thing this is
-         mc_body :: Located (body GhcRn)         -- Type checker for a body of
-                                                -- an alternative
-                 -> ExpRhoType
-                 -> TcM (Located (body GhcTc)) }
 tcMatches ctxt pat_tys rhs_ty (MG { mg_alts = L l matches
                                   , mg_origin = origin })
-  = do { (Scaled _ rhs_ty):pat_tys <- tauifyMultipleMatches matches ((Scaled One rhs_ty):pat_tys) -- return type has implicitly multiplicity 1, it doesn't matter all that much in this case since it isn't used and is eliminated immediately.
-            -- See Note [Case branches must never infer a non-tau type]
+  | null matches  -- Deal with case e of {}
+    -- Since there are no branches, no one else will fill in rhs_ty
+    -- when in inference mode, so we must do it ourselves,
+    -- here, using expTypeToType
+  = do { tcEmitBindingUsage bottomUE
+       ; pat_tys <- mapM scaledExpTypeToType pat_tys
+       ; rhs_ty  <- expTypeToType rhs_ty
+       ; return (MG { mg_alts = L l []
+                    , mg_ext = MatchGroupTc pat_tys rhs_ty
+                    , mg_origin = origin }) }
 
-       ; umatches <- mapM (tcCollectingUsage . tcMatch ctxt pat_tys rhs_ty) matches
+  | otherwise
+  = do { umatches <- mapM (tcCollectingUsage . tcMatch ctxt pat_tys rhs_ty) matches
        ; let (usages,matches') = unzip umatches
        ; tcEmitBindingUsage $ supUEs usages
-       ; pat_tys  <- mapM (\(Scaled m t) -> fmap (Scaled m) (readExpType t)) pat_tys
+       ; pat_tys  <- mapM readScaledExpType pat_tys
        ; rhs_ty   <- readExpType rhs_ty
-       ; return (MG { mg_alts = L l matches'
-                    , mg_ext = MatchGroupTc pat_tys rhs_ty
+       ; return (MG { mg_alts   = L l matches'
+                    , mg_ext    = MatchGroupTc pat_tys rhs_ty
                     , mg_origin = origin }) }
 
 -------------
diff --git a/compiler/GHC/Tc/Gen/Pat.hs b/compiler/GHC/Tc/Gen/Pat.hs
index 181f87304e..c8d021a4fe 100644
--- a/compiler/GHC/Tc/Gen/Pat.hs
+++ b/compiler/GHC/Tc/Gen/Pat.hs
@@ -220,8 +220,9 @@ tcPatBndr penv@(PE { pe_ctxt = LetPat { pc_lvl    = bind_lvl
   = do { (co, bndr_ty) <- case scaledThing exp_pat_ty of
              Check pat_ty    -> promoteTcType bind_lvl pat_ty
              Infer infer_res -> ASSERT( bind_lvl == ir_lvl infer_res )
-                                -- If we were under a constructor that bumped
-                                -- the level, we'd be in checking mode
+                                -- If we were under a constructor that bumped the
+                                -- level, we'd be in checking mode (see tcConArg)
+                                -- hence this assertion
                                 do { bndr_ty <- inferResultToType infer_res
                                    ; return (mkTcNomReflCo bndr_ty, bndr_ty) }
        ; let bndr_mult = scaledMult exp_pat_ty
@@ -629,10 +630,9 @@ There are two bits of rebindable syntax:
 lit1_ty and lit2_ty could conceivably be different.
 var_ty is the type inferred for x, the variable in the pattern.
 
-If the pushed-down pattern type isn't a tau-type, the two pat_ty's above
-could conceivably be different specializations. But this is very much
-like the situation in Note [Case branches must be taus] in GHC.Tc.Gen.Match.
-So we tauify the pat_ty before proceeding.
+If the pushed-down pattern type isn't a tau-type, the two pat_ty's
+above could conceivably be different specializations.  So we use
+expTypeToType on pat_ty before proceeding.
 
 Note that we need to type-check the literal twice, because it is used
 twice, and may be used at different types. The second HsOverLit stored in the
diff --git a/compiler/GHC/Tc/Gen/Sig.hs b/compiler/GHC/Tc/Gen/Sig.hs
index 89fcff3079..aee53733f4 100644
--- a/compiler/GHC/Tc/Gen/Sig.hs
+++ b/compiler/GHC/Tc/Gen/Sig.hs
@@ -36,7 +36,7 @@ import GHC.Tc.Utils.TcType
 import GHC.Tc.Utils.TcMType
 import GHC.Tc.Validity ( checkValidType )
 import GHC.Tc.Utils.Unify( tcSkolemise, unifyType )
-import GHC.Tc.Utils.Instantiate( topInstantiate )
+import GHC.Tc.Utils.Instantiate( topInstantiate, tcInstTypeBndrs )
 import GHC.Tc.Utils.Env( tcLookupId )
 import GHC.Tc.Types.Evidence( HsWrapper, (<.>) )
 import GHC.Core.Type ( mkTyVarBinders )
@@ -488,7 +488,7 @@ tcInstSig :: TcIdSigInfo -> TcM TcIdSigInst
 -- Instantiate a type signature; only used with plan InferGen
 tcInstSig sig@(CompleteSig { sig_bndr = poly_id, sig_loc = loc })
   = setSrcSpan loc $  -- Set the binding site of the tyvars
-    do { (tv_prs, theta, tau) <- tcInstTypeBndrs newMetaTyVarTyVars poly_id
+    do { (tv_prs, theta, tau) <- tcInstTypeBndrs poly_id
               -- See Note [Pattern bindings and complete signatures]
 
        ; return (TISI { sig_inst_sig   = sig
diff --git a/compiler/GHC/Tc/Instance/Class.hs b/compiler/GHC/Tc/Instance/Class.hs
index 1df66632a2..5446a756a3 100644
--- a/compiler/GHC/Tc/Instance/Class.hs
+++ b/compiler/GHC/Tc/Instance/Class.hs
@@ -16,6 +16,7 @@ import GHC.Prelude
 import GHC.Tc.Utils.Env
 import GHC.Tc.Utils.Monad
 import GHC.Tc.Utils.TcType
+import GHC.Tc.Utils.Instantiate( tcInstType )
 import GHC.Tc.Instance.Typeable
 import GHC.Tc.Utils.TcMType
 import GHC.Tc.Types.Evidence
diff --git a/compiler/GHC/Tc/Instance/Family.hs b/compiler/GHC/Tc/Instance/Family.hs
index 9be5c4675b..8a2c5b0e7a 100644
--- a/compiler/GHC/Tc/Instance/Family.hs
+++ b/compiler/GHC/Tc/Instance/Family.hs
@@ -21,6 +21,7 @@ import GHC.Core.Coercion
 import GHC.Tc.Types.Evidence
 import GHC.Iface.Load
 import GHC.Tc.Utils.Monad
+import GHC.Tc.Utils.Instantiate( freshenTyVarBndrs, freshenCoVarBndrsX )
 import GHC.Types.SrcLoc as SrcLoc
 import GHC.Core.TyCon
 import GHC.Tc.Utils.TcType
@@ -35,7 +36,6 @@ import GHC.Data.Maybe
 import GHC.Core.TyCo.Rep
 import GHC.Core.TyCo.FVs
 import GHC.Core.TyCo.Ppr ( pprWithExplicitKindsWhen )
-import GHC.Tc.Utils.TcMType
 import GHC.Types.Name
 import GHC.Utils.Panic
 import GHC.Types.Var.Set
diff --git a/compiler/GHC/Tc/TyCl/Class.hs b/compiler/GHC/Tc/TyCl/Class.hs
index fe9dcf72d9..4430e0e682 100644
--- a/compiler/GHC/Tc/TyCl/Class.hs
+++ b/compiler/GHC/Tc/TyCl/Class.hs
@@ -31,11 +31,12 @@ where
 import GHC.Prelude
 
 import GHC.Hs
-import GHC.Tc.Utils.Env
 import GHC.Tc.Gen.Sig
 import GHC.Tc.Types.Evidence ( idHsWrapper )
 import GHC.Tc.Gen.Bind
+import GHC.Tc.Utils.Env
 import GHC.Tc.Utils.Unify
+import GHC.Tc.Utils.Instantiate( tcSuperSkolTyVars )
 import GHC.Tc.Gen.HsType
 import GHC.Tc.Utils.TcMType
 import GHC.Core.Type     ( piResultTys )
diff --git a/compiler/GHC/Tc/Utils/Instantiate.hs b/compiler/GHC/Tc/Utils/Instantiate.hs
index e72e5742a6..385cd634e8 100644
--- a/compiler/GHC/Tc/Utils/Instantiate.hs
+++ b/compiler/GHC/Tc/Utils/Instantiate.hs
@@ -16,6 +16,12 @@ module GHC.Tc.Utils.Instantiate (
        instCall, instDFunType, instStupidTheta, instTyVarsWith,
        newWanted, newWanteds,
 
+       tcInstType, tcInstTypeBndrs,
+       tcInstSkolTyVars, tcInstSkolTyVarsX, tcInstSkolTyVarsAt,
+       tcSkolDFunType, tcSuperSkolTyVars, tcInstSuperSkolTyVarsX,
+
+       freshenTyVarBndrs, freshenCoVarBndrsX,
+
        tcInstInvisibleTyBindersN, tcInstInvisibleTyBinders, tcInstInvisibleTyBinder,
 
        newOverloadedLit, mkOverLit,
@@ -63,7 +69,7 @@ import GHC.Types.Id.Make( mkDictFunId )
 import GHC.Core( Expr(..) )  -- For the Coercion constructor
 import GHC.Types.Id
 import GHC.Types.Name
-import GHC.Types.Var ( EvVar, tyVarName, VarBndr(..) )
+import GHC.Types.Var
 import GHC.Core.DataCon
 import GHC.Types.Var.Env
 import GHC.Builtin.Names
@@ -74,7 +80,7 @@ import GHC.Utils.Outputable
 import GHC.Types.Basic ( TypeOrKind(..) )
 import qualified GHC.LanguageExtensions as LangExt
 
-import Data.List ( sortBy )
+import Data.List ( sortBy, mapAccumL )
 import Control.Monad( unless )
 import Data.Function ( on )
 
@@ -451,15 +457,192 @@ mkEqBoxTy co ty1 ty2
     mkTyConApp (promoteDataCon eqDataCon) [k, ty1, ty2, mkCoercionTy co]
   where k = tcTypeKind ty1
 
-{-
-************************************************************************
+{- *********************************************************************
 *                                                                      *
-                Literals
+        SkolemTvs (immutable)
 *                                                                      *
-************************************************************************
+********************************************************************* -}
 
+tcInstType :: ([TyVar] -> TcM (TCvSubst, [TcTyVar]))
+                   -- ^ How to instantiate the type variables
+           -> Id                                           -- ^ Type to instantiate
+           -> TcM ([(Name, TcTyVar)], TcThetaType, TcType) -- ^ Result
+                -- (type vars, preds (incl equalities), rho)
+tcInstType inst_tyvars id
+  | null tyvars   -- There may be overloading despite no type variables;
+                  --      (?x :: Int) => Int -> Int
+  = return ([], theta, tau)
+  | otherwise
+  = do { (subst, tyvars') <- inst_tyvars tyvars
+       ; let tv_prs  = map tyVarName tyvars `zip` tyvars'
+             subst'  = extendTCvInScopeSet subst (tyCoVarsOfType rho)
+       ; return (tv_prs, substTheta subst' theta, substTy subst' tau) }
+  where
+    (tyvars, rho) = tcSplitForAllTys (idType id)
+    (theta, tau)  = tcSplitPhiTy rho
+
+tcInstTypeBndrs :: Id -> TcM ([(Name, InvisTVBinder)], TcThetaType, TcType)
+                     -- (type vars, preds (incl equalities), rho)
+-- Instantiate the binders of a type signature with TyVarTvs
+tcInstTypeBndrs id
+  | null tyvars   -- There may be overloading despite no type variables;
+                  --      (?x :: Int) => Int -> Int
+  = return ([], theta, tau)
+  | otherwise
+  = do { (subst, tyvars') <- mapAccumLM inst_invis_bndr emptyTCvSubst tyvars
+       ; let tv_prs  = map (tyVarName . binderVar) tyvars `zip` tyvars'
+             subst'  = extendTCvInScopeSet subst (tyCoVarsOfType rho)
+       ; return (tv_prs, substTheta subst' theta, substTy subst' tau) }
+  where
+    (tyvars, rho) = splitForAllTysInvis (idType id)
+    (theta, tau)  = tcSplitPhiTy rho
+
+    inst_invis_bndr :: TCvSubst -> InvisTVBinder
+                    -> TcM (TCvSubst, InvisTVBinder)
+    inst_invis_bndr subst (Bndr tv spec)
+      = do { (subst', tv') <- newMetaTyVarTyVarX subst tv
+           ; return (subst', Bndr tv' spec) }
+
+tcSkolDFunType :: DFunId -> TcM ([TcTyVar], TcThetaType, TcType)
+-- Instantiate a type signature with skolem constants.
+-- We could give them fresh names, but no need to do so
+tcSkolDFunType dfun
+  = do { (tv_prs, theta, tau) <- tcInstType tcInstSuperSkolTyVars dfun
+       ; return (map snd tv_prs, theta, tau) }
+
+tcSuperSkolTyVars :: [TyVar] -> (TCvSubst, [TcTyVar])
+-- Make skolem constants, but do *not* give them new names, as above
+-- Moreover, make them "super skolems"; see comments with superSkolemTv
+-- see Note [Kind substitution when instantiating]
+-- Precondition: tyvars should be ordered by scoping
+tcSuperSkolTyVars = mapAccumL tcSuperSkolTyVar emptyTCvSubst
+
+tcSuperSkolTyVar :: TCvSubst -> TyVar -> (TCvSubst, TcTyVar)
+tcSuperSkolTyVar subst tv
+  = (extendTvSubstWithClone subst tv new_tv, new_tv)
+  where
+    kind   = substTyUnchecked subst (tyVarKind tv)
+    new_tv = mkTcTyVar (tyVarName tv) kind superSkolemTv
+
+-- | Given a list of @['TyVar']@, skolemize the type variables,
+-- returning a substitution mapping the original tyvars to the
+-- skolems, and the list of newly bound skolems.
+tcInstSkolTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
+-- See Note [Skolemising type variables]
+tcInstSkolTyVars = tcInstSkolTyVarsX emptyTCvSubst
+
+tcInstSkolTyVarsX :: TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
+-- See Note [Skolemising type variables]
+tcInstSkolTyVarsX = tcInstSkolTyVarsPushLevel False
+
+tcInstSuperSkolTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
+-- See Note [Skolemising type variables]
+tcInstSuperSkolTyVars = tcInstSuperSkolTyVarsX emptyTCvSubst
+
+tcInstSuperSkolTyVarsX :: TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
+-- See Note [Skolemising type variables]
+tcInstSuperSkolTyVarsX subst = tcInstSkolTyVarsPushLevel True subst
+
+tcInstSkolTyVarsPushLevel :: Bool -> TCvSubst -> [TyVar]
+                          -> TcM (TCvSubst, [TcTyVar])
+-- Skolemise one level deeper, hence pushTcLevel
+-- See Note [Skolemising type variables]
+tcInstSkolTyVarsPushLevel overlappable subst tvs
+  = do { tc_lvl <- getTcLevel
+       ; let pushed_lvl = pushTcLevel tc_lvl
+       ; tcInstSkolTyVarsAt pushed_lvl overlappable subst tvs }
+
+tcInstSkolTyVarsAt :: TcLevel -> Bool
+                   -> TCvSubst -> [TyVar]
+                   -> TcM (TCvSubst, [TcTyVar])
+tcInstSkolTyVarsAt lvl overlappable subst tvs
+  = freshenTyCoVarsX new_skol_tv subst tvs
+  where
+    details = SkolemTv lvl overlappable
+    new_skol_tv name kind = mkTcTyVar name kind details
+
+------------------
+freshenTyVarBndrs :: [TyVar] -> TcM (TCvSubst, [TyVar])
+-- ^ Give fresh uniques to a bunch of TyVars, but they stay
+--   as TyVars, rather than becoming TcTyVars
+-- Used in 'GHC.Tc.Instance.Family.newFamInst', and 'GHC.Tc.Utils.Instantiate.newClsInst'
+freshenTyVarBndrs = freshenTyCoVars mkTyVar
+
+freshenCoVarBndrsX :: TCvSubst -> [CoVar] -> TcM (TCvSubst, [CoVar])
+-- ^ Give fresh uniques to a bunch of CoVars
+-- Used in "GHC.Tc.Instance.Family.newFamInst"
+freshenCoVarBndrsX subst = freshenTyCoVarsX mkCoVar subst
+
+------------------
+freshenTyCoVars :: (Name -> Kind -> TyCoVar)
+                -> [TyVar] -> TcM (TCvSubst, [TyCoVar])
+freshenTyCoVars mk_tcv = freshenTyCoVarsX mk_tcv emptyTCvSubst
+
+freshenTyCoVarsX :: (Name -> Kind -> TyCoVar)
+                 -> TCvSubst -> [TyCoVar]
+                 -> TcM (TCvSubst, [TyCoVar])
+freshenTyCoVarsX mk_tcv = mapAccumLM (freshenTyCoVarX mk_tcv)
+
+freshenTyCoVarX :: (Name -> Kind -> TyCoVar)
+                -> TCvSubst -> TyCoVar -> TcM (TCvSubst, TyCoVar)
+-- This a complete freshening operation:
+-- the skolems have a fresh unique, and a location from the monad
+-- See Note [Skolemising type variables]
+freshenTyCoVarX mk_tcv subst tycovar
+  = do { loc  <- getSrcSpanM
+       ; uniq <- newUnique
+       ; let old_name = tyVarName tycovar
+             new_name = mkInternalName uniq (getOccName old_name) loc
+             new_kind = substTyUnchecked subst (tyVarKind tycovar)
+             new_tcv  = mk_tcv new_name new_kind
+             subst1   = extendTCvSubstWithClone subst tycovar new_tcv
+       ; return (subst1, new_tcv) }
+
+{- Note [Skolemising type variables]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The tcInstSkolTyVars family of functions instantiate a list of TyVars
+to fresh skolem TcTyVars. Important notes:
+
+a) Level allocation. We generally skolemise /before/ calling
+   pushLevelAndCaptureConstraints.  So we want their level to the level
+   of the soon-to-be-created implication, which has a level ONE HIGHER
+   than the current level.  Hence the pushTcLevel.  It feels like a
+   slight hack.
+
+b) The [TyVar] should be ordered (kind vars first)
+   See Note [Kind substitution when instantiating]
+
+c) It's a complete freshening operation: the skolems have a fresh
+   unique, and a location from the monad
+
+d) The resulting skolems are
+        non-overlappable for tcInstSkolTyVars,
+   but overlappable for tcInstSuperSkolTyVars
+   See GHC.Tc.Deriv.Infer Note [Overlap and deriving] for an example
+   of where this matters.
+
+Note [Kind substitution when instantiating]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When we instantiate a bunch of kind and type variables, first we
+expect them to be topologically sorted.
+Then we have to instantiate the kind variables, build a substitution
+from old variables to the new variables, then instantiate the type
+variables substituting the original kind.
+
+Exemple: If we want to instantiate
+  [(k1 :: *), (k2 :: *), (a :: k1 -> k2), (b :: k1)]
+we want
+  [(?k1 :: *), (?k2 :: *), (?a :: ?k1 -> ?k2), (?b :: ?k1)]
+instead of the bogus
+  [(?k1 :: *), (?k2 :: *), (?a :: k1 -> k2), (?b :: k1)]
 -}
 
+{- *********************************************************************
+*                                                                      *
+                Literals
+*                                                                      *
+********************************************************************* -}
+
 {-
 In newOverloadedLit we convert directly to an Int or Integer if we
 know that's what we want.  This may save some time, by not
@@ -474,8 +657,6 @@ newOverloadedLit :: HsOverLit GhcRn
 newOverloadedLit
   lit@(OverLit { ol_val = val, ol_ext = rebindable }) res_ty
   | not rebindable
-    -- all built-in overloaded lits are tau-types, so we can just
-    -- tauify the ExpType
   = do { res_ty <- expTypeToType res_ty
        ; dflags <- getDynFlags
        ; let platform = targetPlatform dflags
diff --git a/compiler/GHC/Tc/Utils/TcMType.hs b/compiler/GHC/Tc/Utils/TcMType.hs
index 34e4bfe0bb..e8ae500075 100644
--- a/compiler/GHC/Tc/Utils/TcMType.hs
+++ b/compiler/GHC/Tc/Utils/TcMType.hs
@@ -32,15 +32,6 @@ module GHC.Tc.Utils.TcMType (
   isFilledMetaTyVar_maybe, isFilledMetaTyVar, isUnfilledMetaTyVar,
 
   --------------------------------
-  -- Expected types
-  ExpType(..), ExpSigmaType, ExpRhoType,
-  mkCheckExpType,
-  newInferExpType,
-  readExpType, readExpType_maybe,
-  expTypeToType, checkingExpType_maybe, checkingExpType,
-  tauifyExpType, inferResultToType,
-
-  --------------------------------
   -- Creating new evidence variables
   newEvVar, newEvVars, newDict,
   newWanted, newWanteds, cloneWanted, cloneWC,
@@ -58,14 +49,18 @@ module GHC.Tc.Utils.TcMType (
   --------------------------------
   -- Instantiation
   newMetaTyVars, newMetaTyVarX, newMetaTyVarsX,
-  newMetaTyVarTyVars, newMetaTyVarTyVarX,
+  newMetaTyVarTyVarX,
   newTyVarTyVar, cloneTyVarTyVar,
   newPatSigTyVar, newSkolemTyVar, newWildCardX,
-  tcInstType, tcInstTypeBndrs,
-  tcInstSkolTyVars, tcInstSkolTyVarsX, tcInstSkolTyVarsAt,
-  tcSkolDFunType, tcSuperSkolTyVars, tcInstSuperSkolTyVarsX,
 
-  freshenTyVarBndrs, freshenCoVarBndrsX,
+  --------------------------------
+  -- Expected types
+  ExpType(..), ExpSigmaType, ExpRhoType,
+  mkCheckExpType, newInferExpType, tcInfer,
+  readExpType, readExpType_maybe, readScaledExpType,
+  expTypeToType, scaledExpTypeToType,
+  checkingExpType_maybe, checkingExpType,
+  inferResultToType, fillInferResult, promoteTcType,
 
   --------------------------------
   -- Zonking and tidying
@@ -99,6 +94,8 @@ module GHC.Tc.Utils.TcMType (
 -- friends:
 import GHC.Prelude
 
+import {-# SOURCE #-}   GHC.Tc.Utils.Unify( unifyType {- , unifyKind -} )
+
 import GHC.Core.TyCo.Rep
 import GHC.Core.TyCo.Ppr
 import GHC.Tc.Utils.TcType
@@ -133,7 +130,6 @@ import GHC.Types.Basic ( TypeOrKind(..) )
 
 import Control.Monad
 import GHC.Data.Maybe
-import Data.List        ( mapAccumL )
 import Control.Arrow    ( second )
 import qualified Data.Semigroup as Semi
 
@@ -387,16 +383,14 @@ checkCoercionHole cv co
              | otherwise
              = False
 
-{-
-************************************************************************
+{- **********************************************************************
 *
-    Expected types
+                      ExpType functions
 *
-************************************************************************
-
-Note [ExpType]
-~~~~~~~~~~~~~~
+********************************************************************** -}
 
+{- Note [ExpType]
+~~~~~~~~~~~~~~~~~
 An ExpType is used as the "expected type" when type-checking an expression.
 An ExpType can hold a "hole" that can be filled in by the type-checker.
 This allows us to have one tcExpr that works in both checking mode and
@@ -426,14 +420,12 @@ Consider
 
 This is a classic untouchable-variable / ambiguous GADT return type
 scenario. But, with ExpTypes, we'll be inferring the type of the RHS.
-And, because there is only one branch of the case, we won't trigger
-Note [Case branches must never infer a non-tau type] of GHC.Tc.Gen.Match.
 We thus must track a TcLevel in an Inferring ExpType. If we try to
-fill the ExpType and find that the TcLevels don't work out, we
-fill the ExpType with a tau-tv at the low TcLevel, hopefully to
-be worked out later by some means. This is triggered in
-test gadt/gadt-escape1.
+fill the ExpType and find that the TcLevels don't work out, we fill
+the ExpType with a tau-tv at the low TcLevel, hopefully to be worked
+out later by some means -- see fillInferResult, and Note [fillInferResult]
 
+This behaviour triggered in test gadt/gadt-escape1.
 -}
 
 -- actual data definition is in GHC.Tc.Utils.TcType
@@ -453,6 +445,12 @@ readExpType_maybe :: ExpType -> TcM (Maybe TcType)
 readExpType_maybe (Check ty)                   = return (Just ty)
 readExpType_maybe (Infer (IR { ir_ref = ref})) = readMutVar ref
 
+-- | Same as readExpType, but for Scaled ExpTypes
+readScaledExpType :: Scaled ExpType -> TcM (Scaled Type)
+readScaledExpType (Scaled m exp_ty)
+  = do { ty <- readExpType exp_ty
+       ; return (Scaled m ty) }
+
 -- | Extract a type out of an ExpType. Otherwise, panics.
 readExpType :: ExpType -> TcM TcType
 readExpType exp_ty
@@ -472,12 +470,10 @@ checkingExpType :: String -> ExpType -> TcType
 checkingExpType _   (Check ty) = ty
 checkingExpType err et         = pprPanic "checkingExpType" (text err $$ ppr et)
 
-tauifyExpType :: ExpType -> TcM ExpType
--- ^ Turn a (Infer hole) type into a (Check alpha),
--- where alpha is a fresh unification variable
-tauifyExpType (Check ty)      = return (Check ty)  -- No-op for (Check ty)
-tauifyExpType (Infer inf_res) = do { ty <- inferResultToType inf_res
-                                   ; return (Check ty) }
+scaledExpTypeToType :: Scaled ExpType -> TcM (Scaled TcType)
+scaledExpTypeToType (Scaled m exp_ty)
+  = do { ty <- expTypeToType exp_ty
+       ; return (Scaled m ty) }
 
 -- | Extracts the expected type if there is one, or generates a new
 -- TauTv if there isn't.
@@ -488,209 +484,279 @@ expTypeToType (Infer inf_res) = inferResultToType inf_res
 inferResultToType :: InferResult -> TcM Type
 inferResultToType (IR { ir_uniq = u, ir_lvl = tc_lvl
                       , ir_ref = ref })
-  = do { rr  <- newMetaTyVarTyAtLevel tc_lvl runtimeRepTy
-       ; tau <- newMetaTyVarTyAtLevel tc_lvl (tYPE rr)
-             -- See Note [TcLevel of ExpType]
-       ; writeMutVar ref (Just tau)
+  = do { mb_inferred_ty <- readTcRef ref
+       ; tau <- case mb_inferred_ty of
+            Just ty -> do { ensureMonoType ty
+                            -- See Note [inferResultToType]
+                          ; return ty }
+            Nothing -> do { rr  <- newMetaTyVarTyAtLevel tc_lvl runtimeRepTy
+                          ; tau <- newMetaTyVarTyAtLevel tc_lvl (tYPE rr)
+                            -- See Note [TcLevel of ExpType]
+                          ; writeMutVar ref (Just tau)
+                          ; return tau }
        ; traceTc "Forcing ExpType to be monomorphic:"
                  (ppr u <+> text ":=" <+> ppr tau)
        ; return tau }
 
+{- Note [inferResultToType]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+expTypeToType and inferResultType convert an InferResult to a monotype.
+It must be a monotype because if the InferResult isn't already filled in,
+we fill it in with a unification variable (hence monotype).  So to preserve
+order-independence we check for mono-type-ness even if it *is* filled in
+already.
+
+See also Note [TcLevel of ExpType] above, and
+Note [fillInferResult].
+-}
+
+-- | Infer a type using a fresh ExpType
+-- See also Note [ExpType] in "GHC.Tc.Utils.TcMType"
+tcInfer :: (ExpSigmaType -> TcM a) -> TcM (a, TcSigmaType)
+tcInfer tc_check
+  = do { res_ty <- newInferExpType
+       ; result <- tc_check res_ty
+       ; res_ty <- readExpType res_ty
+       ; return (result, res_ty) }
+
+fillInferResult :: TcType -> InferResult -> TcM TcCoercionN
+-- If co = fillInferResult t1 t2
+--    => co :: t1 ~ t2
+-- See Note [fillInferResult]
+fillInferResult act_res_ty (IR { ir_uniq = u, ir_lvl = res_lvl
+                               , ir_ref = ref })
+  = do { mb_exp_res_ty <- readTcRef ref
+       ; case mb_exp_res_ty of
+            Just exp_res_ty
+               -> do { traceTc "Joining inferred ExpType" $
+                       ppr u <> colon <+> ppr act_res_ty <+> char '~' <+> ppr exp_res_ty
+                     ; cur_lvl <- getTcLevel
+                     ; unless (cur_lvl `sameDepthAs` res_lvl) $
+                       ensureMonoType act_res_ty
+                     ; unifyType Nothing act_res_ty exp_res_ty }
+            Nothing
+               -> do { traceTc "Filling inferred ExpType" $
+                       ppr u <+> text ":=" <+> ppr act_res_ty
+                     ; (prom_co, act_res_ty) <- promoteTcType res_lvl act_res_ty
+                     ; writeTcRef ref (Just act_res_ty)
+                     ; return prom_co }
+     }
+
+
+{- Note [fillInferResult]
+~~~~~~~~~~~~~~~~~~~~~~~~~
+When inferring, we use fillInferResult to "fill in" the hole in InferResult
+   data InferResult = IR { ir_uniq :: Unique
+                         , ir_lvl  :: TcLevel
+                         , ir_ref  :: IORef (Maybe TcType) }
+
+There are two things to worry about:
+
+1. What if it is under a GADT or existential pattern match?
+   - GADTs: a unification variable (and Infer's hole is similar) is untouchable
+   - Existentials: be careful about skolem-escape
+
+2. What if it is filled in more than once?  E.g. multiple branches of a case
+     case e of
+        T1 -> e1
+        T2 -> e2
+
+Our typing rules are:
+
+* The RHS of a existential or GADT alternative must always be a
+  monotype, regardless of the number of alternatives.
+
+* Multiple non-existential/GADT branches can have (the same)
+  higher rank type (#18412).  E.g. this is OK:
+      case e of
+        True  -> hr
+        False -> hr
+  where hr:: (forall a. a->a) -> Int
+  c.f. Section 7.1 of "Practical type inference for arbitrary-rank types"
+       We use choice (2) in that Section.
+       (GHC 8.10 and earlier used choice (1).)
+
+  But note that
+      case e of
+        True  -> hr
+        False -> \x -> hr x
+  will fail, because we still /infer/ both branches, so the \x will get
+  a (monotype) unification variable, which will fail to unify with
+  (forall a. a->a)
+
+For (1) we can detect the GADT/existential situation by seeing that
+the current TcLevel is greater than that stored in ir_lvl of the Infer
+ExpType.  We bump the level whenever we go past a GADT/existential match.
+
+Then, before filling the hole use promoteTcType to promote the type
+to the outer ir_lvl.  promoteTcType does this
+  - create a fresh unification variable alpha at level ir_lvl
+  - emits an equality alpha[ir_lvl] ~ ty
+  - fills the hole with alpha
+That forces the type to be a monotype (since unification variables can
+only unify with monotypes); and catches skolem-escapes because the
+alpha is untouchable until the equality floats out.
+
+For (2), we simply look to see if the hole is filled already.
+  - if not, we promote (as above) and fill the hole
+  - if it is filled, we simply unify with the type that is
+    already there
+
+There is one wrinkle.  Suppose we have
+   case e of
+      T1 -> e1 :: (forall a. a->a) -> Int
+      G2 -> e2
+where T1 is not GADT or existential, but G2 is a GADT.  Then supppose the
+T1 alternative fills the hole with (forall a. a->a) -> Int, which is fine.
+But now the G2 alternative must not *just* unify with that else we'd risk
+allowing through (e2 :: (forall a. a->a) -> Int).  If we'd checked G2 first
+we'd have filled the hole with a unification variable, which enforces a
+monotype.
+
+So if we check G2 second, we still want to emit a constraint that restricts
+the RHS to be a monotype. This is done by ensureMonoType, and it works
+by simply generating a constraint (alpha ~ ty), where alpha is a fresh
+unification variable.  We discard the evidence.
+
+-}
 
 {- *********************************************************************
 *                                                                      *
-        SkolemTvs (immutable)
+              Promoting types
 *                                                                      *
 ********************************************************************* -}
 
-tc_inst_internal :: ([VarBndr TyVar flag] -> TcM (TCvSubst, [VarBndr TcTyVar flag]))
-                        -- ^ How to instantiate the type variables
-                 -> [VarBndr TyVar flag] -- ^ Type variable to instantiate
-                 -> Type                 -- ^ rho
-                 -> TcM ([(Name, VarBndr TcTyVar flag)], TcThetaType, TcType) -- ^ Result
-                       -- (type vars, preds (incl equalities), rho)
-tc_inst_internal _inst_tyvars []     rho =
-  let -- There may be overloading despite no type variables;
-      --      (?x :: Int) => Int -> Int
-    (theta, tau) = tcSplitPhiTy rho
-  in
-    return ([], theta, tau)
-tc_inst_internal  inst_tyvars tyvars rho =
-  do { (subst, tyvars') <- inst_tyvars tyvars
-     ; let (theta, tau) = tcSplitPhiTy (substTyAddInScope subst rho)
-           tv_prs       = map (tyVarName . binderVar) tyvars `zip` tyvars'
-     ; return (tv_prs, theta, tau) }
-
-tcInstType :: ([TyVar] -> TcM (TCvSubst, [TcTyVar]))
-                   -- ^ How to instantiate the type variables
-           -> Id                                           -- ^ Type to instantiate
-           -> TcM ([(Name, TcTyVar)], TcThetaType, TcType) -- ^ Result
-                -- (type vars, preds (incl equalities), rho)
-tcInstType inst_tyvars id =
-  do { let (tyvars, rho)    = splitForAllTys (idType id)
-           tyvars'          = mkTyVarBinders () tyvars
-     ;     (tv_prs, preds, rho) <- tc_inst_internal inst_tyvar_bndrs tyvars' rho
-     ; let tv_prs'          = map (\(name, bndr) -> (name, binderVar bndr)) tv_prs
-     ; return (tv_prs', preds, rho) }
-  where
-    inst_tyvar_bndrs :: [VarBndr TyVar ()] -> TcM (TCvSubst, [VarBndr TcTyVar ()])
-    inst_tyvar_bndrs bndrs = do { (subst, tvs) <- inst_tyvars $ binderVars bndrs
-                                ; let tvbnds = map (\tv -> Bndr tv ()) tvs
-                                ; return (subst, tvbnds) }
-
-tcInstTypeBndrs :: ([VarBndr TyVar Specificity] -> TcM (TCvSubst, [VarBndr TcTyVar Specificity]))
-                        -- ^ How to instantiate the type variables
-                -> Id                                                               -- ^ Type to instantiate
-                -> TcM ([(Name, VarBndr TcTyVar Specificity)], TcThetaType, TcType) -- ^ Result
-                     -- (type vars, preds (incl equalities), rho)
-tcInstTypeBndrs inst_tyvars id =
-  let (tyvars, rho) = splitForAllTysInvis (idType id)
-  in tc_inst_internal inst_tyvars tyvars rho
-
-tcSkolDFunType :: DFunId -> TcM ([TcTyVar], TcThetaType, TcType)
--- Instantiate a type signature with skolem constants.
--- We could give them fresh names, but no need to do so
-tcSkolDFunType dfun
-  = do { (tv_prs, theta, tau) <- tcInstType tcInstSuperSkolTyVars dfun
-       ; return (map snd tv_prs, theta, tau) }
-
-tcSuperSkolTyVars :: [TyVar] -> (TCvSubst, [TcTyVar])
--- Make skolem constants, but do *not* give them new names, as above
--- Moreover, make them "super skolems"; see comments with superSkolemTv
--- see Note [Kind substitution when instantiating]
--- Precondition: tyvars should be ordered by scoping
-tcSuperSkolTyVars = mapAccumL tcSuperSkolTyVar emptyTCvSubst
-
-tcSuperSkolTyVar :: TCvSubst -> TyVar -> (TCvSubst, TcTyVar)
-tcSuperSkolTyVar subst tv
-  = (extendTvSubstWithClone subst tv new_tv, new_tv)
-  where
-    kind   = substTyUnchecked subst (tyVarKind tv)
-    new_tv = mkTcTyVar (tyVarName tv) kind superSkolemTv
-
--- | Given a list of @['TyVar']@, skolemize the type variables,
--- returning a substitution mapping the original tyvars to the
--- skolems, and the list of newly bound skolems.
-tcInstSkolTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
--- See Note [Skolemising type variables]
-tcInstSkolTyVars = tcInstSkolTyVarsX emptyTCvSubst
-
-tcInstSkolTyVarsX :: TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
--- See Note [Skolemising type variables]
-tcInstSkolTyVarsX = tcInstSkolTyVarsPushLevel False
-
-tcInstSuperSkolTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
--- See Note [Skolemising type variables]
-tcInstSuperSkolTyVars = tcInstSuperSkolTyVarsX emptyTCvSubst
-
-tcInstSuperSkolTyVarsX :: TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
--- See Note [Skolemising type variables]
-tcInstSuperSkolTyVarsX subst = tcInstSkolTyVarsPushLevel True subst
-
-tcInstSkolTyVarsPushLevel :: Bool -> TCvSubst -> [TyVar]
-                          -> TcM (TCvSubst, [TcTyVar])
--- Skolemise one level deeper, hence pushTcLevel
--- See Note [Skolemising type variables]
-tcInstSkolTyVarsPushLevel overlappable subst tvs
-  = do { tc_lvl <- getTcLevel
-       ; let pushed_lvl = pushTcLevel tc_lvl
-       ; tcInstSkolTyVarsAt pushed_lvl overlappable subst tvs }
-
-tcInstSkolTyVarsAt :: TcLevel -> Bool
-                   -> TCvSubst -> [TyVar]
-                   -> TcM (TCvSubst, [TcTyVar])
-tcInstSkolTyVarsAt lvl overlappable subst tvs
-  = freshenTyCoVarsX new_skol_tv subst tvs
+ensureMonoType :: TcType -> TcM ()
+-- Assuming that the argument type is of kind (TYPE r),
+-- ensure that it is a /monotype/
+-- If it is not a monotype we can see right away (since unification
+-- varibles and type-function applications stand for monotypes), but
+-- we emit a Wanted equality just to delay the error message until later
+ensureMonoType res_ty
+  | isTauTy res_ty   -- isTauTy doesn't need zonking or anything
+  = return ()
+  | otherwise
+  = do { mono_ty <- newOpenFlexiTyVarTy
+       ; let eq_orig = TypeEqOrigin { uo_actual   = res_ty
+                                    , uo_expected = mono_ty
+                                    , uo_thing    = Nothing
+                                    , uo_visible  = False }
+
+       ; _co <- emitWantedEq eq_orig TypeLevel Nominal res_ty mono_ty
+       ; return () }
+
+promoteTcType :: TcLevel -> TcType -> TcM (TcCoercionN, TcType)
+-- See Note [Promoting a type]
+-- See also Note [fillInferResult]
+-- 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
+--
+-- NB: we expect that 'ty' has already kind (TYPE rr) for
+--     some rr::RuntimeRep.  It is, after all, the type of a term.
+promoteTcType dest_lvl ty
+  = do { cur_lvl <- getTcLevel
+       ; if (cur_lvl `sameDepthAs` dest_lvl)
+         then return (mkTcNomReflCo ty, ty)
+         else promote_it }
   where
-    details = SkolemTv lvl overlappable
-    new_skol_tv name kind = mkTcTyVar name kind details
-
-------------------
-freshenTyVarBndrs :: [TyVar] -> TcM (TCvSubst, [TyVar])
--- ^ Give fresh uniques to a bunch of TyVars, but they stay
---   as TyVars, rather than becoming TcTyVars
--- Used in 'GHC.Tc.Instance.Family.newFamInst', and 'GHC.Tc.Utils.Instantiate.newClsInst'
-freshenTyVarBndrs = freshenTyCoVars mkTyVar
-
-freshenCoVarBndrsX :: TCvSubst -> [CoVar] -> TcM (TCvSubst, [CoVar])
--- ^ Give fresh uniques to a bunch of CoVars
--- Used in "GHC.Tc.Instance.Family.newFamInst"
-freshenCoVarBndrsX subst = freshenTyCoVarsX mkCoVar subst
-
-------------------
-freshenTyCoVars :: (Name -> Kind -> TyCoVar)
-                -> [TyVar] -> TcM (TCvSubst, [TyCoVar])
-freshenTyCoVars mk_tcv = freshenTyCoVarsX mk_tcv emptyTCvSubst
-
-freshenTyCoVarsX :: (Name -> Kind -> TyCoVar)
-                 -> TCvSubst -> [TyCoVar]
-                 -> TcM (TCvSubst, [TyCoVar])
-freshenTyCoVarsX mk_tcv = mapAccumLM (freshenTyCoVarX mk_tcv)
-
-freshenTyCoVarX :: (Name -> Kind -> TyCoVar)
-                -> TCvSubst -> TyCoVar -> TcM (TCvSubst, TyCoVar)
--- This a complete freshening operation:
--- the skolems have a fresh unique, and a location from the monad
--- See Note [Skolemising type variables]
-freshenTyCoVarX mk_tcv subst tycovar
-  = do { loc  <- getSrcSpanM
-       ; uniq <- newUnique
-       ; let old_name = tyVarName tycovar
-             new_name = mkInternalName uniq (getOccName old_name) loc
-             new_kind = substTyUnchecked subst (tyVarKind tycovar)
-             new_tcv  = mk_tcv new_name new_kind
-             subst1   = extendTCvSubstWithClone subst tycovar new_tcv
-       ; return (subst1, new_tcv) }
-
-{- Note [Skolemising type variables]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-The tcInstSkolTyVars family of functions instantiate a list of TyVars
-to fresh skolem TcTyVars. Important notes:
-
-a) Level allocation. We generally skolemise /before/ calling
-   pushLevelAndCaptureConstraints.  So we want their level to the level
-   of the soon-to-be-created implication, which has a level ONE HIGHER
-   than the current level.  Hence the pushTcLevel.  It feels like a
-   slight hack.
-
-b) The [TyVar] should be ordered (kind vars first)
-   See Note [Kind substitution when instantiating]
-
-c) It's a complete freshening operation: the skolems have a fresh
-   unique, and a location from the monad
-
-d) The resulting skolems are
-        non-overlappable for tcInstSkolTyVars,
-   but overlappable for tcInstSuperSkolTyVars
-   See GHC.Tc.Deriv.Infer Note [Overlap and deriving] for an example
-   of where this matters.
-
-Note [Kind substitution when instantiating]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-When we instantiate a bunch of kind and type variables, first we
-expect them to be topologically sorted.
-Then we have to instantiate the kind variables, build a substitution
-from old variables to the new variables, then instantiate the type
-variables substituting the original kind.
-
-Exemple: If we want to instantiate
-  [(k1 :: *), (k2 :: *), (a :: k1 -> k2), (b :: k1)]
-we want
-  [(?k1 :: *), (?k2 :: *), (?a :: ?k1 -> ?k2), (?b :: ?k1)]
-instead of the buggous
-  [(?k1 :: *), (?k2 :: *), (?a :: k1 -> k2), (?b :: k1)]
+    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) }
+
+{- Note [Promoting a type]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider (#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.
+-}
 
 
-************************************************************************
+{- *********************************************************************
 *                                                                      *
         MetaTvs (meta type variables; mutable)
 *                                                                      *
-************************************************************************
--}
+********************************************************************* -}
 
-{-
-Note [TyVarTv]
-~~~~~~~~~~~~
+{- Note [TyVarTv]
+~~~~~~~~~~~~~~~~~
 
 A TyVarTv can unify with type *variables* only, including other TyVarTvs and
 skolems. Sometimes, they can unify with type variables that the user would
@@ -1031,18 +1097,11 @@ newMetaTyVarsX subst = mapAccumLM newMetaTyVarX subst
 newMetaTyVarX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
 -- Make a new unification variable tyvar whose Name and Kind come from
 -- an existing TyVar. We substitute kind variables in the kind.
-newMetaTyVarX subst tyvar = new_meta_tv_x TauTv subst tyvar
-
-newMetaTyVarTyVars :: [VarBndr TyVar Specificity]
-                   -> TcM (TCvSubst, [VarBndr TcTyVar Specificity])
-newMetaTyVarTyVars = mapAccumLM newMetaTyVarTyVarX emptyTCvSubst
+newMetaTyVarX = new_meta_tv_x TauTv
 
-newMetaTyVarTyVarX :: TCvSubst -> (VarBndr TyVar Specificity)
-                   -> TcM (TCvSubst, VarBndr TcTyVar Specificity)
+newMetaTyVarTyVarX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
 -- Just like newMetaTyVarX, but make a TyVarTv
-newMetaTyVarTyVarX subst (Bndr tv spec) =
-  do { (subst', tv') <- new_meta_tv_x TyVarTv subst tv
-     ; return (subst', (Bndr tv' spec)) }
+newMetaTyVarTyVarX = new_meta_tv_x TyVarTv
 
 newWildCardX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
 newWildCardX subst tv
diff --git a/compiler/GHC/Tc/Utils/TcType.hs b/compiler/GHC/Tc/Utils/TcType.hs
index 280144ac00..6b0df55f46 100644
--- a/compiler/GHC/Tc/Utils/TcType.hs
+++ b/compiler/GHC/Tc/Utils/TcType.hs
@@ -57,7 +57,7 @@ module GHC.Tc.Utils.TcType (
   -- These are important because they do not look through newtypes
   getTyVar,
   tcSplitForAllTy_maybe,
-  tcSplitForAllTys, tcSplitSomeForAllTys,
+  tcSplitForAllTys,
   tcSplitForAllTysReq, tcSplitForAllTysInvis,
   tcSplitPiTys, tcSplitPiTy_maybe, tcSplitForAllVarBndrs,
   tcSplitPhiTy, tcSplitPredFunTy_maybe,
@@ -1221,14 +1221,6 @@ tcSplitForAllTys ty
   = ASSERT( all isTyVar (fst sty) ) sty
   where sty = splitForAllTys ty
 
--- | Like 'tcSplitForAllTys', but only splits a 'ForAllTy' if @argf_pred argf@
--- is 'True', where @argf@ is the visibility of the @ForAllTy@'s binder and
--- @argf_pred@ is a predicate over visibilities provided as an argument to this
--- function. All split tyvars are annotated with their @argf@.
-tcSplitSomeForAllTys :: (ArgFlag -> Bool) -> Type -> ([TyCoVarBinder], Type)
-tcSplitSomeForAllTys argf_pred ty = ASSERT( all (isTyVar . binderVar) (fst sty) ) sty
-  where sty = splitSomeForAllTys argf_pred ty
-
 -- | Like 'tcSplitForAllTys', but only splits 'ForAllTy's with 'Required' type
 -- variable binders. All split tyvars are annotated with '()'.
 tcSplitForAllTysReq :: Type -> ([TcReqTVBinder], Type)
diff --git a/compiler/GHC/Tc/Utils/Unify.hs b/compiler/GHC/Tc/Utils/Unify.hs
index 5d7afcf057..145520045b 100644
--- a/compiler/GHC/Tc/Utils/Unify.hs
+++ b/compiler/GHC/Tc/Utils/Unify.hs
@@ -61,7 +61,6 @@ import GHC.Types.Name( isSystemName )
 import GHC.Tc.Utils.Instantiate
 import GHC.Core.TyCon
 import GHC.Builtin.Types
-import GHC.Builtin.Types.Prim( tYPE )
 import GHC.Types.Var as Var
 import GHC.Types.Var.Set
 import GHC.Types.Var.Env
@@ -571,10 +570,51 @@ tcSubTypeNC :: CtOrigin       -- Used when instantiating
             -> TcM HsWrapper
 tcSubTypeNC inst_orig ctxt m_thing ty_actual res_ty
   = case res_ty of
-      Infer inf_res     -> instantiateAndFillInferResult inst_orig ty_actual inf_res
       Check ty_expected -> tc_sub_type (unifyType m_thing) inst_orig ctxt
                                        ty_actual ty_expected
 
+      Infer inf_res -> do { (wrap, rho) <- topInstantiate inst_orig ty_actual
+                                   -- See Note [Instantiation of InferResult]
+                          ; co <- fillInferResult rho inf_res
+                          ; return (mkWpCastN co <.> wrap) }
+
+{- Note [Instantiation of InferResult]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We now always instantiate before filling in InferResult, so that
+the result is a TcRhoType: see #17173 for discussion.
+
+For example:
+
+1. 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.
+
+2. 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.
+
+3. Suppose one defines plus = (+). If we instantiate lazily, we will
+   infer plus :: forall a. Num a => a -> a -> a. However, the monomorphism
+   restriction compels us to infer
+      plus :: Integer -> Integer -> Integer
+   (or similar monotype). Indeed, the only way to know whether to apply
+   the monomorphism restriction at all is to instantiate
+
+There is one place where we don't want to instantiate eagerly,
+namely in GHC.Tc.Module.tcRnExpr, which implements GHCi's :type
+command. See Note [Implementing :type] in GHC.Tc.Module.
+-}
+
 ---------------
 tcSubTypeSigma :: UserTypeCtxt -> TcSigmaType -> TcSigmaType -> TcM HsWrapper
 -- External entry point, but no ExpTypes on either side
@@ -768,213 +808,6 @@ tcEqMult origin w_actual w_expected = do
   ; coercion <- uType TypeLevel origin w_actual w_expected
   ; return $ if isReflCo coercion then WpHole else WpMultCoercion coercion }
 
-{- **********************************************************************
-%*                                                                      *
-            ExpType functions: tcInfer, instantiateAndFillInferResult
-%*                                                                      *
-%********************************************************************* -}
-
--- | Infer a type using a fresh ExpType
--- See also Note [ExpType] in "GHC.Tc.Utils.TcMType"
-tcInfer :: (ExpSigmaType -> TcM a) -> TcM (a, TcSigmaType)
-tcInfer tc_check
-  = do { res_ty <- newInferExpType
-       ; result <- tc_check res_ty
-       ; res_ty <- readExpType res_ty
-       ; return (result, res_ty) }
-
-instantiateAndFillInferResult :: CtOrigin -> TcType -> InferResult -> TcM HsWrapper
--- If wrap = instantiateAndFillInferResult t1 t2
---    => wrap :: t1 ~> t2
--- See Note [Instantiation of InferResult]
-instantiateAndFillInferResult orig ty inf_res
-  = do { (wrap, rho) <- topInstantiate orig ty
-       ; co <- fillInferResult rho inf_res
-       ; return (mkWpCastN co <.> wrap) }
-
-fillInferResult :: TcType -> InferResult -> TcM TcCoercionN
--- If wrap = fillInferResult t1 t2
---    => wrap :: t1 ~> t2
-fillInferResult 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 [Instantiation of InferResult]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-We now always instantiate before filling in InferResult, so that
-the result is a TcRhoType: see #17173 for discussion.
-
-For example:
-
-1. 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.
-
-2. 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.
-
-3. Suppose one defines plus = (+). If we instantiate lazily, we will
-   infer plus :: forall a. Num a => a -> a -> a. However, the monomorphism
-   restriction compels us to infer
-      plus :: Integer -> Integer -> Integer
-   (or similar monotype). Indeed, the only way to know whether to apply
-   the monomorphism restriction at all is to instantiate
-
-There is one place where we don't want to instantiate eagerly,
-namely in GHC.Tc.Module.tcRnExpr, which implements GHCi's :type
-command. See Note [Implementing :type] in GHC.Tc.Module.
-
--}
-
-{- *********************************************************************
-*                                                                      *
-              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 (#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.
--}
 
 {- *********************************************************************
 *                                                                      *
diff --git a/testsuite/tests/simplCore/should_compile/T17901.stdout b/testsuite/tests/simplCore/should_compile/T17901.stdout
index 99969cc0c1..7a09f6e2df 100644
--- a/testsuite/tests/simplCore/should_compile/T17901.stdout
+++ b/testsuite/tests/simplCore/should_compile/T17901.stdout
@@ -1,14 +1,14 @@
-                 (wombat1 [Occ=Once*!] :: T -> p)
+                 (wombat1 [Occ=Once*!] :: T -> t)
                    A -> wombat1 T17901.A;
                    B -> wombat1 T17901.B;
                    C -> wombat1 T17901.C
-  = \ (@p) (wombat1 :: T -> p) (x :: T) ->
+  = \ (@t) (wombat1 :: T -> t) (x :: T) ->
       case x of wild { __DEFAULT -> wombat1 wild }
-         Tmpl= \ (@p) (wombat2 [Occ=Once!] :: S -> p) (x [Occ=Once] :: S) ->
+         Tmpl= \ (@t) (wombat2 [Occ=Once!] :: S -> t) (x [Occ=Once] :: S) ->
                  case x of wild [Occ=Once] { __DEFAULT -> wombat2 wild }}]
-  = \ (@p) (wombat2 :: S -> p) (x :: S) ->
+  = \ (@t) (wombat2 :: S -> t) (x :: S) ->
       case x of wild { __DEFAULT -> wombat2 wild }
-         Tmpl= \ (@p) (wombat3 [Occ=Once!] :: W -> p) (x [Occ=Once] :: W) ->
+         Tmpl= \ (@t) (wombat3 [Occ=Once!] :: W -> t) (x [Occ=Once] :: W) ->
                  case x of wild [Occ=Once] { __DEFAULT -> wombat3 wild }}]
-  = \ (@p) (wombat3 :: W -> p) (x :: W) ->
+  = \ (@t) (wombat3 :: W -> t) (x :: W) ->
       case x of wild { __DEFAULT -> wombat3 wild }
diff --git a/testsuite/tests/typecheck/should_compile/T18412.hs b/testsuite/tests/typecheck/should_compile/T18412.hs
new file mode 100644
index 0000000000..67fc5cc1db
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T18412.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE RankNTypes #-}
+
+module T18412 where
+
+hr :: (forall a. a -> a) -> ()
+hr _ = ()
+
+foo x = case x of () -> hr
+
+-- This did not use to be allowed, because the
+-- multiple branches have (the same) polytypes
+-- Enhancement July 2020
+bar x = case x of True -> hr
+                  False -> hr
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 1ace8dbc15..82a30f50f4 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -716,3 +716,4 @@ test('T17775-viewpats-a', normal, compile, [''])
 test('T17775-viewpats-b', normal, compile_fail, [''])
 test('T17775-viewpats-c', normal, compile_fail, [''])
 test('T17775-viewpats-d', normal, compile_fail, [''])
+test('T18412', normal, compile, [''])
diff --git a/testsuite/tests/typecheck/should_fail/T10619.stderr b/testsuite/tests/typecheck/should_fail/T10619.stderr
index 481a08a20c..c26e550f17 100644
--- a/testsuite/tests/typecheck/should_fail/T10619.stderr
+++ b/testsuite/tests/typecheck/should_fail/T10619.stderr
@@ -1,13 +1,11 @@
 
-T10619.hs:9:15: error:
-    • Couldn't match type ‘p’ with ‘forall b. b -> b’
-      Expected: p -> p
-        Actual: (forall a. a -> a) -> forall b. b -> b
-      ‘p’ is a rigid type variable bound by
-        the inferred type of foo :: p1 -> p -> p
-        at T10619.hs:(8,1)-(10,20)
-    • In the expression:
-          (\ x -> x) :: (forall a. a -> a) -> forall b. b -> b
+T10619.hs:10:14: error:
+    • Couldn't match type ‘p1’ with ‘forall a. a -> a’
+      Expected: (forall a. a -> a) -> forall b. b -> b
+        Actual: p1 -> p1
+      Cannot instantiate unification variable ‘p1’
+      with a type involving polytypes: forall a. a -> a
+    • In the expression: \ y -> y
       In the expression:
         if True then
             ((\ x -> x) :: (forall a. a -> a) -> forall b. b -> b)
@@ -19,15 +17,13 @@ T10619.hs:9:15: error:
                   ((\ x -> x) :: (forall a. a -> a) -> forall b. b -> b)
               else
                   \ y -> y
-    • Relevant bindings include
-        foo :: p1 -> p -> p (bound at T10619.hs:8:1)
 
 T10619.hs:14:15: error:
     • Couldn't match type ‘p’ with ‘forall a. a -> a’
       Expected: p -> p
         Actual: (forall a. a -> a) -> forall b. b -> b
       ‘p’ is a rigid type variable bound by
-        the inferred type of bar :: p1 -> p -> p
+        the inferred type of bar :: p2 -> p -> p
         at T10619.hs:(12,1)-(14,66)
     • In the expression:
           (\ x -> x) :: (forall a. a -> a) -> forall b. b -> b
@@ -43,21 +39,16 @@ T10619.hs:14:15: error:
               else
                   ((\ x -> x) :: (forall a. a -> a) -> forall b. b -> b)
     • Relevant bindings include
-        bar :: p1 -> p -> p (bound at T10619.hs:12:1)
+        bar :: p2 -> p -> p (bound at T10619.hs:12:1)
 
-T10619.hs:16:13: error:
-    • Couldn't match type ‘p’ with ‘forall b. b -> b’
-      Expected: p -> p
-        Actual: (forall a. a -> a) -> forall b. b -> b
-      ‘p’ is a rigid type variable bound by
-        the inferred type of baz :: Bool -> p -> p
-        at T10619.hs:(16,1)-(17,19)
-    • In the expression:
-          (\ x -> x) :: (forall a. a -> a) -> forall b. b -> b
-      In an equation for ‘baz’:
-          baz True = (\ x -> x) :: (forall a. a -> a) -> forall b. b -> b
-    • Relevant bindings include
-        baz :: Bool -> p -> p (bound at T10619.hs:16:1)
+T10619.hs:17:13: error:
+    • Couldn't match type ‘p0’ with ‘forall a. a -> a’
+      Expected: (forall a. a -> a) -> forall b. b -> b
+        Actual: p0 -> p0
+      Cannot instantiate unification variable ‘p0’
+      with a type involving polytypes: forall a. a -> a
+    • In the expression: \ y -> y
+      In an equation for ‘baz’: baz False = \ y -> y
 
 T10619.hs:20:14: error:
     • Couldn't match type ‘p’ with ‘forall a. a -> a’
diff --git a/testsuite/tests/typecheck/should_fail/VtaFail.stderr b/testsuite/tests/typecheck/should_fail/VtaFail.stderr
index 87a2bea3fe..1b496b8380 100644
--- a/testsuite/tests/typecheck/should_fail/VtaFail.stderr
+++ b/testsuite/tests/typecheck/should_fail/VtaFail.stderr
@@ -7,7 +7,7 @@ VtaFail.hs:7:16: error:
           answer_nosig = pairup_nosig @Int @Bool 5 True
 
 VtaFail.hs:14:17: error:
-    • Cannot apply expression of type ‘p0 -> p0’
+    • Cannot apply expression of type ‘p1 -> p1’
       to a visible type argument ‘Int’
     • In the expression: (\ x -> x) @Int 12
       In an equation for ‘answer_lambda’:
diff --git a/testsuite/tests/typecheck/should_fail/tcfail002.stderr b/testsuite/tests/typecheck/should_fail/tcfail002.stderr
index 664c910533..7de2d04c08 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail002.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail002.stderr
@@ -1,8 +1,8 @@
 
 tcfail002.hs:4:7: error:
-    • Couldn't match expected type ‘p’ with actual type ‘[p]’
+    • Couldn't match expected type ‘a’ with actual type ‘[a]’
     • In the expression: z
       In an equation for ‘c’: c z = z
     • Relevant bindings include
-        z :: [p] (bound at tcfail002.hs:4:3)
-        c :: [p] -> p (bound at tcfail002.hs:3:1)
+        z :: [a] (bound at tcfail002.hs:4:3)
+        c :: [a] -> a (bound at tcfail002.hs:3:1)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail104.stderr b/testsuite/tests/typecheck/should_fail/tcfail104.stderr
index 9844b53268..0d9b338216 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail104.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail104.stderr
@@ -1,19 +1,22 @@
 
-tcfail104.hs:14:12: error:
+tcfail104.hs:16:12: error:
+    • Couldn't match type: Char -> Char
+                     with: forall a. a -> a
+      Expected: (forall a. a -> a) -> Char -> Char
+        Actual: (Char -> Char) -> Char -> Char
+    • In the expression: \ x -> x
+      In the expression:
+        if v then (\ (x :: forall a. a -> a) -> x) else (\ x -> x)
+      In the expression:
+        (if v then (\ (x :: forall a. a -> a) -> x) else (\ x -> x)) id 'c'
+
+tcfail104.hs:22:12: error:
     • Couldn't match type: forall a. a -> a
                      with: Char -> Char
       Expected: (Char -> Char) -> Char -> Char
         Actual: (forall a. a -> a) -> Char -> Char
     • In the expression: \ (x :: forall a. a -> a) -> x
       In the expression:
-        if v then (\ (x :: forall a. a -> a) -> x) else (\ x -> x)
+        if v then (\ x -> x) else (\ (x :: forall a. a -> a) -> x)
       In the expression:
-        (if v then (\ (x :: forall a. a -> a) -> x) else (\ x -> x)) id 'c'
-
-tcfail104.hs:22:15: error:
-    • Couldn't match expected type: Char -> Char
-                  with actual type: forall a. a -> a
-    • When checking that the pattern signature: forall a. a -> a
-        fits the type of its context: Char -> Char
-      In the pattern: x :: forall a. a -> a
-      In the expression: \ (x :: forall a. a -> a) -> x
+        (if v then (\ x -> x) else (\ (x :: forall a. a -> a) -> x)) id 'c'