TcMType.hs 63.8 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, writeMetaTyVarRef,
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
41
42
  --------------------------------
  -- Creating fresh type variables for pm checking
  genInstSkolTyVarsX,

43
  --------------------------------
44
  -- Creating new evidence variables
45
  newEvVar, newEvVars, newDict,
46
  newWanted, newWanteds, cloneWanted, cloneWC,
47
  emitWanted, emitWantedEq, emitWantedEvVar, emitWantedEvVars,
48
  newTcEvBinds, addTcEvBind,
49

50
51
52
53
  newCoercionHole, fillCoercionHole, isFilledCoercionHole,
  unpackCoercionHole, unpackCoercionHole_maybe,
  checkCoercionHole,

54
55
  --------------------------------
  -- Instantiation
56
  newMetaTyVars, newMetaTyVarX, newMetaTyVarsX,
57
58
  newMetaSigTyVars, newMetaSigTyVarX,
  newSigTyVar, newWildCardX,
59
  tcInstType,
60
61
  tcInstSkolTyVars, tcInstSuperSkolTyVarsX,
  tcInstSigTyVars,
62
  tcSkolDFunType, tcSuperSkolTyVars,
63

64
  instSkolTyCoVars, freshenTyVarBndrs, freshenCoVarBndrsX,
65

66
  --------------------------------
67
  -- Zonking and tidying
68
69
  zonkTidyTcType, zonkTidyOrigin,
  mkTypeErrorThing, mkTypeErrorThingArgs,
70
  tidyEvVar, tidyCt, tidySkolemInfo,
71
  skolemiseRuntimeUnk,
72
73
  zonkTcTyVar, zonkTcTyVars, zonkTcTyVarToTyVar,
  zonkTyCoVarsAndFV, zonkTcTypeAndFV,
74
  zonkTyCoVarsAndFVList,
75
  zonkTcTypeAndSplitDepVars, zonkTcTypesAndSplitDepVars,
76
  zonkQuantifiedTyVar,
77
  quantifyTyVars, quantifyZonkedTyVars,
Simon Peyton Jones's avatar
Simon Peyton Jones committed
78
  zonkTcTyCoVarBndr, zonkTcTyVarBinder,
79
  zonkTcType, zonkTcTypes, zonkCo,
80
  zonkTyCoVarKind, zonkTcTypeMapper,
81

82
  zonkEvVar, zonkWC, zonkSimples, zonkId, zonkCt, zonkSkolemInfo,
83

Richard Eisenberg's avatar
Richard Eisenberg committed
84
85
86
87
88
  tcGetGlobalTyCoVars,

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

#include "HsVersions.h"

-- friends:
94
import TyCoRep
95
96
import TcType
import Type
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
97
import Kind
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 PrelNames
112
import Util
113
import Outputable
114
import FastString
Simon Peyton Jones's avatar
Simon Peyton Jones committed
115
import SrcLoc
116
import Bag
117
import Pair
118
import UniqFM
119
import qualified GHC.LanguageExtensions as LangExt
120

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

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

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

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

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

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

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

158
159
160
newEvVars :: TcThetaType -> TcM [EvVar]
newEvVars theta = mapM newEvVar theta

161
--------------
batterseapower's avatar
batterseapower committed
162

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

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

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

182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
cloneWanted :: Ct -> TcM CtEvidence
cloneWanted ct
  = newWanted (ctEvOrigin ev) Nothing (ctEvPred ev)
  where
    ev = ctEvidence ct

