Fix #11334.
[ghc.git] / compiler / typecheck / TcMType.hs
index 2fffcd4..b905f53 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,73 +19,98 @@ module TcMType (
   newFlexiTyVar,
   newFlexiTyVarTy,              -- Kind -> TcM TcType
   newFlexiTyVarTys,             -- Int -> Kind -> TcM [TcType]
-  newReturnTyVar, newReturnTyVarTy,
+  newOpenFlexiTyVarTy,
   newMetaKindVar, newMetaKindVars,
-  mkTcTyVarName, cloneMetaTyVar,
+  cloneMetaTyVar,
+  newFmvTyVar, newFskTyVar,
 
-  newMetaTyVar, readMetaTyVar, writeMetaTyVar, writeMetaTyVarRef,
+  readMetaTyVar, writeMetaTyVar, writeMetaTyVarRef,
   newMetaDetails, isFilledMetaTyVar, isUnfilledMetaTyVar,
 
   --------------------------------
+  -- Expected types
+  ExpType(..), ExpSigmaType, ExpRhoType,
+  mkCheckExpType, newOpenInferExpType, readExpType, readExpType_maybe,
+  writeExpType, expTypeToType, checkingExpType_maybe, checkingExpType,
+  tauifyExpType,
+
+  --------------------------------
+  -- Creating fresh type variables for pm checking
+  genInstSkolTyVarsX,
+
+  --------------------------------
   -- Creating new evidence variables
-  newEvVar, newEvVars, newEq, newDict,
+  newEvVar, newEvVars, newDict,
+  newWanted, newWanteds,
+  emitWanted, emitWantedEq, emitWantedEvVar, emitWantedEvVars,
   newTcEvBinds, addTcEvBind,
 
+  newCoercionHole, fillCoercionHole, isFilledCoercionHole,
+  unpackCoercionHole, unpackCoercionHole_maybe,
+  checkCoercionHole,
+
   --------------------------------
   -- Instantiation
-  tcInstTyVars, tcInstTyVarX, newSigTyVar,
+  newMetaTyVars, newMetaTyVarX, newMetaSigTyVars,
+  newSigTyVar,
   tcInstType,
-  tcInstSkolTyVars, tcInstSuperSkolTyVarsX,
+  tcInstSkolTyVars, tcInstSkolTyVarsLoc, tcInstSuperSkolTyVarsX,
   tcInstSigTyVarsLoc, tcInstSigTyVars,
   tcInstSkolType,
   tcSkolDFunType, tcSuperSkolTyVars,
 
-  instSkolTyVars, freshenTyVarBndrs,
+  instSkolTyCoVars, freshenTyVarBndrs, freshenCoVarBndrsX,
 
   --------------------------------
   -- Zonking and tidying
-  zonkTcPredType, zonkTidyTcType, zonkTidyOrigin,
+  zonkTidyTcType, zonkTidyOrigin,
+  mkTypeErrorThing, mkTypeErrorThingArgs,
   tidyEvVar, tidyCt, tidySkolemInfo,
   skolemiseUnboundMetaTyVar,
-  zonkTcTyVar, zonkTcTyVars, zonkTyVarsAndFV, zonkTcTypeAndFV,
-  zonkQuantifiedTyVar, quantifyTyVars,
-  zonkTcTyVarBndr, zonkTcType, zonkTcTypes, zonkTcThetaType,
+  zonkTcTyVar, zonkTcTyVars, zonkTyCoVarsAndFV, zonkTcTypeAndFV,
+  zonkQuantifiedTyVar, zonkQuantifiedTyVarOrType, quantifyTyVars,
+  defaultKindVar,
+  zonkTcTyCoVarBndr, zonkTcTyBinder, zonkTcType, zonkTcTypes, zonkCo,
+  zonkTyCoVarKind, zonkTcTypeMapper,
 
-  zonkTcKind, defaultKindVarToStar,
   zonkEvVar, zonkWC, zonkSimples, zonkId, zonkCt, zonkSkolemInfo,
 
-  tcGetGlobalTyVars,
-
-  --------------------------------
-  -- (Named) Wildcards
-  newWildcardVar, newWildcardVarMetaKind
+  tcGetGlobalTyCoVars
   ) where
 
 #include "HsVersions.h"
 
 -- friends:
-import TypeRep
+import TyCoRep
 import TcType
 import Type
+import Kind
+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 PrelNames
-import DynFlags
 import Util
 import Outputable
 import FastString
 import SrcLoc
 import Bag
+import Pair
+import qualified GHC.LanguageExtensions as LangExt
 
 import Control.Monad
