TcMType.hs 69.1 KB
Newer Older
Austin Seipp's avatar
Austin Seipp committed
1 2 3 4
{-
(c) The University of Glasgow 2006
(c) The GRASP/AQUA Project, Glasgow University, 1992-1998

5

6 7 8 9
Monadic type operations

This module contains monadic operations over types that contain
mutable type variables
Austin Seipp's avatar
Austin Seipp committed
10
-}
11

12
{-# LANGUAGE CPP, TupleSections, MultiWayIf #-}
Ian Lynagh's avatar
Ian Lynagh committed
13

14
module TcMType (
15
  TcTyVar, TcKind, TcType, TcTauType, TcThetaType, TcTyVarSet,
16 17 18

  --------------------------------
  -- Creating new mutable type variables
19
  newFlexiTyVar,
20 21
  newFlexiTyVarTy,              -- Kind -> TcM TcType
  newFlexiTyVarTys,             -- Int -> Kind -> TcM [TcType]
22 23
  newOpenFlexiTyVarTy, newOpenTypeKind,
  newMetaKindVar, newMetaKindVars, newMetaTyVarTyAtLevel,
24 25
  cloneMetaTyVar,
  newFmvTyVar, newFskTyVar,
26

27
  readMetaTyVar, writeMetaTyVar,
28
  newMetaDetails, isFilledMetaTyVar, isUnfilledMetaTyVar,
29

30 31 32
  --------------------------------
  -- Expected types
  ExpType(..), ExpSigmaType, ExpRhoType,
33 34 35 36
  mkCheckExpType,
  newInferExpType, newInferExpTypeInst, newInferExpTypeNoInst,
  readExpType, readExpType_maybe,
  expTypeToType, checkingExpType_maybe, checkingExpType,
37
  tauifyExpType, inferResultToType,
38

39
  --------------------------------
40
  -- Creating new evidence variables
41
  newEvVar, newEvVars, newDict,
42
  newWanted, newWanteds, cloneWanted, cloneWC,
43
  emitWanted, emitWantedEq, emitWantedEvVar, emitWantedEvVars,
44
  newTcEvBinds, newNoTcEvBinds, addTcEvBind,
45

46 47 48 49
  newCoercionHole, fillCoercionHole, isFilledCoercionHole,
  unpackCoercionHole, unpackCoercionHole_maybe,
  checkCoercionHole,

50 51
  --------------------------------
  -- Instantiation
52
  newMetaTyVars, newMetaTyVarX, newMetaTyVarsX,
53
  newMetaSigTyVars, newMetaSigTyVarX,
54
  newSigTyVar, newSkolemTyVar, newWildCardX,
55
  tcInstType,
56 57
  tcInstSkolTyVars,tcInstSkolTyVarsX,
  tcInstSuperSkolTyVarsX,
58
  tcSkolDFunType, tcSuperSkolTyVars,
59

60
  instSkolTyCoVarsX, freshenTyVarBndrs, freshenCoVarBndrsX,
61

62
  --------------------------------
63
  -- Zonking and tidying
64
  zonkTidyTcType, zonkTidyTcTypes, zonkTidyOrigin,
65
  tidyEvVar, tidyCt, tidySkolemInfo,
66
  skolemiseRuntimeUnk,
67 68
  zonkTcTyVar, zonkTcTyVars,
  zonkTcTyVarToTyVar, zonkSigTyVarPairs,
69
  zonkTyCoVarsAndFV, zonkTcTypeAndFV,
70
  zonkTyCoVarsAndFVList,
71
  zonkTcTypeAndSplitDepVars, zonkTcTypesAndSplitDepVars,
72
  zonkQuantifiedTyVar, defaultTyVar,
73
  quantifyTyVars,
Simon Peyton Jones's avatar
Simon Peyton Jones committed
74
  zonkTcTyCoVarBndr, zonkTcTyVarBinder,
75
  zonkTcType, zonkTcTypes, zonkCo,
76
  zonkTyCoVarKind, zonkTcTypeMapper,
77
  zonkTcTypeInKnot,
78

Simon Peyton Jones's avatar
Simon Peyton Jones committed
79 80 81
  zonkEvVar, zonkWC, zonkSimples,
  zonkId, zonkCoVar,
  zonkCt, zonkSkolemInfo,
82

83 84 85 86 87
  tcGetGlobalTyCoVars,

  ------------------------------
  -- Levity polymorphism
  ensureNotLevPoly, checkForLevPoly, checkForLevPolyX, formatLevPolyErr
88 89 90 91 92
  ) where

#include "HsVersions.h"

-- friends:
93 94
import GhcPrelude

95
import TyCoRep
96 97
import TcType
import Type
98
import Coercion
99 100
import Class
import Var
101 102

-- others:
103
import TcRnMonad        -- TcType, amongst others
104
import TcEvidence
105
import Id
106
import Name
107
import VarSet
108 109 110
import TysWiredIn
import TysPrim
import VarEnv
111
import NameEnv
112
import PrelNames
113
import Util
114
import Outputable
115
import FastString
Simon Peyton Jones's avatar
Simon Peyton Jones committed
116
import SrcLoc
117
import Bag
118
import Pair
David Feuer's avatar
David Feuer committed
119
import UniqSet
120
import qualified GHC.LanguageExtensions as LangExt
121

Ian Lynagh's avatar
Ian Lynagh committed
122
import Control.Monad
123
import Maybes
124
import Data.List        ( mapAccumL )
125
import Control.Arrow    ( second )
126

Austin Seipp's avatar
Austin Seipp committed
127 128 129
{-
************************************************************************
*                                                                      *
130
        Kind variables
Austin Seipp's avatar
Austin Seipp committed
131 132 133
*                                                                      *
************************************************************************
-}
134

135 136 137
mkKindName :: Unique -> Name
mkKindName unique = mkSystemName unique kind_var_occ

138 139
kind_var_occ :: OccName -- Just one for all MetaKindVars
                        -- They may be jiggled by tidying
140 141
kind_var_occ = mkOccName tvName "k"

dreixel's avatar
dreixel committed
142
newMetaKindVar :: TcM TcKind
143
newMetaKindVar = do { uniq <- newUnique
144
                    ; details <- newMetaDetails TauTv
145
                    ; let kv = mkTcTyVar (mkKindName uniq) liftedTypeKind details
146
                    ; traceTc "newMetaKindVar" (ppr kv)
147
                    ; return (mkTyVarTy kv) }
148

dreixel's avatar
dreixel committed
149 150
newMetaKindVars :: Int -> TcM [TcKind]
newMetaKindVars n = mapM (\ _ -> newMetaKindVar) (nOfThem n ())
151

Austin Seipp's avatar
Austin Seipp committed
152 153 154
{-
************************************************************************
*                                                                      *
155
     Evidence variables; range over constraints we can abstract over
Austin Seipp's avatar
Austin Seipp committed
156 157 158
*                                                                      *
************************************************************************
-}
159

160 161 162
newEvVars :: TcThetaType -> TcM [EvVar]
newEvVars theta = mapM newEvVar theta

163
--------------
batterseapower's avatar
batterseapower committed
164

165
newEvVar :: TcPredType -> TcRnIf gbl lcl EvVar
166
-- Creates new *rigid* variables for predicates
167
newEvVar ty = do { name <- newSysName (predTypeOccName ty)
168 169 170
                 ; return (mkLocalIdOrCoVar name ty) }

newWanted :: CtOrigin -> Maybe TypeOrKind -> PredType -> TcM CtEvidence
171
-- Deals with both equality and non-equality predicates
172 173
newWanted orig t_or_k pty
  = do loc <- getCtLocM orig t_or_k
Simon Peyton Jones's avatar
Simon Peyton Jones committed
174
       d <- if isEqPred pty then HoleDest  <$> newCoercionHole pty
175 176 177
                            else EvVarDest <$> newEvVar pty
       return $ CtWanted { ctev_dest = d
                         , ctev_pred = pty
178
                         , ctev_nosh = WDeriv
179 180 181 182 183
                         , ctev_loc = loc }

newWanteds :: CtOrigin -> ThetaType -> TcM [CtEvidence]
newWanteds orig = mapM (newWanted orig Nothing)

184 185 186
----------------------------------------------
-- Cloning constraints
----------------------------------------------
187

188 189 190 191 192 193 194
cloneWanted :: Ct -> TcM Ct
cloneWanted ct
  | ev@(CtWanted { ctev_dest = HoleDest {}, ctev_pred = pty }) <- ctEvidence ct
  = do { co_hole <- newCoercionHole pty
       ; return (mkNonCanonical (ev { ctev_dest = HoleDest co_hole })) }
  | otherwise
  = return ct
195

196
cloneWC :: WantedConstraints -> TcM WantedConstraints
197 198 199 200 201
-- Clone all the evidence bindings in
--   a) the ic_bind field of any implications
--   b) the CoercionHoles of any wanted constraints
-- so that solving the WantedConstraints will not have any visible side
-- effect, /except/ from causing unifications
202
cloneWC wc@(WC { wc_simple = simples, wc_impl = implics })
203 204
  = do { simples' <- mapBagM cloneWanted simples
       ; implics' <- mapBagM cloneImplication implics
205
       ; return (wc { wc_simple = simples', wc_impl = implics' }) }