cloneWC :: WantedConstraints -> TcM WantedConstraints
cloneWC wc@(WC { wc_simple = simples, wc_impl = implics })
  = do { simples' <- mapBagM clone_one simples
       ; implics' <- mapBagM clone_implic implics
       ; return (wc { wc_simple = simples', wc_impl = implics' }) }
  where
    clone_one ct = do { ev <- cloneWanted ct; return (mkNonCanonical ev) }

    clone_implic implic@(Implic { ic_wanted = inner_wanted })
      = do { inner_wanted' <- cloneWC inner_wanted
           ; return (implic { ic_wanted = inner_wanted' }) }

200
201
202
203
204
205
206
207
208
209
210
211
212
-- | Emits a new Wanted. Deals with both equalities and non-equalities.
emitWanted :: CtOrigin -> TcPredType -> TcM EvTerm
emitWanted origin pty
  = do { ev <- newWanted origin Nothing pty
       ; emitSimple $ mkNonCanonical ev
       ; return $ ctEvTerm ev }

-- | Emits a new equality constraint
emitWantedEq :: CtOrigin -> TypeOrKind -> Role -> TcType -> TcType -> TcM Coercion
emitWantedEq origin t_or_k role ty1 ty2
  = do { hole <- newCoercionHole
       ; loc <- getCtLocM origin (Just t_or_k)
       ; emitSimple $ mkNonCanonical $
213
214
         CtWanted { ctev_pred = pty, ctev_dest = HoleDest hole
                  , ctev_nosh = WDeriv, ctev_loc = loc }
215
216
217
218
219
220
221
222
223
224
225
226
       ; return (mkHoleCo hole role ty1 ty2) }
  where
    pty = mkPrimEqPredRole role ty1 ty2

-- | Creates a new EvVar and immediately emits it as a Wanted.
-- No equality predicates here.
emitWantedEvVar :: CtOrigin -> TcPredType -> TcM EvVar
emitWantedEvVar origin ty
  = do { new_cv <- newEvVar ty
       ; loc <- getCtLocM origin Nothing
       ; let ctev = CtWanted { ctev_dest = EvVarDest new_cv
                             , ctev_pred = ty
227
                             , ctev_nosh = WDeriv
228
229
230
231
232
233
                             , ctev_loc  = loc }
       ; emitSimple $ mkNonCanonical ctev
       ; return new_cv }

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

newDict :: Class -> [TcType] -> TcM DictId
236
newDict cls tys
237
  = do { name <- newSysName (mkDictOcc (getOccName cls))
batterseapower's avatar
batterseapower committed
238
239
240
       ; return (mkLocalId name (mkClassPred cls tys)) }

predTypeOccName :: PredType -> OccName
241
predTypeOccName ty = case classifyPredType ty of
batterseapower's avatar
batterseapower committed
242
    ClassPred cls _ -> mkDictOcc (getOccName cls)
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
243
    EqPred _ _ _    -> mkVarOccFS (fsLit "cobox")
batterseapower's avatar
batterseapower committed
244
    IrredPred _     -> mkVarOccFS (fsLit "irred")
245

246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
{-
************************************************************************
*                                                                      *
        Coercion holes
*                                                                      *
************************************************************************
-}

newCoercionHole :: TcM CoercionHole
newCoercionHole
  = do { u <- newUnique
       ; traceTc "New coercion hole:" (ppr u)
       ; ref <- newMutVar Nothing
       ; return $ CoercionHole u ref }

-- | Put a value in a coercion hole
fillCoercionHole :: CoercionHole -> Coercion -> TcM ()
fillCoercionHole (CoercionHole u ref) co
  = do {
#ifdef DEBUG
       ; cts <- readTcRef ref
       ; whenIsJust cts $ \old_co ->
         pprPanic "Filling a filled coercion hole" (ppr u $$ ppr co $$ ppr old_co)
#endif
       ; traceTc "Filling coercion hole" (ppr u <+> text ":=" <+> ppr co)
       ; writeTcRef ref (Just co) }

-- | Is a coercion hole filled in?
isFilledCoercionHole :: CoercionHole -> TcM Bool
isFilledCoercionHole (CoercionHole _ ref) = isJust <$> readTcRef ref

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

-- | Retrieve the contents of a coercion hole, if it is filled
unpackCoercionHole_maybe :: CoercionHole -> TcM (Maybe Coercion)
unpackCoercionHole_maybe (CoercionHole _ ref) = readTcRef ref

-- | Check that a coercion is appropriate for filling a hole. (The hole
-- itself is needed only for printing. NB: This must be /lazy/ in the coercion,
-- as it's used in TcHsSyn in the presence of knots.
-- Always returns the checked coercion, but this return value is necessary
-- so that the input coercion is forced only when the output is forced.
checkCoercionHole :: Coercion -> CoercionHole -> Role -> Type -> Type -> TcM Coercion
checkCoercionHole co h r t1 t2
-- co is already zonked, but t1 and t2 might not be
  | debugIsOn
  = do { t1 <- zonkTcType t1
       ; t2 <- zonkTcType t2
       ; let (Pair _t1 _t2, _role) = coercionKindRole co
       ; return $
         ASSERT2( t1 `eqType` _t1 && t2 `eqType` _t2 && r == _role
                , (text "Bad coercion hole" <+>
                   ppr h <> colon <+> vcat [ ppr _t1, ppr _t2, ppr _role
                                           , ppr co, ppr t1, ppr t2
                                           , ppr r ]) )
         co }
  | otherwise
  = return co

312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
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
{-
************************************************************************
*
    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 #.
364
365
366
367
368
369
370
371
newInferExpTypeNoInst :: TcM ExpSigmaType
newInferExpTypeNoInst = newInferExpType False

newInferExpTypeInst :: TcM ExpRhoType
newInferExpTypeInst = newInferExpType True

newInferExpType :: Bool -> TcM ExpType
newInferExpType inst
372
  = do { u <- newUnique
373
       ; tclvl <- getTcLevel
374
       ; traceTc "newOpenInferExpType" (ppr u <+> ppr inst <+> ppr tclvl)
375
       ; ref <- newMutVar Nothing
376
       ; return (Infer (IR { ir_uniq = u, ir_lvl = tclvl
377
                           , ir_ref = ref, ir_inst = inst })) }
378
379
380
381

-- | 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)
382
383
readExpType_maybe (Check ty)                   = return (Just ty)
readExpType_maybe (Infer (IR { ir_ref = ref})) = readMutVar ref
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403

-- | 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)

404
405
tauifyExpType :: ExpType -> TcM ExpType
-- ^ Turn a (Infer hole) type into a (Check alpha),
406
-- where alpha is a fresh unification variable
407
408
409
tauifyExpType (Check ty)      = return (Check ty)  -- No-op for (Check ty)
tauifyExpType (Infer inf_res) = do { ty <- inferResultToType inf_res
                                   ; return (Check ty) }
410

411
412
413
-- | Extracts the expected type if there is one, or generates a new
-- TauTv if there isn't.
expTypeToType :: ExpType -> TcM TcType
414
415
416
417
418
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
419
420
421
                      , ir_ref = ref })
  = do { rr  <- newMetaTyVarTyAtLevel tc_lvl runtimeRepTy
       ; tau <- newMetaTyVarTyAtLevel tc_lvl (tYPE rr)
422
             -- See Note [TcLevel of ExpType]
423
424
       ; writeMutVar ref (Just tau)
       ; traceTc "Forcing ExpType to be monomorphic:"
425
                 (ppr u <+> text ":=" <+> ppr tau)
426
       ; return tau }
427

428

429
{- *********************************************************************
Austin Seipp's avatar
Austin Seipp committed
430
*                                                                      *
431
        SkolemTvs (immutable)
Austin Seipp's avatar
Austin Seipp committed
432
*                                                                      *
433
********************************************************************* -}
434

435
436
tcInstType :: ([TyVar] -> TcM (TCvSubst, [TcTyVar]))
                   -- ^ How to instantiate the type variables
437
438
           -> Id                                            -- ^ Type to instantiate
           -> TcM ([(Name, TcTyVar)], TcThetaType, TcType)  -- ^ Result
439
                -- (type vars, preds (incl equalities), rho)
440
441
tcInstType inst_tyvars id
  = case tcSplitForAllTys (idType id) of
442
        ([],    rho) -> let     -- There may be overloading despite no type variables;
443
                                --      (?x :: Int) => Int -> Int
444
445
446
                                (theta, tau) = tcSplitPhiTy rho
                            in
                            return ([], theta, tau)
447

448
        (tyvars, rho) -> do { (subst, tyvars') <- inst_tyvars tyvars
449
                            ; let (theta, tau) = tcSplitPhiTy (substTyAddInScope subst rho)
450
451
                                  tv_prs       = map tyVarName tyvars `zip` tyvars'
                            ; return (tv_prs, theta, tau) }
452

453
tcSkolDFunType :: DFunId -> TcM ([TcTyVar], TcThetaType, TcType)
454
455
-- Instantiate a type signature with skolem constants.
-- We could give them fresh names, but no need to do so
456
457
458
tcSkolDFunType dfun
  = do { (tv_prs, theta, tau) <- tcInstType tcInstSuperSkolTyVars dfun
       ; return (map snd tv_prs, theta, tau) }
459

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

467
tcSuperSkolTyVar :: TCvSubst -> TyVar -> (TCvSubst, TcTyVar)
468
tcSuperSkolTyVar subst tv
469
  = (extendTvSubstWithClone subst tv new_tv, new_tv)
dreixel's avatar
dreixel committed
470
  where
471
    kind   = substTyUnchecked subst (tyVarKind tv)
472
473
    new_tv = mkTcTyVar (tyVarName tv) kind superSkolemTv

474
475
476
477
478
479
-- | 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.
480
481
tcInstSkolTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
tcInstSkolTyVars = tcInstSkolTyVars' False emptyTCvSubst
dreixel's avatar
dreixel committed
482

483
484
485
486
tcInstSuperSkolTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
tcInstSuperSkolTyVars = tcInstSuperSkolTyVarsX emptyTCvSubst

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

489
tcInstSkolTyVars' :: Bool -> TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
490
491
-- Precondition: tyvars should be ordered (kind vars first)
-- see Note [Kind substitution when instantiating]
492
-- Get the location from the monad; this is a complete freshening operation
493
tcInstSkolTyVars' overlappable subst tvs
494
  = do { loc <- getSrcSpanM
495
496
       ; lvl <- getTcLevel
       ; instSkolTyCoVarsX (mkTcSkolTyVar lvl loc overlappable) subst tvs }
497

498
499
500
501
502
503
504
mkTcSkolTyVar :: TcLevel -> SrcSpan -> Bool -> TcTyVarMaker
mkTcSkolTyVar lvl loc overlappable
  = \ uniq old_name kind -> mkTcTyVar (mkInternalName uniq (getOccName old_name) loc)
                                      kind details
  where
    details = SkolemTv (pushTcLevel lvl) overlappable
              -- NB: skolems bump the level
505

506
tcInstSigTyVars :: SrcSpan -> [TyVar]
507
508
509
510
                -> TcM (TCvSubst, [TcTyVar])
tcInstSigTyVars loc tvs
  = do { lvl <- getTcLevel
       ; instSkolTyCoVars (mkTcSkolTyVar lvl loc False) tvs }
511

512
------------------
513
freshenTyVarBndrs :: [TyVar] -> TcRnIf gbl lcl (TCvSubst, [TyVar])
514
515
516
-- ^ Give fresh uniques to a bunch of TyVars, but they stay
--   as TyVars, rather than becoming TcTyVars
-- Used in FamInst.newFamInst, and Inst.newClsInst
517
freshenTyVarBndrs = instSkolTyCoVars mk_tv
518
519
  where
    mk_tv uniq old_name kind = mkTyVar (setNameUnique old_name uniq) kind
520

521
522
523
524
525
526
527
freshenCoVarBndrsX :: TCvSubst -> [CoVar] -> TcRnIf gbl lcl (TCvSubst, [CoVar])
-- ^ Give fresh uniques to a bunch of CoVars
-- Used in FamInst.newFamInst
freshenCoVarBndrsX subst = instSkolTyCoVarsX mk_cv subst
  where
    mk_cv uniq old_name kind = mkCoVar (setNameUnique old_name uniq) kind

528
------------------
529
530
type TcTyVarMaker = Unique -> Name -> Kind -> TyCoVar
instSkolTyCoVars :: TcTyVarMaker -> [TyVar] -> TcRnIf gbl lcl (TCvSubst, [TyCoVar])
531
instSkolTyCoVars mk_tcv = instSkolTyCoVarsX mk_tcv emptyTCvSubst
532

533
instSkolTyCoVarsX :: TcTyVarMaker
534
535
                  -> TCvSubst -> [TyCoVar] -> TcRnIf gbl lcl (TCvSubst, [TyCoVar])
instSkolTyCoVarsX mk_tcv = mapAccumLM (instSkolTyCoVarX mk_tcv)
536

537
instSkolTyCoVarX :: TcTyVarMaker
538
539
                 -> TCvSubst -> TyCoVar -> TcRnIf gbl lcl (TCvSubst, TyCoVar)
instSkolTyCoVarX mk_tcv subst tycovar
540
541
  = do  { uniq <- newUnique  -- using a new unique is critical. See
                             -- Note [Skolems in zonkSyntaxExpr] in TcHsSyn
542
543
544
545
546
547
        ; let new_tcv = mk_tcv uniq old_name kind
              subst1 | isTyVar new_tcv
                     = extendTvSubstWithClone subst tycovar new_tcv
                     | otherwise
                     = extendCvSubstWithClone subst tycovar new_tcv
        ; return (subst1, new_tcv) }
548
  where
549
    old_name = tyVarName tycovar
550
    kind     = substTyUnchecked subst (tyVarKind tycovar)
551

552
553
554
555
556
newFskTyVar :: TcType -> TcM TcTyVar
newFskTyVar fam_ty
  = do { uniq <- newUnique
       ; let name = mkSysTvName uniq (fsLit "fsk")
       ; return (mkTcTyVar name (typeKind fam_ty) (FlatSkol fam_ty)) }
Austin Seipp's avatar
Austin Seipp committed
557
{-
dreixel's avatar
dreixel committed
558
559
560
Note [Kind substitution when instantiating]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When we instantiate a bunch of kind and type variables, first we
561
expect them to be topologically sorted.
dreixel's avatar
dreixel committed
562
563
564
565
566
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
567
  [(k1 :: *), (k2 :: *), (a :: k1 -> k2), (b :: k1)]
dreixel's avatar
dreixel committed
568
we want
569
  [(?k1 :: *), (?k2 :: *), (?a :: ?k1 -> ?k2), (?b :: ?k1)]
dreixel's avatar
dreixel committed
570
instead of the buggous
571
  [(?k1 :: *), (?k2 :: *), (?a :: k1 -> k2), (?b :: k1)]
dreixel's avatar
dreixel committed
572

573

Austin Seipp's avatar
Austin Seipp committed
574
575
************************************************************************
*                                                                      *
576
        MetaTvs (meta type variables; mutable)
Austin Seipp's avatar
Austin Seipp committed
577
578
579
*                                                                      *
************************************************************************
-}
580

581
582
583
584
585
586
mkMetaTyVarName :: Unique -> FastString -> Name
-- Makes a /System/ Name, which is eagerly eliminated by
-- the unifier; see TcUnify.nicer_to_update_tv1, and
-- TcCanonical.canEqTyVarTyVar (nicer_to_update_tv2)
mkMetaTyVarName uniq str = mkSysTvName uniq str

587
588
newSigTyVar :: Name -> Kind -> TcM TcTyVar
newSigTyVar name kind
Jan Stolarek's avatar
Jan Stolarek committed
589
  = do { details <- newMetaDetails SigTv
590
       ; return (mkTcTyVar name kind details) }
591

592
593
594
595
596
597
598
599
600
601
602
603
604
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
       ; cur_lvl <- getTcLevel
       ; let details = MetaTv { mtv_info  = FlatMetaTv
                              , mtv_ref   = ref
                              , mtv_tclvl = fmvTcLevel cur_lvl }
             name = mkMetaTyVarName uniq (fsLit "s")
       ; return (mkTcTyVar name (typeKind fam_ty) details) }

605
606
607
newMetaDetails :: MetaInfo -> TcM TcTyVarDetails
newMetaDetails info
  = do { ref <- newMutVar Flexi
608
       ; tclvl <- getTcLevel
609
610
611
       ; return (MetaTv { mtv_info = info
                        , mtv_ref = ref
                        , mtv_tclvl = tclvl }) }
612

613
614
615
cloneMetaTyVar :: TcTyVar -> TcM TcTyVar
cloneMetaTyVar tv
  = ASSERT( isTcTyVar tv )
616
    do  { uniq <- newUnique
617
618
        ; ref  <- newMutVar Flexi
        ; let name'    = setNameUnique (tyVarName tv) uniq
619
              details' = case tcTyVarDetails tv of
620
621
622
623
                           details@(MetaTv {}) -> details { mtv_ref = ref }
                           _ -> pprPanic "cloneMetaTyVar" (ppr tv)
        ; return (mkTcTyVar name' (tyVarKind tv) details') }

dreixel's avatar
dreixel committed
624
-- Works for both type and kind variables
625
626
readMetaTyVar :: TyVar -> TcM MetaDetails
readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
627
                      readMutVar (metaTyVarRef tyvar)
628

629
630
631
isFilledMetaTyVar :: TyVar -> TcM Bool
-- True of a filled-in (Indirect) meta type variable
isFilledMetaTyVar tv
632
  | MetaTv { mtv_ref = ref } <- tcTyVarDetails tv
633
634
  = do  { details <- readMutVar ref
        ; return (isIndirect details) }
635
636
  | otherwise = return False

637
isUnfilledMetaTyVar :: TyVar -> TcM Bool
638
-- True of a un-filled-in (Flexi) meta type variable
639
isUnfilledMetaTyVar tv
640
  | MetaTv { mtv_ref = ref } <- tcTyVarDetails tv
641
642
  = do  { details <- readMutVar ref
        ; return (isFlexi details) }
643
644
645
  | otherwise = return False

--------------------
dreixel's avatar
dreixel committed
646
-- Works with both type and kind variables
647
writeMetaTyVar :: TcTyVar -> TcType -> TcM ()
648
649
-- Write into a currently-empty MetaTyVar

Ian Lynagh's avatar
Ian Lynagh committed
650
writeMetaTyVar tyvar ty
651
  | not debugIsOn
652
  = writeMetaTyVarRef tyvar (metaTyVarRef tyvar) ty
653
654
655
656
657
658

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

659
  | MetaTv { mtv_ref = ref } <- tcTyVarDetails tyvar
660
661
662
663
  = writeMetaTyVarRef tyvar ref ty

  | otherwise
  = WARN( True, text "Writing to non-meta tyvar" <+> ppr tyvar )
664
    return ()
665
666
667

--------------------
writeMetaTyVarRef :: TcTyVar -> TcRef MetaDetails -> TcType -> TcM ()
668
-- Here the tyvar is for error checking only;
669
670
-- the ref cell must be for the same tyvar
writeMetaTyVarRef tyvar ref ty
671
  | not debugIsOn
672
673
674
  = do { traceTc "writeMetaTyVar" (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)
                                   <+> text ":=" <+> ppr ty)
       ; writeTcRef ref (Indirect ty) }