-import Data.List        ( partition, mapAccumL )
+import Maybes
+import Data.List        ( mapAccumL, partition )
+import Control.Arrow    ( second )
 
 {-
 ************************************************************************
@@ -104,8 +129,8 @@ kind_var_occ = mkOccName tvName "k"
 
 newMetaKindVar :: TcM TcKind
 newMetaKindVar = do { uniq <- newUnique
-                    ; details <- newMetaDetails (TauTv False)
-                    ; let kv = mkTcTyVar (mkKindName uniq) superKind details
+                    ; details <- newMetaDetails TauTv
+                    ; let kv = mkTcTyVar (mkKindName uniq) liftedTypeKind details
                     ; return (mkTyVarTy kv) }
 
 newMetaKindVars :: Int -> TcM [TcKind]
@@ -124,15 +149,56 @@ 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) }
-
-newEq :: TcType -> TcType -> TcM EvVar
-newEq ty1 ty2
-  = do { name <- newSysName (mkVarOccFS (fsLit "cobox"))
-       ; return (mkLocalId name (mkTcEqPred ty1 ty2)) }
+                 ; 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
+                            else EvVarDest <$> newEvVar pty
+       return $ CtWanted { ctev_dest = d
+                         , ctev_pred = pty
+                         , ctev_loc = loc }
+
+newWanteds :: CtOrigin -> ThetaType -> TcM [CtEvidence]
+newWanteds orig = mapM (newWanted orig Nothing)
+
+-- | 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
+       ; loc <- getCtLocM origin (Just t_or_k)
+       ; emitSimple $ mkNonCanonical $
+           CtWanted { ctev_pred = pty, ctev_dest = HoleDest hole, ctev_loc = loc }
+       ; return (mkHoleCo hole role ty1 ty2) }
+  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_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
@@ -143,9 +209,211 @@ predTypeOccName :: PredType -> OccName
 predTypeOccName ty = case classifyPredType ty of
     ClassPred cls _ -> mkDictOcc (getOccName cls)
     EqPred _ _ _    -> mkVarOccFS (fsLit "cobox")
-    TuplePred _     -> mkVarOccFS (fsLit "tup")
     IrredPred _     -> mkVarOccFS (fsLit "irred")
 
+{-
+************************************************************************
+*                                                                      *
+        Coercion holes
+*                                                                      *
+************************************************************************
+-}
+
+newCoercionHole :: TcM CoercionHole
+newCoercionHole
+  = do { u <- newUnique
+       ; traceTc "New coercion hole:" (ppr u)
+       ; ref <- newMutVar Nothing
+       ; return $ CoercionHole u ref }
+
+-- | Put a value in a coercion hole
+fillCoercionHole :: CoercionHole -> Coercion -> TcM ()
+fillCoercionHole (CoercionHole u ref) co
+  = do {
+#ifdef DEBUG
+       ; cts <- readTcRef ref
+       ; whenIsJust cts $ \old_co ->
+         pprPanic "Filling a filled coercion hole" (ppr u $$ ppr co $$ ppr old_co)
+#endif
+       ; traceTc "Filling coercion hole" (ppr u <+> text ":=" <+> ppr co)
+       ; writeTcRef ref (Just co) }
+
+-- | Is a coercion hole filled in?
+isFilledCoercionHole :: CoercionHole -> TcM Bool
+isFilledCoercionHole (CoercionHole _ 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 _ 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 :: Coercion -> CoercionHole -> Role -> Type -> Type -> TcM Coercion
+checkCoercionHole co h r t1 t2
+-- co is already zonked, but t1 and t2 might not be
+  | debugIsOn
+  = do { t1 <- zonkTcType t1
+       ; t2 <- zonkTcType t2
+       ; let (Pair _t1 _t2, _role) = coercionKindRole co
+       ; return $
+         ASSERT2( t1 `eqType` _t1 && t2 `eqType` _t2 && r == _role
+                , (text "Bad coercion hole" <+>
+                   ppr h <> colon <+> vcat [ ppr _t1, ppr _t2, ppr _role
+                                           , ppr co, ppr t1, ppr t2
+                                           , ppr r ]) )
+         co }
+  | otherwise
+  = return co
+
+{-
+************************************************************************
+*
+    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 #.
+newOpenInferExpType :: TcM ExpType
+newOpenInferExpType
+  = do { rr <- newFlexiTyVarTy runtimeRepTy
+       ; u <- newUnique
+       ; tclvl <- getTcLevel
+       ; let ki = tYPE rr
+       ; traceTc "newOpenInferExpType" (ppr u <+> dcolon <+> ppr ki)
+       ; ref <- newMutVar Nothing
+       ; return (Infer u tclvl ki ref) }
+
+-- | 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 _ _ _ 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) }
+
+-- | Write into an 'ExpType'. It must be an 'Infer'.
+writeExpType :: ExpType -> TcType -> TcM ()
+writeExpType (Infer u tc_lvl ki ref) ty
+  | debugIsOn
+  = do { ki1 <- zonkTcType (typeKind ty)
+       ; ki2 <- zonkTcType ki
+       ; MASSERT2( ki1 `eqType` ki2, ppr ki1 $$ ppr ki2 $$ ppr u )
+       ; lvl_now <- getTcLevel
+       ; MASSERT2( tc_lvl == lvl_now, ppr u $$ ppr tc_lvl $$ ppr lvl_now )
+       ; cts <- readTcRef ref
+       ; case cts of
+           Just already_there -> pprPanic "writeExpType"
+                                   (vcat [ ppr u
+                                         , ppr ty
+                                         , ppr already_there ])
+           Nothing -> write }
+  | otherwise
+  = write
+  where
+    write = do { traceTc "Filling ExpType" $
+                   ppr u <+> text ":=" <+> ppr ty
+               ; writeTcRef ref (Just ty) }
+writeExpType (Check ty1) ty2 = pprPanic "writeExpType" (ppr ty1 $$ ppr ty2)
+
+-- | 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 unificaiton variable
+tauifyExpType exp_ty = do { ty <- expTypeToType exp_ty
+                          ; 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 u tc_lvl ki ref)
+  = do { uniq <- newUnique
+       ; tv_ref <- newMutVar Flexi
+       ; let details = MetaTv { mtv_info = TauTv
+                              , mtv_ref  = tv_ref
+                              , mtv_tclvl = tc_lvl }
+             name   = mkMetaTyVarName uniq (fsLit "t")
+             tau_tv = mkTcTyVar name ki details
+             tau    = mkTyVarTy tau_tv
+             -- can't use newFlexiTyVarTy because we need to set the tc_lvl
+             -- See also Note [TcLevel of ExpType]
+
+       ; writeMutVar ref (Just tau)
+       ; traceTc "Forcing ExpType to be monomorphic:"
+                 (ppr u <+> dcolon <+> ppr ki <+> text ":=" <+> ppr tau)
+       ; return tau }
 
 {-
 ************************************************************************
@@ -155,20 +423,21 @@ predTypeOccName ty = case classifyPredType ty of
 ************************************************************************
 -}
 