206 207 208 209 210 211 212 213 214 215

cloneImplication :: Implication -> TcM Implication
cloneImplication implic@(Implic { ic_binds = binds, ic_wanted = inner_wanted })
  = do { binds'        <- cloneEvBindsVar binds
       ; inner_wanted' <- cloneWC inner_wanted
       ; return (implic { ic_binds = binds', ic_wanted = inner_wanted' }) }

----------------------------------------------
-- Emitting constraints
----------------------------------------------
216

217
-- | Emits a new Wanted. Deals with both equalities and non-equalities.
218
emitWanted :: CtOrigin -> TcPredType -> TcM EvTerm
219 220 221
emitWanted origin pty
  = do { ev <- newWanted origin Nothing pty
       ; emitSimple $ mkNonCanonical ev
222
       ; return $ ctEvTerm ev }
223 224 225 226

-- | Emits a new equality constraint
emitWantedEq :: CtOrigin -> TypeOrKind -> Role -> TcType -> TcType -> TcM Coercion
emitWantedEq origin t_or_k role ty1 ty2
Simon Peyton Jones's avatar
Simon Peyton Jones committed
227
  = do { hole <- newCoercionHole pty
228 229
       ; loc <- getCtLocM origin (Just t_or_k)
       ; emitSimple $ mkNonCanonical $
230 231
         CtWanted { ctev_pred = pty, ctev_dest = HoleDest hole
                  , ctev_nosh = WDeriv, ctev_loc = loc }
Simon Peyton Jones's avatar
Simon Peyton Jones committed
232
       ; return (HoleCo hole) }
233 234 235 236 237 238 239 240 241 242 243
  where
    pty = mkPrimEqPredRole role ty1 ty2

-- | Creates a new EvVar and immediately emits it as a Wanted.
-- No equality predicates here.
emitWantedEvVar :: CtOrigin -> TcPredType -> TcM EvVar
emitWantedEvVar origin ty
  = do { new_cv <- newEvVar ty
       ; loc <- getCtLocM origin Nothing
       ; let ctev = CtWanted { ctev_dest = EvVarDest new_cv
                             , ctev_pred = ty
244
                             , ctev_nosh = WDeriv
245 246 247 248 249 250
                             , ctev_loc  = loc }
       ; emitSimple $ mkNonCanonical ctev
       ; return new_cv }

emitWantedEvVars :: CtOrigin -> [TcPredType] -> TcM [EvVar]
emitWantedEvVars orig = mapM (emitWantedEvVar orig)
251 252

newDict :: Class -> [TcType] -> TcM DictId
253
newDict cls tys
254
  = do { name <- newSysName (mkDictOcc (getOccName cls))
batterseapower's avatar
batterseapower committed
255 256 257
       ; return (mkLocalId name (mkClassPred cls tys)) }

predTypeOccName :: PredType -> OccName
258
predTypeOccName ty = case classifyPredType ty of
batterseapower's avatar
batterseapower committed
259
    ClassPred cls _ -> mkDictOcc (getOccName cls)
260 261 262
    EqPred {}       -> mkVarOccFS (fsLit "co")
    IrredPred {}    -> mkVarOccFS (fsLit "irred")
    ForAllPred {}   -> mkVarOccFS (fsLit "df")
263

264 265 266 267 268 269 270 271
{-
************************************************************************
*                                                                      *
        Coercion holes
*                                                                      *
************************************************************************
-}