675

676
  -- Everything from here on only happens if DEBUG is on
677
  | otherwise
678
  = do { meta_details <- readMutVar ref;
dreixel's avatar
dreixel committed
679
       -- Zonk kinds to allow the error check to work
680
681
       ; zonked_tv_kind <- zonkTcType tv_kind
       ; zonked_ty_kind <- zonkTcType ty_kind
682
683
684
685
686
687
688
689
690
691
       ; let kind_check_ok = isPredTy tv_kind  -- Don't check kinds for updates
                                               -- to coercion variables
                          || tcEqKind zonked_ty_kind zonked_tv_kind

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

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

       -- Check for double updates
694
695
696
697
698
699
700
701
702
703
704
       ; 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) }
705
706
707
  where
    tv_kind = tyVarKind tyvar
    ty_kind = typeKind ty
708

709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
    tv_lvl = tcTyVarLevel tyvar
    ty_lvl = tcTypeLevel ty

    level_check_ok = isFmvTyVar tyvar
                  || not (ty_lvl `strictlyDeeperThan` tv_lvl)
    level_check_msg = ppr ty_lvl $$ ppr tv_lvl $$ ppr tyvar $$ ppr ty

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


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

731
732
733
734
{-
% Generating fresh variables for pattern match check
-}

735
736
737
738
-- UNINSTANTIATED VERSION OF tcInstSkolTyCoVars
genInstSkolTyVarsX :: SrcSpan -> TCvSubst -> [TyVar]
                   -> TcRnIf gbl lcl (TCvSubst, [TcTyVar])