-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 :: ([TyVar] -> TcM (TCvSubst, [TcTyVar]))
+                   -- ^ How to instantiate the type variables
+           -> TcType                                  -- ^ Type to instantiate
+           -> TcM ([TcTyVar], TcThetaType, TcType)  -- ^ Result
+                -- (type vars, preds (incl equalities), rho)
 tcInstType inst_tyvars ty
   = case tcSplitForAllTys ty of
-        ([],     rho) -> let    -- There may be overloading despite no type variables;
+        ([],    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)
+                            ; let (theta, tau) = tcSplitPhiTy (substTyUnchecked subst rho)
                             ; return (tyvars', theta, tau) }
 
 tcSkolDFunType :: Type -> TcM ([TcTyVar], TcThetaType, TcType)
@@ -176,36 +445,41 @@ tcSkolDFunType :: Type -> TcM ([TcTyVar], TcThetaType, TcType)
 -- We could give them fresh names, but no need to do so
 tcSkolDFunType ty = tcInstType tcInstSuperSkolTyVars ty
 
-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
+-- Wrappers
+-- we need to be able to do this from outside the TcM monad:
+tcInstSkolTyVarsLoc :: SrcSpan -> [TyVar] -> TcRnIf gbl lcl (TCvSubst, [TcTyVar])
+tcInstSkolTyVarsLoc loc = instSkolTyCoVars (mkTcSkolTyVar loc False)
+
+tcInstSkolTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
+tcInstSkolTyVars = tcInstSkolTyVars' False emptyTCvSubst
 
-tcInstSuperSkolTyVars :: [TyVar] -> TcM (TvSubst, [TcTyVar])
-tcInstSuperSkolTyVars = tcInstSuperSkolTyVarsX emptyTvSubst
+tcInstSuperSkolTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
+tcInstSuperSkolTyVars = tcInstSuperSkolTyVarsX emptyTCvSubst
 
-tcInstSuperSkolTyVarsX :: TvSubst -> [TyVar] -> TcM (TvSubst, [TcTyVar])
+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 }
+       ; instSkolTyCoVarsX (mkTcSkolTyVar loc overlappable) subst tvs }
 
 mkTcSkolTyVar :: SrcSpan -> Bool -> Unique -> Name -> Kind -> TcTyVar
 mkTcSkolTyVar loc overlappable uniq old_name kind
