never executed always true always false
    1 
    2 {-# LANGUAGE MultiWayIf      #-}
    3 {-# LANGUAGE TupleSections   #-}
    4 
    5 {-# OPTIONS_GHC -Wno-incomplete-record-updates #-}
    6 {-
    7 (c) The University of Glasgow 2006
    8 (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
    9 
   10 -}
   11 
   12 -- | Monadic type operations
   13 --
   14 -- This module contains monadic operations over types that contain mutable type
   15 -- variables.
   16 module GHC.Tc.Utils.TcMType (
   17   TcTyVar, TcKind, TcType, TcTauType, TcThetaType, TcTyVarSet,
   18 
   19   --------------------------------
   20   -- Creating new mutable type variables
   21   newFlexiTyVar,
   22   newNamedFlexiTyVar,
   23   newFlexiTyVarTy,              -- Kind -> TcM TcType
   24   newFlexiTyVarTys,             -- Int -> Kind -> TcM [TcType]
   25   newOpenFlexiTyVar, newOpenFlexiTyVarTy, newOpenTypeKind,
   26   newOpenBoxedTypeKind,
   27   newMetaKindVar, newMetaKindVars, newMetaTyVarTyAtLevel,
   28   newAnonMetaTyVar, cloneMetaTyVar,
   29   newCycleBreakerTyVar,
   30 
   31   newMultiplicityVar,
   32   readMetaTyVar, writeMetaTyVar, writeMetaTyVarRef,
   33   newTauTvDetailsAtLevel, newMetaDetails, newMetaTyVarName,
   34   isFilledMetaTyVar_maybe, isFilledMetaTyVar, isUnfilledMetaTyVar,
   35 
   36   --------------------------------
   37   -- Creating new evidence variables
   38   newEvVar, newEvVars, newDict,
   39   newWanted, newWanteds, cloneWanted, cloneWC,
   40   emitWanted, emitWantedEq, emitWantedEvVar, emitWantedEvVars,
   41   emitDerivedEqs,
   42   newTcEvBinds, newNoTcEvBinds, addTcEvBind,
   43   emitNewExprHole,
   44 
   45   newCoercionHole, fillCoercionHole, isFilledCoercionHole,
   46   unpackCoercionHole, unpackCoercionHole_maybe,
   47   checkCoercionHole,
   48 
   49   newImplication,
   50 
   51   --------------------------------
   52   -- Instantiation
   53   newMetaTyVars, newMetaTyVarX, newMetaTyVarsX,
   54   newMetaTyVarTyVarX,
   55   newTyVarTyVar, cloneTyVarTyVar,
   56   newPatSigTyVar, newSkolemTyVar, newWildCardX,
   57 
   58   --------------------------------
   59   -- Expected types
   60   ExpType(..), ExpSigmaType, ExpRhoType,
   61   mkCheckExpType, newInferExpType, tcInfer,
   62   readExpType, readExpType_maybe, readScaledExpType,
   63   expTypeToType, scaledExpTypeToType,
   64   checkingExpType_maybe, checkingExpType,
   65   inferResultToType, fillInferResult, promoteTcType,
   66 
   67   --------------------------------
   68   -- Zonking and tidying
   69   zonkTidyTcType, zonkTidyTcTypes, zonkTidyOrigin, zonkTidyOrigins,
   70   tidyEvVar, tidyCt, tidyHole, tidySkolemInfo,
   71     zonkTcTyVar, zonkTcTyVars,
   72   zonkTcTyVarToTyVar, zonkInvisTVBinder,
   73   zonkTyCoVarsAndFV, zonkTcTypeAndFV, zonkDTyCoVarSetAndFV,
   74   zonkTyCoVarsAndFVList,
   75 
   76   zonkTcType, zonkTcTypes, zonkCo,
   77   zonkTyCoVarKind, zonkTyCoVarKindBinder,
   78   zonkEvVar, zonkWC, zonkImplication, zonkSimples,
   79   zonkId, zonkCoVar,
   80   zonkCt, zonkSkolemInfo,
   81 
   82   ---------------------------------
   83   -- Promotion, defaulting, skolemisation
   84   defaultTyVar, promoteMetaTyVarTo, promoteTyVarSet,
   85   quantifyTyVars, isQuantifiableTv,
   86   skolemiseUnboundMetaTyVar, zonkAndSkolemise, skolemiseQuantifiedTyVar,
   87   doNotQuantifyTyVars,
   88 
   89   candidateQTyVarsOfType,  candidateQTyVarsOfKind,
   90   candidateQTyVarsOfTypes, candidateQTyVarsOfKinds,
   91   CandidatesQTvs(..), delCandidates,
   92   candidateKindVars, partitionCandidates,
   93 
   94   ------------------------------
   95   -- Representation polymorphism
   96   checkTypeHasFixedRuntimeRep,
   97   ) where
   98 
   99 import GHC.Prelude
  100 
  101 import GHC.Driver.Session
  102 import qualified GHC.LanguageExtensions as LangExt
  103 
  104 import GHC.Tc.Types.Origin
  105 import GHC.Tc.Utils.Monad        -- TcType, amongst others
  106 import GHC.Tc.Types.Constraint
  107 import GHC.Tc.Types.Evidence
  108 import {-# SOURCE #-} GHC.Tc.Utils.Unify( unifyType {- , unifyKind -} )
  109 import GHC.Tc.Utils.TcType
  110 import GHC.Tc.Errors.Types
  111 
  112 import GHC.Core.TyCo.Rep
  113 import GHC.Core.TyCo.Ppr
  114 import GHC.Core.Type
  115 import GHC.Core.TyCon
  116 import GHC.Core.Coercion
  117 import GHC.Core.Class
  118 import GHC.Core.Predicate
  119 import GHC.Core.InstEnv (ClsInst(is_tys))
  120 
  121 import GHC.Types.Var
  122 import GHC.Types.Id as Id
  123 import GHC.Types.Name
  124 import GHC.Types.Var.Set
  125 
  126 import GHC.Builtin.Types
  127 import GHC.Types.Error
  128 import GHC.Types.Var.Env
  129 import GHC.Types.Name.Env
  130 import GHC.Types.Unique.Set
  131 import GHC.Types.Basic ( TypeOrKind(..)
  132                        , DefaultKindVars(..), DefaultVarsOfKind(..), allVarsOfKindDefault )
  133 
  134 import GHC.Data.FastString
  135 import GHC.Data.Bag
  136 import GHC.Data.Pair
  137 
  138 import GHC.Utils.Misc
  139 import GHC.Utils.Outputable
  140 import GHC.Utils.Panic
  141 import GHC.Utils.Panic.Plain
  142 import GHC.Utils.Constants (debugIsOn)
  143 import GHC.Utils.Trace
  144 
  145 import Control.Monad
  146 import GHC.Data.Maybe
  147 import qualified Data.Semigroup as Semi
  148 
  149 {-
  150 ************************************************************************
  151 *                                                                      *
  152         Kind variables
  153 *                                                                      *
  154 ************************************************************************
  155 -}
  156 
  157 newMetaKindVar :: TcM TcKind
  158 newMetaKindVar
  159   = do { details <- newMetaDetails TauTv
  160        ; name    <- newMetaTyVarName (fsLit "k")
  161                     -- All MetaKindVars are called "k"
  162                     -- They may be jiggled by tidying
  163        ; let kv = mkTcTyVar name liftedTypeKind details
  164        ; traceTc "newMetaKindVar" (ppr kv)
  165        ; return (mkTyVarTy kv) }
  166 
  167 newMetaKindVars :: Int -> TcM [TcKind]
  168 newMetaKindVars n = replicateM n newMetaKindVar
  169 
  170 {-
  171 ************************************************************************
  172 *                                                                      *
  173      Evidence variables; range over constraints we can abstract over
  174 *                                                                      *
  175 ************************************************************************
  176 -}
  177 
  178 newEvVars :: TcThetaType -> TcM [EvVar]
  179 newEvVars theta = mapM newEvVar theta
  180 
  181 --------------
  182 
  183 newEvVar :: TcPredType -> TcRnIf gbl lcl EvVar
  184 -- Creates new *rigid* variables for predicates
  185 newEvVar ty = do { name <- newSysName (predTypeOccName ty)
  186                  ; return (mkLocalIdOrCoVar name Many ty) }
  187 
  188 newWanted :: CtOrigin -> Maybe TypeOrKind -> PredType -> TcM CtEvidence
  189 -- Deals with both equality and non-equality predicates
  190 newWanted orig t_or_k pty
  191   = do loc <- getCtLocM orig t_or_k
  192        d <- if isEqPrimPred pty then HoleDest  <$> newCoercionHole pty
  193                                 else EvVarDest <$> newEvVar pty
  194        return $ CtWanted { ctev_dest = d
  195                          , ctev_pred = pty
  196                          , ctev_nosh = WDeriv
  197                          , ctev_loc = loc }
  198 
  199 newWanteds :: CtOrigin -> ThetaType -> TcM [CtEvidence]
  200 newWanteds orig = mapM (newWanted orig Nothing)
  201 
  202 ----------------------------------------------
  203 -- Cloning constraints
  204 ----------------------------------------------
  205 
  206 cloneWanted :: Ct -> TcM Ct
  207 cloneWanted ct
  208   | ev@(CtWanted { ctev_pred = pty, ctev_dest = HoleDest _ }) <- ctEvidence ct
  209   = do { co_hole <- newCoercionHole pty
  210        ; return (mkNonCanonical (ev { ctev_dest = HoleDest co_hole })) }
  211   | otherwise
  212   = return ct
  213 
  214 cloneWC :: WantedConstraints -> TcM WantedConstraints
  215 -- Clone all the evidence bindings in
  216 --   a) the ic_bind field of any implications
  217 --   b) the CoercionHoles of any wanted constraints
  218 -- so that solving the WantedConstraints will not have any visible side
  219 -- effect, /except/ from causing unifications
  220 cloneWC wc@(WC { wc_simple = simples, wc_impl = implics })
  221   = do { simples' <- mapBagM cloneWanted simples
  222        ; implics' <- mapBagM cloneImplication implics
  223        ; return (wc { wc_simple = simples', wc_impl = implics' }) }
  224 
  225 cloneImplication :: Implication -> TcM Implication
  226 cloneImplication implic@(Implic { ic_binds = binds, ic_wanted = inner_wanted })
  227   = do { binds'        <- cloneEvBindsVar binds
  228        ; inner_wanted' <- cloneWC inner_wanted
  229        ; return (implic { ic_binds = binds', ic_wanted = inner_wanted' }) }
  230 
  231 ----------------------------------------------
  232 -- Emitting constraints
  233 ----------------------------------------------
  234 
  235 -- | Emits a new Wanted. Deals with both equalities and non-equalities.
  236 emitWanted :: CtOrigin -> TcPredType -> TcM EvTerm
  237 emitWanted origin pty
  238   = do { ev <- newWanted origin Nothing pty
  239        ; emitSimple $ mkNonCanonical ev
  240        ; return $ ctEvTerm ev }
  241 
  242 emitDerivedEqs :: CtOrigin -> [(TcType,TcType)] -> TcM ()
  243 -- Emit some new derived nominal equalities
  244 emitDerivedEqs origin pairs
  245   | null pairs
  246   = return ()
  247   | otherwise
  248   = do { loc <- getCtLocM origin Nothing
  249        ; emitSimples (listToBag (map (mk_one loc) pairs)) }
  250   where
  251     mk_one loc (ty1, ty2)
  252        = mkNonCanonical $
  253          CtDerived { ctev_pred = mkPrimEqPred ty1 ty2
  254                    , ctev_loc = loc }
  255 
  256 -- | Emits a new equality constraint
  257 emitWantedEq :: CtOrigin -> TypeOrKind -> Role -> TcType -> TcType -> TcM Coercion
  258 emitWantedEq origin t_or_k role ty1 ty2
  259   = do { hole <- newCoercionHole pty
  260        ; loc <- getCtLocM origin (Just t_or_k)
  261        ; emitSimple $ mkNonCanonical $
  262          CtWanted { ctev_pred = pty, ctev_dest = HoleDest hole
  263                   , ctev_nosh = WDeriv, ctev_loc = loc }
  264        ; return (HoleCo hole) }
  265   where
  266     pty = mkPrimEqPredRole role ty1 ty2
  267 
  268 -- | Creates a new EvVar and immediately emits it as a Wanted.
  269 -- No equality predicates here.
  270 emitWantedEvVar :: CtOrigin -> TcPredType -> TcM EvVar
  271 emitWantedEvVar origin ty
  272   = do { new_cv <- newEvVar ty
  273        ; loc <- getCtLocM origin Nothing
  274        ; let ctev = CtWanted { ctev_dest = EvVarDest new_cv
  275                              , ctev_pred = ty
  276                              , ctev_nosh = WDeriv
  277                              , ctev_loc  = loc }
  278        ; emitSimple $ mkNonCanonical ctev
  279        ; return new_cv }
  280 
  281 emitWantedEvVars :: CtOrigin -> [TcPredType] -> TcM [EvVar]
  282 emitWantedEvVars orig = mapM (emitWantedEvVar orig)
  283 
  284 -- | Emit a new wanted expression hole
  285 emitNewExprHole :: OccName         -- of the hole
  286                 -> Type -> TcM HoleExprRef
  287 emitNewExprHole occ ty
  288   = do { u <- newUnique
  289        ; ref <- newTcRef (pprPanic "unfilled unbound-variable evidence" (ppr u))
  290        ; let her = HER ref ty u
  291 
  292        ; loc <- getCtLocM (ExprHoleOrigin occ) (Just TypeLevel)
  293 
  294        ; let hole = Hole { hole_sort = ExprHole her
  295                          , hole_occ  = occ
  296                          , hole_ty   = ty
  297                          , hole_loc  = loc }
  298        ; emitHole hole
  299        ; return her }
  300 
  301 newDict :: Class -> [TcType] -> TcM DictId
  302 newDict cls tys
  303   = do { name <- newSysName (mkDictOcc (getOccName cls))
  304        ; return (mkLocalId name Many (mkClassPred cls tys)) }
  305 
  306 predTypeOccName :: PredType -> OccName
  307 predTypeOccName ty = case classifyPredType ty of
  308     ClassPred cls _ -> mkDictOcc (getOccName cls)
  309     EqPred {}       -> mkVarOccFS (fsLit "co")
  310     IrredPred {}    -> mkVarOccFS (fsLit "irred")
  311     ForAllPred {}   -> mkVarOccFS (fsLit "df")
  312     SpecialPred special_pred _ ->
  313       case special_pred of
  314         ConcretePrimPred -> mkVarOccFS (fsLit "concr")
  315 
  316 -- | Create a new 'Implication' with as many sensible defaults for its fields
  317 -- as possible. Note that the 'ic_tclvl', 'ic_binds', and 'ic_info' fields do
  318 -- /not/ have sensible defaults, so they are initialized with lazy thunks that
  319 -- will 'panic' if forced, so one should take care to initialize these fields
  320 -- after creation.
  321 --
  322 -- This is monadic to look up the 'TcLclEnv', which is used to initialize
  323 -- 'ic_env', and to set the -Winaccessible-code flag. See
  324 -- Note [Avoid -Winaccessible-code when deriving] in "GHC.Tc.TyCl.Instance".
  325 newImplication :: TcM Implication
  326 newImplication
  327   = do env <- getLclEnv
  328        warn_inaccessible <- woptM Opt_WarnInaccessibleCode
  329        return (implicationPrototype { ic_env = env
  330                                     , ic_warn_inaccessible = warn_inaccessible })
  331 
  332 {-
  333 ************************************************************************
  334 *                                                                      *
  335         Coercion holes
  336 *                                                                      *
  337 ************************************************************************
  338 -}
  339 
  340 newCoercionHole :: TcPredType -> TcM CoercionHole
  341 newCoercionHole pred_ty
  342   = do { co_var <- newEvVar pred_ty
  343        ; traceTc "New coercion hole:" (ppr co_var)
  344        ; ref <- newMutVar Nothing
  345        ; return $ CoercionHole { ch_co_var = co_var, ch_ref = ref } }
  346 
  347 -- | Put a value in a coercion hole
  348 fillCoercionHole :: CoercionHole -> Coercion -> TcM ()
  349 fillCoercionHole (CoercionHole { ch_ref = ref, ch_co_var = cv }) co = do
  350   when debugIsOn $ do
  351     cts <- readTcRef ref
  352     whenIsJust cts $ \old_co ->
  353       pprPanic "Filling a filled coercion hole" (ppr cv $$ ppr co $$ ppr old_co)
  354   traceTc "Filling coercion hole" (ppr cv <+> text ":=" <+> ppr co)
  355   writeTcRef ref (Just co)
  356 
  357 -- | Is a coercion hole filled in?
  358 isFilledCoercionHole :: CoercionHole -> TcM Bool
  359 isFilledCoercionHole (CoercionHole { ch_ref = ref }) = isJust <$> readTcRef ref
  360 
  361 -- | Retrieve the contents of a coercion hole. Panics if the hole
  362 -- is unfilled
  363 unpackCoercionHole :: CoercionHole -> TcM Coercion
  364 unpackCoercionHole hole
  365   = do { contents <- unpackCoercionHole_maybe hole
  366        ; case contents of
  367            Just co -> return co
  368            Nothing -> pprPanic "Unfilled coercion hole" (ppr hole) }
  369 
  370 -- | Retrieve the contents of a coercion hole, if it is filled
  371 unpackCoercionHole_maybe :: CoercionHole -> TcM (Maybe Coercion)
  372 unpackCoercionHole_maybe (CoercionHole { ch_ref = ref }) = readTcRef ref
  373 
  374 -- | Check that a coercion is appropriate for filling a hole. (The hole
  375 -- itself is needed only for printing.)
  376 -- Always returns the checked coercion, but this return value is necessary
  377 -- so that the input coercion is forced only when the output is forced.
  378 checkCoercionHole :: CoVar -> Coercion -> TcM Coercion
  379 checkCoercionHole cv co
  380   | debugIsOn
  381   = do { cv_ty <- zonkTcType (varType cv)
  382                   -- co is already zonked, but cv might not be
  383        ; return $
  384          assertPpr (ok cv_ty)
  385                    (text "Bad coercion hole" <+>
  386                     ppr cv <> colon <+> vcat [ ppr t1, ppr t2, ppr role
  387                                              , ppr cv_ty ])
  388          co }
  389   | otherwise
  390   = return co
  391 
  392   where
  393     (Pair t1 t2, role) = coercionKindRole co
  394     ok cv_ty | EqPred cv_rel cv_t1 cv_t2 <- classifyPredType cv_ty
  395              =  t1 `eqType` cv_t1
  396              && t2 `eqType` cv_t2
  397              && role == eqRelRole cv_rel
  398              | otherwise
  399              = False
  400 
  401 {- **********************************************************************
  402 *
  403                       ExpType functions
  404 *
  405 ********************************************************************** -}
  406 
  407 {- Note [ExpType]
  408 ~~~~~~~~~~~~~~~~~
  409 An ExpType is used as the "expected type" when type-checking an expression.
  410 An ExpType can hold a "hole" that can be filled in by the type-checker.
  411 This allows us to have one tcExpr that works in both checking mode and
  412 synthesis mode (that is, bidirectional type-checking). Previously, this
  413 was achieved by using ordinary unification variables, but we don't need
  414 or want that generality. (For example, #11397 was caused by doing the
  415 wrong thing with unification variables.) Instead, we observe that these
  416 holes should
  417 
  418 1. never be nested
  419 2. never appear as the type of a variable
  420 3. be used linearly (never be duplicated)
  421 
  422 By defining ExpType, separately from Type, we can achieve goals 1 and 2
  423 statically.
  424 
  425 See also [wiki:typechecking]
  426 
  427 Note [TcLevel of ExpType]
  428 ~~~~~~~~~~~~~~~~~~~~~~~~~
  429 Consider
  430 
  431   data G a where
  432     MkG :: G Bool
  433 
  434   foo MkG = True
  435 
  436 This is a classic untouchable-variable / ambiguous GADT return type
  437 scenario. But, with ExpTypes, we'll be inferring the type of the RHS.
  438 We thus must track a TcLevel in an Inferring ExpType. If we try to
  439 fill the ExpType and find that the TcLevels don't work out, we fill
  440 the ExpType with a tau-tv at the low TcLevel, hopefully to be worked
  441 out later by some means -- see fillInferResult, and Note [fillInferResult]
  442 
  443 This behaviour triggered in test gadt/gadt-escape1.
  444 -}
  445 
  446 -- actual data definition is in GHC.Tc.Utils.TcType
  447 
  448 newInferExpType :: TcM ExpType
  449 newInferExpType
  450   = do { u <- newUnique
  451        ; tclvl <- getTcLevel
  452        ; traceTc "newInferExpType" (ppr u <+> ppr tclvl)
  453        ; ref <- newMutVar Nothing
  454        ; return (Infer (IR { ir_uniq = u, ir_lvl = tclvl
  455                            , ir_ref = ref })) }
  456 
  457 -- | Extract a type out of an ExpType, if one exists. But one should always
  458 -- exist. Unless you're quite sure you know what you're doing.
  459 readExpType_maybe :: ExpType -> TcM (Maybe TcType)
  460 readExpType_maybe (Check ty)                   = return (Just ty)
  461 readExpType_maybe (Infer (IR { ir_ref = ref})) = readMutVar ref
  462 
  463 -- | Same as readExpType, but for Scaled ExpTypes
  464 readScaledExpType :: Scaled ExpType -> TcM (Scaled Type)
  465 readScaledExpType (Scaled m exp_ty)
  466   = do { ty <- readExpType exp_ty
  467        ; return (Scaled m ty) }
  468 
  469 -- | Extract a type out of an ExpType. Otherwise, panics.
  470 readExpType :: ExpType -> TcM TcType
  471 readExpType exp_ty
  472   = do { mb_ty <- readExpType_maybe exp_ty
  473        ; case mb_ty of
  474            Just ty -> return ty
  475            Nothing -> pprPanic "Unknown expected type" (ppr exp_ty) }
  476 
  477 -- | Returns the expected type when in checking mode.
  478 checkingExpType_maybe :: ExpType -> Maybe TcType
  479 checkingExpType_maybe (Check ty) = Just ty
  480 checkingExpType_maybe (Infer {}) = Nothing
  481 
  482 -- | Returns the expected type when in checking mode. Panics if in inference
  483 -- mode.
  484 checkingExpType :: String -> ExpType -> TcType
  485 checkingExpType _   (Check ty) = ty
  486 checkingExpType err et         = pprPanic "checkingExpType" (text err $$ ppr et)
  487 
  488 scaledExpTypeToType :: Scaled ExpType -> TcM (Scaled TcType)
  489 scaledExpTypeToType (Scaled m exp_ty)
  490   = do { ty <- expTypeToType exp_ty
  491        ; return (Scaled m ty) }
  492 
  493 -- | Extracts the expected type if there is one, or generates a new
  494 -- TauTv if there isn't.
  495 expTypeToType :: ExpType -> TcM TcType
  496 expTypeToType (Check ty)      = return ty
  497 expTypeToType (Infer inf_res) = inferResultToType inf_res
  498 
  499 inferResultToType :: InferResult -> TcM Type
  500 inferResultToType (IR { ir_uniq = u, ir_lvl = tc_lvl
  501                       , ir_ref = ref })
  502   = do { mb_inferred_ty <- readTcRef ref
  503        ; tau <- case mb_inferred_ty of
  504             Just ty -> do { ensureMonoType ty
  505                             -- See Note [inferResultToType]
  506                           ; return ty }
  507             Nothing -> do { rr  <- newMetaTyVarTyAtLevel tc_lvl runtimeRepTy
  508                           ; tau <- newMetaTyVarTyAtLevel tc_lvl (tYPE rr)
  509                             -- See Note [TcLevel of ExpType]
  510                           ; writeMutVar ref (Just tau)
  511                           ; return tau }
  512        ; traceTc "Forcing ExpType to be monomorphic:"
  513                  (ppr u <+> text ":=" <+> ppr tau)
  514        ; return tau }
  515 
  516 {- Note [inferResultToType]
  517 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
  518 expTypeToType and inferResultType convert an InferResult to a monotype.
  519 It must be a monotype because if the InferResult isn't already filled in,
  520 we fill it in with a unification variable (hence monotype).  So to preserve
  521 order-independence we check for mono-type-ness even if it *is* filled in
  522 already.
  523 
  524 See also Note [TcLevel of ExpType] above, and
  525 Note [fillInferResult].
  526 -}
  527 
  528 -- | Infer a type using a fresh ExpType
  529 -- See also Note [ExpType] in "GHC.Tc.Utils.TcMType"
  530 tcInfer :: (ExpSigmaType -> TcM a) -> TcM (a, TcSigmaType)
  531 tcInfer tc_check
  532   = do { res_ty <- newInferExpType
  533        ; result <- tc_check res_ty
  534        ; res_ty <- readExpType res_ty
  535        ; return (result, res_ty) }
  536 
  537 fillInferResult :: TcType -> InferResult -> TcM TcCoercionN
  538 -- If co = fillInferResult t1 t2
  539 --    => co :: t1 ~ t2
  540 -- See Note [fillInferResult]
  541 fillInferResult act_res_ty (IR { ir_uniq = u, ir_lvl = res_lvl
  542                                , ir_ref = ref })
  543   = do { mb_exp_res_ty <- readTcRef ref
  544        ; case mb_exp_res_ty of
  545             Just exp_res_ty
  546                -> do { traceTc "Joining inferred ExpType" $
  547                        ppr u <> colon <+> ppr act_res_ty <+> char '~' <+> ppr exp_res_ty
  548                      ; cur_lvl <- getTcLevel
  549                      ; unless (cur_lvl `sameDepthAs` res_lvl) $
  550                        ensureMonoType act_res_ty
  551                      ; unifyType Nothing act_res_ty exp_res_ty }
  552             Nothing
  553                -> do { traceTc "Filling inferred ExpType" $
  554                        ppr u <+> text ":=" <+> ppr act_res_ty
  555                      ; (prom_co, act_res_ty) <- promoteTcType res_lvl act_res_ty
  556                      ; writeTcRef ref (Just act_res_ty)
  557                      ; return prom_co }
  558      }
  559 
  560 
  561 {- Note [fillInferResult]
  562 ~~~~~~~~~~~~~~~~~~~~~~~~~
  563 When inferring, we use fillInferResult to "fill in" the hole in InferResult
  564    data InferResult = IR { ir_uniq :: Unique
  565                          , ir_lvl  :: TcLevel
  566                          , ir_ref  :: IORef (Maybe TcType) }
  567 
  568 There are two things to worry about:
  569 
  570 1. What if it is under a GADT or existential pattern match?
  571    - GADTs: a unification variable (and Infer's hole is similar) is untouchable
  572    - Existentials: be careful about skolem-escape
  573 
  574 2. What if it is filled in more than once?  E.g. multiple branches of a case
  575      case e of
  576         T1 -> e1
  577         T2 -> e2
  578 
  579 Our typing rules are:
  580 
  581 * The RHS of a existential or GADT alternative must always be a
  582   monotype, regardless of the number of alternatives.
  583 
  584 * Multiple non-existential/GADT branches can have (the same)
  585   higher rank type (#18412).  E.g. this is OK:
  586       case e of
  587         True  -> hr
  588         False -> hr
  589   where hr:: (forall a. a->a) -> Int
  590   c.f. Section 7.1 of "Practical type inference for arbitrary-rank types"
  591        We use choice (2) in that Section.
  592        (GHC 8.10 and earlier used choice (1).)
  593 
  594   But note that
  595       case e of
  596         True  -> hr
  597         False -> \x -> hr x
  598   will fail, because we still /infer/ both branches, so the \x will get
  599   a (monotype) unification variable, which will fail to unify with
  600   (forall a. a->a)
  601 
  602 For (1) we can detect the GADT/existential situation by seeing that
  603 the current TcLevel is greater than that stored in ir_lvl of the Infer
  604 ExpType.  We bump the level whenever we go past a GADT/existential match.
  605 
  606 Then, before filling the hole use promoteTcType to promote the type
  607 to the outer ir_lvl.  promoteTcType does this
  608   - create a fresh unification variable alpha at level ir_lvl
  609   - emits an equality alpha[ir_lvl] ~ ty
  610   - fills the hole with alpha
  611 That forces the type to be a monotype (since unification variables can
  612 only unify with monotypes); and catches skolem-escapes because the
  613 alpha is untouchable until the equality floats out.
  614 
  615 For (2), we simply look to see if the hole is filled already.
  616   - if not, we promote (as above) and fill the hole
  617   - if it is filled, we simply unify with the type that is
  618     already there
  619 
  620 There is one wrinkle.  Suppose we have
  621    case e of
  622       T1 -> e1 :: (forall a. a->a) -> Int
  623       G2 -> e2
  624 where T1 is not GADT or existential, but G2 is a GADT.  Then supppose the
  625 T1 alternative fills the hole with (forall a. a->a) -> Int, which is fine.
  626 But now the G2 alternative must not *just* unify with that else we'd risk
  627 allowing through (e2 :: (forall a. a->a) -> Int).  If we'd checked G2 first
  628 we'd have filled the hole with a unification variable, which enforces a
  629 monotype.
  630 
  631 So if we check G2 second, we still want to emit a constraint that restricts
  632 the RHS to be a monotype. This is done by ensureMonoType, and it works
  633 by simply generating a constraint (alpha ~ ty), where alpha is a fresh
  634 unification variable.  We discard the evidence.
  635 
  636 -}
  637 
  638 {- *********************************************************************
  639 *                                                                      *
  640               Promoting types
  641 *                                                                      *
  642 ********************************************************************* -}
  643 
  644 ensureMonoType :: TcType -> TcM ()
  645 -- Assuming that the argument type is of kind (TYPE r),
  646 -- ensure that it is a /monotype/
  647 -- If it is not a monotype we can see right away (since unification
  648 -- varibles and type-function applications stand for monotypes), but
  649 -- we emit a Wanted equality just to delay the error message until later
  650 ensureMonoType res_ty
  651   | isTauTy res_ty   -- isTauTy doesn't need zonking or anything
  652   = return ()
  653   | otherwise
  654   = do { mono_ty <- newOpenFlexiTyVarTy
  655        ; let eq_orig = TypeEqOrigin { uo_actual   = res_ty
  656                                     , uo_expected = mono_ty
  657                                     , uo_thing    = Nothing
  658                                     , uo_visible  = False }
  659 
  660        ; _co <- emitWantedEq eq_orig TypeLevel Nominal res_ty mono_ty
  661        ; return () }
  662 
  663 promoteTcType :: TcLevel -> TcType -> TcM (TcCoercionN, TcType)
  664 -- See Note [Promoting a type]
  665 -- See also Note [fillInferResult]
  666 -- promoteTcType level ty = (co, ty')
  667 --   * Returns ty'  whose max level is just 'level'
  668 --             and  whose kind is ~# to the kind of 'ty'
  669 --             and  whose kind has form TYPE rr
  670 --   * and co :: ty ~ ty'
  671 --   * and emits constraints to justify the coercion
  672 --
  673 -- NB: we expect that 'ty' has already kind (TYPE rr) for
  674 --     some rr::RuntimeRep.  It is, after all, the type of a term.
  675 promoteTcType dest_lvl ty
  676   = do { cur_lvl <- getTcLevel
  677        ; if (cur_lvl `sameDepthAs` dest_lvl)
  678          then return (mkTcNomReflCo ty, ty)
  679          else promote_it }
  680   where
  681     promote_it :: TcM (TcCoercion, TcType)
  682     promote_it  -- Emit a constraint  (alpha :: TYPE rr) ~ ty
  683                 -- where alpha and rr are fresh and from level dest_lvl
  684       = do { rr      <- newMetaTyVarTyAtLevel dest_lvl runtimeRepTy
  685            ; prom_ty <- newMetaTyVarTyAtLevel dest_lvl (tYPE rr)
  686            ; let eq_orig = TypeEqOrigin { uo_actual   = ty
  687                                         , uo_expected = prom_ty
  688                                         , uo_thing    = Nothing
  689                                         , uo_visible  = False }
  690 
  691            ; co <- emitWantedEq eq_orig TypeLevel Nominal ty prom_ty
  692            ; return (co, prom_ty) }
  693 
  694 {- Note [Promoting a type]
  695 ~~~~~~~~~~~~~~~~~~~~~~~~~~
  696 Consider (#12427)
  697 
  698   data T where
  699     MkT :: (Int -> Int) -> a -> T
  700 
  701   h y = case y of MkT v w -> v
  702 
  703 We'll infer the RHS type with an expected type ExpType of
  704   (IR { ir_lvl = l, ir_ref = ref, ... )
  705 where 'l' is the TcLevel of the RHS of 'h'.  Then the MkT pattern
  706 match will increase the level, so we'll end up in tcSubType, trying to
  707 unify the type of v,
  708   v :: Int -> Int
  709 with the expected type.  But this attempt takes place at level (l+1),
  710 rightly so, since v's type could have mentioned existential variables,
  711 (like w's does) and we want to catch that.
  712 
  713 So we
  714   - create a new meta-var alpha[l+1]
  715   - fill in the InferRes ref cell 'ref' with alpha
  716   - emit an equality constraint, thus
  717         [W] alpha[l+1] ~ (Int -> Int)
  718 
  719 That constraint will float outwards, as it should, unless v's
  720 type mentions a skolem-captured variable.
  721 
  722 This approach fails if v has a higher rank type; see
  723 Note [Promotion and higher rank types]
  724 
  725 
  726 Note [Promotion and higher rank types]
  727 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  728 If v had a higher-rank type, say v :: (forall a. a->a) -> Int,
  729 then we'd emit an equality
  730         [W] alpha[l+1] ~ ((forall a. a->a) -> Int)
  731 which will sadly fail because we can't unify a unification variable
  732 with a polytype.  But there is nothing really wrong with the program
  733 here.
  734 
  735 We could just about solve this by "promote the type" of v, to expose
  736 its polymorphic "shape" while still leaving constraints that will
  737 prevent existential escape.  But we must be careful!  Exposing
  738 the "shape" of the type is precisely what we must NOT do under
  739 a GADT pattern match!  So in this case we might promote the type
  740 to
  741         (forall a. a->a) -> alpha[l+1]
  742 and emit the constraint
  743         [W] alpha[l+1] ~ Int
  744 Now the promoted type can fill the ref cell, while the emitted
  745 equality can float or not, according to the usual rules.
  746 
  747 But that's not quite right!  We are exposing the arrow! We could
  748 deal with that too:
  749         (forall a. mu[l+1] a a) -> alpha[l+1]
  750 with constraints
  751         [W] alpha[l+1] ~ Int
  752         [W] mu[l+1] ~ (->)
  753 Here we abstract over the '->' inside the forall, in case that
  754 is subject to an equality constraint from a GADT match.
  755 
  756 Note that we kept the outer (->) because that's part of
  757 the polymorphic "shape".  And because of impredicativity,
  758 GADT matches can't give equalities that affect polymorphic
  759 shape.
  760 
  761 This reasoning just seems too complicated, so I decided not
  762 to do it.  These higher-rank notes are just here to record
  763 the thinking.
  764 -}
  765 
  766 
  767 {- *********************************************************************
  768 *                                                                      *
  769         MetaTvs (meta type variables; mutable)
  770 *                                                                      *
  771 ********************************************************************* -}
  772 
  773 {- Note [TyVarTv]
  774 ~~~~~~~~~~~~~~~~~
  775 A TyVarTv can unify with type *variables* only, including other TyVarTvs and
  776 skolems.  They are used in two places:
  777 
  778 1. In kind signatures, see GHC.Tc.TyCl
  779       Note [Inferring kinds for type declarations]
  780    and Note [Kind checking for GADTs]
  781 
  782 2. In partial type signatures.  See GHC.Tc.Types
  783    Note [Quantified variables in partial type signatures]
  784 
  785 Sometimes, they can unify with type variables that the user would
  786 rather keep distinct; see #11203 for an example.  So, any client of
  787 this function needs to either allow the TyVarTvs to unify with each
  788 other or check that they don't. In the case of (1) the check is done
  789 in GHC.Tc.TyCl.swizzleTcTyConBndrs.  In case of (2) it's done by
  790 findDupTyVarTvs in GHC.Tc.Gen.Bind.chooseInferredQuantifiers.
  791 
  792 Historical note: Before #15050 this (under the name SigTv) was also
  793 used for ScopedTypeVariables in patterns, to make sure these type
  794 variables only refer to other type variables, but this restriction was
  795 dropped, and ScopedTypeVariables can now refer to full types (GHC
  796 Proposal 29).
  797 -}
  798 
  799 newMetaTyVarName :: FastString -> TcM Name
  800 -- Makes a /System/ Name, which is eagerly eliminated by
  801 -- the unifier; see GHC.Tc.Utils.Unify.nicer_to_update_tv1, and
  802 -- GHC.Tc.Solver.Canonical.canEqTyVarTyVar (nicer_to_update_tv2)
  803 newMetaTyVarName str
  804   = do { uniq <- newUnique
  805        ; return (mkSystemName uniq (mkTyVarOccFS str)) }
  806 
  807 cloneMetaTyVarName :: Name -> TcM Name
  808 cloneMetaTyVarName name
  809   = do { uniq <- newUnique
  810        ; return (mkSystemName uniq (nameOccName name)) }
  811          -- See Note [Name of an instantiated type variable]
  812 
  813 {- Note [Name of an instantiated type variable]
  814 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  815 At the moment we give a unification variable a System Name, which
  816 influences the way it is tidied; see TypeRep.tidyTyVarBndr.
  817 -}
  818 
  819 metaInfoToTyVarName :: MetaInfo -> FastString
  820 metaInfoToTyVarName  meta_info =
  821   case meta_info of
  822        TauTv          -> fsLit "t"
  823        TyVarTv        -> fsLit "a"
  824        RuntimeUnkTv   -> fsLit "r"
  825        CycleBreakerTv -> fsLit "b"
  826 
  827 newAnonMetaTyVar :: MetaInfo -> Kind -> TcM TcTyVar
  828 newAnonMetaTyVar mi = newNamedAnonMetaTyVar (metaInfoToTyVarName mi) mi
  829 
  830 newNamedAnonMetaTyVar :: FastString -> MetaInfo -> Kind -> TcM TcTyVar
  831 -- Make a new meta tyvar out of thin air
  832 newNamedAnonMetaTyVar tyvar_name meta_info kind
  833 
  834   = do  { name    <- newMetaTyVarName tyvar_name
  835         ; details <- newMetaDetails meta_info
  836         ; let tyvar = mkTcTyVar name kind details
  837         ; traceTc "newAnonMetaTyVar" (ppr tyvar)
  838         ; return tyvar }
  839 
  840 -- makes a new skolem tv
  841 newSkolemTyVar :: Name -> Kind -> TcM TcTyVar
  842 newSkolemTyVar name kind
  843   = do { lvl <- getTcLevel
  844        ; return (mkTcTyVar name kind (SkolemTv lvl False)) }
  845 
  846 newTyVarTyVar :: Name -> Kind -> TcM TcTyVar
  847 -- See Note [TyVarTv]
  848 -- Does not clone a fresh unique
  849 newTyVarTyVar name kind
  850   = do { details <- newMetaDetails TyVarTv
  851        ; let tyvar = mkTcTyVar name kind details
  852        ; traceTc "newTyVarTyVar" (ppr tyvar)
  853        ; return tyvar }
  854 
  855 cloneTyVarTyVar :: Name -> Kind -> TcM TcTyVar
  856 -- See Note [TyVarTv]
  857 -- Clones a fresh unique
  858 cloneTyVarTyVar name kind
  859   = do { details <- newMetaDetails TyVarTv
  860        ; uniq <- newUnique
  861        ; let name' = name `setNameUnique` uniq
  862              tyvar = mkTcTyVar name' kind details
  863          -- Don't use cloneMetaTyVar, which makes a SystemName
  864          -- We want to keep the original more user-friendly Name
  865          -- In practical terms that means that in error messages,
  866          -- when the Name is tidied we get 'a' rather than 'a0'
  867        ; traceTc "cloneTyVarTyVar" (ppr tyvar)
  868        ; return tyvar }
  869 
  870 newPatSigTyVar :: Name -> Kind -> TcM TcTyVar
  871 newPatSigTyVar name kind
  872   = do { details <- newMetaDetails TauTv
  873        ; uniq <- newUnique
  874        ; let name' = name `setNameUnique` uniq
  875              tyvar = mkTcTyVar name' kind details
  876          -- Don't use cloneMetaTyVar;
  877          -- same reasoning as in newTyVarTyVar
  878        ; traceTc "newPatSigTyVar" (ppr tyvar)
  879        ; return tyvar }
  880 
  881 cloneAnonMetaTyVar :: MetaInfo -> TyVar -> TcKind -> TcM TcTyVar
  882 -- Make a fresh MetaTyVar, basing the name
  883 -- on that of the supplied TyVar
  884 cloneAnonMetaTyVar info tv kind
  885   = do  { details <- newMetaDetails info
  886         ; name    <- cloneMetaTyVarName (tyVarName tv)
  887         ; let tyvar = mkTcTyVar name kind details
  888         ; traceTc "cloneAnonMetaTyVar" (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar))
  889         ; return tyvar }
  890 
  891 -- Make a new CycleBreakerTv. See Note [Type variable cycles]
  892 -- in GHC.Tc.Solver.Canonical.
  893 newCycleBreakerTyVar :: TcKind -> TcM TcTyVar
  894 newCycleBreakerTyVar kind
  895   = do { details <- newMetaDetails CycleBreakerTv
  896        ; name <- newMetaTyVarName (fsLit "cbv")
  897        ; return (mkTcTyVar name kind details) }
  898 
  899 newMetaDetails :: MetaInfo -> TcM TcTyVarDetails
  900 newMetaDetails info
  901   = do { ref <- newMutVar Flexi
  902        ; tclvl <- getTcLevel
  903        ; return (MetaTv { mtv_info = info
  904                         , mtv_ref = ref
  905                         , mtv_tclvl = tclvl }) }
  906 
  907 newTauTvDetailsAtLevel :: TcLevel -> TcM TcTyVarDetails
  908 newTauTvDetailsAtLevel tclvl
  909   = do { ref <- newMutVar Flexi
  910        ; return (MetaTv { mtv_info  = TauTv
  911                         , mtv_ref   = ref
  912                         , mtv_tclvl = tclvl }) }
  913 
  914 cloneMetaTyVar :: TcTyVar -> TcM TcTyVar
  915 cloneMetaTyVar tv
  916   = assert (isTcTyVar tv) $
  917     do  { ref  <- newMutVar Flexi
  918         ; name' <- cloneMetaTyVarName (tyVarName tv)
  919         ; let details' = case tcTyVarDetails tv of
  920                            details@(MetaTv {}) -> details { mtv_ref = ref }
  921                            _ -> pprPanic "cloneMetaTyVar" (ppr tv)
  922               tyvar = mkTcTyVar name' (tyVarKind tv) details'
  923         ; traceTc "cloneMetaTyVar" (ppr tyvar)
  924         ; return tyvar }
  925 
  926 -- Works for both type and kind variables
  927 readMetaTyVar :: TyVar -> TcM MetaDetails
  928 readMetaTyVar tyvar = assertPpr (isMetaTyVar tyvar) (ppr tyvar) $
  929                       readMutVar (metaTyVarRef tyvar)
  930 
  931 isFilledMetaTyVar_maybe :: TcTyVar -> TcM (Maybe Type)
  932 isFilledMetaTyVar_maybe tv
  933  | MetaTv { mtv_ref = ref } <- tcTyVarDetails tv
  934  = do { cts <- readTcRef ref
  935       ; case cts of
  936           Indirect ty -> return (Just ty)
  937           Flexi       -> return Nothing }
  938  | otherwise
  939  = return Nothing
  940 
  941 isFilledMetaTyVar :: TyVar -> TcM Bool
  942 -- True of a filled-in (Indirect) meta type variable
  943 isFilledMetaTyVar tv = isJust <$> isFilledMetaTyVar_maybe tv
  944 
  945 isUnfilledMetaTyVar :: TyVar -> TcM Bool
  946 -- True of a un-filled-in (Flexi) meta type variable
  947 -- NB: Not the opposite of isFilledMetaTyVar
  948 isUnfilledMetaTyVar tv
  949   | MetaTv { mtv_ref = ref } <- tcTyVarDetails tv
  950   = do  { details <- readMutVar ref
  951         ; return (isFlexi details) }
  952   | otherwise = return False
  953 
  954 --------------------
  955 -- Works with both type and kind variables
  956 writeMetaTyVar :: TcTyVar -> TcType -> TcM ()
  957 -- Write into a currently-empty MetaTyVar
  958 
  959 writeMetaTyVar tyvar ty
  960   | not debugIsOn
  961   = writeMetaTyVarRef tyvar (metaTyVarRef tyvar) ty
  962 
  963 -- Everything from here on only happens if DEBUG is on
  964   | not (isTcTyVar tyvar)
  965   = massertPpr False (text "Writing to non-tc tyvar" <+> ppr tyvar)
  966 
  967   | MetaTv { mtv_ref = ref } <- tcTyVarDetails tyvar
  968   = writeMetaTyVarRef tyvar ref ty
  969 
  970   | otherwise
  971   = massertPpr False (text "Writing to non-meta tyvar" <+> ppr tyvar)
  972 
  973 --------------------
  974 writeMetaTyVarRef :: TcTyVar -> TcRef MetaDetails -> TcType -> TcM ()
  975 -- Here the tyvar is for error checking only;
  976 -- the ref cell must be for the same tyvar
  977 writeMetaTyVarRef tyvar ref ty
  978   | not debugIsOn
  979   = do { traceTc "writeMetaTyVar" (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)
  980                                    <+> text ":=" <+> ppr ty)
  981        ; writeTcRef ref (Indirect ty) }
  982 
  983   -- Everything from here on only happens if DEBUG is on
  984   -- Need to zonk 'ty' because we may only recently have promoted
  985   -- its free meta-tyvars (see Solver.Interact.tryToSolveByUnification)
  986   | otherwise
  987   = do { meta_details <- readMutVar ref;
  988        -- Zonk kinds to allow the error check to work
  989        ; zonked_tv_kind <- zonkTcType tv_kind
  990        ; zonked_ty      <- zonkTcType ty
  991        ; let zonked_ty_kind = tcTypeKind zonked_ty
  992              zonked_ty_lvl  = tcTypeLevel zonked_ty
  993              level_check_ok  = not (zonked_ty_lvl `strictlyDeeperThan` tv_lvl)
  994              level_check_msg = ppr zonked_ty_lvl $$ ppr tv_lvl $$ ppr tyvar $$ ppr ty
  995              kind_check_ok = zonked_ty_kind `eqType` zonked_tv_kind
  996              -- Hack alert! eqType, not tcEqType. see:
  997              -- Note [coreView vs tcView] in GHC.Core.Type
  998              -- Note [Extra-constraint holes in partial type signatures] in GHC.Tc.Gen.HsType
  999 
 1000              kind_msg = hang (text "Ill-kinded update to meta tyvar")
 1001                            2 (    ppr tyvar <+> text "::" <+> (ppr tv_kind $$ ppr zonked_tv_kind)
 1002                               <+> text ":="
 1003                               <+> ppr ty <+> text "::" <+> (ppr zonked_ty_kind) )
 1004 
 1005        ; traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty)
 1006 
 1007        -- Check for double updates
 1008        ; massertPpr (isFlexi meta_details) (double_upd_msg meta_details)
 1009 
 1010        -- Check for level OK
 1011        ; massertPpr level_check_ok level_check_msg
 1012 
 1013        -- Check Kinds ok
 1014        ; massertPpr kind_check_ok kind_msg
 1015 
 1016        -- Do the write
 1017        ; writeMutVar ref (Indirect ty) }
 1018   where
 1019     tv_kind = tyVarKind tyvar
 1020 
 1021     tv_lvl = tcTyVarLevel tyvar
 1022 
 1023 
 1024     double_upd_msg details = hang (text "Double update of meta tyvar")
 1025                                 2 (ppr tyvar $$ ppr details)
 1026 
 1027 {-
 1028 ************************************************************************
 1029 *                                                                      *
 1030         MetaTvs: TauTvs
 1031 *                                                                      *
 1032 ************************************************************************
 1033 
 1034 Note [Never need to instantiate coercion variables]
 1035 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1036 With coercion variables sloshing around in types, it might seem that we
 1037 sometimes need to instantiate coercion variables. This would be problematic,
 1038 because coercion variables inhabit unboxed equality (~#), and the constraint
 1039 solver thinks in terms only of boxed equality (~). The solution is that
 1040 we never need to instantiate coercion variables in the first place.
 1041 
 1042 The tyvars that we need to instantiate come from the types of functions,
 1043 data constructors, and patterns. These will never be quantified over
 1044 coercion variables, except for the special case of the promoted Eq#. But,
 1045 that can't ever appear in user code, so we're safe!
 1046 -}
 1047 
 1048 
 1049 newMultiplicityVar :: TcM TcType
 1050 newMultiplicityVar = newFlexiTyVarTy multiplicityTy
 1051 
 1052 newFlexiTyVar :: Kind -> TcM TcTyVar
 1053 newFlexiTyVar kind = newAnonMetaTyVar TauTv kind
 1054 
 1055 -- | Create a new flexi ty var with a specific name
 1056 newNamedFlexiTyVar :: FastString -> Kind -> TcM TcTyVar
 1057 newNamedFlexiTyVar fs kind = newNamedAnonMetaTyVar fs TauTv kind
 1058 
 1059 newFlexiTyVarTy :: Kind -> TcM TcType
 1060 newFlexiTyVarTy kind = do
 1061     tc_tyvar <- newFlexiTyVar kind
 1062     return (mkTyVarTy tc_tyvar)
 1063 
 1064 newFlexiTyVarTys :: Int -> Kind -> TcM [TcType]
 1065 newFlexiTyVarTys n kind = replicateM n (newFlexiTyVarTy kind)
 1066 
 1067 newOpenTypeKind :: TcM TcKind
 1068 newOpenTypeKind
 1069   = do { rr <- newFlexiTyVarTy runtimeRepTy
 1070        ; return (tYPE rr) }
 1071 
 1072 -- | Create a tyvar that can be a lifted or unlifted type.
 1073 -- Returns alpha :: TYPE kappa, where both alpha and kappa are fresh
 1074 newOpenFlexiTyVarTy :: TcM TcType
 1075 newOpenFlexiTyVarTy
 1076   = do { tv <- newOpenFlexiTyVar
 1077        ; return (mkTyVarTy tv) }
 1078 
 1079 newOpenFlexiTyVar :: TcM TcTyVar
 1080 newOpenFlexiTyVar
 1081   = do { kind <- newOpenTypeKind
 1082        ; newFlexiTyVar kind }
 1083 
 1084 newOpenBoxedTypeKind :: TcM TcKind
 1085 newOpenBoxedTypeKind
 1086   = do { lev <- newFlexiTyVarTy (mkTyConTy levityTyCon)
 1087        ; let rr = mkTyConApp boxedRepDataConTyCon [lev]
 1088        ; return (tYPE rr) }
 1089 
 1090 newMetaTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
 1091 -- Instantiate with META type variables
 1092 -- Note that this works for a sequence of kind, type, and coercion variables
 1093 -- variables.  Eg    [ (k:*), (a:k->k) ]
 1094 --             Gives [ (k7:*), (a8:k7->k7) ]
 1095 newMetaTyVars = newMetaTyVarsX emptyTCvSubst
 1096     -- emptyTCvSubst has an empty in-scope set, but that's fine here
 1097     -- Since the tyvars are freshly made, they cannot possibly be
 1098     -- captured by any existing for-alls.
 1099 
 1100 newMetaTyVarsX :: TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
 1101 -- Just like newMetaTyVars, but start with an existing substitution.
 1102 newMetaTyVarsX subst = mapAccumLM newMetaTyVarX subst
 1103 
 1104 newMetaTyVarX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
 1105 -- Make a new unification variable tyvar whose Name and Kind come from
 1106 -- an existing TyVar. We substitute kind variables in the kind.
 1107 newMetaTyVarX = new_meta_tv_x TauTv
 1108 
 1109 newMetaTyVarTyVarX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
 1110 -- Just like newMetaTyVarX, but make a TyVarTv
 1111 newMetaTyVarTyVarX = new_meta_tv_x TyVarTv
 1112 
 1113 newWildCardX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
 1114 newWildCardX subst tv
 1115   = do { new_tv <- newAnonMetaTyVar TauTv (substTy subst (tyVarKind tv))
 1116        ; return (extendTvSubstWithClone subst tv new_tv, new_tv) }
 1117 
 1118 new_meta_tv_x :: MetaInfo -> TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
 1119 new_meta_tv_x info subst tv
 1120   = do  { new_tv <- cloneAnonMetaTyVar info tv substd_kind
 1121         ; let subst1 = extendTvSubstWithClone subst tv new_tv
 1122         ; return (subst1, new_tv) }
 1123   where
 1124     substd_kind = substTyUnchecked subst (tyVarKind tv)
 1125       -- NOTE: #12549 is fixed so we could use
 1126       -- substTy here, but the tc_infer_args problem
 1127       -- is not yet fixed so leaving as unchecked for now.
 1128       -- OLD NOTE:
 1129       -- Unchecked because we call newMetaTyVarX from
 1130       -- tcInstTyBinder, which is called from tcInferTyApps
 1131       -- which does not yet take enough trouble to ensure
 1132       -- the in-scope set is right; e.g. #12785 trips
 1133       -- if we use substTy here
 1134 
 1135 newMetaTyVarTyAtLevel :: TcLevel -> TcKind -> TcM TcType
 1136 newMetaTyVarTyAtLevel tc_lvl kind
 1137   = do  { details <- newTauTvDetailsAtLevel tc_lvl
 1138         ; name    <- newMetaTyVarName (fsLit "p")
 1139         ; return (mkTyVarTy (mkTcTyVar name kind details)) }
 1140 
 1141 {- *********************************************************************
 1142 *                                                                      *
 1143           Finding variables to quantify over
 1144 *                                                                      *
 1145 ********************************************************************* -}
 1146 
 1147 {- Note [Dependent type variables]
 1148 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1149 In Haskell type inference we quantify over type variables; but we only
 1150 quantify over /kind/ variables when -XPolyKinds is on.  Without -XPolyKinds
 1151 we default the kind variables to *.
 1152 
 1153 So, to support this defaulting, and only for that reason, when
 1154 collecting the free vars of a type (in candidateQTyVarsOfType and friends),
 1155 prior to quantifying, we must keep the type and kind variables separate.
 1156 
 1157 But what does that mean in a system where kind variables /are/ type
 1158 variables? It's a fairly arbitrary distinction based on how the
 1159 variables appear:
 1160 
 1161   - "Kind variables" appear in the kind of some other free variable
 1162     or in the kind of a locally quantified type variable
 1163     (forall (a :: kappa). ...) or in the kind of a coercion
 1164     (a |> (co :: kappa1 ~ kappa2)).
 1165 
 1166      These are the ones we default to * if -XPolyKinds is off
 1167 
 1168   - "Type variables" are all free vars that are not kind variables
 1169 
 1170 E.g.  In the type    T k (a::k)
 1171       'k' is a kind variable, because it occurs in the kind of 'a',
 1172           even though it also appears at "top level" of the type
 1173       'a' is a type variable, because it doesn't
 1174 
 1175 We gather these variables using a CandidatesQTvs record:
 1176   DV { dv_kvs: Variables free in the kind of a free type variable
 1177                or of a forall-bound type variable
 1178      , dv_tvs: Variables syntactically free in the type }
 1179 
 1180 So:  dv_kvs            are the kind variables of the type
 1181      (dv_tvs - dv_kvs) are the type variable of the type
 1182 
 1183 Note that
 1184 
 1185 * A variable can occur in both.
 1186       T k (x::k)    The first occurrence of k makes it
 1187                     show up in dv_tvs, the second in dv_kvs
 1188 
 1189 * We include any coercion variables in the "dependent",
 1190   "kind-variable" set because we never quantify over them.
 1191 
 1192 * The "kind variables" might depend on each other; e.g
 1193      (k1 :: k2), (k2 :: *)
 1194   The "type variables" do not depend on each other; if
 1195   one did, it'd be classified as a kind variable!
 1196 
 1197 Note [CandidatesQTvs determinism and order]
 1198 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1199 * Determinism: when we quantify over type variables we decide the
 1200   order in which they appear in the final type. Because the order of
 1201   type variables in the type can end up in the interface file and
 1202   affects some optimizations like worker-wrapper, we want this order to
 1203   be deterministic.
 1204 
 1205   To achieve that we use deterministic sets of variables that can be
 1206   converted to lists in a deterministic order. For more information
 1207   about deterministic sets see Note [Deterministic UniqFM] in GHC.Types.Unique.DFM.
 1208 
 1209 * Order: as well as being deterministic, we use an
 1210   accumulating-parameter style for candidateQTyVarsOfType so that we
 1211   add variables one at a time, left to right.  That means we tend to
 1212   produce the variables in left-to-right order.  This is just to make
 1213   it bit more predictable for the programmer.
 1214 
 1215 Note [Naughty quantification candidates]
 1216 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1217 Consider (#14880, dependent/should_compile/T14880-2), suppose
 1218 we are trying to generalise this type:
 1219 
 1220   forall arg. ... (alpha[tau]:arg) ...
 1221 
 1222 We have a metavariable alpha whose kind mentions a skolem variable
 1223 bound inside the very type we are generalising.
 1224 This can arise while type-checking a user-written type signature
 1225 (see the test case for the full code).
 1226 
 1227 We cannot generalise over alpha!  That would produce a type like
 1228   forall {a :: arg}. forall arg. ...blah...
 1229 The fact that alpha's kind mentions arg renders it completely
 1230 ineligible for generalisation.
 1231 
 1232 However, we are not going to learn any new constraints on alpha,
 1233 because its kind isn't even in scope in the outer context (but see Wrinkle).
 1234 So alpha is entirely unconstrained.
 1235 
 1236 What then should we do with alpha?  During generalization, every
 1237 metavariable is either (A) promoted, (B) generalized, or (C) zapped
 1238 (according to Note [Recipe for checking a signature] in GHC.Tc.Gen.HsType).
 1239 
 1240  * We can't generalise it.
 1241  * We can't promote it, because its kind prevents that
 1242  * We can't simply leave it be, because this type is about to
 1243    go into the typing environment (as the type of some let-bound
 1244    variable, say), and then chaos erupts when we try to instantiate.
 1245 
 1246 Previously, we zapped it to Any. This worked, but it had the unfortunate
 1247 effect of causing Any sometimes to appear in error messages. If this
 1248 kind of signature happens, the user probably has made a mistake -- no
 1249 one really wants Any in their types. So we now error. This must be
 1250 a hard error (failure in the monad) to avoid other messages from mentioning
 1251 Any.
 1252 
 1253 We do this eager erroring in candidateQTyVars, which always precedes
 1254 generalisation, because at that moment we have a clear picture of what
 1255 skolems are in scope within the type itself (e.g. that 'forall arg').
 1256 
 1257 This change is inspired by and described in Section 7.2 of "Kind Inference
 1258 for Datatypes", POPL'20.
 1259 
 1260 NB: this is all rather similar to, but sadly not the same as
 1261     Note [Error on unconstrained meta-variables]
 1262 
 1263 Wrinkle:
 1264 
 1265 We must make absolutely sure that alpha indeed is not
 1266 from an outer context. (Otherwise, we might indeed learn more information
 1267 about it.) This can be done easily: we just check alpha's TcLevel.
 1268 That level must be strictly greater than the ambient TcLevel in order
 1269 to treat it as naughty. We say "strictly greater than" because the call to
 1270 candidateQTyVars is made outside the bumped TcLevel, as stated in the
 1271 comment to candidateQTyVarsOfType. The level check is done in go_tv
 1272 in collect_cand_qtvs. Skipping this check caused #16517.
 1273 
 1274 -}
 1275 
 1276 data CandidatesQTvs
 1277   -- See Note [Dependent type variables]
 1278   -- See Note [CandidatesQTvs determinism and order]
 1279   --
 1280   -- Invariants:
 1281   --   * All variables are fully zonked, including their kinds
 1282   --   * All variables are at a level greater than the ambient level
 1283   --     See Note [Use level numbers for quantification]
 1284   --
 1285   -- This *can* contain skolems. For example, in `data X k :: k -> Type`
 1286   -- we need to know that the k is a dependent variable. This is done
 1287   -- by collecting the candidates in the kind after skolemising. It also
 1288   -- comes up when generalizing a associated type instance, where instance
 1289   -- variables are skolems. (Recall that associated type instances are generalized
 1290   -- independently from their enclosing class instance, and the associated
 1291   -- type instance may be generalized by more, fewer, or different variables
 1292   -- than the class instance.)
 1293   --
 1294   = DV { dv_kvs :: DTyVarSet    -- "kind" metavariables (dependent)
 1295        , dv_tvs :: DTyVarSet    -- "type" metavariables (non-dependent)
 1296          -- A variable may appear in both sets
 1297          -- E.g.   T k (x::k)    The first occurrence of k makes it
 1298          --                      show up in dv_tvs, the second in dv_kvs
 1299          -- See Note [Dependent type variables]
 1300 
 1301        , dv_cvs :: CoVarSet
 1302          -- These are covars. Included only so that we don't repeatedly
 1303          -- look at covars' kinds in accumulator. Not used by quantifyTyVars.
 1304     }
 1305 
 1306 instance Semi.Semigroup CandidatesQTvs where
 1307    (DV { dv_kvs = kv1, dv_tvs = tv1, dv_cvs = cv1 })
 1308      <> (DV { dv_kvs = kv2, dv_tvs = tv2, dv_cvs = cv2 })
 1309           = DV { dv_kvs = kv1 `unionDVarSet` kv2
 1310                , dv_tvs = tv1 `unionDVarSet` tv2
 1311                , dv_cvs = cv1 `unionVarSet` cv2 }
 1312 
 1313 instance Monoid CandidatesQTvs where
 1314    mempty = DV { dv_kvs = emptyDVarSet, dv_tvs = emptyDVarSet, dv_cvs = emptyVarSet }
 1315    mappend = (Semi.<>)
 1316 
 1317 instance Outputable CandidatesQTvs where
 1318   ppr (DV {dv_kvs = kvs, dv_tvs = tvs, dv_cvs = cvs })
 1319     = text "DV" <+> braces (pprWithCommas id [ text "dv_kvs =" <+> ppr kvs
 1320                                              , text "dv_tvs =" <+> ppr tvs
 1321                                              , text "dv_cvs =" <+> ppr cvs ])
 1322 
 1323 isEmptyCandidates :: CandidatesQTvs -> Bool
 1324 isEmptyCandidates (DV { dv_kvs = kvs, dv_tvs = tvs })
 1325   = isEmptyDVarSet kvs && isEmptyDVarSet tvs
 1326 
 1327 -- | Extract out the kind vars (in order) and type vars (in order) from
 1328 -- a 'CandidatesQTvs'. The lists are guaranteed to be distinct. Keeping
 1329 -- the lists separate is important only in the -XNoPolyKinds case.
 1330 candidateVars :: CandidatesQTvs -> ([TcTyVar], [TcTyVar])
 1331 candidateVars (DV { dv_kvs = dep_kv_set, dv_tvs = nondep_tkv_set })
 1332   = (dep_kvs, nondep_tvs)
 1333   where
 1334     dep_kvs = scopedSort $ dVarSetElems dep_kv_set
 1335       -- scopedSort: put the kind variables into
 1336       --    well-scoped order.
 1337       --    E.g.  [k, (a::k)] not the other way round
 1338 
 1339     nondep_tvs = dVarSetElems (nondep_tkv_set `minusDVarSet` dep_kv_set)
 1340       -- See Note [Dependent type variables]
 1341       -- The `minus` dep_tkvs removes any kind-level vars
 1342       --    e.g. T k (a::k)   Since k appear in a kind it'll
 1343       --    be in dv_kvs, and is dependent. So remove it from
 1344       --    dv_tvs which will also contain k
 1345       -- NB kinds of tvs are already zonked
 1346 
 1347 candidateKindVars :: CandidatesQTvs -> TyVarSet
 1348 candidateKindVars dvs = dVarSetToVarSet (dv_kvs dvs)
 1349 
 1350 partitionCandidates :: CandidatesQTvs -> (TyVar -> Bool) -> (TyVarSet, CandidatesQTvs)
 1351 -- The selected TyVars are returned as a non-deterministic TyVarSet
 1352 partitionCandidates dvs@(DV { dv_kvs = kvs, dv_tvs = tvs }) pred
 1353   = (extracted, dvs { dv_kvs = rest_kvs, dv_tvs = rest_tvs })
 1354   where
 1355     (extracted_kvs, rest_kvs) = partitionDVarSet pred kvs
 1356     (extracted_tvs, rest_tvs) = partitionDVarSet pred tvs
 1357     extracted = dVarSetToVarSet extracted_kvs `unionVarSet` dVarSetToVarSet extracted_tvs
 1358 
 1359 -- | Gathers free variables to use as quantification candidates (in
 1360 -- 'quantifyTyVars'). This might output the same var
 1361 -- in both sets, if it's used in both a type and a kind.
 1362 -- The variables to quantify must have a TcLevel strictly greater than
 1363 -- the ambient level. (See Wrinkle in Note [Naughty quantification candidates])
 1364 -- See Note [CandidatesQTvs determinism and order]
 1365 -- See Note [Dependent type variables]
 1366 candidateQTyVarsOfType :: TcType       -- not necessarily zonked
 1367                        -> TcM CandidatesQTvs
 1368 candidateQTyVarsOfType ty = collect_cand_qtvs ty False emptyVarSet mempty ty
 1369 
 1370 -- | Like 'candidateQTyVarsOfType', but over a list of types
 1371 -- The variables to quantify must have a TcLevel strictly greater than
 1372 -- the ambient level. (See Wrinkle in Note [Naughty quantification candidates])
 1373 candidateQTyVarsOfTypes :: [Type] -> TcM CandidatesQTvs
 1374 candidateQTyVarsOfTypes tys = foldlM (\acc ty -> collect_cand_qtvs ty False emptyVarSet acc ty)
 1375                                      mempty tys
 1376 
 1377 -- | Like 'candidateQTyVarsOfType', but consider every free variable
 1378 -- to be dependent. This is appropriate when generalizing a *kind*,
 1379 -- instead of a type. (That way, -XNoPolyKinds will default the variables
 1380 -- to Type.)
 1381 candidateQTyVarsOfKind :: TcKind       -- Not necessarily zonked
 1382                        -> TcM CandidatesQTvs
 1383 candidateQTyVarsOfKind ty = collect_cand_qtvs ty True emptyVarSet mempty ty
 1384 
 1385 candidateQTyVarsOfKinds :: [TcKind]    -- Not necessarily zonked
 1386                        -> TcM CandidatesQTvs
 1387 candidateQTyVarsOfKinds tys = foldM (\acc ty -> collect_cand_qtvs ty True emptyVarSet acc ty)
 1388                                     mempty tys
 1389 
 1390 delCandidates :: CandidatesQTvs -> [Var] -> CandidatesQTvs
 1391 delCandidates (DV { dv_kvs = kvs, dv_tvs = tvs, dv_cvs = cvs }) vars
 1392   = DV { dv_kvs = kvs `delDVarSetList` vars
 1393        , dv_tvs = tvs `delDVarSetList` vars
 1394        , dv_cvs = cvs `delVarSetList`  vars }
 1395 
 1396 collect_cand_qtvs
 1397   :: TcType          -- original type that we started recurring into; for errors
 1398   -> Bool            -- True <=> consider every fv in Type to be dependent
 1399   -> VarSet          -- Bound variables (locals only)
 1400   -> CandidatesQTvs  -- Accumulating parameter
 1401   -> Type            -- Not necessarily zonked
 1402   -> TcM CandidatesQTvs
 1403 
 1404 -- Key points:
 1405 --   * Looks through meta-tyvars as it goes;
 1406 --     no need to zonk in advance
 1407 --
 1408 --   * Needs to be monadic anyway, because it handles naughty
 1409 --     quantification; see Note [Naughty quantification candidates]
 1410 --
 1411 --   * Returns fully-zonked CandidateQTvs, including their kinds
 1412 --     so that subsequent dependency analysis (to build a well
 1413 --     scoped telescope) works correctly
 1414 
 1415 collect_cand_qtvs orig_ty is_dep bound dvs ty
 1416   = go dvs ty
 1417   where
 1418     is_bound tv = tv `elemVarSet` bound
 1419 
 1420     -----------------
 1421     go :: CandidatesQTvs -> TcType -> TcM CandidatesQTvs
 1422     -- Uses accumulating-parameter style
 1423     go dv (AppTy t1 t2)    = foldlM go dv [t1, t2]
 1424     go dv (TyConApp tc tys) = go_tc_args dv (tyConBinders tc) tys
 1425     go dv (FunTy _ w arg res) = foldlM go dv [w, arg, res]
 1426     go dv (LitTy {})        = return dv
 1427     go dv (CastTy ty co)    = do dv1 <- go dv ty
 1428                                  collect_cand_qtvs_co orig_ty bound dv1 co
 1429     go dv (CoercionTy co)   = collect_cand_qtvs_co orig_ty bound dv co
 1430 
 1431     go dv (TyVarTy tv)
 1432       | is_bound tv = return dv
 1433       | otherwise   = do { m_contents <- isFilledMetaTyVar_maybe tv
 1434                          ; case m_contents of
 1435                              Just ind_ty -> go dv ind_ty
 1436                              Nothing     -> go_tv dv tv }
 1437 
 1438     go dv (ForAllTy (Bndr tv _) ty)
 1439       = do { dv1 <- collect_cand_qtvs orig_ty True bound dv (tyVarKind tv)
 1440            ; collect_cand_qtvs orig_ty is_dep (bound `extendVarSet` tv) dv1 ty }
 1441 
 1442       -- This makes sure that we default e.g. the alpha in Proxy alpha (Any alpha).
 1443       -- Tested in polykinds/NestedProxies.
 1444       -- We just might get this wrong in AppTy, but I don't think that's possible
 1445       -- with -XNoPolyKinds. And fixing it would be non-performant, as we'd need
 1446       -- to look at kinds.
 1447     go_tc_args dv (tc_bndr:tc_bndrs) (ty:tys)
 1448       = do { dv1 <- collect_cand_qtvs orig_ty (is_dep || isNamedTyConBinder tc_bndr)
 1449                                       bound dv ty
 1450            ; go_tc_args dv1 tc_bndrs tys }
 1451     go_tc_args dv _bndrs tys  -- _bndrs might be non-empty: undersaturation
 1452                               -- tys might be non-empty: oversaturation
 1453                               -- either way, the foldlM is correct
 1454       = foldlM go dv tys
 1455 
 1456     -----------------
 1457     go_tv dv@(DV { dv_kvs = kvs, dv_tvs = tvs }) tv
 1458       | tv `elemDVarSet` kvs
 1459       = return dv  -- We have met this tyvar already
 1460 
 1461       | not is_dep
 1462       , tv `elemDVarSet` tvs
 1463       = return dv  -- We have met this tyvar already
 1464 
 1465       | otherwise
 1466       = do { tv_kind <- zonkTcType (tyVarKind tv)
 1467                  -- This zonk is annoying, but it is necessary, both to
 1468                  -- ensure that the collected candidates have zonked kinds
 1469                  -- (#15795) and to make the naughty check
 1470                  -- (which comes next) works correctly
 1471 
 1472            ; let tv_kind_vars = tyCoVarsOfType tv_kind
 1473            ; cur_lvl <- getTcLevel
 1474            ; if |  tcTyVarLevel tv <= cur_lvl
 1475                 -> return dv   -- this variable is from an outer context; skip
 1476                                -- See Note [Use level numbers for quantification]
 1477 
 1478                 |  intersectsVarSet bound tv_kind_vars
 1479                    -- the tyvar must not be from an outer context, but we have
 1480                    -- already checked for this.
 1481                    -- See Note [Naughty quantification candidates]
 1482                 -> do { traceTc "Naughty quantifier" $
 1483                           vcat [ ppr tv <+> dcolon <+> ppr tv_kind
 1484                                , text "bound:" <+> pprTyVars (nonDetEltsUniqSet bound)
 1485                                , text "fvs:" <+> pprTyVars (nonDetEltsUniqSet tv_kind_vars) ]
 1486 
 1487                       ; let escapees = intersectVarSet bound tv_kind_vars
 1488                       ; naughtyQuantification orig_ty tv escapees }
 1489 
 1490                 |  otherwise
 1491                 -> do { let tv' = tv `setTyVarKind` tv_kind
 1492                             dv' | is_dep    = dv { dv_kvs = kvs `extendDVarSet` tv' }
 1493                                 | otherwise = dv { dv_tvs = tvs `extendDVarSet` tv' }
 1494                                 -- See Note [Order of accumulation]
 1495 
 1496                         -- See Note [Recurring into kinds for candidateQTyVars]
 1497                       ; collect_cand_qtvs orig_ty True bound dv' tv_kind } }
 1498 
 1499 collect_cand_qtvs_co :: TcType -- original type at top of recursion; for errors
 1500                      -> VarSet -- bound variables
 1501                      -> CandidatesQTvs -> Coercion
 1502                      -> TcM CandidatesQTvs
 1503 collect_cand_qtvs_co orig_ty bound = go_co
 1504   where
 1505     go_co dv (Refl ty)             = collect_cand_qtvs orig_ty True bound dv ty
 1506     go_co dv (GRefl _ ty mco)      = do dv1 <- collect_cand_qtvs orig_ty True bound dv ty
 1507                                         go_mco dv1 mco
 1508     go_co dv (TyConAppCo _ _ cos)  = foldlM go_co dv cos
 1509     go_co dv (AppCo co1 co2)       = foldlM go_co dv [co1, co2]
 1510     go_co dv (FunCo _ w co1 co2)   = foldlM go_co dv [w, co1, co2]
 1511     go_co dv (AxiomInstCo _ _ cos) = foldlM go_co dv cos
 1512     go_co dv (AxiomRuleCo _ cos)   = foldlM go_co dv cos
 1513     go_co dv (UnivCo prov _ t1 t2) = do dv1 <- go_prov dv prov
 1514                                         dv2 <- collect_cand_qtvs orig_ty True bound dv1 t1
 1515                                         collect_cand_qtvs orig_ty True bound dv2 t2
 1516     go_co dv (SymCo co)            = go_co dv co
 1517     go_co dv (TransCo co1 co2)     = foldlM go_co dv [co1, co2]
 1518     go_co dv (NthCo _ _ co)        = go_co dv co
 1519     go_co dv (LRCo _ co)           = go_co dv co
 1520     go_co dv (InstCo co1 co2)      = foldlM go_co dv [co1, co2]
 1521     go_co dv (KindCo co)           = go_co dv co
 1522     go_co dv (SubCo co)            = go_co dv co
 1523 
 1524     go_co dv (HoleCo hole)
 1525       = do m_co <- unpackCoercionHole_maybe hole
 1526            case m_co of
 1527              Just co -> go_co dv co
 1528              Nothing -> go_cv dv (coHoleCoVar hole)
 1529 
 1530     go_co dv (CoVarCo cv) = go_cv dv cv
 1531 
 1532     go_co dv (ForAllCo tcv kind_co co)
 1533       = do { dv1 <- go_co dv kind_co
 1534            ; collect_cand_qtvs_co orig_ty (bound `extendVarSet` tcv) dv1 co }
 1535 
 1536     go_mco dv MRefl    = return dv
 1537     go_mco dv (MCo co) = go_co dv co
 1538 
 1539     go_prov dv (PhantomProv co)    = go_co dv co
 1540     go_prov dv (ProofIrrelProv co) = go_co dv co
 1541     go_prov dv (PluginProv _)      = return dv
 1542     go_prov dv (CorePrepProv _)    = return dv
 1543 
 1544     go_cv :: CandidatesQTvs -> CoVar -> TcM CandidatesQTvs
 1545     go_cv dv@(DV { dv_cvs = cvs }) cv
 1546       | is_bound cv         = return dv
 1547       | cv `elemVarSet` cvs = return dv
 1548 
 1549         -- See Note [Recurring into kinds for candidateQTyVars]
 1550       | otherwise           = collect_cand_qtvs orig_ty True bound
 1551                                     (dv { dv_cvs = cvs `extendVarSet` cv })
 1552                                     (idType cv)
 1553 
 1554     is_bound tv = tv `elemVarSet` bound
 1555 
 1556 {- Note [Order of accumulation]
 1557 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1558 You might be tempted (like I was) to use unitDVarSet and mappend
 1559 rather than extendDVarSet.  However, the union algorithm for
 1560 deterministic sets depends on (roughly) the size of the sets. The
 1561 elements from the smaller set end up to the right of the elements from
 1562 the larger one. When sets are equal, the left-hand argument to
 1563 `mappend` goes to the right of the right-hand argument.
 1564 
 1565 In our case, if we use unitDVarSet and mappend, we learn that the free
 1566 variables of (a -> b -> c -> d) are [b, a, c, d], and we then quantify
 1567 over them in that order. (The a comes after the b because we union the
 1568 singleton sets as ({a} `mappend` {b}), producing {b, a}. Thereafter,
 1569 the size criterion works to our advantage.) This is just annoying to
 1570 users, so I use `extendDVarSet`, which unambiguously puts the new
 1571 element to the right.
 1572 
 1573 Note that the unitDVarSet/mappend implementation would not be wrong
 1574 against any specification -- just suboptimal and confounding to users.
 1575 
 1576 Note [Recurring into kinds for candidateQTyVars]
 1577 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1578 First, read Note [Closing over free variable kinds] in GHC.Core.TyCo.FVs, paying
 1579 attention to the end of the Note about using an empty bound set when
 1580 traversing a variable's kind.
 1581 
 1582 That Note concludes with the recommendation that we empty out the bound
 1583 set when recurring into the kind of a type variable. Yet, we do not do
 1584 this here. I have two tasks in order to convince you that this code is
 1585 right. First, I must show why it is safe to ignore the reasoning in that
 1586 Note. Then, I must show why is is necessary to contradict the reasoning in
 1587 that Note.
 1588 
 1589 Why it is safe: There can be no
 1590 shadowing in the candidateQ... functions: they work on the output of
 1591 type inference, which is seeded by the renamer and its insistence to
 1592 use different Uniques for different variables. (In contrast, the Core
 1593 functions work on the output of optimizations, which may introduce
 1594 shadowing.) Without shadowing, the problem studied by
 1595 Note [Closing over free variable kinds] in GHC.Core.TyCo.FVs cannot happen.
 1596 
 1597 Why it is necessary:
 1598 Wiping the bound set would be just plain wrong here. Consider
 1599 
 1600   forall k1 k2 (a :: k1). Proxy k2 (a |> (hole :: k1 ~# k2))
 1601 
 1602 We really don't want to think k1 and k2 are free here. (It's true that we'll
 1603 never be able to fill in `hole`, but we don't want to go off the rails just
 1604 because we have an insoluble coercion hole.) So: why is it wrong to wipe
 1605 the bound variables here but right in Core? Because the final statement
 1606 in Note [Closing over free variable kinds] in GHC.Core.TyCo.FVs is wrong: not
 1607 every variable is either free or bound. A variable can be a hole, too!
 1608 The reasoning in that Note then breaks down.
 1609 
 1610 And the reasoning applies just as well to free non-hole variables, so we
 1611 retain the bound set always.
 1612 
 1613 -}
 1614 
 1615 {- *********************************************************************
 1616 *                                                                      *
 1617              Quantification
 1618 *                                                                      *
 1619 ************************************************************************
 1620 
 1621 Note [quantifyTyVars]
 1622 ~~~~~~~~~~~~~~~~~~~~~
 1623 quantifyTyVars is given the free vars of a type that we
 1624 are about to wrap in a forall.
 1625 
 1626 It takes these free type/kind variables (partitioned into dependent and
 1627 non-dependent variables) skolemises metavariables with a TcLevel greater
 1628 than the ambient level (see Note [Use level numbers for quantification]).
 1629 
 1630 * This function distinguishes between dependent and non-dependent
 1631   variables only to keep correct defaulting behavior with -XNoPolyKinds.
 1632   With -XPolyKinds, it treats both classes of variables identically.
 1633 
 1634 * quantifyTyVars never quantifies over
 1635     - a coercion variable (or any tv mentioned in the kind of a covar)
 1636     - a runtime-rep variable
 1637 
 1638 Note [Use level numbers for quantification]
 1639 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1640 The level numbers assigned to metavariables are very useful. Not only
 1641 do they track touchability (Note [TcLevel invariants] in GHC.Tc.Utils.TcType),
 1642 but they also allow us to determine which variables to
 1643 generalise. The rule is this:
 1644 
 1645   When generalising, quantify only metavariables with a TcLevel greater
 1646   than the ambient level.
 1647 
 1648 This works because we bump the level every time we go inside a new
 1649 source-level construct. In a traditional generalisation algorithm, we
 1650 would gather all free variables that aren't free in an environment.
 1651 However, if a variable is in that environment, it will always have a lower
 1652 TcLevel: it came from an outer scope. So we can replace the "free in
 1653 environment" check with a level-number check.
 1654 
 1655 Here is an example:
 1656 
 1657   f x = x + (z True)
 1658     where
 1659       z y = x * x
 1660 
 1661 We start by saying (x :: alpha[1]). When inferring the type of z, we'll
 1662 quickly discover that z :: alpha[1]. But it would be disastrous to
 1663 generalise over alpha in the type of z. So we need to know that alpha
 1664 comes from an outer environment. By contrast, the type of y is beta[2],
 1665 and we are free to generalise over it. What's the difference between
 1666 alpha[1] and beta[2]? Their levels. beta[2] has the right TcLevel for
 1667 generalisation, and so we generalise it. alpha[1] does not, and so
 1668 we leave it alone.
 1669 
 1670 Note that not *every* variable with a higher level will get
 1671 generalised, either due to the monomorphism restriction or other
 1672 quirks. See, for example, the code in GHC.Tc.Solver.decideMonoTyVars
 1673 and in GHC.Tc.Gen.HsType.kindGeneralizeSome, both of which exclude
 1674 certain otherwise-eligible variables from being generalised.
 1675 
 1676 Using level numbers for quantification is implemented in the candidateQTyVars...
 1677 functions, by adding only those variables with a level strictly higher than
 1678 the ambient level to the set of candidates.
 1679 
 1680 Note [quantifyTyVars determinism]
 1681 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1682 The results of quantifyTyVars are wrapped in a forall and can end up in the
 1683 interface file. One such example is inferred type signatures. They also affect
 1684 the results of optimizations, for example worker-wrapper. This means that to
 1685 get deterministic builds quantifyTyVars needs to be deterministic.
 1686 
 1687 To achieve this CandidatesQTvs is backed by deterministic sets which allows them
 1688 to be later converted to a list in a deterministic order.
 1689 
 1690 For more information about deterministic sets see
 1691 Note [Deterministic UniqFM] in GHC.Types.Unique.DFM.
 1692 -}
 1693 
 1694 quantifyTyVars :: DefaultVarsOfKind
 1695                -> CandidatesQTvs   -- See Note [Dependent type variables]
 1696                                    -- Already zonked
 1697                -> TcM [TcTyVar]
 1698 -- See Note [quantifyTyVars]
 1699 -- Can be given a mixture of TcTyVars and TyVars, in the case of
 1700 --   associated type declarations. Also accepts covars, but *never* returns any.
 1701 -- According to Note [Use level numbers for quantification] and the
 1702 -- invariants on CandidateQTvs, we do not have to filter out variables
 1703 -- free in the environment here. Just quantify unconditionally, subject
 1704 -- to the restrictions in Note [quantifyTyVars].
 1705 quantifyTyVars def_varsOfKind dvs
 1706        -- short-circuit common case
 1707   | isEmptyCandidates dvs
 1708   = do { traceTc "quantifyTyVars has nothing to quantify" empty
 1709        ; return [] }
 1710 
 1711   | otherwise
 1712   = do { traceTc "quantifyTyVars {"
 1713            ( vcat [ text "def_varsOfKind =" <+> ppr def_varsOfKind
 1714                   , text "dvs =" <+> ppr dvs ])
 1715 
 1716        ; undefaulted <- defaultTyVars def_varsOfKind dvs
 1717        ; final_qtvs  <- mapMaybeM zonk_quant undefaulted
 1718 
 1719        ; traceTc "quantifyTyVars }"
 1720            (vcat [ text "undefaulted:" <+> pprTyVars undefaulted
 1721                  , text "final_qtvs:"  <+> pprTyVars final_qtvs ])
 1722 
 1723        -- We should never quantify over coercion variables; check this
 1724        ; let co_vars = filter isCoVar final_qtvs
 1725        ; massertPpr (null co_vars) (ppr co_vars)
 1726 
 1727        ; return final_qtvs }
 1728   where
 1729     -- zonk_quant returns a tyvar if it should be quantified over;
 1730     -- otherwise, it returns Nothing. The latter case happens for
 1731     -- non-meta-tyvars
 1732     zonk_quant tkv
 1733       | not (isTyVar tkv)
 1734       = return Nothing   -- this can happen for a covar that's associated with
 1735                          -- a coercion hole. Test case: typecheck/should_compile/T2494
 1736 
 1737       | not (isTcTyVar tkv)
 1738       = return (Just tkv)  -- For associated types in a class with a standalone
 1739                            -- kind signature, we have the class variables in
 1740                            -- scope, and they are TyVars not TcTyVars
 1741       | otherwise
 1742       = Just <$> skolemiseQuantifiedTyVar tkv
 1743 
 1744 isQuantifiableTv :: TcLevel   -- Level of the context, outside the quantification
 1745                  -> TcTyVar
 1746                  -> Bool
 1747 isQuantifiableTv outer_tclvl tcv
 1748   | isTcTyVar tcv  -- Might be a CoVar; change this when gather covars separately
 1749   = tcTyVarLevel tcv > outer_tclvl
 1750   | otherwise
 1751   = False
 1752 
 1753 zonkAndSkolemise :: TcTyCoVar -> TcM TcTyCoVar
 1754 -- A tyvar binder is never a unification variable (TauTv),
 1755 -- rather it is always a skolem. It *might* be a TyVarTv.
 1756 -- (Because non-CUSK type declarations use TyVarTvs.)
 1757 -- Regardless, it may have a kind that has not yet been zonked,
 1758 -- and may include kind unification variables.
 1759 zonkAndSkolemise tyvar
 1760   | isTyVarTyVar tyvar
 1761      -- We want to preserve the binding location of the original TyVarTv.
 1762      -- This is important for error messages. If we don't do this, then
 1763      -- we get bad locations in, e.g., typecheck/should_fail/T2688
 1764   = do { zonked_tyvar <- zonkTcTyVarToTyVar tyvar
 1765        ; skolemiseQuantifiedTyVar zonked_tyvar }
 1766 
 1767   | otherwise
 1768   = assertPpr (isImmutableTyVar tyvar || isCoVar tyvar) (pprTyVar tyvar) $
 1769     zonkTyCoVarKind tyvar
 1770 
 1771 skolemiseQuantifiedTyVar :: TcTyVar -> TcM TcTyVar
 1772 -- The quantified type variables often include meta type variables
 1773 -- we want to freeze them into ordinary type variables
 1774 -- The meta tyvar is updated to point to the new skolem TyVar.  Now any
 1775 -- bound occurrences of the original type variable will get zonked to
 1776 -- the immutable version.
 1777 --
 1778 -- We leave skolem TyVars alone; they are immutable.
 1779 --
 1780 -- This function is called on both kind and type variables,
 1781 -- but kind variables *only* if PolyKinds is on.
 1782 
 1783 skolemiseQuantifiedTyVar tv
 1784   = case tcTyVarDetails tv of
 1785       SkolemTv {} -> do { kind <- zonkTcType (tyVarKind tv)
 1786                         ; return (setTyVarKind tv kind) }
 1787         -- It might be a skolem type variable,
 1788         -- for example from a user type signature
 1789 
 1790       MetaTv {} -> skolemiseUnboundMetaTyVar tv
 1791 
 1792       _other -> pprPanic "skolemiseQuantifiedTyVar" (ppr tv) -- RuntimeUnk
 1793 
 1794 defaultTyVar :: DefaultKindVars
 1795              -> DefaultVarsOfKind
 1796              -> TcTyVar   -- If it's a MetaTyVar then it is unbound
 1797              -> TcM Bool  -- True <=> defaulted away altogether
 1798 
 1799 defaultTyVar def_kindVars def_varsOfKind tv
 1800   | not (isMetaTyVar tv)
 1801   = return False
 1802 
 1803   | isTyVarTyVar tv
 1804     -- Do not default TyVarTvs. Doing so would violate the invariants
 1805     -- on TyVarTvs; see Note [TyVarTv] in GHC.Tc.Utils.TcMType.
 1806     -- #13343 is an example; #14555 is another
 1807     -- See Note [Inferring kinds for type declarations] in GHC.Tc.TyCl
 1808   = return False
 1809 
 1810 
 1811   | isRuntimeRepVar tv
 1812   , def_runtimeRep def_varsOfKind
 1813   -- Do not quantify over a RuntimeRep var
 1814   -- unless it is a TyVarTv, handled earlier
 1815   = do { traceTc "Defaulting a RuntimeRep var to LiftedRep" (ppr tv)
 1816        ; writeMetaTyVar tv liftedRepTy
 1817        ; return True }
 1818   | isLevityVar tv
 1819   , def_levity def_varsOfKind
 1820   = do { traceTc "Defaulting a Levity var to Lifted" (ppr tv)
 1821        ; writeMetaTyVar tv liftedDataConTy
 1822        ; return True }
 1823   | isMultiplicityVar tv
 1824   , def_multiplicity def_varsOfKind
 1825   = do { traceTc "Defaulting a Multiplicty var to Many" (ppr tv)
 1826        ; writeMetaTyVar tv manyDataConTy
 1827        ; return True }
 1828 
 1829   | DefaultKinds <- def_kindVars -- -XNoPolyKinds and this is a kind var
 1830   = default_kind_var tv          -- so default it to * if possible
 1831 
 1832   | otherwise
 1833   = return False
 1834 
 1835   where
 1836     default_kind_var :: TyVar -> TcM Bool
 1837        -- defaultKindVar is used exclusively with -XNoPolyKinds
 1838        -- See Note [Defaulting with -XNoPolyKinds]
 1839        -- It takes an (unconstrained) meta tyvar and defaults it.
 1840        -- Works only on vars of type *; for other kinds, it issues an error.
 1841     default_kind_var kv
 1842       | isLiftedTypeKind (tyVarKind kv)
 1843       = do { traceTc "Defaulting a kind var to *" (ppr kv)
 1844            ; writeMetaTyVar kv liftedTypeKind
 1845            ; return True }
 1846       | otherwise
 1847       = do { addErr $ TcRnUnknownMessage $ mkPlainError noHints $
 1848                (vcat [ text "Cannot default kind variable" <+> quotes (ppr kv')
 1849                      , text "of kind:" <+> ppr (tyVarKind kv')
 1850                      , text "Perhaps enable PolyKinds or add a kind signature" ])
 1851            -- We failed to default it, so return False to say so.
 1852            -- Hence, it'll get skolemised.  That might seem odd, but we must either
 1853            -- promote, skolemise, or zap-to-Any, to satisfy GHC.Tc.Gen.HsType
 1854            --    Note [Recipe for checking a signature]
 1855            -- Otherwise we get level-number assertion failures. It doesn't matter much
 1856            -- because we are in an error situation anyway.
 1857            ; return False
 1858         }
 1859       where
 1860         (_, kv') = tidyOpenTyCoVar emptyTidyEnv kv
 1861 
 1862 -- | Default some unconstrained type variables:
 1863 --     RuntimeRep tyvars default to LiftedRep
 1864 --     Multiplicity tyvars default to Many
 1865 --     Type tyvars from dv_kvs default to Type, when -XNoPolyKinds
 1866 --     (under -XNoPolyKinds, non-defaulting vars in dv_kvs is an error)
 1867 defaultTyVars :: DefaultVarsOfKind
 1868               -> CandidatesQTvs  -- ^ all candidates for quantification
 1869               -> TcM [TcTyVar]   -- ^ those variables not defaulted
 1870 defaultTyVars def_varsOfKind dvs
 1871   = do { poly_kinds <- xoptM LangExt.PolyKinds
 1872        ; let
 1873            def_kinds = if poly_kinds then Don'tDefaultKinds else DefaultKinds
 1874        ; defaulted_kvs <- mapM (defaultTyVar def_kinds         def_varsOfKind ) dep_kvs
 1875        ; defaulted_tvs <- mapM (defaultTyVar Don'tDefaultKinds def_varsOfKind ) nondep_tvs
 1876        ; let undefaulted_kvs = [ kv | (kv, False) <- dep_kvs    `zip` defaulted_kvs ]
 1877              undefaulted_tvs = [ tv | (tv, False) <- nondep_tvs `zip` defaulted_tvs ]
 1878        ; return (undefaulted_kvs ++ undefaulted_tvs) }
 1879           -- NB: kvs before tvs because tvs may depend on kvs
 1880   where
 1881     (dep_kvs, nondep_tvs) = candidateVars dvs
 1882 
 1883 skolemiseUnboundMetaTyVar :: TcTyVar -> TcM TyVar
 1884 -- We have a Meta tyvar with a ref-cell inside it
 1885 -- Skolemise it, so that we are totally out of Meta-tyvar-land
 1886 -- We create a skolem TcTyVar, not a regular TyVar
 1887 --   See Note [Zonking to Skolem]
 1888 skolemiseUnboundMetaTyVar tv
 1889   = assertPpr (isMetaTyVar tv) (ppr tv) $
 1890     do  { when debugIsOn (check_empty tv)
 1891         ; here <- getSrcSpanM    -- Get the location from "here"
 1892                                  -- ie where we are generalising
 1893         ; kind <- zonkTcType (tyVarKind tv)
 1894         ; let tv_name     = tyVarName tv
 1895               -- See Note [Skolemising and identity]
 1896               final_name | isSystemName tv_name
 1897                          = mkInternalName (nameUnique tv_name)
 1898                                           (nameOccName tv_name) here
 1899                          | otherwise
 1900                          = tv_name
 1901               final_tv = mkTcTyVar final_name kind details
 1902 
 1903         ; traceTc "Skolemising" (ppr tv <+> text ":=" <+> ppr final_tv)
 1904         ; writeMetaTyVar tv (mkTyVarTy final_tv)
 1905         ; return final_tv }
 1906 
 1907   where
 1908     details = SkolemTv (metaTyVarTcLevel tv) False
 1909     check_empty tv       -- [Sept 04] Check for non-empty.
 1910       = when debugIsOn $  -- See note [Silly Type Synonym]
 1911         do { cts <- readMetaTyVar tv
 1912            ; case cts of
 1913                Flexi       -> return ()
 1914                Indirect ty -> warnPprTrace True (ppr tv $$ ppr ty) $
 1915                               return () }
 1916 
 1917 {- Note [Error on unconstrained meta-variables]
 1918 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1919 Consider
 1920 
 1921   type C :: Type -> Type -> Constraint
 1922   class (forall a. a b ~ a c) => C b c
 1923 
 1924 or
 1925 
 1926   type T = forall a. Proxy a
 1927 
 1928 or
 1929 
 1930   data (forall a. a b ~ a c) => T b c
 1931 
 1932 We will infer a :: Type -> kappa... but then we get no further information
 1933 on kappa. What to do?
 1934 
 1935  A. We could choose kappa := Type. But this only works when the kind of kappa
 1936     is Type (true in this example, but not always).
 1937  B. We could default to Any.
 1938  C. We could quantify.
 1939  D. We could error.
 1940 
 1941 We choose (D), as described in #17567. Discussion of alternatives is below.
 1942 
 1943 NB: this is all rather similar to, but sadly not the same as
 1944     Note [Naughty quantification candidates]
 1945 
 1946 (One last example: type instance F Int = Proxy Any, where the unconstrained
 1947 kind variable is the inferred kind of Any. The four examples here illustrate
 1948 all cases in which this Note applies.)
 1949 
 1950 To do this, we must take an extra step before doing the final zonk to create
 1951 e.g. a TyCon. (There is no problem in the final term-level zonk. See the
 1952 section on alternative (B) below.) This extra step is needed only for
 1953 constructs that do not quantify their free meta-variables, such as a class
 1954 constraint or right-hand side of a type synonym.
 1955 
 1956 Specifically: before the final zonk, every construct must either call
 1957 quantifyTyVars or doNotQuantifyTyVars. The latter issues an error
 1958 if it is passed any free variables. (Exception: we still default
 1959 RuntimeRep and Multiplicity variables.)
 1960 
 1961 Because no meta-variables remain after quantifying or erroring, we perform
 1962 the zonk with NoFlexi, which panics upon seeing a meta-variable.
 1963 
 1964 Alternatives not implemented:
 1965 
 1966 A. As stated above, this works only sometimes. We might have a free
 1967    meta-variable of kind Nat, for example.
 1968 
 1969 B. This is what we used to do, but it caused Any to appear in error
 1970    messages sometimes. See #17567 for several examples. Defaulting to
 1971    Any during the final, whole-program zonk is OK, though, because
 1972    we are completely done type-checking at that point. No chance to
 1973    leak into an error message.
 1974 
 1975 C. Examine the class declaration at the top of this Note again.
 1976    Where should we quantify? We might imagine quantifying and
 1977    putting the kind variable in the forall of the quantified constraint.
 1978    But what if there are nested foralls? Which one should get the
 1979    variable? Other constructs have other problems. (For example,
 1980    the right-hand side of a type family instance equation may not
 1981    be a poly-type.)
 1982 
 1983    More broadly, the GHC AST defines a set of places where it performs
 1984    implicit lexical generalization. For example, in a type
 1985    signature
 1986 
 1987      f :: Proxy a -> Bool
 1988 
 1989    the otherwise-unbound a is lexically quantified, giving us
 1990 
 1991      f :: forall a. Proxy a -> Bool
 1992 
 1993    The places that allow lexical quantification are marked in the AST with
 1994    HsImplicitBndrs. HsImplicitBndrs offers a binding site for otherwise-unbound
 1995    variables.
 1996 
 1997    Later, during type-checking, we discover that a's kind is unconstrained.
 1998    We thus quantify *again*, to
 1999 
 2000      f :: forall {k} (a :: k). Proxy @k a -> Bool
 2001 
 2002    It is this second quantification that this Note is really about --
 2003    let's call it *inferred quantification*.
 2004    So there are two sorts of implicit quantification in types:
 2005      1. Lexical quantification: signalled by HsImplicitBndrs, occurs over
 2006         variables mentioned by the user but with no explicit binding site,
 2007         suppressed by a user-written forall (by the forall-or-nothing rule,
 2008         in Note [forall-or-nothing rule] in GHC.Hs.Type).
 2009      2. Inferred quantification: no signal in HsSyn, occurs over unconstrained
 2010         variables invented by the type-checker, possible only with -XPolyKinds,
 2011         unaffected by forall-or-nothing rule
 2012    These two quantifications are performed in different compiler phases, and are
 2013    essentially unrelated. However, it is convenient
 2014    for programmers to remember only one set of implicit quantification
 2015    sites. So, we choose to use the same places (those with HsImplicitBndrs)
 2016    for lexical quantification as for inferred quantification of unconstrained
 2017    meta-variables. Accordingly, there is no quantification in a class
 2018    constraint, or the other constructs that call doNotQuantifyTyVars.
 2019 -}
 2020 
 2021 doNotQuantifyTyVars :: CandidatesQTvs
 2022                     -> (TidyEnv -> TcM (TidyEnv, SDoc))
 2023                             -- ^ like "the class context (D a b, E foogle)"
 2024                     -> TcM ()
 2025 -- See Note [Error on unconstrained meta-variables]
 2026 doNotQuantifyTyVars dvs where_found
 2027   | isEmptyCandidates dvs
 2028   = traceTc "doNotQuantifyTyVars has nothing to error on" empty
 2029 
 2030   | otherwise
 2031   = do { traceTc "doNotQuantifyTyVars" (ppr dvs)
 2032        ; undefaulted <- defaultTyVars allVarsOfKindDefault dvs
 2033           -- could have regular TyVars here, in an associated type RHS, or
 2034           -- bound by a type declaration head. So filter looking only for
 2035           -- metavars. e.g. b and c in `class (forall a. a b ~ a c) => C b c`
 2036           -- are OK
 2037        ; let leftover_metas = filter isMetaTyVar undefaulted
 2038        ; unless (null leftover_metas) $
 2039          do { let (tidy_env1, tidied_tvs) = tidyOpenTyCoVars emptyTidyEnv leftover_metas
 2040             ; (tidy_env2, where_doc) <- where_found tidy_env1
 2041             ; let msg = TcRnUnknownMessage $ mkPlainError noHints $ pprWithExplicitKindsWhen True $
 2042                     vcat [ text "Uninferrable type variable"
 2043                            <> plural tidied_tvs
 2044                            <+> pprWithCommas pprTyVar tidied_tvs
 2045                            <+> text "in"
 2046                          , where_doc ]
 2047             ; failWithTcM (tidy_env2, msg) }
 2048        ; traceTc "doNotQuantifyTyVars success" empty }
 2049 
 2050 {- Note [Defaulting with -XNoPolyKinds]
 2051 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 2052 Consider
 2053 
 2054   data Compose f g a = Mk (f (g a))
 2055 
 2056 We infer
 2057 
 2058   Compose :: forall k1 k2. (k2 -> *) -> (k1 -> k2) -> k1 -> *
 2059   Mk :: forall k1 k2 (f :: k2 -> *) (g :: k1 -> k2) (a :: k1).
 2060         f (g a) -> Compose k1 k2 f g a
 2061 
 2062 Now, in another module, we have -XNoPolyKinds -XDataKinds in effect.
 2063 What does 'Mk mean? Pre GHC-8.0 with -XNoPolyKinds,
 2064 we just defaulted all kind variables to *. But that's no good here,
 2065 because the kind variables in 'Mk aren't of kind *, so defaulting to *
 2066 is ill-kinded.
 2067 
 2068 After some debate on #11334, we decided to issue an error in this case.
 2069 The code is in defaultKindVar.
 2070 
 2071 Note [What is a meta variable?]
 2072 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 2073 A "meta type-variable", also know as a "unification variable" is a placeholder
 2074 introduced by the typechecker for an as-yet-unknown monotype.
 2075 
 2076 For example, when we see a call `reverse (f xs)`, we know that we calling
 2077     reverse :: forall a. [a] -> [a]
 2078 So we know that the argument `f xs` must be a "list of something". But what is
 2079 the "something"? We don't know until we explore the `f xs` a bit more. So we set
 2080 out what we do know at the call of `reverse` by instantiating its type with a fresh
 2081 meta tyvar, `alpha` say. So now the type of the argument `f xs`, and of the
 2082 result, is `[alpha]`. The unification variable `alpha` stands for the
 2083 as-yet-unknown type of the elements of the list.
 2084 
 2085 As type inference progresses we may learn more about `alpha`. For example, suppose
 2086 `f` has the type
 2087     f :: forall b. b -> [Maybe b]
 2088 Then we instantiate `f`'s type with another fresh unification variable, say
 2089 `beta`; and equate `f`'s result type with reverse's argument type, thus
 2090 `[alpha] ~ [Maybe beta]`.
 2091 
 2092 Now we can solve this equality to learn that `alpha ~ Maybe beta`, so we've
 2093 refined our knowledge about `alpha`. And so on.
 2094 
 2095 If you found this Note useful, you may also want to have a look at
 2096 Section 5 of "Practical type inference for higher rank types" (Peyton Jones,
 2097 Vytiniotis, Weirich and Shields. J. Functional Programming. 2011).
 2098 
 2099 Note [What is zonking?]
 2100 ~~~~~~~~~~~~~~~~~~~~~~~
 2101 GHC relies heavily on mutability in the typechecker for efficient operation.
 2102 For this reason, throughout much of the type checking process meta type
 2103 variables (the MetaTv constructor of TcTyVarDetails) are represented by mutable
 2104 variables (known as TcRefs).
 2105 
 2106 Zonking is the process of ripping out these mutable variables and replacing them
 2107 with a real Type. This involves traversing the entire type expression, but the
 2108 interesting part of replacing the mutable variables occurs in zonkTyVarOcc.
 2109 
 2110 There are two ways to zonk a Type:
 2111 
 2112  * zonkTcTypeToType, which is intended to be used at the end of type-checking
 2113    for the final zonk. It has to deal with unfilled metavars, either by filling
 2114    it with a value like Any or failing (determined by the UnboundTyVarZonker
 2115    used).
 2116 
 2117  * zonkTcType, which will happily ignore unfilled metavars. This is the
 2118    appropriate function to use while in the middle of type-checking.
 2119 
 2120 Note [Zonking to Skolem]
 2121 ~~~~~~~~~~~~~~~~~~~~~~~~
 2122 We used to zonk quantified type variables to regular TyVars.  However, this
 2123 leads to problems.  Consider this program from the regression test suite:
 2124 
 2125   eval :: Int -> String -> String -> String
 2126   eval 0 root actual = evalRHS 0 root actual
 2127 
 2128   evalRHS :: Int -> a
 2129   evalRHS 0 root actual = eval 0 root actual
 2130 
 2131 It leads to the deferral of an equality (wrapped in an implication constraint)
 2132 
 2133   forall a. () => ((String -> String -> String) ~ a)
 2134 
 2135 which is propagated up to the toplevel (see GHC.Tc.Solver.tcSimplifyInferCheck).
 2136 In the meantime `a' is zonked and quantified to form `evalRHS's signature.
 2137 This has the *side effect* of also zonking the `a' in the deferred equality
 2138 (which at this point is being handed around wrapped in an implication
 2139 constraint).
 2140 
 2141 Finally, the equality (with the zonked `a') will be handed back to the
 2142 simplifier by GHC.Tc.Module.tcRnSrcDecls calling GHC.Tc.Solver.tcSimplifyTop.
 2143 If we zonk `a' with a regular type variable, we will have this regular type
 2144 variable now floating around in the simplifier, which in many places assumes to
 2145 only see proper TcTyVars.
 2146 
 2147 We can avoid this problem by zonking with a skolem TcTyVar.  The
 2148 skolem is rigid (which we require for a quantified variable), but is
 2149 still a TcTyVar that the simplifier knows how to deal with.
 2150 
 2151 Note [Skolemising and identity]
 2152 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 2153 In some places, we make a TyVarTv for a binder. E.g.
 2154     class C a where ...
 2155 As Note [Inferring kinds for type declarations] discusses,
 2156 we make a TyVarTv for 'a'.  Later we skolemise it, and we'd
 2157 like to retain its identity, location info etc.  (If we don't
 2158 retain its identity we'll have to do some pointless swizzling;
 2159 see GHC.Tc.TyCl.swizzleTcTyConBndrs.  If we retain its identity
 2160 but not its location we'll lose the detailed binding site info.
 2161 
 2162 Conclusion: use the Name of the TyVarTv.  But we don't want
 2163 to do that when skolemising random unification variables;
 2164 there the location we want is the skolemisation site.
 2165 
 2166 Fortunately we can tell the difference: random unification
 2167 variables have System Names.  That's why final_name is
 2168 set based on the isSystemName test.
 2169 
 2170 
 2171 Note [Silly Type Synonyms]
 2172 ~~~~~~~~~~~~~~~~~~~~~~~~~~
 2173 Consider this:
 2174         type C u a = u  -- Note 'a' unused
 2175 
 2176         foo :: (forall a. C u a -> C u a) -> u
 2177         foo x = ...
 2178 
 2179         bar :: Num u => u
 2180         bar = foo (\t -> t + t)
 2181 
 2182 * From the (\t -> t+t) we get type  {Num d} =>  d -> d
 2183   where d is fresh.
 2184 
 2185 * Now unify with type of foo's arg, and we get:
 2186         {Num (C d a)} =>  C d a -> C d a
 2187   where a is fresh.
 2188 
 2189 * Now abstract over the 'a', but float out the Num (C d a) constraint
 2190   because it does not 'really' mention a.  (see exactTyVarsOfType)
 2191   The arg to foo becomes
 2192         \/\a -> \t -> t+t
 2193 
 2194 * So we get a dict binding for Num (C d a), which is zonked to give
 2195         a = ()
 2196   [Note Sept 04: now that we are zonking quantified type variables
 2197   on construction, the 'a' will be frozen as a regular tyvar on
 2198   quantification, so the floated dict will still have type (C d a).
 2199   Which renders this whole note moot; happily!]
 2200 
 2201 * Then the \/\a abstraction has a zonked 'a' in it.
 2202 
 2203 All very silly.   I think its harmless to ignore the problem.  We'll end up with
 2204 a \/\a in the final result but all the occurrences of a will be zonked to ()
 2205 -}
 2206 
 2207 {- *********************************************************************
 2208 *                                                                      *
 2209               Promotion
 2210 *                                                                      *
 2211 ********************************************************************* -}
 2212 
 2213 promoteMetaTyVarTo :: TcLevel -> TcTyVar -> TcM Bool
 2214 -- When we float a constraint out of an implication we must restore
 2215 -- invariant (WantedInv) in Note [TcLevel invariants] in GHC.Tc.Utils.TcType
 2216 -- Return True <=> we did some promotion
 2217 -- Also returns either the original tyvar (no promotion) or the new one
 2218 -- See Note [Promoting unification variables]
 2219 promoteMetaTyVarTo tclvl tv
 2220   | assertPpr (isMetaTyVar tv) (ppr tv) $
 2221     tcTyVarLevel tv `strictlyDeeperThan` tclvl
 2222   = do { cloned_tv <- cloneMetaTyVar tv
 2223        ; let rhs_tv = setMetaTyVarTcLevel cloned_tv tclvl
 2224        ; writeMetaTyVar tv (mkTyVarTy rhs_tv)
 2225        ; traceTc "promoteTyVar" (ppr tv <+> text "-->" <+> ppr rhs_tv)
 2226        ; return True }
 2227    | otherwise
 2228    = return False
 2229 
 2230 -- Returns whether or not *any* tyvar is defaulted
 2231 promoteTyVarSet :: TcTyVarSet -> TcM Bool
 2232 promoteTyVarSet tvs
 2233   = do { tclvl <- getTcLevel
 2234        ; bools <- mapM (promoteMetaTyVarTo tclvl)  $
 2235                   filter isPromotableMetaTyVar $
 2236                   nonDetEltsUniqSet tvs
 2237          -- Non-determinism is OK because order of promotion doesn't matter
 2238        ; return (or bools) }
 2239 
 2240 
 2241 {- *********************************************************************
 2242 *                                                                      *
 2243               Zonking types
 2244 *                                                                      *
 2245 ********************************************************************* -}
 2246 
 2247 zonkTcTypeAndFV :: TcType -> TcM DTyCoVarSet
 2248 -- Zonk a type and take its free variables
 2249 -- With kind polymorphism it can be essential to zonk *first*
 2250 -- so that we find the right set of free variables.  Eg
 2251 --    forall k1. forall (a:k2). a
 2252 -- where k2:=k1 is in the substitution.  We don't want
 2253 -- k2 to look free in this type!
 2254 zonkTcTypeAndFV ty
 2255   = tyCoVarsOfTypeDSet <$> zonkTcType ty
 2256 
 2257 zonkTyCoVar :: TyCoVar -> TcM TcType
 2258 -- Works on TyVars and TcTyVars
 2259 zonkTyCoVar tv | isTcTyVar tv = zonkTcTyVar tv
 2260                | isTyVar   tv = mkTyVarTy <$> zonkTyCoVarKind tv
 2261                | otherwise    = assertPpr (isCoVar tv) (ppr tv) $
 2262                                 mkCoercionTy . mkCoVarCo <$> zonkTyCoVarKind tv
 2263    -- Hackily, when typechecking type and class decls
 2264    -- we have TyVars in scope added (only) in
 2265    -- GHC.Tc.Gen.HsType.bindTyClTyVars, but it seems
 2266    -- painful to make them into TcTyVars there
 2267 
 2268 zonkTyCoVarsAndFV :: TyCoVarSet -> TcM TyCoVarSet
 2269 zonkTyCoVarsAndFV tycovars
 2270   = tyCoVarsOfTypes <$> mapM zonkTyCoVar (nonDetEltsUniqSet tycovars)
 2271   -- It's OK to use nonDetEltsUniqSet here because we immediately forget about
 2272   -- the ordering by turning it into a nondeterministic set and the order
 2273   -- of zonking doesn't matter for determinism.
 2274 
 2275 zonkDTyCoVarSetAndFV :: DTyCoVarSet -> TcM DTyCoVarSet
 2276 zonkDTyCoVarSetAndFV tycovars
 2277   = mkDVarSet <$> (zonkTyCoVarsAndFVList $ dVarSetElems tycovars)
 2278 
 2279 -- Takes a list of TyCoVars, zonks them and returns a
 2280 -- deterministically ordered list of their free variables.
 2281 zonkTyCoVarsAndFVList :: [TyCoVar] -> TcM [TyCoVar]
 2282 zonkTyCoVarsAndFVList tycovars
 2283   = tyCoVarsOfTypesList <$> mapM zonkTyCoVar tycovars
 2284 
 2285 zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
 2286 zonkTcTyVars tyvars = mapM zonkTcTyVar tyvars
 2287 
 2288 -----------------  Types
 2289 zonkTyCoVarKind :: TyCoVar -> TcM TyCoVar
 2290 zonkTyCoVarKind tv = do { kind' <- zonkTcType (tyVarKind tv)
 2291                         ; return (setTyVarKind tv kind') }
 2292 
 2293 zonkTyCoVarKindBinder :: (VarBndr TyCoVar fl) -> TcM (VarBndr TyCoVar fl)
 2294 zonkTyCoVarKindBinder (Bndr tv fl) = do { kind' <- zonkTcType (tyVarKind tv)
 2295                                         ; return $ Bndr (setTyVarKind tv kind') fl }
 2296 
 2297 {-
 2298 ************************************************************************
 2299 *                                                                      *
 2300               Zonking constraints
 2301 *                                                                      *
 2302 ************************************************************************
 2303 -}
 2304 
 2305 zonkImplication :: Implication -> TcM Implication
 2306 zonkImplication implic@(Implic { ic_skols  = skols
 2307                                , ic_given  = given
 2308                                , ic_wanted = wanted
 2309                                , ic_info   = info })
 2310   = do { skols'  <- mapM zonkTyCoVarKind skols  -- Need to zonk their kinds!
 2311                                                 -- as #7230 showed
 2312        ; given'  <- mapM zonkEvVar given
 2313        ; info'   <- zonkSkolemInfo info
 2314        ; wanted' <- zonkWCRec wanted
 2315        ; return (implic { ic_skols  = skols'
 2316                         , ic_given  = given'
 2317                         , ic_wanted = wanted'
 2318                         , ic_info   = info' }) }
 2319 
 2320 zonkEvVar :: EvVar -> TcM EvVar
 2321 zonkEvVar var = updateIdTypeAndMultM zonkTcType var
 2322 
 2323 
 2324 zonkWC :: WantedConstraints -> TcM WantedConstraints
 2325 zonkWC wc = zonkWCRec wc
 2326 
 2327 zonkWCRec :: WantedConstraints -> TcM WantedConstraints
 2328 zonkWCRec (WC { wc_simple = simple, wc_impl = implic, wc_holes = holes })
 2329   = do { simple' <- zonkSimples simple
 2330        ; implic' <- mapBagM zonkImplication implic
 2331        ; holes'  <- mapBagM zonkHole holes
 2332        ; return (WC { wc_simple = simple', wc_impl = implic', wc_holes = holes' }) }
 2333 
 2334 zonkSimples :: Cts -> TcM Cts
 2335 zonkSimples cts = do { cts' <- mapBagM zonkCt cts
 2336                      ; traceTc "zonkSimples done:" (ppr cts')
 2337                      ; return cts' }
 2338 
 2339 zonkHole :: Hole -> TcM Hole
 2340 zonkHole hole@(Hole { hole_ty = ty })
 2341   = do { ty' <- zonkTcType ty
 2342        ; return (hole { hole_ty = ty' }) }
 2343 
 2344 {- Note [zonkCt behaviour]
 2345 ~~~~~~~~~~~~~~~~~~~~~~~~~~
 2346 zonkCt tries to maintain the canonical form of a Ct.  For example,
 2347   - a CDictCan should stay a CDictCan;
 2348   - a CIrredCan should stay a CIrredCan with its cc_reason flag intact
 2349 
 2350 Why?, for example:
 2351 - For CDictCan, the @GHC.Tc.Solver.expandSuperClasses@ step, which runs after the
 2352   simple wanted and plugin loop, looks for @CDictCan@s. If a plugin is in use,
 2353   constraints are zonked before being passed to the plugin. This means if we
 2354   don't preserve a canonical form, @expandSuperClasses@ fails to expand
 2355   superclasses. This is what happened in #11525.
 2356 
 2357 - For CIrredCan we want to see if a constraint is insoluble with insolubleWC
 2358 
 2359 On the other hand, we change CEqCan to CNonCanonical, because of all of
 2360 CEqCan's invariants, which can break during zonking. (Example: a ~R alpha, where
 2361 we have alpha := N Int, where N is a newtype.) Besides, the constraint
 2362 will be canonicalised again, so there is little benefit in keeping the
 2363 CEqCan structure.
 2364 
 2365 NB: Constraints are always rewritten etc by the canonicaliser in
 2366 @GHC.Tc.Solver.Canonical@ even if they come in as CDictCan. Only canonical constraints that
 2367 are actually in the inert set carry all the guarantees. So it is okay if zonkCt
 2368 creates e.g. a CDictCan where the cc_tyars are /not/ fully reduced.
 2369 -}
 2370 
 2371 zonkCt :: Ct -> TcM Ct
 2372 -- See Note [zonkCt behaviour]
 2373 zonkCt ct@(CDictCan { cc_ev = ev, cc_tyargs = args })
 2374   = do { ev'   <- zonkCtEvidence ev
 2375        ; args' <- mapM zonkTcType args
 2376        ; return $ ct { cc_ev = ev', cc_tyargs = args' } }
 2377 
 2378 zonkCt (CEqCan { cc_ev = ev })
 2379   = mkNonCanonical <$> zonkCtEvidence ev
 2380 
 2381 zonkCt ct@(CIrredCan { cc_ev = ev }) -- Preserve the cc_reason flag
 2382   = do { ev' <- zonkCtEvidence ev
 2383        ; return (ct { cc_ev = ev' }) }
 2384 
 2385 zonkCt ct
 2386   = do { fl' <- zonkCtEvidence (ctEvidence ct)
 2387        ; return (mkNonCanonical fl') }
 2388 
 2389 zonkCtEvidence :: CtEvidence -> TcM CtEvidence
 2390 zonkCtEvidence ctev@(CtGiven { ctev_pred = pred })
 2391   = do { pred' <- zonkTcType pred
 2392        ; return (ctev { ctev_pred = pred'}) }
 2393 zonkCtEvidence ctev@(CtWanted { ctev_pred = pred, ctev_dest = dest })
 2394   = do { pred' <- zonkTcType pred
 2395        ; let dest' = case dest of
 2396                        EvVarDest ev -> EvVarDest $ setVarType ev pred'
 2397                          -- necessary in simplifyInfer
 2398                        HoleDest h   -> HoleDest h
 2399        ; return (ctev { ctev_pred = pred', ctev_dest = dest' }) }
 2400 zonkCtEvidence ctev@(CtDerived { ctev_pred = pred })
 2401   = do { pred' <- zonkTcType pred
 2402        ; return (ctev { ctev_pred = pred' }) }
 2403 
 2404 zonkSkolemInfo :: SkolemInfo -> TcM SkolemInfo
 2405 zonkSkolemInfo (SigSkol cx ty tv_prs)  = do { ty' <- zonkTcType ty
 2406                                             ; return (SigSkol cx ty' tv_prs) }
 2407 zonkSkolemInfo (InferSkol ntys) = do { ntys' <- mapM do_one ntys
 2408                                      ; return (InferSkol ntys') }
 2409   where
 2410     do_one (n, ty) = do { ty' <- zonkTcType ty; return (n, ty') }
 2411 zonkSkolemInfo skol_info = return skol_info
 2412 
 2413 {-
 2414 %************************************************************************
 2415 %*                                                                      *
 2416 \subsection{Zonking -- the main work-horses: zonkTcType, zonkTcTyVar}
 2417 *                                                                      *
 2418 *              For internal use only!                                  *
 2419 *                                                                      *
 2420 ************************************************************************
 2421 
 2422 -}
 2423 
 2424 -- For unbound, mutable tyvars, zonkType uses the function given to it
 2425 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
 2426 --      type variable and zonks the kind too
 2427 zonkTcType  :: TcType -> TcM TcType
 2428 zonkTcTypes :: [TcType] -> TcM [TcType]
 2429 zonkCo      :: Coercion -> TcM Coercion
 2430 
 2431 (zonkTcType, zonkTcTypes, zonkCo, _)
 2432   = mapTyCo zonkTcTypeMapper
 2433 
 2434 -- | A suitable TyCoMapper for zonking a type during type-checking,
 2435 -- before all metavars are filled in.
 2436 zonkTcTypeMapper :: TyCoMapper () TcM
 2437 zonkTcTypeMapper = TyCoMapper
 2438   { tcm_tyvar = const zonkTcTyVar
 2439   , tcm_covar = const (\cv -> mkCoVarCo <$> zonkTyCoVarKind cv)
 2440   , tcm_hole  = hole
 2441   , tcm_tycobinder = \_env tv _vis -> ((), ) <$> zonkTyCoVarKind tv
 2442   , tcm_tycon      = zonkTcTyCon }
 2443   where
 2444     hole :: () -> CoercionHole -> TcM Coercion
 2445     hole _ hole@(CoercionHole { ch_ref = ref, ch_co_var = cv })
 2446       = do { contents <- readTcRef ref
 2447            ; case contents of
 2448                Just co -> do { co' <- zonkCo co
 2449                              ; checkCoercionHole cv co' }
 2450                Nothing -> do { cv' <- zonkCoVar cv
 2451                              ; return $ HoleCo (hole { ch_co_var = cv' }) } }
 2452 
 2453 zonkTcTyCon :: TcTyCon -> TcM TcTyCon
 2454 -- Only called on TcTyCons
 2455 -- A non-poly TcTyCon may have unification
 2456 -- variables that need zonking, but poly ones cannot
 2457 zonkTcTyCon tc
 2458  | tcTyConIsPoly tc = return tc
 2459  | otherwise        = do { tck' <- zonkTcType (tyConKind tc)
 2460                          ; return (setTcTyConKind tc tck') }
 2461 
 2462 zonkTcTyVar :: TcTyVar -> TcM TcType
 2463 -- Simply look through all Flexis
 2464 zonkTcTyVar tv
 2465   | isTcTyVar tv
 2466   = case tcTyVarDetails tv of
 2467       SkolemTv {}   -> zonk_kind_and_return
 2468       RuntimeUnk {} -> zonk_kind_and_return
 2469       MetaTv { mtv_ref = ref }
 2470          -> do { cts <- readMutVar ref
 2471                ; case cts of
 2472                     Flexi       -> zonk_kind_and_return
 2473                     Indirect ty -> do { zty <- zonkTcType ty
 2474                                       ; writeTcRef ref (Indirect zty)
 2475                                         -- See Note [Sharing in zonking]
 2476                                       ; return zty } }
 2477 
 2478   | otherwise -- coercion variable
 2479   = zonk_kind_and_return
 2480   where
 2481     zonk_kind_and_return = do { z_tv <- zonkTyCoVarKind tv
 2482                               ; return (mkTyVarTy z_tv) }
 2483 
 2484 -- Variant that assumes that any result of zonking is still a TyVar.
 2485 -- Should be used only on skolems and TyVarTvs
 2486 zonkTcTyVarToTyVar :: HasDebugCallStack => TcTyVar -> TcM TcTyVar
 2487 zonkTcTyVarToTyVar tv
 2488   = do { ty <- zonkTcTyVar tv
 2489        ; let tv' = case tcGetTyVar_maybe ty of
 2490                      Just tv' -> tv'
 2491                      Nothing  -> pprPanic "zonkTcTyVarToTyVar"
 2492                                           (ppr tv $$ ppr ty)
 2493        ; return tv' }
 2494 
 2495 zonkInvisTVBinder :: VarBndr TcTyVar spec -> TcM (VarBndr TyVar spec)
 2496 zonkInvisTVBinder (Bndr tv spec) = do { tv' <- zonkTcTyVarToTyVar tv
 2497                                       ; return (Bndr tv' spec) }
 2498 
 2499 -- zonkId is used *during* typechecking just to zonk the Id's type
 2500 zonkId :: TcId -> TcM TcId
 2501 zonkId id = Id.updateIdTypeAndMultM zonkTcType id
 2502 
 2503 zonkCoVar :: CoVar -> TcM CoVar
 2504 zonkCoVar = zonkId
 2505 
 2506 {- Note [Sharing in zonking]
 2507 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 2508 Suppose we have
 2509    alpha :-> beta :-> gamma :-> ty
 2510 where the ":->" means that the unification variable has been
 2511 filled in with Indirect. Then when zonking alpha, it'd be nice
 2512 to short-circuit beta too, so we end up with
 2513    alpha :-> zty
 2514    beta  :-> zty
 2515    gamma :-> zty
 2516 where zty is the zonked version of ty.  That way, if we come across
 2517 beta later, we'll have less work to do.  (And indeed the same for
 2518 alpha.)
 2519 
 2520 This is easily achieved: just overwrite (Indirect ty) with (Indirect
 2521 zty).  Non-systematic perf comparisons suggest that this is a modest
 2522 win.
 2523 
 2524 But c.f Note [Sharing when zonking to Type] in GHC.Tc.Utils.Zonk.
 2525 
 2526 %************************************************************************
 2527 %*                                                                      *
 2528                  Tidying
 2529 *                                                                      *
 2530 ************************************************************************
 2531 -}
 2532 
 2533 zonkTidyTcType :: TidyEnv -> TcType -> TcM (TidyEnv, TcType)
 2534 zonkTidyTcType env ty = do { ty' <- zonkTcType ty
 2535                            ; return (tidyOpenType env ty') }
 2536 
 2537 zonkTidyTcTypes :: TidyEnv -> [TcType] -> TcM (TidyEnv, [TcType])
 2538 zonkTidyTcTypes = zonkTidyTcTypes' []
 2539   where zonkTidyTcTypes' zs env [] = return (env, reverse zs)
 2540         zonkTidyTcTypes' zs env (ty:tys)
 2541           = do { (env', ty') <- zonkTidyTcType env ty
 2542                ; zonkTidyTcTypes' (ty':zs) env' tys }
 2543 
 2544 zonkTidyOrigin :: TidyEnv -> CtOrigin -> TcM (TidyEnv, CtOrigin)
 2545 zonkTidyOrigin env (GivenOrigin skol_info)
 2546   = do { skol_info1 <- zonkSkolemInfo skol_info
 2547        ; let skol_info2 = tidySkolemInfo env skol_info1
 2548        ; return (env, GivenOrigin skol_info2) }
 2549 zonkTidyOrigin env orig@(TypeEqOrigin { uo_actual   = act
 2550                                       , uo_expected = exp })
 2551   = do { (env1, act') <- zonkTidyTcType env  act
 2552        ; (env2, exp') <- zonkTidyTcType env1 exp
 2553        ; return ( env2, orig { uo_actual   = act'
 2554                              , uo_expected = exp' }) }
 2555 zonkTidyOrigin env (KindEqOrigin ty1 ty2 orig t_or_k)
 2556   = do { (env1, ty1')  <- zonkTidyTcType env  ty1
 2557        ; (env2, ty2')  <- zonkTidyTcType env1 ty2
 2558        ; (env3, orig') <- zonkTidyOrigin env2 orig
 2559        ; return (env3, KindEqOrigin ty1' ty2' orig' t_or_k) }
 2560 zonkTidyOrigin env (FunDepOrigin1 p1 o1 l1 p2 o2 l2)
 2561   = do { (env1, p1') <- zonkTidyTcType env  p1
 2562        ; (env2, p2') <- zonkTidyTcType env1 p2
 2563        ; return (env2, FunDepOrigin1 p1' o1 l1 p2' o2 l2) }
 2564 zonkTidyOrigin env (FunDepOrigin2 p1 o1 p2 l2)
 2565   = do { (env1, p1') <- zonkTidyTcType env  p1
 2566        ; (env2, p2') <- zonkTidyTcType env1 p2
 2567        ; (env3, o1') <- zonkTidyOrigin env2 o1
 2568        ; return (env3, FunDepOrigin2 p1' o1' p2' l2) }
 2569 zonkTidyOrigin env (CycleBreakerOrigin orig)
 2570   = do { (env1, orig') <- zonkTidyOrigin env orig
 2571        ; return (env1, CycleBreakerOrigin orig') }
 2572 zonkTidyOrigin env (InstProvidedOrigin mod cls_inst)
 2573   = do { (env1, is_tys') <- mapAccumLM zonkTidyTcType env (is_tys cls_inst)
 2574        ; return (env1, InstProvidedOrigin mod (cls_inst {is_tys = is_tys'})) }
 2575 zonkTidyOrigin env (FixedRuntimeRepOrigin ty frr_orig)
 2576   = do { (env1, ty') <- zonkTidyTcType env ty
 2577        ; return (env1, FixedRuntimeRepOrigin ty' frr_orig)}
 2578 zonkTidyOrigin env orig = return (env, orig)
 2579 
 2580 zonkTidyOrigins :: TidyEnv -> [CtOrigin] -> TcM (TidyEnv, [CtOrigin])
 2581 zonkTidyOrigins = mapAccumLM zonkTidyOrigin
 2582 
 2583 ----------------
 2584 tidyCt :: TidyEnv -> Ct -> Ct
 2585 -- Used only in error reporting
 2586 tidyCt env ct
 2587   = ct { cc_ev = tidy_ev (ctEvidence ct) }
 2588   where
 2589     tidy_ev :: CtEvidence -> CtEvidence
 2590      -- NB: we do not tidy the ctev_evar field because we don't
 2591      --     show it in error messages
 2592     tidy_ev ctev = ctev { ctev_pred = tidyType env (ctev_pred ctev) }
 2593 
 2594 tidyHole :: TidyEnv -> Hole -> Hole
 2595 tidyHole env h@(Hole { hole_ty = ty }) = h { hole_ty = tidyType env ty }
 2596 
 2597 ----------------
 2598 tidyEvVar :: TidyEnv -> EvVar -> EvVar
 2599 tidyEvVar env var = updateIdTypeAndMult (tidyType env) var
 2600 
 2601 ----------------
 2602 tidySkolemInfo :: TidyEnv -> SkolemInfo -> SkolemInfo
 2603 tidySkolemInfo env (DerivSkol ty)         = DerivSkol (tidyType env ty)
 2604 tidySkolemInfo env (SigSkol cx ty tv_prs) = tidySigSkol env cx ty tv_prs
 2605 tidySkolemInfo env (InferSkol ids)        = InferSkol (mapSnd (tidyType env) ids)
 2606 tidySkolemInfo env (UnifyForAllSkol ty)   = UnifyForAllSkol (tidyType env ty)
 2607 tidySkolemInfo _   info                   = info
 2608 
 2609 tidySigSkol :: TidyEnv -> UserTypeCtxt
 2610             -> TcType -> [(Name,TcTyVar)] -> SkolemInfo
 2611 -- We need to take special care when tidying SigSkol
 2612 -- See Note [SigSkol SkolemInfo] in "GHC.Tc.Types.Origin"
 2613 tidySigSkol env cx ty tv_prs
 2614   = SigSkol cx (tidy_ty env ty) tv_prs'
 2615   where
 2616     tv_prs' = mapSnd (tidyTyCoVarOcc env) tv_prs
 2617     inst_env = mkNameEnv tv_prs'
 2618 
 2619     tidy_ty env (ForAllTy (Bndr tv vis) ty)
 2620       = ForAllTy (Bndr tv' vis) (tidy_ty env' ty)
 2621       where
 2622         (env', tv') = tidy_tv_bndr env tv
 2623 
 2624     tidy_ty env ty@(FunTy InvisArg w arg res) -- Look under  c => t
 2625       = ty { ft_mult = tidy_ty env w,
 2626              ft_arg = tidyType env arg,
 2627              ft_res = tidy_ty env res }
 2628 
 2629     tidy_ty env ty = tidyType env ty
 2630 
 2631     tidy_tv_bndr :: TidyEnv -> TyCoVar -> (TidyEnv, TyCoVar)
 2632     tidy_tv_bndr env@(occ_env, subst) tv
 2633       | Just tv' <- lookupNameEnv inst_env (tyVarName tv)
 2634       = ((occ_env, extendVarEnv subst tv tv'), tv')
 2635 
 2636       | otherwise
 2637       = tidyVarBndr env tv
 2638 
 2639 -------------------------------------------------------------------------
 2640 {-
 2641 %************************************************************************
 2642 %*                                                                      *
 2643              Representation polymorphism checks
 2644 *                                                                       *
 2645 ***********************************************************************-}
 2646 
 2647 -- | Check that the specified type has a fixed runtime representation.
 2648 --
 2649 -- If it isn't, throw a representation-polymorphism error appropriate
 2650 -- for the context (as specified by the 'FixedRuntimeRepProvenance').
 2651 --
 2652 -- Unlike the other representation polymorphism checks, which emit
 2653 -- 'Concrete#' constraints, this function does not emit any constraints,
 2654 -- as it has enough information to immediately make a decision.
 2655 --
 2656 -- See (1) in Note [Representation polymorphism checking] in GHC.Tc.Utils.Concrete
 2657 checkTypeHasFixedRuntimeRep :: FixedRuntimeRepProvenance -> Type -> TcM ()
 2658 checkTypeHasFixedRuntimeRep prov ty =
 2659   unless (typeHasFixedRuntimeRep ty)
 2660     (addDetailedDiagnostic $ TcRnTypeDoesNotHaveFixedRuntimeRep ty prov)
 2661 
 2662 {-
 2663 %************************************************************************
 2664 %*                                                                      *
 2665              Error messages
 2666 *                                                                       *
 2667 *************************************************************************
 2668 
 2669 -}
 2670 
 2671 -- See Note [Naughty quantification candidates]
 2672 naughtyQuantification :: TcType   -- original type user wanted to quantify
 2673                       -> TcTyVar  -- naughty var
 2674                       -> TyVarSet -- skolems that would escape
 2675                       -> TcM a
 2676 naughtyQuantification orig_ty tv escapees
 2677   = do { orig_ty1 <- zonkTcType orig_ty  -- in case it's not zonked
 2678 
 2679        ; escapees' <- mapM zonkTcTyVarToTyVar $
 2680                       nonDetEltsUniqSet escapees
 2681                      -- we'll just be printing, so no harmful non-determinism
 2682 
 2683        ; let fvs  = tyCoVarsOfTypeWellScoped orig_ty1
 2684              env0 = tidyFreeTyCoVars emptyTidyEnv fvs
 2685              env  = env0 `delTidyEnvList` escapees'
 2686                     -- this avoids gratuitous renaming of the escaped
 2687                     -- variables; very confusing to users!
 2688 
 2689              orig_ty'   = tidyType env orig_ty1
 2690              ppr_tidied = pprTyVars . map (tidyTyCoVarOcc env)
 2691              msg = TcRnUnknownMessage $ mkPlainError noHints $
 2692                    pprWithExplicitKindsWhen True $
 2693                    vcat [ sep [ text "Cannot generalise type; skolem" <> plural escapees'
 2694                               , quotes $ ppr_tidied escapees'
 2695                               , text "would escape" <+> itsOrTheir escapees' <+> text "scope"
 2696                               ]
 2697                         , sep [ text "if I tried to quantify"
 2698                               , ppr_tidied [tv]
 2699                               , text "in this type:"
 2700                               ]
 2701                         , nest 2 (pprTidiedType orig_ty')
 2702                         , text "(Indeed, I sometimes struggle even printing this correctly,"
 2703                         , text " due to its ill-scoped nature.)"
 2704                         ]
 2705 
 2706        ; failWithTcM (env, msg) }