Treat isConstraintKind more consistently
[ghc.git] / compiler / typecheck / TcMType.hs
index a9c608d..873b50b 100644 (file)
@@ -9,7 +9,7 @@ This module contains monadic operations over types that contain
 mutable type variables
 -}
 
-{-# LANGUAGE CPP #-}
+{-# LANGUAGE CPP, TupleSections, MultiWayIf #-}
 
 module TcMType (
   TcTyVar, TcKind, TcType, TcTauType, TcThetaType, TcTyVarSet,
@@ -19,69 +19,110 @@ module TcMType (
   newFlexiTyVar,
   newFlexiTyVarTy,              -- Kind -> TcM TcType
   newFlexiTyVarTys,             -- Int -> Kind -> TcM [TcType]
-  newReturnTyVar, newReturnTyVarTy,
-  newMetaKindVar, newMetaKindVars,
-  mkTcTyVarName, cloneMetaTyVar,
+  newOpenFlexiTyVarTy, newOpenTypeKind,
+  newMetaKindVar, newMetaKindVars, newMetaTyVarTyAtLevel,
+  cloneMetaTyVar,
+  newFmvTyVar, newFskTyVar,
 
-  newMetaTyVar, readMetaTyVar, writeMetaTyVar, writeMetaTyVarRef,
+  readMetaTyVar, writeMetaTyVar,
   newMetaDetails, isFilledMetaTyVar, isUnfilledMetaTyVar,
 
   --------------------------------
+  -- Expected types
+  ExpType(..), ExpSigmaType, ExpRhoType,
+  mkCheckExpType,
+  newInferExpType, newInferExpTypeInst, newInferExpTypeNoInst,
+  readExpType, readExpType_maybe,
+  expTypeToType, checkingExpType_maybe, checkingExpType,
+  tauifyExpType, inferResultToType,
+
+  --------------------------------
   -- Creating new evidence variables
-  newEvVar, newEvVars, newEq, newDict,
-  newTcEvBinds, addTcEvBind,
+  newEvVar, newEvVars, newDict,
+  newWanted, newWanteds, cloneWanted, cloneSimple, cloneWC,
+  emitWanted, emitWantedEq, emitWantedEvVar, emitWantedEvVars,
+  newTcEvBinds, newNoTcEvBinds, addTcEvBind,
+
+  newCoercionHole, fillCoercionHole, isFilledCoercionHole,
+  unpackCoercionHole, unpackCoercionHole_maybe,
+  checkCoercionHole,
 
   --------------------------------
   -- Instantiation
-  tcInstTyVars, tcInstTyVarX, newSigTyVar, newSigKindVar,
+  newMetaTyVars, newMetaTyVarX, newMetaTyVarsX,
+  newMetaSigTyVars, newMetaSigTyVarX,
+  newSigTyVar, newSkolemTyVar, newWildCardX,
   tcInstType,
-  tcInstSkolTyVars, tcInstSuperSkolTyVarsX,
-  tcInstSigTyVarsLoc, tcInstSigTyVars,
-  tcInstSkolType,
+  tcInstSkolTyVars,tcInstSkolTyVarsX,
+  tcInstSuperSkolTyVarsX,
   tcSkolDFunType, tcSuperSkolTyVars,
 
-  instSkolTyVars, freshenTyVarBndrs,
+  instSkolTyCoVarsX, freshenTyVarBndrs, freshenCoVarBndrsX,
 
   --------------------------------
   -- Zonking and tidying
-  zonkTcPredType, zonkTidyTcType, zonkTidyOrigin,
+  zonkTidyTcType, zonkTidyTcTypes, zonkTidyOrigin,
   tidyEvVar, tidyCt, tidySkolemInfo,
-  skolemiseUnboundMetaTyVar,
-  zonkTcTyVar, zonkTcTyVars, zonkTyVarsAndFV, zonkTcTypeAndFV,
-  zonkQuantifiedTyVar, quantifyTyVars,
-  zonkTcTyVarBndr, zonkTcType, zonkTcTypes, zonkTcThetaType,
-
-  zonkTcKind, defaultKindVarToStar,
-  zonkEvVar, zonkWC, zonkSimples, zonkId, zonkCt, zonkSkolemInfo,
-
-  tcGetGlobalTyVars
+  skolemiseRuntimeUnk,
+  zonkTcTyVar, zonkTcTyVars,
+  zonkTcTyVarToTyVar, zonkSigTyVarPairs,
+  zonkTyCoVarsAndFV, zonkTcTypeAndFV,
+  zonkTyCoVarsAndFVList,
+  zonkTcTypeAndSplitDepVars, zonkTcTypesAndSplitDepVars,
+  zonkQuantifiedTyVar, defaultTyVar,
+  quantifyTyVars,
+  zonkTcTyCoVarBndr, zonkTcTyVarBinder,
+  zonkTcType, zonkTcTypes, zonkCo,
+  zonkTyCoVarKind, zonkTcTypeMapper,
+  zonkTcTypeInKnot,
+
+  zonkEvVar, zonkWC, zonkSimples,
+  zonkId, zonkCoVar,
+  zonkCt, zonkSkolemInfo,
+
+  tcGetGlobalTyCoVars,
+
+  ------------------------------
+  -- Levity polymorphism
+  ensureNotLevPoly, checkForLevPoly, checkForLevPolyX, formatLevPolyErr
   ) where
 
 #include "HsVersions.h"
 
 -- friends:
-import TypeRep
+import GhcPrelude
+
+import TyCoRep
 import TcType
 import Type
+import Coercion
 import Class
 import Var
-import VarEnv
 
 -- others:
 import TcRnMonad        -- TcType, amongst others
+import TcEvidence
 import Id
 import Name
 import VarSet
+import TysWiredIn
+import TysPrim
+import VarEnv
+import NameEnv
 import PrelNames
-import DynFlags
 import Util
 import Outputable
 import FastString
 import SrcLoc
 import Bag
+import Pair
+import UniqSet
+import qualified GHC.LanguageExtensions as LangExt
 
 import Control.Monad
-import Data.List        ( partition, mapAccumL )
+import Maybes
+import Data.List        ( mapAccumL )
+import Control.Arrow    ( second )
 
 {-
 ************************************************************************
@@ -101,7 +142,8 @@ kind_var_occ = mkOccName tvName "k"
 newMetaKindVar :: TcM TcKind
 newMetaKindVar = do { uniq <- newUnique
                     ; details <- newMetaDetails TauTv
-                    ; let kv = mkTcTyVar (mkKindName uniq) superKind details
+                    ; let kv = mkTcTyVar (mkKindName uniq) liftedTypeKind details
+                    ; traceTc "newMetaKindVar" (ppr kv)
                     ; return (mkTyVarTy kv) }
 
 newMetaKindVars :: Int -> TcM [TcKind]
@@ -120,15 +162,78 @@ newEvVars theta = mapM newEvVar theta
 
 --------------
 
-newEvVar :: TcPredType -> TcM EvVar
+newEvVar :: TcPredType -> TcRnIf gbl lcl EvVar
 -- Creates new *rigid* variables for predicates
 newEvVar ty = do { name <- newSysName (predTypeOccName ty)
-                 ; return (mkLocalId name ty) }
+                 ; return (mkLocalIdOrCoVar name ty) }
+
+newWanted :: CtOrigin -> Maybe TypeOrKind -> PredType -> TcM CtEvidence
+-- Deals with both equality and non-equality predicates
+newWanted orig t_or_k pty
+  = do loc <- getCtLocM orig t_or_k
+       d <- if isEqPred pty then HoleDest  <$> newCoercionHole pty
+                            else EvVarDest <$> newEvVar pty
+       return $ CtWanted { ctev_dest = d
+                         , ctev_pred = pty
+                         , ctev_nosh = WDeriv
+                         , ctev_loc = loc }
+
+newWanteds :: CtOrigin -> ThetaType -> TcM [CtEvidence]
+newWanteds orig = mapM (newWanted orig Nothing)
+
+cloneWanted :: Ct -> TcM CtEvidence
+cloneWanted ct
+  = newWanted (ctEvOrigin ev) Nothing (ctEvPred ev)
+  where
+    ev = ctEvidence ct
 
-newEq :: TcType -> TcType -> TcM EvVar
-newEq ty1 ty2
-  = do { name <- newSysName (mkVarOccFS (fsLit "cobox"))
-       ; return (mkLocalId name (mkTcEqPred ty1 ty2)) }
+cloneSimple :: Ct -> TcM Ct
+cloneSimple = fmap mkNonCanonical . cloneWanted
+
+cloneWC :: WantedConstraints -> TcM WantedConstraints
+cloneWC wc@(WC { wc_simple = simples, wc_impl = implics })
+  = do { simples' <- mapBagM cloneSimple simples
+       ; implics' <- mapBagM clone_implic implics
+       ; return (wc { wc_simple = simples', wc_impl = implics' }) }
+  where
+    clone_implic implic@(Implic { ic_wanted = inner_wanted })
+      = do { inner_wanted' <- cloneWC inner_wanted
+           ; return (implic { ic_wanted = inner_wanted' }) }
+
+-- | Emits a new Wanted. Deals with both equalities and non-equalities.
+emitWanted :: CtOrigin -> TcPredType -> TcM EvTerm
+emitWanted origin pty
+  = do { ev <- newWanted origin Nothing pty
+       ; emitSimple $ mkNonCanonical ev
+       ; return $ ctEvTerm ev }
+
+-- | Emits a new equality constraint
+emitWantedEq :: CtOrigin -> TypeOrKind -> Role -> TcType -> TcType -> TcM Coercion
+emitWantedEq origin t_or_k role ty1 ty2
+  = do { hole <- newCoercionHole pty
+       ; loc <- getCtLocM origin (Just t_or_k)
+       ; emitSimple $ mkNonCanonical $
+         CtWanted { ctev_pred = pty, ctev_dest = HoleDest hole
+                  , ctev_nosh = WDeriv, ctev_loc = loc }
+       ; return (HoleCo hole) }
+  where
+    pty = mkPrimEqPredRole role ty1 ty2
+
+-- | Creates a new EvVar and immediately emits it as a Wanted.
+-- No equality predicates here.
+emitWantedEvVar :: CtOrigin -> TcPredType -> TcM EvVar
+emitWantedEvVar origin ty
+  = do { new_cv <- newEvVar ty
+       ; loc <- getCtLocM origin Nothing
+       ; let ctev = CtWanted { ctev_dest = EvVarDest new_cv
+                             , ctev_pred = ty
+                             , ctev_nosh = WDeriv
+                             , ctev_loc  = loc }
+       ; emitSimple $ mkNonCanonical ctev
+       ; return new_cv }
+
+emitWantedEvVars :: CtOrigin -> [TcPredType] -> TcM [EvVar]
+emitWantedEvVars orig = mapM (emitWantedEvVar orig)
 
 newDict :: Class -> [TcType] -> TcM DictId
 newDict cls tys
@@ -138,136 +243,362 @@ newDict cls tys
 predTypeOccName :: PredType -> OccName
 predTypeOccName ty = case classifyPredType ty of
     ClassPred cls _ -> mkDictOcc (getOccName cls)
-    EqPred _ _ _    -> mkVarOccFS (fsLit "cobox")
-    IrredPred     -> mkVarOccFS (fsLit "irred")
-
+    EqPred {}       -> mkVarOccFS (fsLit "co")
+    IrredPred {}    -> mkVarOccFS (fsLit "irred")
+    ForAllPred {}   -> mkVarOccFS (fsLit "df")
 
 {-
 ************************************************************************
 *                                                                      *
-        SkolemTvs (immutable)
+        Coercion holes
 *                                                                      *
 ************************************************************************
 -}
 
-tcInstType :: ([TyVar] -> TcM (TvSubst, [TcTyVar]))     -- How to instantiate the type variables
-           -> TcType                                    -- Type to instantiate
-           -> TcM ([TcTyVar], TcThetaType, TcType)      -- Result
-                -- (type vars (excl coercion vars), preds (incl equalities), rho)
-tcInstType inst_tyvars ty
-  = case tcSplitForAllTys ty of
-        ([],     rho) -> let    -- There may be overloading despite no type variables;
+newCoercionHole :: TcPredType -> TcM CoercionHole
+newCoercionHole pred_ty
+  = do { co_var <- newEvVar pred_ty
+       ; traceTc "New coercion hole:" (ppr co_var)
+       ; ref <- newMutVar Nothing
+       ; return $ CoercionHole { ch_co_var = co_var, ch_ref = ref } }
+
+-- | Put a value in a coercion hole
+fillCoercionHole :: CoercionHole -> Coercion -> TcM ()
+fillCoercionHole (CoercionHole { ch_ref = ref, ch_co_var = cv }) co
+  = do {
+#if defined(DEBUG)
+       ; cts <- readTcRef ref
+       ; whenIsJust cts $ \old_co ->
+         pprPanic "Filling a filled coercion hole" (ppr cv $$ ppr co $$ ppr old_co)
+#endif
+       ; traceTc "Filling coercion hole" (ppr cv <+> text ":=" <+> ppr co)
+       ; writeTcRef ref (Just co) }
+
+-- | Is a coercion hole filled in?
+isFilledCoercionHole :: CoercionHole -> TcM Bool
+isFilledCoercionHole (CoercionHole { ch_ref = ref }) = isJust <$> readTcRef ref
+
+-- | Retrieve the contents of a coercion hole. Panics if the hole
+-- is unfilled
+unpackCoercionHole :: CoercionHole -> TcM Coercion
+unpackCoercionHole hole
+  = do { contents <- unpackCoercionHole_maybe hole
+       ; case contents of
+           Just co -> return co
+           Nothing -> pprPanic "Unfilled coercion hole" (ppr hole) }
+
+-- | Retrieve the contents of a coercion hole, if it is filled
+unpackCoercionHole_maybe :: CoercionHole -> TcM (Maybe Coercion)
+unpackCoercionHole_maybe (CoercionHole { ch_ref = ref }) = readTcRef ref
+
+-- | Check that a coercion is appropriate for filling a hole. (The hole
+-- itself is needed only for printing. NB: This must be /lazy/ in the coercion,
+-- as it's used in TcHsSyn in the presence of knots.
+-- Always returns the checked coercion, but this return value is necessary
+-- so that the input coercion is forced only when the output is forced.
+checkCoercionHole :: CoVar -> Coercion -> TcM Coercion
+checkCoercionHole cv co
+  | debugIsOn
+  = do { cv_ty <- zonkTcType (varType cv)
+                  -- co is already zonked, but cv might not be
+       ; return $
+         ASSERT2( ok cv_ty
+                , (text "Bad coercion hole" <+>
+                   ppr cv <> colon <+> vcat [ ppr t1, ppr t2, ppr role
+                                            , ppr cv_ty ]) )
+         co }
+  | otherwise
+  = return co
+
+  where
+    (Pair t1 t2, role) = coercionKindRole co
+    ok cv_ty | EqPred cv_rel cv_t1 cv_t2 <- classifyPredType cv_ty
+             =  t1 `eqType` cv_t1
+             && t2 `eqType` cv_t2
+             && role == eqRelRole cv_rel
+             | otherwise
+             = False
+
+{-
+************************************************************************
+*
+    Expected types
+*
+************************************************************************
+
+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
+synthesis mode (that is, bidirectional type-checking). Previously, this
+was achieved by using ordinary unification variables, but we don't need
+or want that generality. (For example, #11397 was caused by doing the
+wrong thing with unification variables.) Instead, we observe that these
+holes should
+
+1. never be nested
+2. never appear as the type of a variable
+3. be used linearly (never be duplicated)
+
+By defining ExpType, separately from Type, we can achieve goals 1 and 2
+statically.
+
+See also [wiki:Typechecking]
+
+Note [TcLevel of ExpType]
+~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+
+  data G a where
+    MkG :: G Bool
+
+  foo MkG = True
+
+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 TcMatches.
+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.
+
+-}
+
+-- actual data definition is in TcType
+
+-- | Make an 'ExpType' suitable for inferring a type of kind * or #.
+newInferExpTypeNoInst :: TcM ExpSigmaType
+newInferExpTypeNoInst = newInferExpType False
+
+newInferExpTypeInst :: TcM ExpRhoType
+newInferExpTypeInst = newInferExpType True
+
+newInferExpType :: Bool -> TcM ExpType
+newInferExpType inst
+  = do { u <- newUnique
+       ; tclvl <- getTcLevel
+       ; traceTc "newOpenInferExpType" (ppr u <+> ppr inst <+> ppr tclvl)
+       ; ref <- newMutVar Nothing
+       ; return (Infer (IR { ir_uniq = u, ir_lvl = tclvl
+                           , ir_ref = ref, ir_inst = inst })) }
+
+-- | Extract a type out of an ExpType, if one exists. But one should always
+-- exist. Unless you're quite sure you know what you're doing.
+readExpType_maybe :: ExpType -> TcM (Maybe TcType)
+readExpType_maybe (Check ty)                   = return (Just ty)
+readExpType_maybe (Infer (IR { ir_ref = ref})) = readMutVar ref
+
+-- | Extract a type out of an ExpType. Otherwise, panics.
+readExpType :: ExpType -> TcM TcType
+readExpType exp_ty
+  = do { mb_ty <- readExpType_maybe exp_ty
+       ; case mb_ty of
+           Just ty -> return ty
+           Nothing -> pprPanic "Unknown expected type" (ppr exp_ty) }
+
+-- | Returns the expected type when in checking mode.
+checkingExpType_maybe :: ExpType -> Maybe TcType
+checkingExpType_maybe (Check ty) = Just ty
+checkingExpType_maybe _          = Nothing
+
+-- | Returns the expected type when in checking mode. Panics if in inference
+-- mode.
+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) }
+
+-- | Extracts the expected type if there is one, or generates a new
+-- TauTv if there isn't.
+expTypeToType :: ExpType -> TcM TcType
+expTypeToType (Check ty)      = return ty
+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)
+       ; traceTc "Forcing ExpType to be monomorphic:"
+                 (ppr u <+> text ":=" <+> ppr tau)
+       ; return tau }
+
+
+{- *********************************************************************
+*                                                                      *
+        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
+  = case tcSplitForAllTys (idType id) of
+        ([],    rho) -> let     -- There may be overloading despite no type variables;
                                 --      (?x :: Int) => Int -> Int
-                           (theta, tau) = tcSplitPhiTy rho
-                         in
-                         return ([], theta, tau)
+                                (theta, tau) = tcSplitPhiTy rho
+                            in
+                            return ([], theta, tau)
 
         (tyvars, rho) -> do { (subst, tyvars') <- inst_tyvars tyvars
-                            ; let (theta, tau) = tcSplitPhiTy (substTy subst rho)
-                            ; return (tyvars', theta, tau) }
+                            ; let (theta, tau) = tcSplitPhiTy (substTyAddInScope subst rho)
+                                  tv_prs       = map tyVarName tyvars `zip` tyvars'
+                            ; return (tv_prs, theta, tau) }
 
-tcSkolDFunType :: Type -> TcM ([TcTyVar], TcThetaType, TcType)
+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 ty = tcInstType tcInstSuperSkolTyVars ty
+tcSkolDFunType dfun
+  = do { (tv_prs, theta, tau) <- tcInstType tcInstSuperSkolTyVars dfun
+       ; return (map snd tv_prs, theta, tau) }
 
-tcSuperSkolTyVars :: [TyVar] -> (TvSubst, [TcTyVar])
+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 (kind vars first)
-tcSuperSkolTyVars = mapAccumL tcSuperSkolTyVar (mkTopTvSubst [])
+-- Precondition: tyvars should be ordered by scoping
+tcSuperSkolTyVars = mapAccumL tcSuperSkolTyVar emptyTCvSubst
 
-tcSuperSkolTyVar :: TvSubst -> TyVar -> (TvSubst, TcTyVar)
+tcSuperSkolTyVar :: TCvSubst -> TyVar -> (TCvSubst, TcTyVar)
 tcSuperSkolTyVar subst tv
-  = (extendTvSubst subst tv (mkTyVarTy new_tv), new_tv)
+  = (extendTvSubstWithClone subst tv new_tv, new_tv)
   where
-    kind   = substTy subst (tyVarKind tv)
+    kind   = substTyUnchecked subst (tyVarKind tv)
     new_tv = mkTcTyVar (tyVarName tv) kind superSkolemTv
 
-tcInstSkolTyVars :: [TyVar] -> TcM (TvSubst, [TcTyVar])
-tcInstSkolTyVars = tcInstSkolTyVars' False emptyTvSubst
+-- | 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.  See also
+-- tcInstSkolTyVars' for a precondition.  The resulting
+-- skolems are non-overlappable; see Note [Overlap and deriving]
+-- for an example where this matters.
+tcInstSkolTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
+tcInstSkolTyVars = tcInstSkolTyVarsX emptyTCvSubst
 
-tcInstSuperSkolTyVars :: [TyVar] -> TcM (TvSubst, [TcTyVar])
-tcInstSuperSkolTyVars = tcInstSuperSkolTyVarsX emptyTvSubst
+tcInstSkolTyVarsX :: TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
+tcInstSkolTyVarsX = tcInstSkolTyVars' False
 
-tcInstSuperSkolTyVarsX :: TvSubst -> [TyVar] -> TcM (TvSubst, [TcTyVar])
+tcInstSuperSkolTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
+tcInstSuperSkolTyVars = tcInstSuperSkolTyVarsX emptyTCvSubst
+
+tcInstSuperSkolTyVarsX :: TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
 tcInstSuperSkolTyVarsX subst = tcInstSkolTyVars' True subst
 
-tcInstSkolTyVars' :: Bool -> TvSubst -> [TyVar] -> TcM (TvSubst, [TcTyVar])
+tcInstSkolTyVars' :: Bool -> TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
 -- Precondition: tyvars should be ordered (kind vars first)
 -- see Note [Kind substitution when instantiating]
 -- Get the location from the monad; this is a complete freshening operation
 tcInstSkolTyVars' overlappable subst tvs
   = do { loc <- getSrcSpanM
-       ; instSkolTyVarsX (mkTcSkolTyVar loc overlappable) subst tvs }
-
-mkTcSkolTyVar :: SrcSpan -> Bool -> Unique -> Name -> Kind -> TcTyVar
-mkTcSkolTyVar loc overlappable uniq old_name kind
-  = mkTcTyVar (mkInternalName uniq (getOccName old_name) loc)
-              kind
-              (SkolemTv overlappable)
-
-tcInstSigTyVarsLoc :: SrcSpan -> [TyVar] -> TcRnIf gbl lcl (TvSubst, [TcTyVar])
--- We specify the location
-tcInstSigTyVarsLoc loc = instSkolTyVars (mkTcSkolTyVar loc False)
-
-tcInstSigTyVars :: [TyVar] -> TcRnIf gbl lcl (TvSubst, [TcTyVar])
--- Get the location from the TyVar itself, not the monad
-tcInstSigTyVars
-  = instSkolTyVars mk_tv
+       ; lvl <- getTcLevel
+       ; instSkolTyCoVarsX (mkTcSkolTyVar lvl loc overlappable) subst tvs }
+
+mkTcSkolTyVar :: TcLevel -> SrcSpan -> Bool -> TcTyCoVarMaker gbl lcl
+-- Allocates skolems whose level is ONE GREATER THAN the passed-in tc_lvl
+-- See Note [Skolem level allocation]
+mkTcSkolTyVar tc_lvl loc overlappable old_name kind
+  = do { uniq <- newUnique
+       ; let name = mkInternalName uniq (getOccName old_name) loc
+       ; return (mkTcTyVar name kind details) }
   where
-    mk_tv uniq old_name kind
-       = mkTcTyVar (setNameUnique old_name uniq) kind (SkolemTv False)
+    details = SkolemTv (pushTcLevel tc_lvl) overlappable
+              -- pushTcLevel: see Note [Skolem level allocation]
+
+{- Note [Skolem level allocation]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We generally allocate skolems /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.  Applies also to vanillaSkolemTv.
 
-tcInstSkolType :: TcType -> TcM ([TcTyVar], TcThetaType, TcType)
--- Instantiate a type with fresh skolem constants
--- Binding location comes from the monad
-tcInstSkolType ty = tcInstType tcInstSkolTyVars ty
+-}
 
 ------------------
-freshenTyVarBndrs :: [TyVar] -> TcRnIf gbl lcl (TvSubst, [TyVar])
+freshenTyVarBndrs :: [TyVar] -> TcRnIf gbl lcl (TCvSubst, [TyVar])
 -- ^ Give fresh uniques to a bunch of TyVars, but they stay
 --   as TyVars, rather than becoming TcTyVars
 -- Used in FamInst.newFamInst, and Inst.newClsInst
-freshenTyVarBndrs = instSkolTyVars mk_tv
+freshenTyVarBndrs = instSkolTyCoVars mk_tv
   where
-    mk_tv uniq old_name kind = mkTyVar (setNameUnique old_name uniq) kind
+    mk_tv old_name kind
+       = do { uniq <- newUnique
+            ; return (mkTyVar (setNameUnique old_name uniq) kind) }
+
+freshenCoVarBndrsX :: TCvSubst -> [CoVar] -> TcRnIf gbl lcl (TCvSubst, [CoVar])
+-- ^ Give fresh uniques to a bunch of CoVars
+-- Used in FamInst.newFamInst
+freshenCoVarBndrsX subst = instSkolTyCoVarsX mk_cv subst
+  where
+    mk_cv old_name kind
+      = do { uniq <- newUnique
+           ; return (mkCoVar (setNameUnique old_name uniq) kind) }
 
 ------------------
-instSkolTyVars :: (Unique -> Name -> Kind -> TyVar)
-                -> [TyVar] -> TcRnIf gbl lcl (TvSubst, [TyVar])
-instSkolTyVars mk_tv = instSkolTyVarsX mk_tv emptyTvSubst
-
-instSkolTyVarsX :: (Unique -> Name -> Kind -> TyVar)
-                -> TvSubst -> [TyVar] -> TcRnIf gbl lcl (TvSubst, [TyVar])
-instSkolTyVarsX mk_tv = mapAccumLM (instSkolTyVarX mk_tv)
-
-instSkolTyVarX :: (Unique -> Name -> Kind -> TyVar)
-               -> TvSubst -> TyVar -> TcRnIf gbl lcl (TvSubst, TyVar)
-instSkolTyVarX mk_tv subst tyvar
-  = do  { uniq <- newUnique
-        ; let new_tv = mk_tv uniq old_name kind
-        ; return (extendTvSubst subst tyvar (mkTyVarTy new_tv), new_tv) }
+type TcTyCoVarMaker gbl lcl = Name -> Kind -> TcRnIf gbl lcl TyCoVar
+     -- The TcTyCoVarMaker should make a fresh Name, based on the old one
+     -- Freshness is critical. See Note [Skolems in zonkSyntaxExpr] in TcHsSyn
+
+instSkolTyCoVars :: TcTyCoVarMaker gbl lcl -> [TyVar] -> TcRnIf gbl lcl (TCvSubst, [TyCoVar])
+instSkolTyCoVars mk_tcv = instSkolTyCoVarsX mk_tcv emptyTCvSubst
+
+instSkolTyCoVarsX :: TcTyCoVarMaker gbl lcl
+                  -> TCvSubst -> [TyCoVar] -> TcRnIf gbl lcl (TCvSubst, [TyCoVar])
+instSkolTyCoVarsX mk_tcv = mapAccumLM (instSkolTyCoVarX mk_tcv)
+
+instSkolTyCoVarX :: TcTyCoVarMaker gbl lcl
+                 -> TCvSubst -> TyCoVar -> TcRnIf gbl lcl (TCvSubst, TyCoVar)
+instSkolTyCoVarX mk_tcv subst tycovar
+  = do  { new_tcv <- mk_tcv old_name kind
+        ; let subst1 | isTyVar new_tcv
+                     = extendTvSubstWithClone subst tycovar new_tcv
+                     | otherwise
+                     = extendCvSubstWithClone subst tycovar new_tcv
+        ; return (subst1, new_tcv) }
   where
-    old_name = tyVarName tyvar
-    kind     = substTy subst (tyVarKind tyvar)
+    old_name = tyVarName tycovar
+    kind     = substTyUnchecked subst (tyVarKind tycovar)
+
+newFskTyVar :: TcType -> TcM TcTyVar
+newFskTyVar fam_ty
+  = do { uniq <- newUnique
+       ; ref  <- newMutVar Flexi
+       ; tclvl <- getTcLevel
+       ; let details = MetaTv { mtv_info  = FlatSkolTv
+                              , mtv_ref   = ref
+                              , mtv_tclvl = tclvl }
+             name = mkMetaTyVarName uniq (fsLit "fsk")
+       ; return (mkTcTyVar name (typeKind fam_ty) details) }
 
 {-
 Note [Kind substitution when instantiating]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 When we instantiate a bunch of kind and type variables, first we
-expect them to be sorted (kind variables first, then type variables).
+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 :: BOX), (k2 :: BOX), (a :: k1 -> k2), (b :: k1)]
+  [(k1 :: *), (k2 :: *), (a :: k1 -> k2), (b :: k1)]
 we want
-  [(?k1 :: BOX), (?k2 :: BOX), (?a :: ?k1 -> ?k2), (?b :: ?k1)]
+  [(?k1 :: *), (?k2 :: *), (?a :: ?k1 -> ?k2), (?b :: ?k1)]
 instead of the buggous
-  [(?k1 :: BOX), (?k2 :: BOX), (?a :: k1 -> k2), (?b :: k1)]
+  [(?k1 :: *), (?k2 :: *), (?a :: k1 -> k2), (?b :: k1)]
 
 
 ************************************************************************
@@ -277,36 +608,45 @@ instead of the buggous
 ************************************************************************
 -}
 
-newMetaTyVar :: MetaInfo -> Kind -> TcM TcTyVar
--- Make a new meta tyvar out of thin air
-newMetaTyVar meta_info kind
-  = do  { uniq <- newUnique
-        ; let name = mkTcTyVarName uniq s
-              s = case meta_info of
-                        ReturnTv    -> fsLit "r"
-                        TauTv       -> fsLit "t"
-                        FlatMetaTv  -> fsLit "fmv"
-                        SigTv       -> fsLit "a"
-        ; details <- newMetaDetails meta_info
-        ; return (mkTcTyVar name kind details) }
-
-newSigKindVar :: Name -> TcM TcTyVar
-newSigKindVar name = newSigTyVar name superKind
-
+-- a SigTv can unify with type *variables* only, including other SigTvs
+-- and skolems. Sometimes, they can unify with type variables that the
+-- user would rather keep distinct; see #11203 for an example.
+-- So, any client of this
+-- function needs to either allow the SigTvs to unify with each other
+-- (say, for pattern-bound scoped type variables), or check that they
+-- don't (say, with a call to findDubSigTvs).
 newSigTyVar :: Name -> Kind -> TcM TcTyVar
 newSigTyVar name kind
   = do { details <- newMetaDetails SigTv
-       ; uniq    <- newUnique
-       ; let fresh_name = setNameUnique name uniq
-                 -- Use the same OccName so that the tidy-er
-                 -- doesn't gratuitously rename 'a' to 'a0' etc
-       ; return (mkTcTyVar fresh_name kind details) }
+       ; let tyvar = mkTcTyVar name kind details
+       ; traceTc "newSigTyVar" (ppr tyvar)
+       ; return tyvar }
+
+-- makes a new skolem tv
+newSkolemTyVar :: Name -> Kind -> TcM TcTyVar
+newSkolemTyVar name kind = do { lvl <- getTcLevel
+                              ; return (mkTcTyVar name kind (SkolemTv lvl False)) }
+
+newFmvTyVar :: TcType -> TcM TcTyVar
+-- Very like newMetaTyVar, except sets mtv_tclvl to one less
+-- so that the fmv is untouchable.
+newFmvTyVar fam_ty
+  = do { uniq <- newUnique
+       ; ref  <- newMutVar Flexi
+       ; tclvl <- getTcLevel
+       ; let details = MetaTv { mtv_info  = FlatMetaTv
+                              , mtv_ref   = ref
+                              , mtv_tclvl = tclvl }
+             name = mkMetaTyVarName uniq (fsLit "s")
+       ; return (mkTcTyVar name (typeKind fam_ty) details) }
 
 newMetaDetails :: MetaInfo -> TcM TcTyVarDetails
 newMetaDetails info
   = do { ref <- newMutVar Flexi
        ; tclvl <- getTcLevel
-       ; return (MetaTv { mtv_info = info, mtv_ref = ref, mtv_tclvl = tclvl }) }
+       ; return (MetaTv { mtv_info = info
+                        , mtv_ref = ref
+                        , mtv_tclvl = tclvl }) }
 
 cloneMetaTyVar :: TcTyVar -> TcM TcTyVar
 cloneMetaTyVar tv
@@ -317,20 +657,18 @@ cloneMetaTyVar tv
               details' = case tcTyVarDetails tv of
                            details@(MetaTv {}) -> details { mtv_ref = ref }
                            _ -> pprPanic "cloneMetaTyVar" (ppr tv)
-        ; return (mkTcTyVar name' (tyVarKind tv) details') }
-
-mkTcTyVarName :: Unique -> FastString -> Name
-mkTcTyVarName uniq str = mkSysTvName uniq str
+              tyvar = mkTcTyVar name' (tyVarKind tv) details'
+        ; traceTc "cloneMetaTyVar" (ppr tyvar)
+        ; return tyvar }
 
 -- Works for both type and kind variables
 readMetaTyVar :: TyVar -> TcM MetaDetails
 readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