@@ -213,14 +487,15 @@ mkTcSkolTyVar loc overlappable uniq old_name kind
               kind
               (SkolemTv overlappable)
 
-tcInstSigTyVarsLoc :: SrcSpan -> [TyVar] -> TcRnIf gbl lcl (TvSubst, [TcTyVar])
+tcInstSigTyVarsLoc :: SrcSpan -> [TyVar]
+                   -> TcRnIf gbl lcl (TCvSubst, [TcTyVar])
 -- We specify the location
-tcInstSigTyVarsLoc loc = instSkolTyVars (mkTcSkolTyVar loc False)
+tcInstSigTyVarsLoc loc = instSkolTyCoVars (mkTcSkolTyVar loc False)
 
-tcInstSigTyVars :: [TyVar] -> TcRnIf gbl lcl (TvSubst, [TcTyVar])
+tcInstSigTyVars :: [TyVar] -> TcRnIf gbl lcl (TCvSubst, [TcTyVar])
 -- Get the location from the TyVar itself, not the monad
 tcInstSigTyVars
-  = instSkolTyVars mk_tv
+  = instSkolTyCoVars mk_tv
   where
     mk_tv uniq old_name kind
        = mkTcTyVar (setNameUnique old_name uniq) kind (SkolemTv False)
@@ -231,48 +506,65 @@ tcInstSkolType :: TcType -> TcM ([TcTyVar], TcThetaType, TcType)
 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
 
-------------------
-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)
+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 uniq old_name kind = mkCoVar (setNameUnique old_name uniq) kind
 
-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) }
+------------------
+instSkolTyCoVars :: (Unique -> Name -> Kind -> TyCoVar)
+                 -> [TyVar] -> TcRnIf gbl lcl (TCvSubst, [TyCoVar])
+instSkolTyCoVars mk_tcv = instSkolTyCoVarsX mk_tcv emptyTCvSubst
+
+instSkolTyCoVarsX :: (Unique -> Name -> Kind -> TyCoVar)
+                  -> TCvSubst -> [TyCoVar] -> TcRnIf gbl lcl (TCvSubst, [TyCoVar])
+instSkolTyCoVarsX mk_tcv = mapAccumLM (instSkolTyCoVarX mk_tcv)
+
+instSkolTyCoVarX :: (Unique -> Name -> Kind -> TyCoVar)
+                 -> TCvSubst -> TyCoVar -> TcRnIf gbl lcl (TCvSubst, TyCoVar)
+instSkolTyCoVarX mk_tcv subst tycovar
+  = do  { uniq <- newUnique  -- using a new unique is critical. See
+                             -- Note [Skolems in zonkSyntaxExpr] in TcHsSyn
+        ; let new_tcv = mk_tcv uniq old_name kind
+              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
+       ; let name = mkSysTvName uniq (fsLit "fsk")
+       ; return (mkTcTyVar name (typeKind fam_ty) (FlatSkol fam_ty)) }
 {-
 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)]
 
 
 ************************************************************************
@@ -282,40 +574,37 @@ 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 True  -> fsLit "w"
-                        TauTv False -> fsLit "t"
-                        FlatMetaTv  -> fsLit "fmv"
-                        SigTv       -> fsLit "a"
-        ; details <- newMetaDetails meta_info
-        ; return (mkTcTyVar name kind details) }
-
-newNamedMetaTyVar :: Name -> MetaInfo -> Kind -> TcM TcTyVar
--- Make a new meta tyvar out of thin air
-newNamedMetaTyVar name meta_info kind
-  = do { details <- newMetaDetails meta_info
-       ; return (mkTcTyVar name kind details) }
+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 = mkSysTvName uniq str
 
 newSigTyVar :: Name -> Kind -> TcM TcTyVar
 newSigTyVar name kind
+  = do { details <- newMetaDetails SigTv
+       ; return (mkTcTyVar name kind details) }
+
+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
-       ; let name' = setNameUnique name uniq
-                      -- Use the same OccName so that the tidy-er
-                      -- doesn't gratuitously rename 'a' to 'a0' etc
-       ; details <- newMetaDetails SigTv
-       ; return (mkTcTyVar name' kind details) }
+       ; ref  <- newMutVar Flexi
+       ; cur_lvl <- getTcLevel
+       ; let details = MetaTv { mtv_info  = FlatMetaTv
+                              , mtv_ref   = ref
+                              , mtv_tclvl = fmvTcLevel cur_lvl }
+             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
@@ -328,11 +617,6 @@ cloneMetaTyVar tv
                            _ -> pprPanic "cloneMetaTyVar" (ppr tv)
         ; return (mkTcTyVar name' (tyVarKind tv) details') }
 