-- Precondition: tyvars should be scoping-ordered
739
740
-- see Note [Kind substitution when instantiating]
-- Get the location from the monad; this is a complete freshening operation
741
742
genInstSkolTyVarsX loc subst tvs
  = instSkolTyCoVarsX (mkTcSkolTyVar topTcLevel loc False) subst tvs
743

Austin Seipp's avatar
Austin Seipp committed
744
745
746
{-
************************************************************************
*                                                                      *
747
        MetaTvs: TauTvs
Austin Seipp's avatar
Austin Seipp committed
748
749
*                                                                      *
************************************************************************
750
751
752
753
754
755
756
757
758
759
760
761
762

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
763
-}
764

765
766
767
768
769
770
771
772
773
774
775
776
newAnonMetaTyVar :: MetaInfo -> Kind -> TcM TcTyVar
-- Make a new meta tyvar out of thin air
newAnonMetaTyVar meta_info kind
  = do  { uniq <- newUnique
        ; let name = mkMetaTyVarName uniq s
              s = case meta_info of
                        TauTv       -> fsLit "t"
                        FlatMetaTv  -> fsLit "fmv"
                        SigTv       -> fsLit "a"
        ; details <- newMetaDetails meta_info
        ; return (mkTcTyVar name kind details) }

777
newFlexiTyVar :: Kind -> TcM TcTyVar
778
newFlexiTyVar kind = newAnonMetaTyVar TauTv kind
779