-                      readMutVar (metaTvRef tyvar)
+                      readMutVar (metaTyVarRef tyvar)
 
 isFilledMetaTyVar :: TyVar -> TcM Bool
 -- True of a filled-in (Indirect) meta type variable
 isFilledMetaTyVar tv
-  | not (isTcTyVar tv) = return False
   | MetaTv { mtv_ref = ref } <- tcTyVarDetails tv
   = do  { details <- readMutVar ref
         ; return (isIndirect details) }
@@ -339,7 +677,6 @@ isFilledMetaTyVar tv
 isUnfilledMetaTyVar :: TyVar -> TcM Bool
 -- True of a un-filled-in (Flexi) meta type variable
 isUnfilledMetaTyVar tv
-  | not (isTcTyVar tv) = return False
   | MetaTv { mtv_ref = ref } <- tcTyVarDetails tv
   = do  { details <- readMutVar ref
         ; return (isFlexi details) }
@@ -352,7 +689,7 @@ writeMetaTyVar :: TcTyVar -> TcType -> TcM ()
 
 writeMetaTyVar tyvar ty
   | not debugIsOn
-  = writeMetaTyVarRef tyvar (metaTvRef tyvar) ty
+  = writeMetaTyVarRef tyvar (metaTyVarRef tyvar) ty
 
 -- Everything from here on only happens if DEBUG is on
   | not (isTcTyVar tyvar)