-mkTcTyVarName :: Unique -> FastString -> Name
--- Make sure that fresh TcTyVar names finish with a digit
--- leaving the un-cluttered names free for user names
-mkTcTyVarName uniq str = mkSysTvName uniq str
-
 -- Works for both type and kind variables
 readMetaTyVar :: TyVar -> TcM MetaDetails
 readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
@@ -341,7 +625,6 @@ readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr 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) }
@@ -350,7 +633,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) }
@@ -383,15 +665,16 @@ 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
   | 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_kind <- zonkTcType ty_kind
 
        -- Check for double updates
        ; ASSERT2( isFlexi meta_details,
@@ -402,7 +685,7 @@ writeMetaTyVarRef tyvar ref 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))
+               && not (zonked_ty_kind `tcEqKind` 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 ":="
@@ -413,52 +696,105 @@ writeMetaTyVarRef tyvar ref ty
     ty_kind = typeKind ty
 
 {-
+% Generating fresh variables for pattern match check
+-}
+
+-- UNINSTANTIATED VERSION OF tcInstSkolTyCoVars
+genInstSkolTyVarsX :: SrcSpan -> TCvSubst -> [TyVar]
+                   -> TcRnIf gbl lcl (TCvSubst, [TcTyVar])
+-- Precondition: tyvars should be scoping-ordered
+-- see Note [Kind substitution when instantiating]
+-- Get the location from the monad; this is a complete freshening operation
+genInstSkolTyVarsX loc subst tvs = instSkolTyCoVarsX (mkTcSkolTyVar loc False) subst tvs
+
+{-
 ************************************************************************
 *                                                                      *
         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!
 -}
 
+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"
+                        SigTv       -> fsLit "a"
+        ; details <- newMetaDetails meta_info
+        ; return (mkTcTyVar name kind details) }
+
 newFlexiTyVar :: Kind -> TcM TcTyVar
-newFlexiTyVar kind = newMetaTyVar (TauTv False) kind
+newFlexiTyVar kind = newAnonMetaTyVar TauTv kind
 
 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
+-- | Create a tyvar that can be a lifted or unlifted type.
+newOpenFlexiTyVarTy :: TcM TcType
+newOpenFlexiTyVarTy
+  = do { rr <- newFlexiTyVarTy runtimeRepTy
+       ; newFlexiTyVarTy (tYPE rr) }
 
-newReturnTyVarTy :: Kind -> TcM TcType
-newReturnTyVarTy kind = TyVarTy <$> newReturnTyVar kind
+newMetaSigTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
+newMetaSigTyVars = mapAccumLM newMetaSigTyVarX emptyTCvSubst
 
-tcInstTyVars :: [TKVar] -> TcM (TvSubst, [TcTyVar])
+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
+
+newMetaSigTyVarX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
+-- Just like newMetaTyVarX, but make a SigTv
+newMetaSigTyVarX subst tyvar = new_meta_tv_x SigTv subst tyvar
+
+new_meta_tv_x :: MetaInfo -> TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
+new_meta_tv_x info subst tyvar
   = do  { uniq <- newUnique
-        ; details <- newMetaDetails (TauTv False)
+        ; details <- newMetaDetails info
         ; let name   = mkSystemName uniq (getOccName tyvar)
-              kind   = substTy subst (tyVarKind tyvar)
+                       -- See Note [Name of an instantiated type variable]
+              kind   = substTyUnchecked subst (tyVarKind tyvar)
               new_tv = mkTcTyVar name kind details
-        ; return (extendTvSubst subst tyvar (mkTyVarTy new_tv), new_tv) }
+              subst1 = extendTvSubstWithClone subst tyvar new_tv
+        ; return (subst1, 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.
 
-{-
 ************************************************************************
 *                                                                      *
              Quantification
@@ -467,66 +803,96 @@ tcInstTyVarX subst tyvar
 
 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).
+
+This function bothers to distinguish between dependent and non-dependent
+variables only to keep correct defaulting behavior with -XNoPolyKinds.
+With -XPolyKinds, it treats both classes of variables identically.
+
+Note that this function can accept covars, but will never return them.
+This is because we never want to infer a quantified covar!
 -}
 