780
newFlexiTyVarTy :: Kind -> TcM TcType
781
782
newFlexiTyVarTy kind = do
    tc_tyvar <- newFlexiTyVar kind
783
    return (mkTyVarTy tc_tyvar)
784
785

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

788
789
790
791
792
newOpenTypeKind :: TcM TcKind
newOpenTypeKind
  = do { rr <- newFlexiTyVarTy runtimeRepTy
       ; return (tYPE rr) }

793
-- | Create a tyvar that can be a lifted or unlifted type.
794
-- Returns alpha :: TYPE kappa, where both alpha and kappa are fresh
795
796
newOpenFlexiTyVarTy :: TcM TcType
newOpenFlexiTyVarTy
797
798
  = do { kind <- newOpenTypeKind
       ; newFlexiTyVarTy kind }
799

800
801
802
803
newMetaSigTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
newMetaSigTyVars = mapAccumLM newMetaSigTyVarX emptyTCvSubst

newMetaTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
804
-- Instantiate with META type variables
805
806
807
-- Note that this works for a sequence of kind, type, and coercion variables
-- variables.  Eg    [ (k:*), (a:k->k) ]
--             Gives [ (k7:*), (a8:k7->k7) ]
808
newMetaTyVars = mapAccumLM newMetaTyVarX emptyTCvSubst
809
    -- emptyTCvSubst has an empty in-scope set, but that's fine here