@@ -372,34 +709,70 @@ writeMetaTyVarRef :: TcTyVar -> TcRef MetaDetails -> TcType -> TcM ()
 -- the ref cell must be for the same tyvar
 writeMetaTyVarRef tyvar ref ty
   | not debugIsOn
-  = do { traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty)
-       ; writeMutVar ref (Indirect ty) }
+  = do { traceTc "writeMetaTyVar" (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)
+                                   <+> text ":=" <+> ppr ty)
+       ; writeTcRef ref (Indirect ty) }
 
--- Everything from here on only happens if DEBUG is on
+  -- Everything from here on only happens if DEBUG is on
   | otherwise
   = do { meta_details <- readMutVar ref;
        -- Zonk kinds to allow the error check to work
-       ; zonked_tv_kind <- zonkTcKind tv_kind
-       ; zonked_ty_kind <- zonkTcKind ty_kind
+       ; zonked_tv_kind <- zonkTcType tv_kind
+       ; zonked_ty      <- zonkTcType ty
+       ; let zonked_ty_kind = typeKind zonked_ty  -- need to zonk even before typeKind;
+                                                  -- otherwise, we can panic in piResultTy
+             kind_check_ok = tcIsConstraintKind zonked_tv_kind
+                          || tcEqKind zonked_ty_kind zonked_tv_kind
+             -- Hack alert! tcIsConstraintKind: see TcHsType
+             -- Note [Extra-constraint holes in partial type signatures]
+
+             kind_msg = hang (text "Ill-kinded update to meta tyvar")
+                           2 (    ppr tyvar <+> text "::" <+> (ppr tv_kind $$ ppr zonked_tv_kind)
+                              <+> text ":="
+                              <+> ppr ty <+> text "::" <+> (ppr zonked_ty_kind) )
+
+       ; traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty)
 
        -- Check for double updates