-quantifyTyVars :: TcTyVarSet -> TcTyVarSet -> TcM [TcTyVar]
+quantifyTyVars :: TcTyCoVarSet   -- global tvs
+               -> Pair TcTyCoVarSet    -- dependent tvs       We only distinguish
+                                       -- nondependent tvs    between these for
+                                       --                     -XNoPolyKinds
+               -> 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
+--   associated type declarations. Also accepts covars, but *never* returns any.
+
+quantifyTyVars gbl_tvs (Pair dep_tkvs nondep_tkvs)
+  = do { dep_tkvs    <- zonkTyCoVarsAndFV dep_tkvs
+       ; nondep_tkvs <- (`minusVarSet` dep_tkvs) <$>
+                        zonkTyCoVarsAndFV nondep_tkvs
+       ; gbl_tvs     <- zonkTyCoVarsAndFV gbl_tvs
+
+       ; let all_cvs    = filterVarSet isCoVar $
+                          dep_tkvs `unionVarSet` nondep_tkvs `minusVarSet` gbl_tvs
+             dep_kvs    = varSetElemsWellScoped $
+                          dep_tkvs `minusVarSet` gbl_tvs
+                                   `minusVarSet` (closeOverKinds all_cvs)
+                             -- remove any tvs that a covar depends on
 
-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
+             nondep_tvs = varSetElemsWellScoped $
+                          nondep_tkvs `minusVarSet` gbl_tvs
+                           -- no worry about dependent cvs here, as these vars
+                           -- are non-dependent
+
+                          -- 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_vars2 <- if poly_kinds
+                      then return dep_kvs
+                      else do { let (meta_kvs, skolem_kvs) = partition is_meta dep_kvs
+                                    is_meta kv = isTcTyVar kv && isMetaTyVar kv
+
+                              ; mapM_ defaultKindVar meta_kvs
+                              ; return skolem_kvs }  -- should be empty
+
+       ; let quant_vars = dep_vars2 ++ nondep_tvs
+
+       ; traceTc "quantifyTyVars"
+           (vcat [ text "globals:" <+> ppr gbl_tvs
+                 , text "nondep:" <+> ppr nondep_tvs
+                 , text "dep:" <+> ppr dep_kvs
+                 , text "dep2:" <+> ppr dep_vars2
+                 , text "quant_vars:" <+> ppr quant_vars ])
+
+       ; mapMaybeM zonk_quant quant_vars }
            -- Because of the order, any kind variables
            -- mentioned in the kinds of the type variables refer to
            -- the now-quantified versions
   where
     zonk_quant tkv
       | isTcTyVar tkv = zonkQuantifiedTyVar tkv
-      | otherwise     = return tkv
+      | otherwise     = return $ Just tkv
       -- For associated types, we have the class variables
       -- in scope, and they are TyVars not TcTyVars
 
-zonkQuantifiedTyVar :: TcTyVar -> TcM TcTyVar
+zonkQuantifiedTyVar :: TcTyVar -> TcM (Maybe 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
+-- default their kind (e.g. from TYPE v to TYPE Lifted)
 -- 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.
@@ -535,11 +901,24 @@ 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 }
+--
+-- This returns a tyvar if it should be quantified over; otherwise,
+-- it returns Nothing. Nothing is
+-- returned only if zonkQuantifiedTyVar is passed a RuntimeRep meta-tyvar,
+-- in order to default to PtrRepLifted.
+zonkQuantifiedTyVar tv = left_only `liftM` zonkQuantifiedTyVarOrType tv
+  where left_only :: Either a b -> Maybe a
+        left_only (Left x) =  Just x
+        left_only (Right _) = Nothing
+
+-- | Like zonkQuantifiedTyVar, but if zonking reveals that the tyvar
+-- should become a type (when defaulting a RuntimeRep var to PtrRepLifted), it
+-- returns the type instead.
+zonkQuantifiedTyVarOrType :: TcTyVar -> TcM (Either TcTyVar TcType)
+zonkQuantifiedTyVarOrType tv
+  = case tcTyVarDetails tv of
+      SkolemTv {} -> do { kind <- zonkTcType (tyVarKind tv)
+                        ; return $ Left $ setTyVarKind tv kind }
         -- It might be a skolem type variable,
         -- for example from a user type signature
 
@@ -552,19 +931,33 @@ zonkQuantifiedTyVar tv
                      Flexi -> return ()
                      Indirect ty -> WARN( True, ppr tv $$ ppr ty )
                                     return ()
-             skolemiseUnboundMetaTyVar tv vanillaSkolemTv
+             if isRuntimeRepVar tv
+             then do { writeMetaTyVar tv ptrRepLiftedTy
+                     ; return (Right ptrRepLiftedTy) }
+             else Left `liftM` 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 }
+-- | Take an (unconstrained) meta tyvar and default it. Works only on
+-- vars of type RuntimeRep and of type *. For other kinds, it issues
+-- an error. See Note [Defaulting with -XNoPolyKinds]
+defaultKindVar :: TcTyVar -> TcM Kind
+defaultKindVar kv
+  | ASSERT( isMetaTyVar kv )
+    isRuntimeRepVar kv
+  = writeMetaTyVar kv ptrRepLiftedTy >> return ptrRepLiftedTy
+  | isStarKind (tyVarKind kv)
+  = writeMetaTyVar kv liftedTypeKind >> return liftedTypeKind
+  | otherwise
+  = do { 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" ])
+       ; return (mkTyVarTy kv) }
+  where
+    (_, kv') = tidyOpenTyCoVar emptyTidyEnv kv
 
 skolemiseUnboundMetaTyVar :: 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]