Simon Peyton Jones's avatar
Simon Peyton Jones committed
272 273 274 275
newCoercionHole :: TcPredType -> TcM CoercionHole
newCoercionHole pred_ty
  = do { co_var <- newEvVar pred_ty
       ; traceTc "New coercion hole:" (ppr co_var)
276
       ; ref <- newMutVar Nothing
Simon Peyton Jones's avatar
Simon Peyton Jones committed
277
       ; return $ CoercionHole { ch_co_var = co_var, ch_ref = ref } }
278 279 280

-- | Put a value in a coercion hole
fillCoercionHole :: CoercionHole -> Coercion -> TcM ()
Simon Peyton Jones's avatar
Simon Peyton Jones committed
281
fillCoercionHole (CoercionHole { ch_ref = ref, ch_co_var = cv }) co
282
  = do {
Ben Gamari's avatar
Ben Gamari committed
283
#if defined(DEBUG)
284 285
       ; cts <- readTcRef ref
       ; whenIsJust cts $ \old_co ->
Simon Peyton Jones's avatar
Simon Peyton Jones committed
286
         pprPanic "Filling a filled coercion hole" (ppr cv $$ ppr co $$ ppr old_co)
287
#endif
Simon Peyton Jones's avatar
Simon Peyton Jones committed
288
       ; traceTc "Filling coercion hole" (ppr cv <+> text ":=" <+> ppr co)
289 290 291 292
       ; writeTcRef ref (Just co) }

-- | Is a coercion hole filled in?
isFilledCoercionHole :: CoercionHole -> TcM Bool
Simon Peyton Jones's avatar
Simon Peyton Jones committed
293
isFilledCoercionHole (CoercionHole { ch_ref = ref }) = isJust <$> readTcRef ref
294 295 296 297 298 299 300 301 302 303 304 305

-- | Retrieve the contents of a coercion hole. Panics if the hole
-- is unfilled
unpackCoercionHole :: CoercionHole -> TcM Coercion
unpackCoercionHole hole
  = do { contents <- unpackCoercionHole_maybe hole
       ; case contents of
           Just co -> return co
           Nothing -> pprPanic "Unfilled coercion hole" (ppr hole) }

-- | Retrieve the contents of a coercion hole, if it is filled
unpackCoercionHole_maybe :: CoercionHole -> TcM (Maybe Coercion)
Simon Peyton Jones's avatar
Simon Peyton Jones committed
306
unpackCoercionHole_maybe (CoercionHole { ch_ref = ref }) = readTcRef ref
307 308 309 310 311 312