-       ; ASSERT2( isFlexi meta_details,
-                  hang (text "Double update of meta tyvar")
-                   2 (ppr tyvar $$ ppr meta_details) )
-
-         traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty)
-       ; writeMutVar ref (Indirect ty)
-       ; when (   not (isPredTy tv_kind)
-                    -- Don't check kinds for updates to coercion variables
-               && not (zonked_ty_kind `tcIsSubKind` zonked_tv_kind))
-       $ WARN( True, hang (text "Ill-kinded update to meta tyvar")
-                        2 (    ppr tyvar <+> text "::" <+> (ppr tv_kind $$ ppr zonked_tv_kind)
-                           <+> text ":="
-                           <+> ppr ty    <+> text "::" <+> (ppr ty_kind $$ ppr zonked_ty_kind) ) )
-         (return ()) }
+       ; MASSERT2( isFlexi meta_details, double_upd_msg meta_details )
+
+       -- Check for level OK
+       -- See Note [Level check when unifying]
+       ; MASSERT2( level_check_ok, level_check_msg )
+
+       -- Check Kinds ok
+       ; MASSERT2( kind_check_ok, kind_msg )
+
+       -- Do the write
+       ; writeMutVar ref (Indirect ty) }
   where
     tv_kind = tyVarKind tyvar