@@ -572,27 +965,90 @@ skolemiseUnboundMetaTyVar tv details
   = ASSERT2( isMetaTyVar tv, ppr tv )
     do  { span <- getSrcSpanM    -- Get the location from "here"
                                  -- ie where we are generalising
-        ; uniq <- newUnique      -- Remove it from TcMetaTyVar unique land
-        ; kind <- zonkTcKind (tyVarKind tv)
-        ; let tv_name = getOccName tv
-              new_tv_name = if isWildcardVar tv
-                            then generaliseWildcardVarName tv_name
-                            else tv_name
-              final_name = mkInternalName uniq new_tv_name span
-              final_kind = defaultKind kind
-              final_tv   = mkTcTyVar final_name final_kind details
-
-        ; traceTc "Skolemising" (ppr tv <+> ptext (sLit ":=") <+> ppr final_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_tv    = mkTcTyVar final_name kind details
+
+        ; traceTc "Skolemising" (ppr tv <+> text ":=" <+> ppr final_tv)
         ; writeMetaTyVar tv (mkTyVarTy final_tv)
         ; return final_tv }
-  where
-    -- If a wildcard type called _a is generalised, we rename it to w_a
-    generaliseWildcardVarName :: OccName -> OccName
-    generaliseWildcardVarName name | startsWithUnderscore name
-      = mkOccNameFS (occNameSpace name) (appendFS (fsLit "w") (occNameFS name))
-    generaliseWildcardVarName name = name
 
 {-
+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 TcType. 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
@@ -665,58 +1121,59 @@ 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
+zonkTcTypeAndFV :: TcType -> TcM TyCoVarSet
 -- 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) }
+-- NB: This might be called from within the knot, so don't use
+-- smart constructors. See Note [Zonking within the knot] in TcHsType
+zonkTcTypeAndFV ty
+  = tyCoVarsOfType <$> mapType (zonkTcTypeMapper { tcm_smart = False }) () ty
 