dreixel's avatar
dreixel committed
810
811
812
    -- Since the tyvars are freshly made, they cannot possibly be
    -- captured by any existing for-alls.

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

818
819
820
821
newMetaTyVarsX :: TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
-- Just like newMetaTyVars, but start with an existing substitution.
newMetaTyVarsX subst = mapAccumLM newMetaTyVarX subst

822
823
newMetaSigTyVarX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
-- Just like newMetaTyVarX, but make a SigTv
824
825
newMetaSigTyVarX subst tyvar = new_meta_tv_x SigTv subst tyvar

826
827
828
829
830
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) }

831
new_meta_tv_x :: MetaInfo -> TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
832
new_meta_tv_x info subst tv
833
  = do  { uniq <- newUnique
834
        ; details <- newMetaDetails info
835
        ; let name   = mkSystemName uniq (getOccName tv)
836
                       -- See Note [Name of an instantiated type variable]
837
              kind   = substTyUnchecked subst (tyVarKind tv)
838
839
840
841
                       -- 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:
842
843
844
845
846
                       -- Unchecked because we call newMetaTyVarX from
                       -- tcInstBinderX, which is called from tc_infer_args
                       -- 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
847
              new_tv = mkTcTyVar name kind details
848
              subst1 = extendTvSubstWithClone subst tv new_tv
849
        ; return (subst1, new_tv) }