-- | Check that a coercion is appropriate for filling a hole. (The hole
-- itself is needed only for printing. NB: This must be /lazy/ in the coercion,
-- as it's used in TcHsSyn in the presence of knots.
-- Always returns the checked coercion, but this return value is necessary
-- so that the input coercion is forced only when the output is forced.
Simon Peyton Jones's avatar
Simon Peyton Jones committed
313 314
checkCoercionHole :: CoVar -> Coercion -> TcM Coercion
checkCoercionHole cv co
315
  | debugIsOn
Simon Peyton Jones's avatar
Simon Peyton Jones committed
316 317
  = do { cv_ty <- zonkTcType (varType cv)
                  -- co is already zonked, but cv might not be
318
       ; return $
Simon Peyton Jones's avatar
Simon Peyton Jones committed
319
         ASSERT2( ok cv_ty
320
                , (text "Bad coercion hole" <+>
Simon Peyton Jones's avatar
Simon Peyton Jones committed
321 322
                   ppr cv <> colon <+> vcat [ ppr t1, ppr t2, ppr role
                                            , ppr cv_ty ]) )
323 324 325 326
         co }
  | otherwise
  = return co

Simon Peyton Jones's avatar
Simon Peyton Jones committed
327 328 329 330 331 332 333 334 335
  where
    (Pair t1 t2, role) = coercionKindRole co
    ok cv_ty | EqPred cv_rel cv_t1 cv_t2 <- classifyPredType cv_ty
             =  t1 `eqType` cv_t1
             && t2 `eqType` cv_t2
             && role == eqRelRole cv_rel
             | otherwise
             = False

336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387
{-
************************************************************************
*
    Expected types
*
************************************************************************

Note [ExpType]
~~~~~~~~~~~~~~

An ExpType is used as the "expected type" when type-checking an expression.
An ExpType can hold a "hole" that can be filled in by the type-checker.
This allows us to have one tcExpr that works in both checking mode and
synthesis mode (that is, bidirectional type-checking). Previously, this
was achieved by using ordinary unification variables, but we don't need
or want that generality. (For example, #11397 was caused by doing the
wrong thing with unification variables.) Instead, we observe that these
holes should

1. never be nested
2. never appear as the type of a variable
3. be used linearly (never be duplicated)

By defining ExpType, separately from Type, we can achieve goals 1 and 2
statically.

See also [wiki:Typechecking]

Note [TcLevel of ExpType]
~~~~~~~~~~~~~~~~~~~~~~~~~
Consider

  data G a where
    MkG :: G Bool

  foo MkG = True

This is a classic untouchable-variable / ambiguous GADT return type
scenario. But, with ExpTypes, we'll be inferring the type of the RHS.
And, because there is only one branch of the case, we won't trigger
Note [Case branches must never infer a non-tau type] of TcMatches.
We thus must track a TcLevel in an Inferring ExpType. If we try to
fill the ExpType and find that the TcLevels don't work out, we
fill the ExpType with a tau-tv at the low TcLevel, hopefully to
be worked out later by some means. This is triggered in
test gadt/gadt-escape1.

-}

-- actual data definition is in TcType

-- | Make an 'ExpType' suitable for inferring a type of kind * or #.
388 389 390 391 392 393 394 395
newInferExpTypeNoInst :: TcM ExpSigmaType
newInferExpTypeNoInst = newInferExpType False

newInferExpTypeInst :: TcM ExpRhoType
newInferExpTypeInst = newInferExpType True

newInferExpType :: Bool -> TcM ExpType
newInferExpType inst
396
  = do { u <- newUnique
397
       ; tclvl <- getTcLevel
398
       ; traceTc "newOpenInferExpType" (ppr u <+> ppr inst <+> ppr tclvl)
399
       ; ref <- newMutVar Nothing
400
       ; return (Infer (IR { ir_uniq = u, ir_lvl = tclvl
401
                           , ir_ref = ref, ir_inst = inst })) }
402 403 404 405

-- | Extract a type out of an ExpType, if one exists. But one should always
-- exist. Unless you're quite sure you know what you're doing.
readExpType_maybe :: ExpType -> TcM (Maybe TcType)
406 407
readExpType_maybe (Check ty)                   = return (Just ty)
readExpType_maybe (Infer (IR { ir_ref = ref})) = readMutVar ref
408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427

-- | Extract a type out of an ExpType. Otherwise, panics.
readExpType :: ExpType -> TcM TcType
readExpType exp_ty
  = do { mb_ty <- readExpType_maybe exp_ty
       ; case mb_ty of
           Just ty -> return ty
           Nothing -> pprPanic "Unknown expected type" (ppr exp_ty) }

-- | Returns the expected type when in checking mode.
checkingExpType_maybe :: ExpType -> Maybe TcType
checkingExpType_maybe (Check ty) = Just ty
checkingExpType_maybe _          = Nothing

-- | Returns the expected type when in checking mode. Panics if in inference
-- mode.
checkingExpType :: String -> ExpType -> TcType
checkingExpType _   (Check ty) = ty
checkingExpType err et         = pprPanic "checkingExpType" (text err $$ ppr et)

428 429
tauifyExpType :: ExpType -> TcM ExpType
-- ^ Turn a (Infer hole) type into a (Check alpha),
430
-- where alpha is a fresh unification variable
431 432 433
tauifyExpType (Check ty)      = return (Check ty)  -- No-op for (Check ty)
tauifyExpType (Infer inf_res) = do { ty <- inferResultToType inf_res
                                   ; return (Check ty) }
434

435 436 437
-- | Extracts the expected type if there is one, or generates a new
-- TauTv if there isn't.
expTypeToType :: ExpType -> TcM TcType
438 439 440 441 442
expTypeToType (Check ty)      = return ty
expTypeToType (Infer inf_res) = inferResultToType inf_res

inferResultToType :: InferResult -> TcM Type
inferResultToType (IR { ir_uniq = u, ir_lvl = tc_lvl
443 444 445
                      , ir_ref = ref })
  = do { rr  <- newMetaTyVarTyAtLevel tc_lvl runtimeRepTy
       ; tau <- newMetaTyVarTyAtLevel tc_lvl (tYPE rr)
446
             -- See Note [TcLevel of ExpType]
447 448
       ; writeMutVar ref (Just tau)
       ; traceTc "Forcing ExpType to be monomorphic:"
449
                 (ppr u <+> text ":=" <+> ppr tau)
450
       ; return tau }
451

452

453
{- *********************************************************************
Austin Seipp's avatar
Austin Seipp committed
454
*                                                                      *
455
        SkolemTvs (immutable)
Austin Seipp's avatar
Austin Seipp committed
456
*                                                                      *
457
********************************************************************* -}
458

459 460
tcInstType :: ([TyVar] -> TcM (TCvSubst, [TcTyVar]))
                   -- ^ How to instantiate the type variables
461 462
           -> Id                                            -- ^ Type to instantiate
           -> TcM ([(Name, TcTyVar)], TcThetaType, TcType)  -- ^ Result
463
                -- (type vars, preds (incl equalities), rho)
464 465
tcInstType inst_tyvars id
  = case tcSplitForAllTys (idType id) of
466
        ([],    rho) -> let     -- There may be overloading despite no type variables;
467
                                --      (?x :: Int) => Int -> Int
468 469 470
                                (theta, tau) = tcSplitPhiTy rho
                            in
                            return ([], theta, tau)
471

472
        (tyvars, rho) -> do { (subst, tyvars') <- inst_tyvars tyvars
473
                            ; let (theta, tau) = tcSplitPhiTy (substTyAddInScope subst rho)
474 475
                                  tv_prs       = map tyVarName tyvars `zip` tyvars'
                            ; return (tv_prs, theta, tau) }
476

477
tcSkolDFunType :: DFunId -> TcM ([TcTyVar], TcThetaType, TcType)
478 479
-- Instantiate a type signature with skolem constants.
-- We could give them fresh names, but no need to do so
480 481 482
tcSkolDFunType dfun
  = do { (tv_prs, theta, tau) <- tcInstType tcInstSuperSkolTyVars dfun
       ; return (map snd tv_prs, theta, tau) }
483

484
tcSuperSkolTyVars :: [TyVar] -> (TCvSubst, [TcTyVar])
485
-- Make skolem constants, but do *not* give them new names, as above
486
-- Moreover, make them "super skolems"; see comments with superSkolemTv
dreixel's avatar
dreixel committed
487
-- see Note [Kind substitution when instantiating]
488
-- Precondition: tyvars should be ordered by scoping
489
tcSuperSkolTyVars = mapAccumL tcSuperSkolTyVar emptyTCvSubst
490

491
tcSuperSkolTyVar :: TCvSubst -> TyVar -> (TCvSubst, TcTyVar)
492
tcSuperSkolTyVar subst tv
493
  = (extendTvSubstWithClone subst tv new_tv, new_tv)
dreixel's avatar
dreixel committed
494
  where
495
    kind   = substTyUnchecked subst (tyVarKind tv)
496 497
    new_tv = mkTcTyVar (tyVarName tv) kind superSkolemTv

498 499 500 501 502 503
-- | Given a list of @['TyVar']@, skolemize the type variables,
-- returning a substitution mapping the original tyvars to the
-- skolems, and the list of newly bound skolems.  See also
-- tcInstSkolTyVars' for a precondition.  The resulting
-- skolems are non-overlappable; see Note [Overlap and deriving]
-- for an example where this matters.
504
tcInstSkolTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
505 506 507 508
tcInstSkolTyVars = tcInstSkolTyVarsX emptyTCvSubst

tcInstSkolTyVarsX :: TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
tcInstSkolTyVarsX = tcInstSkolTyVars' False
dreixel's avatar
dreixel committed
509

510 511 512 513
tcInstSuperSkolTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
tcInstSuperSkolTyVars = tcInstSuperSkolTyVarsX emptyTCvSubst

tcInstSuperSkolTyVarsX :: TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
514
tcInstSuperSkolTyVarsX subst = tcInstSkolTyVars' True subst
515

516
tcInstSkolTyVars' :: Bool -> TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
517 518
-- Precondition: tyvars should be ordered (kind vars first)
-- see Note [Kind substitution when instantiating]
519
-- Get the location from the monad; this is a complete freshening operation
520
tcInstSkolTyVars' overlappable subst tvs
521
  = do { loc <- getSrcSpanM
522 523
       ; lvl <- getTcLevel
       ; instSkolTyCoVarsX (mkTcSkolTyVar lvl loc overlappable) subst tvs }
524

525
mkTcSkolTyVar :: TcLevel -> SrcSpan -> Bool -> TcTyCoVarMaker gbl lcl
526 527 528
-- Allocates skolems whose level is ONE GREATER THAN the passed-in tc_lvl
-- See Note [Skolem level allocation]
mkTcSkolTyVar tc_lvl loc overlappable old_name kind
529 530 531
  = do { uniq <- newUnique
       ; let name = mkInternalName uniq (getOccName old_name) loc
       ; return (mkTcTyVar name kind details) }
532
  where
533 534 535 536 537 538 539 540 541 542 543
    details = SkolemTv (pushTcLevel tc_lvl) overlappable
              -- pushTcLevel: see Note [Skolem level allocation]

{- Note [Skolem level allocation]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We generally allocate skolems /before/ calling pushLevelAndCaptureConstraints.
So we want their level to the level of the soon-to-be-created implication,
which has a level one higher than the current level.  Hence the pushTcLevel.
It feels like a slight hack.  Applies also to vanillaSkolemTv.

-}
544

545
------------------
546
freshenTyVarBndrs :: [TyVar] -> TcRnIf gbl lcl (TCvSubst, [TyVar])
547 548 549
-- ^ Give fresh uniques to a bunch of TyVars, but they stay
--   as TyVars, rather than becoming TcTyVars
-- Used in FamInst.newFamInst, and Inst.newClsInst
550
freshenTyVarBndrs = instSkolTyCoVars mk_tv
551
  where
552 553 554
    mk_tv old_name kind
       = do { uniq <- newUnique
            ; return (mkTyVar (setNameUnique old_name uniq) kind) }
555

556 557 558 559 560
freshenCoVarBndrsX :: TCvSubst -> [CoVar] -> TcRnIf gbl lcl (TCvSubst, [CoVar])
-- ^ Give fresh uniques to a bunch of CoVars
-- Used in FamInst.newFamInst
freshenCoVarBndrsX subst = instSkolTyCoVarsX mk_cv subst
  where
561 562 563
    mk_cv old_name kind
      = do { uniq <- newUnique
           ; return (mkCoVar (setNameUnique old_name uniq) kind) }
564

565
------------------
566 567 568 569 570
type TcTyCoVarMaker gbl lcl = Name -> Kind -> TcRnIf gbl lcl TyCoVar
     -- The TcTyCoVarMaker should make a fresh Name, based on the old one
     -- Freshness is critical. See Note [Skolems in zonkSyntaxExpr] in TcHsSyn

instSkolTyCoVars :: TcTyCoVarMaker gbl lcl -> [TyVar] -> TcRnIf gbl lcl (TCvSubst, [TyCoVar])
571
instSkolTyCoVars mk_tcv = instSkolTyCoVarsX mk_tcv emptyTCvSubst
572

573
instSkolTyCoVarsX :: TcTyCoVarMaker gbl lcl
574 575
                  -> TCvSubst -> [TyCoVar] -> TcRnIf gbl lcl (TCvSubst, [TyCoVar])
instSkolTyCoVarsX mk_tcv = mapAccumLM (instSkolTyCoVarX mk_tcv)
576

577
instSkolTyCoVarX :: TcTyCoVarMaker gbl lcl
578 579
                 -> TCvSubst -> TyCoVar -> TcRnIf gbl lcl (TCvSubst, TyCoVar)
instSkolTyCoVarX mk_tcv subst tycovar
580 581
  = do  { new_tcv <- mk_tcv old_name kind
        ; let subst1 | isTyVar new_tcv
582 583 584 585
                     = extendTvSubstWithClone subst tycovar new_tcv
                     | otherwise
                     = extendCvSubstWithClone subst tycovar new_tcv
        ; return (subst1, new_tcv) }
586
  where
587
    old_name = tyVarName tycovar
588
    kind     = substTyUnchecked subst (tyVarKind tycovar)
589

590 591 592
newFskTyVar :: TcType -> TcM TcTyVar
newFskTyVar fam_ty
  = do { uniq <- newUnique
593
       ; ref  <- newMutVar Flexi
594
       ; tclvl <- getTcLevel
595 596
       ; let details = MetaTv { mtv_info  = FlatSkolTv
                              , mtv_ref   = ref
597
                              , mtv_tclvl = tclvl }
598 599 600
             name = mkMetaTyVarName uniq (fsLit "fsk")
       ; return (mkTcTyVar name (typeKind fam_ty) details) }

Austin Seipp's avatar
Austin Seipp committed
601
{-
dreixel's avatar
dreixel committed
602 603 604
Note [Kind substitution when instantiating]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When we instantiate a bunch of kind and type variables, first we
605
expect them to be topologically sorted.
dreixel's avatar
dreixel committed
606 607 608 609 610
Then we have to instantiate the kind variables, build a substitution
from old variables to the new variables, then instantiate the type
variables substituting the original kind.

Exemple: If we want to instantiate
611
  [(k1 :: *), (k2 :: *), (a :: k1 -> k2), (b :: k1)]
dreixel's avatar
dreixel committed
612
we want
613
  [(?k1 :: *), (?k2 :: *), (?a :: ?k1 -> ?k2), (?b :: ?k1)]
dreixel's avatar
dreixel committed
614
instead of the buggous
615
  [(?k1 :: *), (?k2 :: *), (?a :: k1 -> k2), (?b :: k1)]
dreixel's avatar
dreixel committed
616

617

Austin Seipp's avatar
Austin Seipp committed
618 619
************************************************************************
*                                                                      *
620
        MetaTvs (meta type variables; mutable)
Austin Seipp's avatar
Austin Seipp committed
621 622 623
*                                                                      *
************************************************************************
-}
624

625 626 627 628 629 630 631
-- a SigTv can unify with type *variables* only, including other SigTvs
-- and skolems. Sometimes, they can unify with type variables that the
-- user would rather keep distinct; see #11203 for an example.
-- So, any client of this
-- function needs to either allow the SigTvs to unify with each other
-- (say, for pattern-bound scoped type variables), or check that they
-- don't (say, with a call to findDubSigTvs).
632 633
newSigTyVar :: Name -> Kind -> TcM TcTyVar
newSigTyVar name kind
Jan Stolarek's avatar
Jan Stolarek committed
634
  = do { details <- newMetaDetails SigTv
635 636 637 638 639 640 641 642
       ; let tyvar = mkTcTyVar name kind details
       ; traceTc "newSigTyVar" (ppr tyvar)
       ; return tyvar }

-- makes a new skolem tv
newSkolemTyVar :: Name -> Kind -> TcM TcTyVar
newSkolemTyVar name kind = do { lvl <- getTcLevel
                              ; return (mkTcTyVar name kind (SkolemTv lvl False)) }
643

644 645 646 647 648 649
newFmvTyVar :: TcType -> TcM TcTyVar
-- Very like newMetaTyVar, except sets mtv_tclvl to one less
-- so that the fmv is untouchable.
newFmvTyVar fam_ty
  = do { uniq <- newUnique
       ; ref  <- newMutVar Flexi
650
       ; tclvl <- getTcLevel
651 652
       ; let details = MetaTv { mtv_info  = FlatMetaTv
                              , mtv_ref   = ref
653
                              , mtv_tclvl = tclvl }
654 655 656
             name = mkMetaTyVarName uniq (fsLit "s")
       ; return (mkTcTyVar name (typeKind fam_ty) details) }

657 658 659
newMetaDetails :: MetaInfo -> TcM TcTyVarDetails
newMetaDetails info
  = do { ref <- newMutVar Flexi
660
       ; tclvl <- getTcLevel
661 662 663
       ; return (MetaTv { mtv_info = info
                        , mtv_ref = ref
                        , mtv_tclvl = tclvl }) }
664

665 666 667
cloneMetaTyVar :: TcTyVar -> TcM TcTyVar
cloneMetaTyVar tv
  = ASSERT( isTcTyVar tv )
668
    do  { uniq <- newUnique
669 670
        ; ref  <- newMutVar Flexi
        ; let name'    = setNameUnique (tyVarName tv) uniq
671
              details' = case tcTyVarDetails tv of
672 673
                           details@(MetaTv {}) -> details { mtv_ref = ref }
                           _ -> pprPanic "cloneMetaTyVar" (ppr tv)
674 675 676
              tyvar = mkTcTyVar name' (tyVarKind tv) details'
        ; traceTc "cloneMetaTyVar" (ppr tyvar)
        ; return tyvar }
677

dreixel's avatar
dreixel committed
678
-- Works for both type and kind variables
679 680
readMetaTyVar :: TyVar -> TcM MetaDetails
readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
681
                      readMutVar (metaTyVarRef tyvar)
682

683 684 685
isFilledMetaTyVar :: TyVar -> TcM Bool
-- True of a filled-in (Indirect) meta type variable
isFilledMetaTyVar tv
686
  | MetaTv { mtv_ref = ref } <- tcTyVarDetails tv
687 688
  = do  { details <- readMutVar ref
        ; return (isIndirect details) }
689 690
  | otherwise = return False

691
isUnfilledMetaTyVar :: TyVar -> TcM Bool
692
-- True of a un-filled-in (Flexi) meta type variable
693
isUnfilledMetaTyVar tv
694
  | MetaTv { mtv_ref = ref } <- tcTyVarDetails tv
695 696
  = do  { details <- readMutVar ref
        ; return (isFlexi details) }
697 698 699
  | otherwise = return False

--------------------
dreixel's avatar
dreixel committed
700
-- Works with both type and kind variables
701
writeMetaTyVar :: TcTyVar -> TcType -> TcM ()
702 703
-- Write into a currently-empty MetaTyVar

Ian Lynagh's avatar
Ian Lynagh committed
704
writeMetaTyVar tyvar ty
705
  | not debugIsOn
706
  = writeMetaTyVarRef tyvar (metaTyVarRef tyvar) ty
707 708 709 710 711 712

-- Everything from here on only happens if DEBUG is on
  | not (isTcTyVar tyvar)
  = WARN( True, text "Writing to non-tc tyvar" <+> ppr tyvar )
    return ()

713
  | MetaTv { mtv_ref = ref } <- tcTyVarDetails tyvar
714 715 716 717
  = writeMetaTyVarRef tyvar ref ty

  | otherwise
  = WARN( True, text "Writing to non-meta tyvar" <+> ppr tyvar )
718
    return ()
719 720 721

--------------------
writeMetaTyVarRef :: TcTyVar -> TcRef MetaDetails -> TcType -> TcM ()
722
-- Here the tyvar is for error checking only;
723 724
-- the ref cell must be for the same tyvar
writeMetaTyVarRef tyvar ref ty
725
  | not debugIsOn
726 727 728
  = do { traceTc "writeMetaTyVar" (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)
                                   <+> text ":=" <+> ppr ty)
       ; writeTcRef ref (Indirect ty) }
729

730
  -- Everything from here on only happens if DEBUG is on
731
  | otherwise
732
  = do { meta_details <- readMutVar ref;
dreixel's avatar
dreixel committed
733
       -- Zonk kinds to allow the error check to work
734
       ; zonked_tv_kind <- zonkTcType tv_kind
735 736 737
       ; zonked_ty      <- zonkTcType ty
       ; let zonked_ty_kind = typeKind zonked_ty  -- need to zonk even before typeKind;
                                                  -- otherwise, we can panic in piResultTy
738
             kind_check_ok = tcIsConstraintKind zonked_tv_kind
739
                          || tcEqKind zonked_ty_kind zonked_tv_kind
740
             -- Hack alert! tcIsConstraintKind: see TcHsType
741
             -- Note [Extra-constraint holes in partial type signatures]
742 743 744 745

             kind_msg = hang (text "Ill-kinded update to meta tyvar")
                           2 (    ppr tyvar <+> text "::" <+> (ppr tv_kind $$ ppr zonked_tv_kind)
                              <+> text ":="
746
                              <+> ppr ty <+> text "::" <+> (ppr zonked_ty_kind) )
747 748

       ; traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty)
dreixel's avatar
dreixel committed
749 750

       -- Check for double updates
751 752 753 754 755 756 757 758 759 760 761
       ; MASSERT2( isFlexi meta_details, double_upd_msg meta_details )

       -- Check for level OK
       -- See Note [Level check when unifying]
       ; MASSERT2( level_check_ok, level_check_msg )

       -- Check Kinds ok
       ; MASSERT2( kind_check_ok, kind_msg )

       -- Do the write
       ; writeMutVar ref (Indirect ty) }