-zonkTyVar :: TyVar -> TcM TcType
+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 (varSetElems 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
-
 {-
 ************************************************************************
 *                                                                      *
@@ -730,8 +1187,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
@@ -775,16 +1232,21 @@ 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)  = do { ty  <- readExpType ty
+                                     ; ty' <- zonkTcType ty
+                                     ; return (SigSkol cx (mkCheckExpType ty')) }
 zonkSkolemInfo (InferSkol ntys) = do { ntys' <- mapM do_one ntys
                                      ; return (InferSkol ntys') }
   where
@@ -792,13 +1254,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
@@ -807,59 +1270,58 @@ zonkId id
   = do { ty' <- zonkTcType (idType id)
        ; return (Id.setIdType id ty') }
 
+-- | 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 -> Role -> Type -> Type
+         -> TcM Coercion
+    hole _ h r t1 t2
+      = do { contents <- unpackCoercionHole_maybe h
+           ; case contents of
+               Just co -> do { co <- zonkCo co
+                             ; checkCoercionHole co h r t1 t2 }
+               Nothing -> do { t1 <- zonkTcType t1
+                             ; t2 <- zonkTcType t2
+                             ; return $ mkHoleCo h r t1 t2 } }
+
+
 -- 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
+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 (MetaTv),
 -- rather it is always a skolems.  BUT 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
+    -- can't use isCoVar, because it looks at a TyCon. Argh.
+  = ASSERT2( isImmutableTyVar tyvar || (not $ isTyVar tyvar), ppr tyvar ) do
     updateTyVarKindM zonkTcType tyvar
 
+-- | Zonk a TyBinder
+zonkTcTyBinder :: TcTyBinder -> TcM TcTyBinder
+zonkTcTyBinder (Anon ty)      = Anon <$> zonkTcType ty
+zonkTcTyBinder (Named tv vis) = Named <$> zonkTcTyCoVarBndr tv <*> pure 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
@@ -868,24 +1330,16 @@ zonkTcTyVar tv
                ; 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) }
 
 {-
-************************************************************************
-*                                                                      *
+%************************************************************************
+%*                                                                      *
                  Tidying
 *                                                                      *
 ************************************************************************
@@ -895,24 +1349,43 @@ zonkTidyTcType :: TidyEnv -> TcType -> TcM (TidyEnv, TcType)
 zonkTidyTcType env ty = do { ty' <- zonkTcType ty
                            ; return (tidyOpenType env ty') }
 
+-- | Make an 'ErrorThing' storing a type.
+mkTypeErrorThing :: TcType -> ErrorThing
+mkTypeErrorThing ty = ErrorThing ty (Just $ length $ snd $ repSplitAppTys ty)
+                                 zonkTidyTcType
+   -- NB: Use *rep*splitAppTys, else we get #11313
+
+-- | Make an 'ErrorThing' storing a type, with some extra args known about
+mkTypeErrorThingArgs :: TcType -> Int -> ErrorThing
+mkTypeErrorThingArgs ty num_args
+  = ErrorThing ty (Just $ (length $ snd $ repSplitAppTys ty) + num_args)
+               zonkTidyTcType
+
 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
+                                      , uo_thing    = m_thing })
   = 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') }
-zonkTidyOrigin env (CoercibleOrigin ty1 ty2)
-  = do { (env1, ty1') <- zonkTidyTcType env  ty1
-       ; (env2, ty2') <- zonkTidyTcType env1 ty2
-       ; return (env2, CoercibleOrigin ty1' ty2') }
+       ; mb_exp <- readExpType_maybe exp  -- it really should be filled in.
+                                          -- unless we're debugging.
+       ; (env2, exp') <- case mb_exp of
+           Just ty -> second mkCheckExpType <$> zonkTidyTcType env1 ty
+           Nothing -> return (env1, exp)
+       ; (env3, m_thing') <- zonkTidyErrorThing env2 m_thing
+       ; return ( env3, orig { uo_actual   = act'
+                             , uo_expected = exp'
+                             , uo_thing    = m_thing' }) }
+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
@@ -924,6 +1397,14 @@ zonkTidyOrigin env (FunDepOrigin2 p1 o1 p2 l2)
        ; return (env3, FunDepOrigin2 p1' o1' p2' l2) }
 zonkTidyOrigin env orig = return (env, orig)
 
+zonkTidyErrorThing :: TidyEnv -> Maybe ErrorThing
+                   -> TcM (TidyEnv, Maybe ErrorThing)
+zonkTidyErrorThing env (Just (ErrorThing thing n_args zonker))
+  = do { (env', thing') <- zonker env thing
+       ; return (env', Just $ ErrorThing thing' n_args zonker) }
+zonkTidyErrorThing env Nothing
+  = return (env, Nothing)
+
 ----------------
 tidyCt :: TidyEnv -> Ct -> Ct
 -- Used only in error reporting
@@ -949,53 +1430,11 @@ 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')
-  where
-    (env', ty') = tidyOpenType env ty
-
-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
-
-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
-
-tidySkolemInfo env info = (env, info)
-
-{-
-************************************************************************
-*                                                                      *
-        (Named) Wildcards
-*                                                                      *
-************************************************************************
--}
-
--- | Create a new meta var with the given kind. This meta var should be used
--- to replace a wildcard in a type. Such a wildcard meta var can be
--- distinguished from other meta vars with the 'isWildcardVar' function.
-newWildcardVar :: Name -> Kind -> TcM TcTyVar
-newWildcardVar name kind = newNamedMetaTyVar name (TauTv True) kind
-
--- | Create a new meta var (which can unify with a type of any kind). This
--- meta var should be used to replace a wildcard in a type. Such a wildcard
--- meta var can be distinguished from other meta vars with the 'isWildcardVar'
--- function.
-newWildcardVarMetaKind :: Name -> TcM TcTyVar
-newWildcardVarMetaKind name = do kind <- newMetaKindVar
-                                 newWildcardVar name kind
-
--- | Return 'True' if the argument is a meta var created for a wildcard (by
--- 'newWildcardVar' or 'newWildcardVarMetaKind').
-isWildcardVar :: TcTyVar -> Bool
-isWildcardVar tv | isTcTyVar tv, MetaTv (TauTv True) _ _ <- tcTyVarDetails tv = True
-isWildcardVar _ = False
+tidySkolemInfo :: TidyEnv -> SkolemInfo -> SkolemInfo
+tidySkolemInfo env (DerivSkol ty)       = DerivSkol (tidyType env ty)
+tidySkolemInfo env (SigSkol cx ty)      = SigSkol cx (mkCheckExpType $
+                                                      tidyType env $
+                                                      checkingExpType "tidySkolemInfo" ty)
+tidySkolemInfo env (InferSkol ids)      = InferSkol (mapSnd (tidyType env) ids)
+tidySkolemInfo env (UnifyForAllSkol ty) = UnifyForAllSkol (tidyType env ty)
+tidySkolemInfo _   info                 = info