850

851
852
newMetaTyVarTyAtLevel :: TcLevel -> TcKind -> TcM TcType
newMetaTyVarTyAtLevel tc_lvl kind
853
854
855
856
857
858
  = do  { uniq <- newUnique
        ; ref  <- newMutVar Flexi
        ; let name = mkMetaTyVarName uniq (fsLit "p")
              details = MetaTv { mtv_info  = TauTv
                               , mtv_ref   = ref
                               , mtv_tclvl = tc_lvl }
859
        ; return (mkTyVarTy (mkTcTyVar name kind details)) }
860

Simon Peyton Jones's avatar
Simon Peyton Jones committed
861
862
863
864
865
{- 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.

Austin Seipp's avatar
Austin Seipp committed
866
867
************************************************************************
*                                                                      *
868
             Quantification
Austin Seipp's avatar
Austin Seipp committed
869
870
*                                                                      *
************************************************************************
871

872
873
Note [quantifyTyVars]
~~~~~~~~~~~~~~~~~~~~~
874
quantifyTyVars is given the free vars of a type that we
875
are about to wrap in a forall.
876

877
878
879
880
881
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
882

883
Step (2) is often unimportant, because the kind variable is often
884
885
886
887
888
also free in the type.  Eg
     Typeable k (a::k)
has free vars {k,a}.  But the type (see Trac #7916)
    (f::k->*) (a::k)
has free vars {f,a}, but we must add 'k' as well! Hence step (3).
889

890
891
892
* 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.
893

894
895
896
* quantifyTyVars never quantifies over
    - a coercion variable
    - a runtime-rep variable
897
898
899
900
901
902
903
904
905
906
907
908
909

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

To achieve this TcDepVars is backed by deterministic sets which allows them
to be later converted to a list in a deterministic order.

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

912
913
quantifyTyVars, quantifyZonkedTyVars
  :: TcTyCoVarSet   -- global tvs
914
  -> TcDepVars      -- See Note [Dependent type variables] in TcType
915
  -> TcM [TcTyVar]
916
-- See Note [quantifyTyVars]
917
-- Can be given a mixture of TcTyVars and TyVars, in the case of
918
919
--   associated type declarations. Also accepts covars, but *never* returns any.

920
921
-- The zonked variant assumes everything is already zonked.

922
quantifyTyVars gbl_tvs (DV { dv_kvs = dep_tkvs, dv_tvs = nondep_tkvs })
923
  = do { dep_tkvs    <- zonkTyCoVarsAndFVDSet dep_tkvs
924
       ; nondep_tkvs <- zonkTyCoVarsAndFVDSet nondep_tkvs
925
       ; gbl_tvs     <- zonkTyCoVarsAndFV gbl_tvs
926
927
       ; quantifyZonkedTyVars gbl_tvs (DV { dv_kvs = dep_tkvs, dv_tvs = nondep_tkvs }) }

928
929
930
quantifyZonkedTyVars gbl_tvs dvs@(DV{ dv_kvs = dep_tkvs, dv_tvs = nondep_tkvs })
  = do { traceTc "quantifyZonkedTyVars" (vcat [ppr dvs, ppr gbl_tvs])
       ; let all_cvs = filterVarSet isCoVar $ dVarSetToVarSet dep_tkvs
931
932
933
934
             dep_kvs = dVarSetElemsWellScoped $
                       dep_tkvs `dVarSetMinusVarSet` gbl_tvs
                                `dVarSetMinusVarSet` closeOverKinds all_cvs
                 -- dVarSetElemsWellScoped: put the kind variables into
935
936
937
938
939
                 --    well-scoped order.
                 --    E.g.  [k, (a::k)] not the other way roud
                 -- closeOverKinds all_cvs: do not quantify over coercion
                 --    variables, or any any tvs that a covar depends on

940
             nondep_tvs = dVarSetElems $
941
942
943
944
945
946
947
948
949
                          (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
950
                 -- No worry about scoping, because these are all
951
952
                 --    type variables
                 -- NB kinds of tvs are zonked by zonkTyCoVarsAndFV
953

dreixel's avatar
dreixel committed
954
955
             -- In the non-PolyKinds case, default the kind variables
             -- to *, and zonk the tyvars as usual.  Notice that this
956
             -- may make quantifyTyVars return a shorter list
dreixel's avatar
dreixel committed
957
             -- than it was passed, but that's ok
958
959
960
961
962
963
       ; poly_kinds  <- xoptM LangExt.PolyKinds
       ; dep_kvs'    <- mapMaybeM (zonk_quant (not poly_kinds)) dep_kvs
       ; nondep_tvs' <- mapMaybeM (zonk_quant False)            nondep_tvs
           -- Because of the order, any kind variables
           -- mentioned in the kinds of the nondep_tvs'
           -- now refer to the dep_kvs'
964
965
966
967
968

       ; traceTc "quantifyTyVars"
           (vcat [ text "globals:" <+> ppr gbl_tvs
                 , text "nondep:" <+> ppr nondep_tvs
                 , text "dep:" <+> ppr dep_kvs
969
970
                 , text "dep_kvs'" <+> ppr dep_kvs'
                 , text "nondep_tvs'" <+> ppr nondep_tvs' ])
971

972
       ; return (dep_kvs' ++ nondep_tvs') }
973
  where
974
975
    zonk_quant default_kind tkv
      | isTcTyVar tkv = zonkQuantifiedTyVar default_kind tkv
976
      | otherwise     = return $ Just tkv
977
      -- For associated types, we have the class variables
978
      -- in scope, and they are TyVars not TcTyVars
979

980
981
982
983
zonkQuantifiedTyVar :: Bool     -- True  <=> this is a kind var and -XNoPolyKinds
                                -- False <=> not a kind var or -XPolyKinds
                    -> TcTyVar
                    -> TcM (Maybe TcTyVar)
984
985
-- The quantified type variables often include meta type variables
-- we want to freeze them into ordinary type variables, and
986
-- default their kind (e.g. from TYPE v to TYPE Lifted)
987
988
-- The meta tyvar is updated to point to the new skolem TyVar.  Now any
-- bound occurrences of the original type variable will get zonked to
989
990
-- the immutable version.
--
991
-- We leave skolem TyVars alone; they are immutable.
dreixel's avatar
dreixel committed
992
993
994
--
-- This function is called on both kind and type variables,
-- but kind variables *only* if PolyKinds is on.
995
--
996
997
998
999
1000
1001
-- This returns a tyvar if it should be quantified over;
-- otherwise, it returns Nothing. The latter case happens for
--    * Kind variables, with -XNoPolyKinds: don't quantify over these
--    * RuntimeRep variables: we never quantify over these

zonkQuantifiedTyVar default_kind tv
1002
1003
  = case tcTyVarDetails tv of
      SkolemTv {} -> do { kind <- zonkTcType (tyVarKind tv)
1004
                        ; return $ Just (setTyVarKind tv kind) }
1005
1006
        -- It might be a skolem type variable,
        -- for example from a user type signature
1007

1008
1009
1010
1011
      MetaTv { mtv_ref = ref }
        -> do { when debugIsOn (check_empty ref)
              ; zonk_meta_tv tv }

1012
1013
      _other -> pprPanic "zonkQuantifiedTyVar" (ppr tv) -- FlatSkol, RuntimeUnk

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
1014
  where
1015
    zonk_meta_tv :: TcTyVar -> TcM (Maybe TcTyVar)
1016
1017
    zonk_meta_tv tv
      | isRuntimeRepVar tv   -- Never quantify over a RuntimeRep var
Richard Eisenberg's avatar
Richard Eisenberg committed
1018
      = do { writeMetaTyVar tv liftedRepTy
1019
           ; return Nothing }
1020
1021

      | default_kind         -- -XNoPolyKinds and this is a kind var
1022
1023
      = do { _ <- default_kind_var tv
           ; return Nothing }
1024
1025

      | otherwise
1026
      = do { tv' <- skolemiseUnboundMetaTyVar tv