762 763
  where
    tv_kind = tyVarKind tyvar
764

765 766 767
    tv_lvl = tcTyVarLevel tyvar
    ty_lvl = tcTypeLevel ty

768
    level_check_ok  = not (ty_lvl `strictlyDeeperThan` tv_lvl)
769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785
    level_check_msg = ppr ty_lvl $$ ppr tv_lvl $$ ppr tyvar $$ ppr ty

    double_upd_msg details = hang (text "Double update of meta tyvar")
                                2 (ppr tyvar $$ ppr details)


{- Note [Level check when unifying]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When unifying
     alpha:lvl := ty
we expect that the TcLevel of 'ty' will be <= lvl.
However, during unflatting we do
     fuv:l := ty:(l+1)
which is usually wrong; hence the check isFmmvTyVar in level_check_ok.
See Note [TcLevel assignment] in TcType.
-}

786 787 788 789 790
{-
% Generating fresh variables for pattern match check
-}


Austin Seipp's avatar
Austin Seipp committed
791 792 793
{-
************************************************************************
*                                                                      *
794
        MetaTvs: TauTvs
Austin Seipp's avatar
Austin Seipp committed
795 796
*                                                                      *
************************************************************************
797 798 799 800 801 802 803 804 805 806 807 808 809

Note [Never need to instantiate coercion variables]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
With coercion variables sloshing around in types, it might seem that we
sometimes need to instantiate coercion variables. This would be problematic,
because coercion variables inhabit unboxed equality (~#), and the constraint
solver thinks in terms only of boxed equality (~). The solution is that
we never need to instantiate coercion variables in the first place.

The tyvars that we need to instantiate come from the types of functions,
data constructors, and patterns. These will never be quantified over
coercion variables, except for the special case of the promoted Eq#. But,
that can't ever appear in user code, so we're safe!
Austin Seipp's avatar
Austin Seipp committed
810
-}
811

812 813 814 815 816 817
mkMetaTyVarName :: Unique -> FastString -> Name
-- Makes a /System/ Name, which is eagerly eliminated by
-- the unifier; see TcUnify.nicer_to_update_tv1, and
-- TcCanonical.canEqTyVarTyVar (nicer_to_update_tv2)
mkMetaTyVarName uniq str = mkSystemName uniq (mkTyVarOccFS str)

818 819 820 821 822 823 824 825
newAnonMetaTyVar :: MetaInfo -> Kind -> TcM TcTyVar
-- Make a new meta tyvar out of thin air
newAnonMetaTyVar meta_info kind
  = do  { uniq <- newUnique
        ; let name = mkMetaTyVarName uniq s
              s = case meta_info of
                        TauTv       -> fsLit "t"
                        FlatMetaTv  -> fsLit "fmv"
826
                        FlatSkolTv  -> fsLit "fsk"
827 828
                        SigTv       -> fsLit "a"
        ; details <- newMetaDetails meta_info
829 830 831
        ; let tyvar = mkTcTyVar name kind details
        ; traceTc "newAnonMetaTyVar" (ppr tyvar)
        ; return tyvar }
832

833 834 835 836 837 838 839
cloneAnonMetaTyVar :: MetaInfo -> TyVar -> TcKind -> TcM TcTyVar
-- Same as newAnonMetaTyVar, but use a supplied TyVar as the source of the print-name
cloneAnonMetaTyVar info tv kind
  = do  { uniq    <- newUnique
        ; details <- newMetaDetails info
        ; let name = mkSystemName uniq (getOccName tv)
                       -- See Note [Name of an instantiated type variable]
840 841 842
              tyvar = mkTcTyVar name kind details
        ; traceTc "cloneAnonMetaTyVar" (ppr tyvar)
        ; return tyvar }
843 844 845 846 847 848 849

{- Note [Name of an instantiated type variable]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
At the moment we give a unification variable a System Name, which
influences the way it is tidied; see TypeRep.tidyTyVarBndr.
-}

850
newFlexiTyVar :: Kind -> TcM TcTyVar
851
newFlexiTyVar kind = newAnonMetaTyVar TauTv kind
852

853
newFlexiTyVarTy :: Kind -> TcM TcType
854 855
newFlexiTyVarTy kind = do
    tc_tyvar <- newFlexiTyVar kind
856
    return (mkTyVarTy tc_tyvar)
857 858

newFlexiTyVarTys :: Int -> Kind -> TcM [TcType]
859
newFlexiTyVarTys n kind = mapM newFlexiTyVarTy (nOfThem n kind)
860

861 862 863 864 865
newOpenTypeKind :: TcM TcKind
newOpenTypeKind
  = do { rr <- newFlexiTyVarTy runtimeRepTy
       ; return (tYPE rr) }

866
-- | Create a tyvar that can be a lifted or unlifted type.
867
-- Returns alpha :: TYPE kappa, where both alpha and kappa are fresh
868 869
newOpenFlexiTyVarTy :: TcM TcType
newOpenFlexiTyVarTy
870 871
  = do { kind <- newOpenTypeKind
       ; newFlexiTyVarTy kind }
872

873 874 875 876
newMetaSigTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
newMetaSigTyVars = mapAccumLM newMetaSigTyVarX emptyTCvSubst

newMetaTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
877
-- Instantiate with META type variables
878 879 880
-- Note that this works for a sequence of kind, type, and coercion variables
-- variables.  Eg    [ (k:*), (a:k->k) ]
--             Gives [ (k7:*), (a8:k7->k7) ]
881
newMetaTyVars = mapAccumLM newMetaTyVarX emptyTCvSubst
882
    -- emptyTCvSubst has an empty in-scope set, but that's fine here
dreixel's avatar
dreixel committed
883 884 885
    -- Since the tyvars are freshly made, they cannot possibly be
    -- captured by any existing for-alls.

886
newMetaTyVarX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
dreixel's avatar
dreixel committed
887 888
-- Make a new unification variable tyvar whose Name and Kind come from
-- an existing TyVar. We substitute kind variables in the kind.
889
newMetaTyVarX subst tyvar = new_meta_tv_x TauTv subst tyvar
890

891 892 893 894
newMetaTyVarsX :: TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
-- Just like newMetaTyVars, but start with an existing substitution.
newMetaTyVarsX subst = mapAccumLM newMetaTyVarX subst

895 896
newMetaSigTyVarX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
-- Just like newMetaTyVarX, but make a SigTv
897 898
newMetaSigTyVarX subst tyvar = new_meta_tv_x SigTv subst tyvar

899 900 901 902 903
newWildCardX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
newWildCardX subst tv
  = do { new_tv <- newAnonMetaTyVar TauTv (substTy subst (tyVarKind tv))
       ; return (extendTvSubstWithClone subst tv new_tv, new_tv) }

904
new_meta_tv_x :: MetaInfo -> TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
905
new_meta_tv_x info subst tv
906 907
  = do  { new_tv <- cloneAnonMetaTyVar info tv substd_kind
        ; let subst1 = extendTvSubstWithClone subst tv new_tv
908
        ; return (subst1, new_tv) }
909 910 911 912 913 914 915
  where
    substd_kind = substTyUnchecked subst (tyVarKind tv)
      -- NOTE: Trac #12549 is fixed so we could use
      -- substTy here, but the tc_infer_args problem
      -- is not yet fixed so leaving as unchecked for now.
      -- OLD NOTE:
      -- Unchecked because we call newMetaTyVarX from
916
      -- tcInstTyBinder, which is called from tcInferApps
917 918 919
      -- which does not yet take enough trouble to ensure
      -- the in-scope set is right; e.g. Trac #12785 trips
      -- if we use substTy here
920

921 922
newMetaTyVarTyAtLevel :: TcLevel -> TcKind -> TcM TcType
newMetaTyVarTyAtLevel tc_lvl kind
923 924 925 926 927 928
  = do  { uniq <- newUnique
        ; ref  <- newMutVar Flexi
        ; let name = mkMetaTyVarName uniq (fsLit "p")
              details = MetaTv { mtv_info  = TauTv
                               , mtv_ref   = ref
                               , mtv_tclvl = tc_lvl }
929
        ; return (mkTyVarTy (mkTcTyVar name kind details)) }
930

931
{- *********************************************************************
Austin Seipp's avatar
Austin Seipp committed
932
*                                                                      *
933
             Quantification
Austin Seipp's avatar
Austin Seipp committed
934 935
*                                                                      *
************************************************************************
936

937 938
Note [quantifyTyVars]
~~~~~~~~~~~~~~~~~~~~~
939
quantifyTyVars is given the free vars of a type that we
940
are about to wrap in a forall.
941

942 943 944 945 946
It takes these free type/kind variables (partitioned into dependent and
non-dependent variables) and
  1. Zonks them and remove globals and covars
  2. Extends kvs1 with free kind vars in the kinds of tvs (removing globals)
  3. Calls zonkQuantifiedTyVar on each
947

948
Step (2) is often unimportant, because the kind variable is often
949 950 951 952
also free in the type.  Eg
     Typeable k (a::k)
has free vars {k,a}.  But the type (see Trac #7916)
    (f::k->*) (a::k)
953
has free vars {f,a}, but we must add 'k' as well! Hence step (2).
954

955 956 957
* This function distinguishes between dependent and non-dependent
  variables only to keep correct defaulting behavior with -XNoPolyKinds.
  With -XPolyKinds, it treats both classes of variables identically.
958

959 960 961
* quantifyTyVars never quantifies over
    - a coercion variable
    - a runtime-rep variable
962 963 964 965 966 967 968 969

Note [quantifyTyVars determinism]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The results of quantifyTyVars are wrapped in a forall and can end up in the
interface file. One such example is inferred type signatures. They also affect
the results of optimizations, for example worker-wrapper. This means that to
get deterministic builds quantifyTyVars needs to be deterministic.

970
To achieve this CandidatesQTvs is backed by deterministic sets which allows them
971 972 973 974
to be later converted to a list in a deterministic order.

For more information about deterministic sets see
Note [Deterministic UniqFM] in UniqDFM.
Austin Seipp's avatar
Austin Seipp committed
975
-}
976

977 978
quantifyTyVars
  :: TcTyCoVarSet     -- Global tvs; already zonked
979
  -> CandidatesQTvs   -- See Note [Dependent type variables] in TcType
980
                      -- Already zonked
981
  -> TcM [TcTyVar]
982
-- See Note [quantifyTyVars]
983
-- Can be given a mixture of TcTyVars and TyVars, in the case of
984 985
--   associated type declarations. Also accepts covars, but *never* returns any.

986 987
quantifyTyVars gbl_tvs dvs@(DV{ dv_kvs = dep_tkvs, dv_tvs = nondep_tkvs })
  = do { traceTc "quantifyTyVars" (vcat [ppr dvs, ppr gbl_tvs])
988
       ; let dep_kvs = dVarSetElemsWellScoped $
989
                       dep_tkvs `dVarSetMinusVarSet` gbl_tvs
990 991 992
                       -- dVarSetElemsWellScoped: put the kind variables into
                       --    well-scoped order.
                       --    E.g.  [k, (a::k)] not the other way roud
993

994
             nondep_tvs = dVarSetElems $
995 996 997 998 999 1000 1001 1002 1003
                          (nondep_tkvs `minusDVarSet` dep_tkvs)
                           `dVarSetMinusVarSet` gbl_tvs
                 -- See Note [Dependent type variables] in TcType
                 -- The `minus` dep_tkvs removes any kind-level vars
                 --    e.g. T k (a::k)   Since k appear in a kind it'll
                 --    be in dv_kvs, and is dependent. So remove it from
                 --    dv_tvs which will also contain k
                 -- No worry about dependent covars here;
                 --    they are all in dep_tkvs
Gabor Greif's avatar
Gabor Greif committed
1004
                 -- No worry about scoping, because these are all
1005 1006
                 --    type variables
                 -- NB kinds of tvs are zonked by zonkTyCoVarsAndFV
1007

dreixel's avatar
dreixel committed
1008 1009
             -- In the non-PolyKinds case, default the kind variables
             -- to *, and zonk the tyvars as usual.  Notice that this
1010
             -- may make quantifyTyVars return a shorter list
dreixel's avatar
dreixel committed
1011
             -- than it was passed, but that's ok
1012 1013 1014
       ; poly_kinds  <- xoptM LangExt.PolyKinds
       ; dep_kvs'    <- mapMaybeM (zonk_quant (not poly_kinds)) dep_kvs
       ; nondep_tvs' <- mapMaybeM (zonk_quant False)            nondep_tvs
1015
       ; let final_qtvs = dep_kvs' ++ nondep_tvs'