-    ty_kind = typeKind ty
+
+    tv_lvl = tcTyVarLevel tyvar
+    ty_lvl = tcTypeLevel ty
+
+    level_check_ok  = not (ty_lvl `strictlyDeeperThan` tv_lvl)
+    level_check_msg = ppr ty_lvl $$ ppr tv_lvl $$ ppr tyvar $$ ppr ty
+
+    double_upd_msg details = hang (text "Double update of meta tyvar")
+                                2 (ppr tyvar $$ ppr details)
+
+
+{- Note [Level check when unifying]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When unifying
+     alpha:lvl := ty
+we expect that the TcLevel of 'ty' will be <= lvl.
+However, during unflatting we do
+     fuv:l := ty:(l+1)
+which is usually wrong; hence the check isFmmvTyVar in level_check_ok.
+See Note [TcLevel assignment] in TcType.
+-}
+
+{-
+% Generating fresh variables for pattern match check
+-}
+
 
 {-
 ************************************************************************
@@ -407,53 +780,141 @@ writeMetaTyVarRef tyvar ref ty
         MetaTvs: TauTvs
 *                                                                      *
 ************************************************************************
+
+Note [Never need to instantiate coercion variables]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+With coercion variables sloshing around in types, it might seem that we
+sometimes need to instantiate coercion variables. This would be problematic,
+because coercion variables inhabit unboxed equality (~#), and the constraint
+solver thinks in terms only of boxed equality (~). The solution is that
+we never need to instantiate coercion variables in the first place.
+
+The tyvars that we need to instantiate come from the types of functions,
+data constructors, and patterns. These will never be quantified over
+coercion variables, except for the special case of the promoted Eq#. But,
+that can't ever appear in user code, so we're safe!
+-}
+
+mkMetaTyVarName :: Unique -> FastString -> Name
+-- Makes a /System/ Name, which is eagerly eliminated by
+-- the unifier; see TcUnify.nicer_to_update_tv1, and
+-- TcCanonical.canEqTyVarTyVar (nicer_to_update_tv2)
+mkMetaTyVarName uniq str = mkSystemName uniq (mkTyVarOccFS str)
+
+newAnonMetaTyVar :: MetaInfo -> Kind -> TcM TcTyVar
+-- Make a new meta tyvar out of thin air
+newAnonMetaTyVar meta_info kind
+  = do  { uniq <- newUnique
+        ; let name = mkMetaTyVarName uniq s
+              s = case meta_info of
+                        TauTv       -> fsLit "t"
+                        FlatMetaTv  -> fsLit "fmv"
+                        FlatSkolTv  -> fsLit "fsk"
+                        SigTv       -> fsLit "a"
+        ; details <- newMetaDetails meta_info
+        ; let tyvar = mkTcTyVar name kind details
+        ; traceTc "newAnonMetaTyVar" (ppr tyvar)
+        ; return tyvar }
+
+cloneAnonMetaTyVar :: MetaInfo -> TyVar -> TcKind -> TcM TcTyVar
+-- Same as newAnonMetaTyVar, but use a supplied TyVar as the source of the print-name
+cloneAnonMetaTyVar info tv kind
+  = do  { uniq    <- newUnique
+        ; details <- newMetaDetails info
+        ; let name = mkSystemName uniq (getOccName tv)
+                       -- See Note [Name of an instantiated type variable]
+              tyvar = mkTcTyVar name kind details
+        ; traceTc "cloneAnonMetaTyVar" (ppr tyvar)
+        ; return tyvar }
+
+{- Note [Name of an instantiated type variable]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+At the moment we give a unification variable a System Name, which
+influences the way it is tidied; see TypeRep.tidyTyVarBndr.
 -}
 
 newFlexiTyVar :: Kind -> TcM TcTyVar
-newFlexiTyVar kind = newMetaTyVar TauTv kind
+newFlexiTyVar kind = newAnonMetaTyVar TauTv kind
 
-newFlexiTyVarTy  :: Kind -> TcM TcType
+newFlexiTyVarTy :: Kind -> TcM TcType
 newFlexiTyVarTy kind = do
     tc_tyvar <- newFlexiTyVar kind
-    return (TyVarTy tc_tyvar)
+    return (mkTyVarTy tc_tyvar)
 
 newFlexiTyVarTys :: Int -> Kind -> TcM [TcType]
 newFlexiTyVarTys n kind = mapM newFlexiTyVarTy (nOfThem n kind)
 
-newReturnTyVar :: Kind -> TcM TcTyVar
-newReturnTyVar kind = newMetaTyVar ReturnTv kind
+newOpenTypeKind :: TcM TcKind
+newOpenTypeKind
+  = do { rr <- newFlexiTyVarTy runtimeRepTy
+       ; return (tYPE rr) }
 
-newReturnTyVarTy :: Kind -> TcM TcType
-newReturnTyVarTy kind = TyVarTy <$> newReturnTyVar kind
+-- | Create a tyvar that can be a lifted or unlifted type.
+-- Returns alpha :: TYPE kappa, where both alpha and kappa are fresh
+newOpenFlexiTyVarTy :: TcM TcType
+newOpenFlexiTyVarTy
+  = do { kind <- newOpenTypeKind
+       ; newFlexiTyVarTy kind }
 
-tcInstTyVars :: [TKVar] -> TcM (TvSubst, [TcTyVar])
+newMetaSigTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
+newMetaSigTyVars = mapAccumLM newMetaSigTyVarX emptyTCvSubst
+
+newMetaTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
 -- Instantiate with META type variables
--- Note that this works for a sequence of kind and type
--- variables.  Eg    [ (k:BOX), (a:k->k) ]
---             Gives [ (k7:BOX), (a8:k7->k7) ]
-tcInstTyVars tyvars = mapAccumLM tcInstTyVarX emptyTvSubst tyvars
-    -- emptyTvSubst has an empty in-scope set, but that's fine here
+-- Note that this works for a sequence of kind, type, and coercion variables
+-- variables.  Eg    [ (k:*), (a:k->k) ]
+--             Gives [ (k7:*), (a8:k7->k7) ]
+newMetaTyVars = mapAccumLM newMetaTyVarX emptyTCvSubst
+    -- emptyTCvSubst has an empty in-scope set, but that's fine here
     -- Since the tyvars are freshly made, they cannot possibly be
     -- captured by any existing for-alls.
 
-tcInstTyVarX :: TvSubst -> TKVar -> TcM (TvSubst, TcTyVar)
+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.
-tcInstTyVarX subst tyvar
+newMetaTyVarX subst tyvar = new_meta_tv_x TauTv subst tyvar
+
+newMetaTyVarsX :: TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
+-- Just like newMetaTyVars, but start with an existing substitution.
+newMetaTyVarsX subst = mapAccumLM newMetaTyVarX subst
+
+newMetaSigTyVarX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
+-- Just like newMetaTyVarX, but make a SigTv
+newMetaSigTyVarX subst tyvar = new_meta_tv_x SigTv subst tyvar
+
+newWildCardX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
+newWildCardX subst tv
+  = do { new_tv <- newAnonMetaTyVar TauTv (substTy subst (tyVarKind tv))
+       ; return (extendTvSubstWithClone subst tv new_tv, new_tv) }
+
+new_meta_tv_x :: MetaInfo -> TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
+new_meta_tv_x info subst tv
+  = do  { new_tv <- cloneAnonMetaTyVar info tv substd_kind
+        ; let subst1 = extendTvSubstWithClone subst tv new_tv
+        ; return (subst1, new_tv) }
+  where
+    substd_kind = substTyUnchecked subst (tyVarKind tv)
+      -- NOTE: Trac #12549 is fixed so we could use
+      -- substTy here, but the tc_infer_args problem
+      -- is not yet fixed so leaving as unchecked for now.
+      -- OLD NOTE:
+      -- Unchecked because we call newMetaTyVarX from
+      -- tcInstTyBinder, which is called from tcInferApps
+      -- which does not yet take enough trouble to ensure
+      -- the in-scope set is right; e.g. Trac #12785 trips
+      -- if we use substTy here
+
+newMetaTyVarTyAtLevel :: TcLevel -> TcKind -> TcM TcType
+newMetaTyVarTyAtLevel tc_lvl kind
   = do  { uniq <- newUnique
-        ; details <- newMetaDetails TauTv
-        ; let name   = mkSystemName uniq (getOccName tyvar)
-                       -- See Note [Name of an instantiated type variable]
-              kind   = substTy subst (tyVarKind tyvar)
-              new_tv = mkTcTyVar name kind details
-        ; return (extendTvSubst subst tyvar (mkTyVarTy new_tv), new_tv) }
-
-{- Note [Name of an instantiated type variable]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-At the moment we give a unification variable a System Name, which
-influences the way it is tidied; see TypeRep.tidyTyVarBndr.
+        ; ref  <- newMutVar Flexi
+        ; let name = mkMetaTyVarName uniq (fsLit "p")
+              details = MetaTv { mtv_info  = TauTv
+                               , mtv_ref   = ref
+                               , mtv_tclvl = tc_lvl }
+        ; return (mkTyVarTy (mkTcTyVar name kind details)) }
 
-************************************************************************
+{- *********************************************************************
 *                                                                      *
              Quantification
 *                                                                      *
@@ -461,66 +922,122 @@ influences the way it is tidied; see TypeRep.tidyTyVarBndr.
 
 Note [quantifyTyVars]
 ~~~~~~~~~~~~~~~~~~~~~
-quantifyTyVars is give the free vars of a type that we
+quantifyTyVars is given the free vars of a type that we
 are about to wrap in a forall.
 
-It takes these free type/kind variables and
-  1. Zonks them and remove globals
-  2. Partitions into type and kind variables (kvs1, tvs)
-  3. Extends kvs1 with free kind vars in the kinds of tvs (removing globals)
-  4. Calls zonkQuantifiedTyVar on each
+It takes these free type/kind variables (partitioned into dependent and
+non-dependent variables) and
+  1. Zonks them and remove globals and covars
+  2. Extends kvs1 with free kind vars in the kinds of tvs (removing globals)
+  3. Calls zonkQuantifiedTyVar on each
 
-Step (3) is often unimportant, because the kind variable is often
+Step (2) is often unimportant, because the kind variable is often
 also free in the type.  Eg
      Typeable k (a::k)
 has free vars {k,a}.  But the type (see Trac #7916)
     (f::k->*) (a::k)
-has free vars {f,a}, but we must add 'k' as well! Hence step (3).
+has free vars {f,a}, but we must add 'k' as well! Hence step (2).
+
+* This function distinguishes between dependent and non-dependent
+  variables only to keep correct defaulting behavior with -XNoPolyKinds.
+  With -XPolyKinds, it treats both classes of variables identically.
+
+* quantifyTyVars never quantifies over
+    - a coercion variable
+    - a runtime-rep variable
+
+Note [quantifyTyVars determinism]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The results of quantifyTyVars are wrapped in a forall and can end up in the
+interface file. One such example is inferred type signatures. They also affect
+the results of optimizations, for example worker-wrapper. This means that to
+get deterministic builds quantifyTyVars needs to be deterministic.
+
+To achieve this CandidatesQTvs is backed by deterministic sets which allows them
+to be later converted to a list in a deterministic order.
+
+For more information about deterministic sets see
+Note [Deterministic UniqFM] in UniqDFM.
 -}
 
-quantifyTyVars :: TcTyVarSet -> TcTyVarSet -> TcM [TcTyVar]
+quantifyTyVars
+  :: TcTyCoVarSet     -- Global tvs; already zonked
+  -> CandidatesQTvs   -- See Note [Dependent type variables] in TcType
+                      -- Already zonked
+  -> TcM [TcTyVar]
 -- See Note [quantifyTyVars]
--- The input is a mixture of type and kind variables; a kind variable k
---   may occur *after* a tyvar mentioning k in its kind
 -- Can be given a mixture of TcTyVars and TyVars, in the case of
---   associated type declarations
-
-quantifyTyVars gbl_tvs tkvs
-  = do { tkvs    <- zonkTyVarsAndFV tkvs
-       ; gbl_tvs <- zonkTyVarsAndFV gbl_tvs
-       ; let (kvs, tvs) = partitionVarSet isKindVar (closeOverKinds tkvs `minusVarSet` gbl_tvs)
-                              -- NB kinds of tvs are zonked by zonkTyVarsAndFV
-             kvs2 = varSetElems kvs
-             qtvs = varSetElems tvs
+--   associated type declarations. Also accepts covars, but *never* returns any.
+
+quantifyTyVars gbl_tvs dvs@(DV{ dv_kvs = dep_tkvs, dv_tvs = nondep_tkvs })
+  = do { traceTc "quantifyTyVars" (vcat [ppr dvs, ppr gbl_tvs])
+       ; let dep_kvs = dVarSetElemsWellScoped $
+                       dep_tkvs `dVarSetMinusVarSet` gbl_tvs
+                       -- dVarSetElemsWellScoped: put the kind variables into
+                       --    well-scoped order.
+                       --    E.g.  [k, (a::k)] not the other way roud
+
+             nondep_tvs = dVarSetElems $
+                          (nondep_tkvs `minusDVarSet` dep_tkvs)
+                           `dVarSetMinusVarSet` gbl_tvs
+                 -- See Note [Dependent type variables] in TcType
+                 -- The `minus` dep_tkvs removes any kind-level vars
+                 --    e.g. T k (a::k)   Since k appear in a kind it'll
+                 --    be in dv_kvs, and is dependent. So remove it from
+                 --    dv_tvs which will also contain k
+                 -- No worry about dependent covars here;
+                 --    they are all in dep_tkvs
+                 -- No worry about scoping, because these are all
+                 --    type variables
+                 -- NB kinds of tvs are zonked by zonkTyCoVarsAndFV
 
              -- In the non-PolyKinds case, default the kind variables
              -- to *, and zonk the tyvars as usual.  Notice that this
              -- may make quantifyTyVars return a shorter list
              -- than it was passed, but that's ok
-       ; poly_kinds <- xoptM Opt_PolyKinds
-       ; qkvs <- if poly_kinds
-                 then return kvs2
-                 else do { let (meta_kvs, skolem_kvs) = partition is_meta kvs2
-                               is_meta kv = isTcTyVar kv && isMetaTyVar kv
-                         ; mapM_ defaultKindVarToStar meta_kvs
-                         ; return skolem_kvs }  -- should be empty
-
-       ; mapM zonk_quant (qkvs ++ qtvs) }
+       ; poly_kinds  <- xoptM LangExt.PolyKinds
+       ; dep_kvs'    <- mapMaybeM (zonk_quant (not poly_kinds)) dep_kvs
+       ; nondep_tvs' <- mapMaybeM (zonk_quant False)            nondep_tvs
+       ; let final_qtvs = dep_kvs' ++ nondep_tvs'
            -- Because of the order, any kind variables
-           -- mentioned in the kinds of the type variables refer to
-           -- the now-quantified versions
+           -- mentioned in the kinds of the nondep_tvs'
+           -- now refer to the dep_kvs'
+
+       ; traceTc "quantifyTyVars"
+           (vcat [ text "globals:" <+> ppr gbl_tvs
+                 , text "nondep:"  <+> pprTyVars nondep_tvs
+                 , text "dep:"     <+> pprTyVars dep_kvs
+                 , text "dep_kvs'" <+> pprTyVars dep_kvs'
+                 , text "nondep_tvs'" <+> pprTyVars nondep_tvs' ])
+
+       -- We should never quantify over coercion variables; check this
+       ; let co_vars = filter isCoVar final_qtvs
+       ; MASSERT2( null co_vars, ppr co_vars )
+
+       ; return final_qtvs }
   where
-    zonk_quant tkv
-      | isTcTyVar tkv = zonkQuantifiedTyVar tkv
-      | otherwise     = return tkv
-      -- For associated types, we have the class variables
-      -- in scope, and they are TyVars not TcTyVars
+    -- zonk_quant returns a tyvar if it should be quantified over;
+    -- otherwise, it returns Nothing. The latter case happens for
+    --    * Kind variables, with -XNoPolyKinds: don't quantify over these
+    --    * RuntimeRep variables: we never quantify over these
+    zonk_quant default_kind tkv
+      | not (isTyVar tkv)
+      = return Nothing   -- this can happen for a covar that's associated with
+                         -- a coercion hole. Test case: typecheck/should_compile/T2494
+
+      | not (isTcTyVar tkv)
+      = return (Just tkv)  -- For associated types, we have the class variables
+                           -- in scope, and they are TyVars not TcTyVars
+      | otherwise
+      = do { deflt_done <- defaultTyVar default_kind tkv
+           ; case deflt_done of
+               True  -> return Nothing
+               False -> do { tv <- zonkQuantifiedTyVar tkv
+                           ; return (Just tv) } }
 
 zonkQuantifiedTyVar :: TcTyVar -> TcM TcTyVar
 -- The quantified type variables often include meta type variables
--- we want to freeze them into ordinary type variables, and
--- default their kind (e.g. from OpenTypeKind to TypeKind)
---                      -- see notes with Kind.defaultKind
+-- we want to freeze them into ordinary type variables
 -- The meta tyvar is updated to point to the new skolem TyVar.  Now any
 -- bound occurrences of the original type variable will get zonked to
 -- the immutable version.
@@ -529,55 +1046,175 @@ zonkQuantifiedTyVar :: TcTyVar -> TcM TcTyVar
 --
 -- This function is called on both kind and type variables,
 -- but kind variables *only* if PolyKinds is on.
+
 zonkQuantifiedTyVar tv
-  = ASSERT2( isTcTyVar tv, ppr tv )
-    case tcTyVarDetails tv of
-      SkolemTv {} -> do { kind <- zonkTcKind (tyVarKind tv)
-                        ; return $ setTyVarKind tv kind }
+  = case tcTyVarDetails tv of
+      SkolemTv {} -> do { kind <- zonkTcType (tyVarKind tv)
+                        ; return (setTyVarKind tv kind) }
         -- It might be a skolem type variable,
         -- for example from a user type signature
 
-      MetaTv { mtv_ref = ref } ->
-          do when debugIsOn $ do
-                 -- [Sept 04] Check for non-empty.
-                 -- See note [Silly Type Synonym]
-                 cts <- readMutVar ref
-                 case cts of
-                     Flexi -> return ()
-                     Indirect ty -> WARN( True, ppr tv $$ ppr ty )
-                                    return ()
-             skolemiseUnboundMetaTyVar tv vanillaSkolemTv
-      _other -> pprPanic "zonkQuantifiedTyVar" (ppr tv) -- FlatSkol, RuntimeUnk
-
-defaultKindVarToStar :: TcTyVar -> TcM Kind
--- We have a meta-kind: unify it with '*'
-defaultKindVarToStar kv
-  = do { ASSERT( isKindVar kv && isMetaTyVar kv )
-         writeMetaTyVar kv liftedTypeKind
-       ; return liftedTypeKind }
-
-skolemiseUnboundMetaTyVar :: TcTyVar -> TcTyVarDetails -> TcM TyVar
+      MetaTv {} -> skolemiseUnboundMetaTyVar tv
+
+      _other -> pprPanic "zonkQuantifiedTyVar" (ppr tv) -- RuntimeUnk
+
+defaultTyVar :: Bool      -- True <=> please default this kind variable to *
+             -> TcTyVar   -- If it's a MetaTyVar then it is unbound
+             -> TcM Bool  -- True <=> defaulted away altogether
+
+defaultTyVar default_kind tv
+  | not (isMetaTyVar tv)
+  = return False
+
+  | isSigTyVar tv
+    -- Do not default SigTvs. Doing so would violate the invariants
+    -- on SigTvs; see Note [Signature skolems] in TcType.
+    -- Trac #13343 is an example; #14555 is another
+    -- See Note [Kind generalisation and SigTvs]
+  = return False
+
+
+  | isRuntimeRepVar tv  -- Do not quantify over a RuntimeRep var
+                        -- unless it is a SigTv, handled earlier
+  = do { traceTc "Defaulting a RuntimeRep var to LiftedRep" (ppr tv)
+       ; writeMetaTyVar tv liftedRepTy
+       ; return True }
+
+  | default_kind                 -- -XNoPolyKinds and this is a kind var
+  = do { default_kind_var tv     -- so default it to * if possible
+       ; return True }
+
+  | otherwise
+  = return False
+
+  where
+    default_kind_var :: TyVar -> TcM ()
+       -- defaultKindVar is used exclusively with -XNoPolyKinds
+       -- See Note [Defaulting with -XNoPolyKinds]
+       -- It takes an (unconstrained) meta tyvar and defaults it.
+       -- Works only on vars of type *; for other kinds, it issues an error.
+    default_kind_var kv
+      | isLiftedTypeKind (tyVarKind kv)
+      = do { traceTc "Defaulting a kind var to *" (ppr kv)
+           ; writeMetaTyVar kv liftedTypeKind }
+      | otherwise
+      = addErr (vcat [ text "Cannot default kind variable" <+> quotes (ppr kv')
+                     , text "of kind:" <+> ppr (tyVarKind kv')
+                     , text "Perhaps enable PolyKinds or add a kind signature" ])
+      where
+        (_, kv') = tidyOpenTyCoVar emptyTidyEnv kv
+
+skolemiseRuntimeUnk :: TcTyVar -> TcM TyVar
+skolemiseRuntimeUnk tv
+  = skolemise_tv tv RuntimeUnk
+
+skolemiseUnboundMetaTyVar :: TcTyVar -> TcM TyVar
+skolemiseUnboundMetaTyVar tv
+  = skolemise_tv tv (SkolemTv (metaTyVarTcLevel tv) False)
+
+skolemise_tv :: TcTyVar -> TcTyVarDetails -> TcM TyVar
 -- We have a Meta tyvar with a ref-cell inside it
--- Skolemise it, including giving it a new Name, so that
+-- Skolemise it, so that
 --   we are totally out of Meta-tyvar-land
 -- We create a skolem TyVar, not a regular TyVar
 --   See Note [Zonking to Skolem]
-skolemiseUnboundMetaTyVar tv details
+skolemise_tv tv details
   = ASSERT2( isMetaTyVar tv, ppr tv )
-    do  { span <- getSrcSpanM    -- Get the location from "here"
+    do  { when debugIsOn (check_empty tv)
+        ; span <- getSrcSpanM    -- Get the location from "here"
                                  -- ie where we are generalising
-        ; kind <- zonkTcKind (tyVarKind tv)
+        ; kind <- zonkTcType (tyVarKind tv)
         ; let uniq        = getUnique tv
+                -- NB: Use same Unique as original tyvar. This is
+                -- important for TcHsType.splitTelescopeTvs to work properly
+
               tv_name     = getOccName tv
               final_name  = mkInternalName uniq tv_name span
-              final_kind  = defaultKind kind
-              final_tv    = mkTcTyVar final_name final_kind details
+              final_tv    = mkTcTyVar final_name kind details
 
-        ; traceTc "Skolemising" (ppr tv <+> ptext (sLit ":=") <+> ppr final_tv)
+        ; traceTc "Skolemising" (ppr tv <+> text ":=" <+> ppr final_tv)
         ; writeMetaTyVar tv (mkTyVarTy final_tv)
         ; return final_tv }
 
-{-
+  where
+    check_empty tv       -- [Sept 04] Check for non-empty.
+      = when debugIsOn $  -- See note [Silly Type Synonym]
+        do { cts <- readMetaTyVar tv
+           ; case cts of
+               Flexi       -> return ()
+               Indirect ty -> WARN( True, ppr tv $$ ppr ty )
+                              return () }
+
+{- Note [Defaulting with -XNoPolyKinds]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+
+  data Compose f g a = Mk (f (g a))
+
+We infer
+
+  Compose :: forall k1 k2. (k2 -> *) -> (k1 -> k2) -> k1 -> *
+  Mk :: forall k1 k2 (f :: k2 -> *) (g :: k1 -> k2) (a :: k1).
+        f (g a) -> Compose k1 k2 f g a
+
+Now, in another module, we have -XNoPolyKinds -XDataKinds in effect.
+What does 'Mk mean? Pre GHC-8.0 with -XNoPolyKinds,
+we just defaulted all kind variables to *. But that's no good here,
+because the kind variables in 'Mk aren't of kind *, so defaulting to *
+is ill-kinded.
+
+After some debate on #11334, we decided to issue an error in this case.
+The code is in defaultKindVar.
+
+Note [What is a meta variable?]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+A "meta type-variable", also know as a "unification variable" is a placeholder
+introduced by the typechecker for an as-yet-unknown monotype.
+
+For example, when we see a call `reverse (f xs)`, we know that we calling
+    reverse :: forall a. [a] -> [a]
+So we know that the argument `f xs` must be a "list of something". But what is
+the "something"? We don't know until we explore the `f xs` a bit more. So we set
+out what we do know at the call of `reverse` by instantiate its type with a fresh
+meta tyvar, `alpha` say. So now the type of the argument `f xs`, and of the
+result, is `[alpha]`. The unification variable `alpha` stands for the
+as-yet-unknown type of the elements of the list.
+
+As type inference progresses we may learn more about `alpha`. For example, suppose
+`f` has the type
+    f :: forall b. b -> [Maybe b]
+Then we instantiate `f`'s type with another fresh unification variable, say
+`beta`; and equate `f`'s result type with reverse's argument type, thus
+`[alpha] ~ [Maybe beta]`.
+
+Now we can solve this equality to learn that `alpha ~ Maybe beta`, so we've
+refined our knowledge about `alpha`. And so on.
+
+If you found this Note useful, you may also want to have a look at
+Section 5 of "Practical type inference for higher rank types" (Peyton Jones,
+Vytiniotis, Weirich and Shields. J. Functional Programming. 2011).
+
+Note [What is zonking?]
+~~~~~~~~~~~~~~~~~~~~~~~
+GHC relies heavily on mutability in the typechecker for efficient operation.
+For this reason, throughout much of the type checking process meta type
+variables (the MetaTv constructor of TcTyVarDetails) are represented by mutable
+variables (known as TcRefs).
+
+Zonking is the process of ripping out these mutable variables and replacing them
+with a real Type. This involves traversing the entire type expression, but the
+interesting part of replacing the mutable variables occurs in zonkTyVarOcc.
+
+There are two ways to zonk a Type:
+
+ * zonkTcTypeToType, which is intended to be used at the end of type-checking
+   for the final zonk. It has to deal with unfilled metavars, either by filling
+   it with a value like Any or failing (determined by the UnboundTyVarZonker
+   used).
+
+ * zonkTcType, which will happily ignore unfilled metavars. This is the
+   appropriate function to use while in the middle of type-checking.
+
 Note [Zonking to Skolem]
 ~~~~~~~~~~~~~~~~~~~~~~~~
 We used to zonk quantified type variables to regular TyVars.  However, this
@@ -650,58 +1287,84 @@ a \/\a in the final result but all the occurrences of a will be zonked to ()
 *                                                                      *
 ************************************************************************
 
-@tcGetGlobalTyVars@ returns a fully-zonked set of tyvars free in the environment.
-To improve subsequent calls to the same function it writes the zonked set back into
-the environment.
 -}
 
-tcGetGlobalTyVars :: TcM TcTyVarSet
-tcGetGlobalTyVars
+-- | @tcGetGlobalTyCoVars@ returns a fully-zonked set of *scoped* tyvars free in
+-- the environment. To improve subsequent calls to the same function it writes
+-- the zonked set back into the environment. Note that this returns all
+-- variables free in anything (term-level or type-level) in scope. We thus
+-- don't have to worry about clashes with things that are not in scope, because
+-- if they are reachable, then they'll be returned here.
+tcGetGlobalTyCoVars :: TcM TcTyVarSet
+tcGetGlobalTyCoVars
   = do { (TcLclEnv {tcl_tyvars = gtv_var}) <- getLclEnv
        ; gbl_tvs  <- readMutVar gtv_var
-       ; gbl_tvs' <- zonkTyVarsAndFV gbl_tvs
+       ; gbl_tvs' <- zonkTyCoVarsAndFV gbl_tvs
        ; writeMutVar gtv_var gbl_tvs'
        ; return gbl_tvs' }
-  where
 
-zonkTcTypeAndFV :: TcType -> TcM TyVarSet
+-- | Zonk a type without using the smart constructors; the result type
+-- is available for inspection within the type-checking knot.
+zonkTcTypeInKnot :: TcType -> TcM TcType
+zonkTcTypeInKnot = mapType (zonkTcTypeMapper { tcm_smart = False }) ()
+
+zonkTcTypeAndFV :: TcType -> TcM DTyCoVarSet
 -- Zonk a type and take its free variables
 -- With kind polymorphism it can be essential to zonk *first*
 -- so that we find the right set of free variables.  Eg
 --    forall k1. forall (a:k2). a
 -- where k2:=k1 is in the substitution.  We don't want
 -- k2 to look free in this type!
-zonkTcTypeAndFV ty = do { ty <- zonkTcType ty; return (tyVarsOfType ty) }
-
-zonkTyVar :: TyVar -> TcM TcType
+-- NB: This might be called from within the knot, so don't use
+-- smart constructors. See Note [Type-checking inside the knot] in TcHsType
+zonkTcTypeAndFV ty
+  = tyCoVarsOfTypeDSet <$> zonkTcTypeInKnot ty
+
+-- | Zonk a type and call 'candidateQTyVarsOfType' on it.
+-- Works within the knot.
+zonkTcTypeAndSplitDepVars :: TcType -> TcM CandidatesQTvs
+zonkTcTypeAndSplitDepVars ty
+  = candidateQTyVarsOfType <$> zonkTcTypeInKnot ty
+
+zonkTcTypesAndSplitDepVars :: [TcType] -> TcM CandidatesQTvs
+zonkTcTypesAndSplitDepVars tys
+  = candidateQTyVarsOfTypes <$> mapM zonkTcTypeInKnot tys
+
+zonkTyCoVar :: TyCoVar -> TcM TcType
 -- Works on TyVars and TcTyVars
-zonkTyVar tv | isTcTyVar tv = zonkTcTyVar tv
-             | otherwise    = return (mkTyVarTy tv)
+zonkTyCoVar tv | isTcTyVar tv = zonkTcTyVar tv
+               | isTyVar   tv = mkTyVarTy <$> zonkTyCoVarKind tv
+               | otherwise    = ASSERT2( isCoVar tv, ppr tv )
+                                mkCoercionTy . mkCoVarCo <$> zonkTyCoVarKind tv
    -- Hackily, when typechecking type and class decls
    -- we have TyVars in scopeadded (only) in
    -- TcHsType.tcTyClTyVars, but it seems
    -- painful to make them into TcTyVars there
 
-zonkTyVarsAndFV :: TyVarSet -> TcM TyVarSet
-zonkTyVarsAndFV tyvars = tyVarsOfTypes <$> mapM zonkTyVar (varSetElems tyvars)
+zonkTyCoVarsAndFV :: TyCoVarSet -> TcM TyCoVarSet
+zonkTyCoVarsAndFV tycovars =
+  tyCoVarsOfTypes <$> mapM zonkTyCoVar (nonDetEltsUniqSet tycovars)
+  -- It's OK to use nonDetEltsUniqSet here because we immediately forget about
+  -- the ordering by turning it into a nondeterministic set and the order
+  -- of zonking doesn't matter for determinism.
+
+-- Takes a list of TyCoVars, zonks them and returns a
+-- deterministically ordered list of their free variables.
+zonkTyCoVarsAndFVList :: [TyCoVar] -> TcM [TyCoVar]
+zonkTyCoVarsAndFVList tycovars =
+  tyCoVarsOfTypesList <$> mapM zonkTyCoVar tycovars
 
 zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
 zonkTcTyVars tyvars = mapM zonkTcTyVar tyvars
 
 -----------------  Types
-zonkTyVarKind :: TyVar -> TcM TyVar
-zonkTyVarKind tv = do { kind' <- zonkTcKind (tyVarKind tv)
-                      ; return (setTyVarKind tv kind') }
+zonkTyCoVarKind :: TyCoVar -> TcM TyCoVar
+zonkTyCoVarKind tv = do { kind' <- zonkTcType (tyVarKind tv)
+                        ; return (setTyVarKind tv kind') }
 
 zonkTcTypes :: [TcType] -> TcM [TcType]
 zonkTcTypes tys = mapM zonkTcType tys
 
-zonkTcThetaType :: TcThetaType -> TcM TcThetaType
-zonkTcThetaType theta = mapM zonkTcPredType theta
-
-zonkTcPredType :: TcPredType -> TcM TcPredType
-zonkTcPredType = zonkTcType
-
 {-
 ************************************************************************
 *                                                                      *
@@ -715,8 +1378,8 @@ zonkImplication implic@(Implic { ic_skols  = skols
                                , ic_given  = given
                                , ic_wanted = wanted
                                , ic_info   = info })
-  = do { skols'  <- mapM zonkTcTyVarBndr skols  -- Need to zonk their kinds!
-                                                -- as Trac #7230 showed
+  = do { skols'  <- mapM zonkTcTyCoVarBndr skols  -- Need to zonk their kinds!
+                                                  -- as Trac #7230 showed
        ; given'  <- mapM zonkEvVar given
        ; info'   <- zonkSkolemInfo info
        ; wanted' <- zonkWCRec wanted
@@ -734,11 +1397,10 @@ zonkWC :: WantedConstraints -> TcM WantedConstraints
 zonkWC wc = zonkWCRec wc
 
 zonkWCRec :: WantedConstraints -> TcM WantedConstraints
-zonkWCRec (WC { wc_simple = simple, wc_impl = implic, wc_insol = insol })
+zonkWCRec (WC { wc_simple = simple, wc_impl = implic })
   = do { simple' <- zonkSimples simple
        ; implic' <- mapBagM zonkImplication implic
-       ; insol'  <- zonkSimples insol
-       ; return (WC { wc_simple = simple', wc_impl = implic', wc_insol = insol' }) }
+       ; return (WC { wc_simple = simple', wc_impl = implic' }) }
 
 zonkSimples :: Cts -> TcM Cts
 zonkSimples cts = do { cts' <- mapBagM zonkCt' cts
@@ -748,28 +1410,83 @@ zonkSimples cts = do { cts' <- mapBagM zonkCt' cts
 zonkCt' :: Ct -> TcM Ct
 zonkCt' ct = zonkCt ct
 
+{- Note [zonkCt behaviour]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+zonkCt tries to maintain the canonical form of a Ct.  For example,
+  - a CDictCan should stay a CDictCan;
+  - a CTyEqCan should stay a CTyEqCan (if the LHS stays as a variable.).
+  - a CHoleCan should stay a CHoleCan
+  - a CIrredCan should stay a CIrredCan with its cc_insol flag intact
+
+Why?, for example:
+- For CDictCan, the @TcSimplify.expandSuperClasses@ step, which runs after the
+  simple wanted and plugin loop, looks for @CDictCan@s. If a plugin is in use,
+  constraints are zonked before being passed to the plugin. This means if we
+  don't preserve a canonical form, @expandSuperClasses@ fails to expand
+  superclasses. This is what happened in Trac #11525.
+
+- For CHoleCan, once we forget that it's a hole, we can never recover that info.
+
+- For CIrredCan we want to see if a constraint is insoluble with insolubleWC
+
+NB: we do not expect to see any CFunEqCans, because zonkCt is only
+called on unflattened constraints.
+
+NB: Constraints are always re-flattened etc by the canonicaliser in
+@TcCanonical@ even if they come in as CDictCan. Only canonical constraints that
+are actually in the inert set carry all the guarantees. So it is okay if zonkCt
+creates e.g. a CDictCan where the cc_tyars are /not/ function free.
+-}
+
 zonkCt :: Ct -> TcM Ct
 zonkCt ct@(CHoleCan { cc_ev = ev })
   = do { ev' <- zonkCtEvidence ev
        ; return $ ct { cc_ev = ev' } }
+
+zonkCt ct@(CDictCan { cc_ev = ev, cc_tyargs = args })
+  = do { ev'   <- zonkCtEvidence ev
+       ; args' <- mapM zonkTcType args
+       ; return $ ct { cc_ev = ev', cc_tyargs = args' } }
+
+zonkCt ct@(CTyEqCan { cc_ev = ev, cc_tyvar = tv, cc_rhs = rhs })
+  = do { ev'    <- zonkCtEvidence ev
+       ; tv_ty' <- zonkTcTyVar tv
+       ; case getTyVar_maybe tv_ty' of
+           Just tv' -> do { rhs' <- zonkTcType rhs
+                          ; return ct { cc_ev    = ev'
+                                      , cc_tyvar = tv'
+                                      , cc_rhs   = rhs' } }
+           Nothing  -> return (mkNonCanonical ev') }
+
+zonkCt ct@(CIrredCan { cc_ev = ev }) -- Preserve the cc_insol flag
+  = do { ev' <- zonkCtEvidence ev
+       ; return (ct { cc_ev = ev' }) }
+
 zonkCt ct
-  = do { fl' <- zonkCtEvidence (cc_ev ct)
+  = ASSERT( not (isCFunEqCan ct) )
+  -- We do not expect to see any CFunEqCans, because zonkCt is only called on
+  -- unflattened constraints.
+    do { fl' <- zonkCtEvidence (ctEvidence ct)
        ; return (mkNonCanonical fl') }
 
 zonkCtEvidence :: CtEvidence -> TcM CtEvidence
 zonkCtEvidence ctev@(CtGiven { ctev_pred = pred })
   = do { pred' <- zonkTcType pred
        ; return (ctev { ctev_pred = pred'}) }
-zonkCtEvidence ctev@(CtWanted { ctev_pred = pred })
+zonkCtEvidence ctev@(CtWanted { ctev_pred = pred, ctev_dest = dest })
   = do { pred' <- zonkTcType pred
-       ; return (ctev { ctev_pred = pred' }) }
+       ; let dest' = case dest of
+                       EvVarDest ev -> EvVarDest $ setVarType ev pred'
+                         -- necessary in simplifyInfer
+                       HoleDest h   -> HoleDest h
+       ; return (ctev { ctev_pred = pred', ctev_dest = dest' }) }
 zonkCtEvidence ctev@(CtDerived { ctev_pred = pred })
   = do { pred' <- zonkTcType pred
        ; return (ctev { ctev_pred = pred' }) }
 
 zonkSkolemInfo :: SkolemInfo -> TcM SkolemInfo
-zonkSkolemInfo (SigSkol cx ty)  = do { ty' <- zonkTcType ty
-                                     ; return (SigSkol cx ty') }
+zonkSkolemInfo (SigSkol cx ty tv_prs)  = do { ty' <- zonkTcType ty
+                                            ; return (SigSkol cx ty' tv_prs) }
 zonkSkolemInfo (InferSkol ntys) = do { ntys' <- mapM do_one ntys
                                      ; return (InferSkol ntys') }
   where
@@ -777,13 +1494,14 @@ zonkSkolemInfo (InferSkol ntys) = do { ntys' <- mapM do_one ntys
 zonkSkolemInfo skol_info = return skol_info
 
 {-
-************************************************************************
-*                                                                      *
+%************************************************************************
+%*                                                                      *
 \subsection{Zonking -- the main work-horses: zonkTcType, zonkTcTyVar}
 *                                                                      *
 *              For internal use only!                                  *
 *                                                                      *
 ************************************************************************
+
 -}
 
 -- zonkId is used *during* typechecking just to zonk the Id's type
@@ -792,85 +1510,100 @@ zonkId id
   = do { ty' <- zonkTcType (idType id)
        ; return (Id.setIdType id ty') }
 
+zonkCoVar :: CoVar -> TcM CoVar
+zonkCoVar = zonkId
+
+-- | A suitable TyCoMapper for zonking a type inside the knot, and
+-- before all metavars are filled in.
+zonkTcTypeMapper :: TyCoMapper () TcM
+zonkTcTypeMapper = TyCoMapper
+  { tcm_smart = True
+  , tcm_tyvar = const zonkTcTyVar
+  , tcm_covar = const (\cv -> mkCoVarCo <$> zonkTyCoVarKind cv)
+  , tcm_hole  = hole
+  , tcm_tybinder = \_env tv _vis -> ((), ) <$> zonkTcTyCoVarBndr tv }
+  where
+    hole :: () -> CoercionHole -> TcM Coercion
+    hole _ hole@(CoercionHole { ch_ref = ref, ch_co_var = cv })
+      = do { contents <- readTcRef ref
+           ; case contents of
+               Just co -> do { co' <- zonkCo co
+                             ; checkCoercionHole cv co' }
+               Nothing -> do { cv' <- zonkCoVar cv
+                             ; return $ HoleCo (hole { ch_co_var = cv' }) } }
+
+
 -- For unbound, mutable tyvars, zonkType uses the function given to it
 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
 --      type variable and zonks the kind too
-
 zonkTcType :: TcType -> TcM TcType
-zonkTcType ty
-  = go ty
-  where
-    go (TyConApp tc tys) = do tys' <- mapM go tys
-                              return (TyConApp tc tys')
-                -- Do NOT establish Type invariants, because
-                -- doing so is strict in the TyCOn.
-                -- See Note [Zonking inside the knot] in TcHsType
-
-    go (LitTy n)         = return (LitTy n)
-
-    go (FunTy arg res)   = do arg' <- go arg
-                              res' <- go res
-                              return (FunTy arg' res')
-
-    go (AppTy fun arg)   = do fun' <- go fun
-                              arg' <- go arg
-                              return (mkAppTy fun' arg')
-                -- NB the mkAppTy; we might have instantiated a
-                -- type variable to a type constructor, so we need
-                -- to pull the TyConApp to the top.
-                -- OK to do this because only strict in the structure
-                -- not in the TyCon.
-                -- See Note [Zonking inside the knot] in TcHsType
-
-        -- The two interesting cases!
-    go (TyVarTy tyvar) | isTcTyVar tyvar = zonkTcTyVar tyvar
-                       | otherwise       = TyVarTy <$> updateTyVarKindM go tyvar
-                -- Ordinary (non Tc) tyvars occur inside quantified types
-
-    go (ForAllTy tv ty) = do { tv' <- zonkTcTyVarBndr tv
-                             ; ty' <- go ty
-                             ; return (ForAllTy tv' ty') }
-
-zonkTcTyVarBndr :: TcTyVar -> TcM TcTyVar
--- A tyvar binder is never a unification variable (MetaTv),
--- rather it is always a skolems.  BUT it may have a kind
+zonkTcType = mapType zonkTcTypeMapper ()
+
+-- | "Zonk" a coercion -- really, just zonk any types in the coercion
+zonkCo :: Coercion -> TcM Coercion
+zonkCo = mapCoercion zonkTcTypeMapper ()
+
+zonkTcTyCoVarBndr :: TcTyCoVar -> TcM TcTyCoVar
+-- A tyvar binder is never a unification variable (TauTv),
+-- rather it is always a skolem. It *might* be a SigTv.
+-- (Because non-CUSK type declarations use SigTvs.)
+-- Regardless, it may have a kind
 -- that has not yet been zonked, and may include kind
 -- unification variables.
-zonkTcTyVarBndr tyvar
-  = ASSERT2( isImmutableTyVar tyvar, ppr tyvar ) do
+zonkTcTyCoVarBndr tyvar
+  | isSigTyVar tyvar
+  = tcGetTyVar "zonkTcTyCoVarBndr SigTv" <$> zonkTcTyVar tyvar
+
+  | otherwise
+    -- can't use isCoVar, because it looks at a TyCon. Argh.
+  = ASSERT2( isImmutableTyVar tyvar || (not $ isTyVar tyvar), pprTyVar tyvar )
     updateTyVarKindM zonkTcType tyvar
 
+zonkTcTyVarBinder :: TyVarBndr TcTyVar vis -> TcM (TyVarBndr TcTyVar vis)
+zonkTcTyVarBinder (TvBndr tv vis)
+  = do { tv' <- zonkTcTyCoVarBndr tv
+       ; return (TvBndr tv' vis) }
+
 zonkTcTyVar :: TcTyVar -> TcM TcType
 -- Simply look through all Flexis
 zonkTcTyVar tv
-  = ASSERT2( isTcTyVar tv, ppr tv ) do
-    case tcTyVarDetails tv of
+  | isTcTyVar tv
+  = case tcTyVarDetails tv of
       SkolemTv {}   -> zonk_kind_and_return
       RuntimeUnk {} -> zonk_kind_and_return
-      FlatSkol ty   -> zonkTcType ty
       MetaTv { mtv_ref = ref }
          -> do { cts <- readMutVar ref
                ; case cts of
                     Flexi       -> zonk_kind_and_return
                     Indirect ty -> zonkTcType ty }
-  where
-    zonk_kind_and_return = do { z_tv <- zonkTyVarKind tv
-                              ; return (TyVarTy z_tv) }
 
-{-
-************************************************************************
-*                                                                      *
-                        Zonking kinds
-*                                                                      *
-************************************************************************
--}
-
-zonkTcKind :: TcKind -> TcM TcKind
-zonkTcKind k = zonkTcType k
+  | otherwise -- coercion variable
+  = zonk_kind_and_return
+  where
+    zonk_kind_and_return = do { z_tv <- zonkTyCoVarKind tv
+                              ; return (mkTyVarTy z_tv) }
+
+-- Variant that assumes that any result of zonking is still a TyVar.
+-- Should be used only on skolems and SigTvs
+zonkTcTyVarToTyVar :: HasDebugCallStack => TcTyVar -> TcM TcTyVar
+zonkTcTyVarToTyVar tv
+  = do { ty <- zonkTcTyVar tv
+       ; let tv' = case tcGetTyVar_maybe ty of
+                     Just tv' -> tv'
+                     Nothing  -> pprPanic "zonkTcTyVarToTyVar"
+                                          (ppr tv $$ ppr ty)
+       ; return tv' }
+
+zonkSigTyVarPairs :: [(Name,TcTyVar)] -> TcM [(Name,TcTyVar)]
+zonkSigTyVarPairs prs
+  = mapM do_one prs
+  where
+    do_one (nm, tv) = do { tv' <- zonkTcTyVarToTyVar tv
+                         ; return (nm, tv') }
 
 {-
-************************************************************************
-*                                                                      *
+%************************************************************************
+%*                                                                      *
                  Tidying
 *                                                                      *
 ************************************************************************
@@ -880,20 +1613,31 @@ zonkTidyTcType :: TidyEnv -> TcType -> TcM (TidyEnv, TcType)
 zonkTidyTcType env ty = do { ty' <- zonkTcType ty
                            ; return (tidyOpenType env ty') }
 
+zonkTidyTcTypes :: TidyEnv -> [TcType] -> TcM (TidyEnv, [TcType])
+zonkTidyTcTypes = zonkTidyTcTypes' []
+  where zonkTidyTcTypes' zs env [] = return (env, reverse zs)
+        zonkTidyTcTypes' zs env (ty:tys)
+          = do { (env', ty') <- zonkTidyTcType env ty
+               ; zonkTidyTcTypes' (ty':zs) env' tys }
+
 zonkTidyOrigin :: TidyEnv -> CtOrigin -> TcM (TidyEnv, CtOrigin)
 zonkTidyOrigin env (GivenOrigin skol_info)
   = do { skol_info1 <- zonkSkolemInfo skol_info
-       ; let (env1, skol_info2) = tidySkolemInfo env skol_info1
-       ; return (env1, GivenOrigin skol_info2) }
-zonkTidyOrigin env (TypeEqOrigin { uo_actual = act, uo_expected = exp })
+       ; let skol_info2 = tidySkolemInfo env skol_info1
+       ; return (env, GivenOrigin skol_info2) }
+zonkTidyOrigin env orig@(TypeEqOrigin { uo_actual   = act
+                                      , uo_expected = exp })
   = do { (env1, act') <- zonkTidyTcType env  act
        ; (env2, exp') <- zonkTidyTcType env1 exp
-       ; return ( env2, TypeEqOrigin { uo_actual = act', uo_expected = exp' }) }
-zonkTidyOrigin env (KindEqOrigin ty1 ty2 orig)
-  = do { (env1, ty1') <- zonkTidyTcType env  ty1
-       ; (env2, ty2') <- zonkTidyTcType env1 ty2
-       ; (env3, orig') <- zonkTidyOrigin env2 orig
-       ; return (env3, KindEqOrigin ty1' ty2' orig') }
+       ; return ( env2, orig { uo_actual   = act'
+                             , uo_expected = exp' }) }
+zonkTidyOrigin env (KindEqOrigin ty1 m_ty2 orig t_or_k)
+  = do { (env1, ty1')   <- zonkTidyTcType env  ty1
+       ; (env2, m_ty2') <- case m_ty2 of
+                             Just ty2 -> second Just <$> zonkTidyTcType env1 ty2
+                             Nothing  -> return (env1, Nothing)
+       ; (env3, orig')  <- zonkTidyOrigin env2 orig
+       ; return (env3, KindEqOrigin ty1' m_ty2' orig' t_or_k) }
 zonkTidyOrigin env (FunDepOrigin1 p1 l1 p2 l2)
   = do { (env1, p1') <- zonkTidyTcType env  p1
        ; (env2, p2') <- zonkTidyTcType env1 p2
@@ -930,25 +1674,89 @@ tidyEvVar :: TidyEnv -> EvVar -> EvVar
 tidyEvVar env var = setVarType var (tidyType env (varType var))
 
 ----------------
-tidySkolemInfo :: TidyEnv -> SkolemInfo -> (TidyEnv, SkolemInfo)
-tidySkolemInfo env (SigSkol cx ty)
-  = (env', SigSkol cx ty')
+tidySkolemInfo :: TidyEnv -> SkolemInfo -> SkolemInfo
+tidySkolemInfo env (DerivSkol ty)         = DerivSkol (tidyType env ty)
+tidySkolemInfo env (SigSkol cx ty tv_prs) = tidySigSkol env cx ty tv_prs
+tidySkolemInfo env (InferSkol ids)        = InferSkol (mapSnd (tidyType env) ids)
+tidySkolemInfo env (UnifyForAllSkol ty)   = UnifyForAllSkol (tidyType env ty)
+tidySkolemInfo _   info                   = info
+
+tidySigSkol :: TidyEnv -> UserTypeCtxt
+            -> TcType -> [(Name,TcTyVar)] -> SkolemInfo
+-- We need to take special care when tidying SigSkol
+-- See Note [SigSkol SkolemInfo] in TcRnTypes
+tidySigSkol env cx ty tv_prs
+  = SigSkol cx (tidy_ty env ty) tv_prs'
   where
-    (env', ty') = tidyOpenType env ty
+    tv_prs' = mapSnd (tidyTyVarOcc env) tv_prs
+    inst_env = mkNameEnv tv_prs'
 
-tidySkolemInfo env (InferSkol ids)
-  = (env', InferSkol ids')
-  where
-    (env', ids') = mapAccumL do_one env ids
-    do_one env (name, ty) = (env', (name, ty'))
-       where
-         (env', ty') = tidyOpenType env ty
+    tidy_ty env (ForAllTy (TvBndr tv vis) ty)
+      = ForAllTy (TvBndr tv' vis) (tidy_ty env' ty)
+      where
+        (env', tv') = tidy_tv_bndr env tv
 
-tidySkolemInfo env (UnifyForAllSkol skol_tvs ty)
-  = (env1, UnifyForAllSkol skol_tvs' ty')
-  where
-    env1 = tidyFreeTyVars env (tyVarsOfType ty `delVarSetList` skol_tvs)
-    (env2, skol_tvs') = tidyTyVarBndrs env1 skol_tvs
-    ty'               = tidyType env2 ty
+    tidy_ty env (FunTy arg res)
+      = FunTy (tidyType env arg) (tidy_ty env res)
+
+    tidy_ty env ty = tidyType env ty
 
-tidySkolemInfo env info = (env, info)
+    tidy_tv_bndr :: TidyEnv -> TyVar -> (TidyEnv, TyVar)
+    tidy_tv_bndr env@(occ_env, subst) tv
+      | Just tv' <- lookupNameEnv inst_env (tyVarName tv)
+      = ((occ_env, extendVarEnv subst tv tv'), tv')
+
+      | otherwise
+      = tidyTyCoVarBndr env tv
+
+-------------------------------------------------------------------------
+{-
+%************************************************************************
+%*                                                                      *
+             Levity polymorphism checks
+*                                                                      *
+************************************************************************
+
+See Note [Levity polymorphism checking] in DsMonad
+
+-}
+
+-- | According to the rules around representation polymorphism
+-- (see https://ghc.haskell.org/trac/ghc/wiki/NoSubKinds), no binder
+-- can have a representation-polymorphic type. This check ensures
+-- that we respect this rule. It is a bit regrettable that this error
+-- occurs in zonking, after which we should have reported all errors.
+-- But it's hard to see where else to do it, because this can be discovered
+-- only after all solving is done. And, perhaps most importantly, this
+-- isn't really a compositional property of a type system, so it's
+-- not a terrible surprise that the check has to go in an awkward spot.
+ensureNotLevPoly :: Type  -- its zonked type
+                 -> SDoc  -- where this happened
+                 -> TcM ()
+ensureNotLevPoly ty doc
+  = whenNoErrs $   -- sometimes we end up zonking bogus definitions of type
+                   -- forall a. a. See, for example, test ghci/scripts/T9140
+    checkForLevPoly doc ty
+
+  -- See Note [Levity polymorphism checking] in DsMonad
+checkForLevPoly :: SDoc -> Type -> TcM ()
+checkForLevPoly = checkForLevPolyX addErr
+
+checkForLevPolyX :: Monad m
+                 => (SDoc -> m ())  -- how to report an error
+                 -> SDoc -> Type -> m ()
+checkForLevPolyX add_err extra ty
+  | isTypeLevPoly ty
+  = add_err (formatLevPolyErr ty $$ extra)
+  | otherwise
+  = return ()
+
+formatLevPolyErr :: Type  -- levity-polymorphic type
+                 -> SDoc
+formatLevPolyErr ty
+  = hang (text "A levity-polymorphic type is not allowed here:")
+       2 (vcat [ text "Type:" <+> pprWithTYPE tidy_ty
+               , text "Kind:" <+> pprWithTYPE tidy_ki ])
+  where
+    (tidy_env, tidy_ty) = tidyOpenType emptyTidyEnv ty
+    tidy_ki             = tidyType tidy_env (typeKind ty)