Fix and document cloneWC
[ghc.git] / compiler / typecheck / TcMType.hs
1 {-
2 (c) The University of Glasgow 2006
3 (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4
5
6 Monadic type operations
7
8 This module contains monadic operations over types that contain
9 mutable type variables
10 -}
11
12 {-# LANGUAGE CPP, TupleSections, MultiWayIf #-}
13
14 module TcMType (
15 TcTyVar, TcKind, TcType, TcTauType, TcThetaType, TcTyVarSet,
16
17 --------------------------------
18 -- Creating new mutable type variables
19 newFlexiTyVar,
20 newFlexiTyVarTy, -- Kind -> TcM TcType
21 newFlexiTyVarTys, -- Int -> Kind -> TcM [TcType]
22 newOpenFlexiTyVarTy, newOpenTypeKind,
23 newMetaKindVar, newMetaKindVars, newMetaTyVarTyAtLevel,
24 cloneMetaTyVar,
25 newFmvTyVar, newFskTyVar,
26
27 readMetaTyVar, writeMetaTyVar,
28 newMetaDetails, isFilledMetaTyVar, isUnfilledMetaTyVar,
29
30 --------------------------------
31 -- Expected types
32 ExpType(..), ExpSigmaType, ExpRhoType,
33 mkCheckExpType,
34 newInferExpType, newInferExpTypeInst, newInferExpTypeNoInst,
35 readExpType, readExpType_maybe,
36 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 newCoercionHole, fillCoercionHole, isFilledCoercionHole,
47 unpackCoercionHole, unpackCoercionHole_maybe,
48 checkCoercionHole,
49
50 --------------------------------
51 -- Instantiation
52 newMetaTyVars, newMetaTyVarX, newMetaTyVarsX,
53 newMetaSigTyVars, newMetaSigTyVarX,
54 newSigTyVar, newSkolemTyVar, newWildCardX,
55 tcInstType,
56 tcInstSkolTyVars,tcInstSkolTyVarsX,
57 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 zonkTcTyVar, zonkTcTyVars,
68 zonkTcTyVarToTyVar, zonkSigTyVarPairs,
69 zonkTyCoVarsAndFV, zonkTcTypeAndFV,
70 zonkTyCoVarsAndFVList,
71 zonkTcTypeAndSplitDepVars, zonkTcTypesAndSplitDepVars,
72 zonkQuantifiedTyVar, defaultTyVar,
73 quantifyTyVars,
74 zonkTcTyCoVarBndr, zonkTcTyVarBinder,
75 zonkTcType, zonkTcTypes, zonkCo,
76 zonkTyCoVarKind, zonkTcTypeMapper,
77 zonkTcTypeInKnot,
78
79 zonkEvVar, zonkWC, zonkSimples,
80 zonkId, zonkCoVar,
81 zonkCt, zonkSkolemInfo,
82
83 tcGetGlobalTyCoVars,
84
85 ------------------------------
86 -- Levity polymorphism
87 ensureNotLevPoly, checkForLevPoly, checkForLevPolyX, formatLevPolyErr
88 ) where
89
90 #include "HsVersions.h"
91
92 -- friends:
93 import GhcPrelude
94
95 import TyCoRep
96 import TcType
97 import Type
98 import Coercion
99 import Class
100 import Var
101
102 -- others:
103 import TcRnMonad -- TcType, amongst others
104 import TcEvidence
105 import Id
106 import Name
107 import VarSet
108 import TysWiredIn
109 import TysPrim
110 import VarEnv
111 import NameEnv
112 import PrelNames
113 import Util
114 import Outputable
115 import FastString
116 import SrcLoc
117 import Bag
118 import Pair
119 import UniqSet
120 import qualified GHC.LanguageExtensions as LangExt
121
122 import Control.Monad
123 import Maybes
124 import Data.List ( mapAccumL )
125 import Control.Arrow ( second )
126
127 {-
128 ************************************************************************
129 * *
130 Kind variables
131 * *
132 ************************************************************************
133 -}
134
135 mkKindName :: Unique -> Name
136 mkKindName unique = mkSystemName unique kind_var_occ
137
138 kind_var_occ :: OccName -- Just one for all MetaKindVars
139 -- They may be jiggled by tidying
140 kind_var_occ = mkOccName tvName "k"
141
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
149 newMetaKindVars :: Int -> TcM [TcKind]
150 newMetaKindVars n = mapM (\ _ -> newMetaKindVar) (nOfThem n ())
151
152 {-
153 ************************************************************************
154 * *
155 Evidence variables; range over constraints we can abstract over
156 * *
157 ************************************************************************
158 -}
159
160 newEvVars :: TcThetaType -> TcM [EvVar]
161 newEvVars theta = mapM newEvVar theta
162
163 --------------
164
165 newEvVar :: TcPredType -> TcRnIf gbl lcl EvVar
166 -- Creates new *rigid* variables for predicates
167 newEvVar ty = do { name <- newSysName (predTypeOccName ty)
168 ; return (mkLocalIdOrCoVar name ty) }
169
170 newWanted :: CtOrigin -> Maybe TypeOrKind -> PredType -> TcM CtEvidence
171 -- Deals with both equality and non-equality predicates
172 newWanted orig t_or_k pty
173 = do loc <- getCtLocM orig t_or_k
174 d <- if isEqPred pty then HoleDest <$> newCoercionHole pty
175 else EvVarDest <$> newEvVar pty
176 return $ CtWanted { ctev_dest = d
177 , ctev_pred = pty
178 , ctev_nosh = WDeriv
179 , ctev_loc = loc }
180
181 newWanteds :: CtOrigin -> ThetaType -> TcM [CtEvidence]
182 newWanteds orig = mapM (newWanted orig Nothing)
183
184 ----------------------------------------------
185 -- Cloning constraints
186 ----------------------------------------------
187
188 cloneWanted :: Ct -> TcM Ct
189 cloneWanted ct
190 | ev@(CtWanted { ctev_dest = HoleDest {}, ctev_pred = pty }) <- ctEvidence ct
191 = do { co_hole <- newCoercionHole pty
192 ; return (mkNonCanonical (ev { ctev_dest = HoleDest co_hole })) }
193 | otherwise
194 = return ct
195
196 cloneWC :: WantedConstraints -> TcM WantedConstraints
197 -- Clone all the evidence bindings in
198 -- a) the ic_bind field of any implications
199 -- b) the CoercionHoles of any wanted constraints
200 -- so that solving the WantedConstraints will not have any visible side
201 -- effect, /except/ from causing unifications
202 cloneWC wc@(WC { wc_simple = simples, wc_impl = implics })
203 = do { simples' <- mapBagM cloneWanted simples
204 ; implics' <- mapBagM cloneImplication implics
205 ; return (wc { wc_simple = simples', wc_impl = implics' }) }
206
207 cloneImplication :: Implication -> TcM Implication
208 cloneImplication implic@(Implic { ic_binds = binds, ic_wanted = inner_wanted })
209 = do { binds' <- cloneEvBindsVar binds
210 ; inner_wanted' <- cloneWC inner_wanted
211 ; return (implic { ic_binds = binds', ic_wanted = inner_wanted' }) }
212
213 ----------------------------------------------
214 -- Emitting constraints
215 ----------------------------------------------
216
217 -- | Emits a new Wanted. Deals with both equalities and non-equalities.
218 emitWanted :: CtOrigin -> TcPredType -> TcM EvTerm
219 emitWanted origin pty
220 = do { ev <- newWanted origin Nothing pty
221 ; emitSimple $ mkNonCanonical ev
222 ; return $ ctEvTerm ev }
223
224 -- | Emits a new equality constraint
225 emitWantedEq :: CtOrigin -> TypeOrKind -> Role -> TcType -> TcType -> TcM Coercion
226 emitWantedEq origin t_or_k role ty1 ty2
227 = do { hole <- newCoercionHole pty
228 ; loc <- getCtLocM origin (Just t_or_k)
229 ; emitSimple $ mkNonCanonical $
230 CtWanted { ctev_pred = pty, ctev_dest = HoleDest hole
231 , ctev_nosh = WDeriv, ctev_loc = loc }
232 ; return (HoleCo hole) }
233 where
234 pty = mkPrimEqPredRole role ty1 ty2
235
236 -- | Creates a new EvVar and immediately emits it as a Wanted.
237 -- No equality predicates here.
238 emitWantedEvVar :: CtOrigin -> TcPredType -> TcM EvVar
239 emitWantedEvVar origin ty
240 = do { new_cv <- newEvVar ty
241 ; loc <- getCtLocM origin Nothing
242 ; let ctev = CtWanted { ctev_dest = EvVarDest new_cv
243 , ctev_pred = ty
244 , ctev_nosh = WDeriv
245 , ctev_loc = loc }
246 ; emitSimple $ mkNonCanonical ctev
247 ; return new_cv }
248
249 emitWantedEvVars :: CtOrigin -> [TcPredType] -> TcM [EvVar]
250 emitWantedEvVars orig = mapM (emitWantedEvVar orig)
251
252 newDict :: Class -> [TcType] -> TcM DictId
253 newDict cls tys
254 = do { name <- newSysName (mkDictOcc (getOccName cls))
255 ; return (mkLocalId name (mkClassPred cls tys)) }
256
257 predTypeOccName :: PredType -> OccName
258 predTypeOccName ty = case classifyPredType ty of
259 ClassPred cls _ -> mkDictOcc (getOccName cls)
260 EqPred {} -> mkVarOccFS (fsLit "co")
261 IrredPred {} -> mkVarOccFS (fsLit "irred")
262 ForAllPred {} -> mkVarOccFS (fsLit "df")
263
264 {-
265 ************************************************************************
266 * *
267 Coercion holes
268 * *
269 ************************************************************************
270 -}
271
272 newCoercionHole :: TcPredType -> TcM CoercionHole
273 newCoercionHole pred_ty
274 = do { co_var <- newEvVar pred_ty
275 ; traceTc "New coercion hole:" (ppr co_var)
276 ; ref <- newMutVar Nothing
277 ; return $ CoercionHole { ch_co_var = co_var, ch_ref = ref } }
278
279 -- | Put a value in a coercion hole
280 fillCoercionHole :: CoercionHole -> Coercion -> TcM ()
281 fillCoercionHole (CoercionHole { ch_ref = ref, ch_co_var = cv }) co
282 = do {
283 #if defined(DEBUG)
284 ; cts <- readTcRef ref
285 ; whenIsJust cts $ \old_co ->
286 pprPanic "Filling a filled coercion hole" (ppr cv $$ ppr co $$ ppr old_co)
287 #endif
288 ; traceTc "Filling coercion hole" (ppr cv <+> text ":=" <+> ppr co)
289 ; writeTcRef ref (Just co) }
290
291 -- | Is a coercion hole filled in?
292 isFilledCoercionHole :: CoercionHole -> TcM Bool
293 isFilledCoercionHole (CoercionHole { ch_ref = ref }) = isJust <$> readTcRef ref
294
295 -- | Retrieve the contents of a coercion hole. Panics if the hole
296 -- is unfilled
297 unpackCoercionHole :: CoercionHole -> TcM Coercion
298 unpackCoercionHole hole
299 = do { contents <- unpackCoercionHole_maybe hole
300 ; case contents of
301 Just co -> return co
302 Nothing -> pprPanic "Unfilled coercion hole" (ppr hole) }
303
304 -- | Retrieve the contents of a coercion hole, if it is filled
305 unpackCoercionHole_maybe :: CoercionHole -> TcM (Maybe Coercion)
306 unpackCoercionHole_maybe (CoercionHole { ch_ref = ref }) = readTcRef ref
307
308 -- | Check that a coercion is appropriate for filling a hole. (The hole
309 -- itself is needed only for printing. NB: This must be /lazy/ in the coercion,
310 -- as it's used in TcHsSyn in the presence of knots.
311 -- Always returns the checked coercion, but this return value is necessary
312 -- so that the input coercion is forced only when the output is forced.
313 checkCoercionHole :: CoVar -> Coercion -> TcM Coercion
314 checkCoercionHole cv co
315 | debugIsOn
316 = do { cv_ty <- zonkTcType (varType cv)
317 -- co is already zonked, but cv might not be
318 ; return $
319 ASSERT2( ok cv_ty
320 , (text "Bad coercion hole" <+>
321 ppr cv <> colon <+> vcat [ ppr t1, ppr t2, ppr role
322 , ppr cv_ty ]) )
323 co }
324 | otherwise
325 = return co
326
327 where
328 (Pair t1 t2, role) = coercionKindRole co
329 ok cv_ty | EqPred cv_rel cv_t1 cv_t2 <- classifyPredType cv_ty
330 = t1 `eqType` cv_t1
331 && t2 `eqType` cv_t2
332 && role == eqRelRole cv_rel
333 | otherwise
334 = False
335
336 {-
337 ************************************************************************
338 *
339 Expected types
340 *
341 ************************************************************************
342
343 Note [ExpType]
344 ~~~~~~~~~~~~~~
345
346 An ExpType is used as the "expected type" when type-checking an expression.
347 An ExpType can hold a "hole" that can be filled in by the type-checker.
348 This allows us to have one tcExpr that works in both checking mode and
349 synthesis mode (that is, bidirectional type-checking). Previously, this
350 was achieved by using ordinary unification variables, but we don't need
351 or want that generality. (For example, #11397 was caused by doing the
352 wrong thing with unification variables.) Instead, we observe that these
353 holes should
354
355 1. never be nested
356 2. never appear as the type of a variable
357 3. be used linearly (never be duplicated)
358
359 By defining ExpType, separately from Type, we can achieve goals 1 and 2
360 statically.
361
362 See also [wiki:Typechecking]
363
364 Note [TcLevel of ExpType]
365 ~~~~~~~~~~~~~~~~~~~~~~~~~
366 Consider
367
368 data G a where
369 MkG :: G Bool
370
371 foo MkG = True
372
373 This is a classic untouchable-variable / ambiguous GADT return type
374 scenario. But, with ExpTypes, we'll be inferring the type of the RHS.
375 And, because there is only one branch of the case, we won't trigger
376 Note [Case branches must never infer a non-tau type] of TcMatches.
377 We thus must track a TcLevel in an Inferring ExpType. If we try to
378 fill the ExpType and find that the TcLevels don't work out, we
379 fill the ExpType with a tau-tv at the low TcLevel, hopefully to
380 be worked out later by some means. This is triggered in
381 test gadt/gadt-escape1.
382
383 -}
384
385 -- actual data definition is in TcType
386
387 -- | Make an 'ExpType' suitable for inferring a type of kind * or #.
388 newInferExpTypeNoInst :: TcM ExpSigmaType
389 newInferExpTypeNoInst = newInferExpType False
390
391 newInferExpTypeInst :: TcM ExpRhoType
392 newInferExpTypeInst = newInferExpType True
393
394 newInferExpType :: Bool -> TcM ExpType
395 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 -- | Extract a type out of an ExpType, if one exists. But one should always
404 -- exist. Unless you're quite sure you know what you're doing.
405 readExpType_maybe :: ExpType -> TcM (Maybe TcType)
406 readExpType_maybe (Check ty) = return (Just ty)
407 readExpType_maybe (Infer (IR { ir_ref = ref})) = readMutVar ref
408
409 -- | Extract a type out of an ExpType. Otherwise, panics.
410 readExpType :: ExpType -> TcM TcType
411 readExpType exp_ty
412 = do { mb_ty <- readExpType_maybe exp_ty
413 ; case mb_ty of
414 Just ty -> return ty
415 Nothing -> pprPanic "Unknown expected type" (ppr exp_ty) }
416
417 -- | Returns the expected type when in checking mode.
418 checkingExpType_maybe :: ExpType -> Maybe TcType
419 checkingExpType_maybe (Check ty) = Just ty
420 checkingExpType_maybe _ = Nothing
421
422 -- | Returns the expected type when in checking mode. Panics if in inference
423 -- mode.
424 checkingExpType :: String -> ExpType -> TcType
425 checkingExpType _ (Check ty) = ty
426 checkingExpType err et = pprPanic "checkingExpType" (text err $$ ppr et)
427
428 tauifyExpType :: ExpType -> TcM ExpType
429 -- ^ Turn a (Infer hole) type into a (Check alpha),
430 -- where alpha is a fresh unification variable
431 tauifyExpType (Check ty) = return (Check ty) -- No-op for (Check ty)
432 tauifyExpType (Infer inf_res) = do { ty <- inferResultToType inf_res
433 ; return (Check ty) }
434
435 -- | Extracts the expected type if there is one, or generates a new
436 -- TauTv if there isn't.
437 expTypeToType :: ExpType -> TcM TcType
438 expTypeToType (Check ty) = return ty
439 expTypeToType (Infer inf_res) = inferResultToType inf_res
440
441 inferResultToType :: InferResult -> TcM Type
442 inferResultToType (IR { ir_uniq = u, ir_lvl = tc_lvl
443 , ir_ref = ref })
444 = do { rr <- newMetaTyVarTyAtLevel tc_lvl runtimeRepTy
445 ; tau <- newMetaTyVarTyAtLevel tc_lvl (tYPE rr)
446 -- See Note [TcLevel of ExpType]
447 ; writeMutVar ref (Just tau)
448 ; traceTc "Forcing ExpType to be monomorphic:"
449 (ppr u <+> text ":=" <+> ppr tau)
450 ; return tau }
451
452
453 {- *********************************************************************
454 * *
455 SkolemTvs (immutable)
456 * *
457 ********************************************************************* -}
458
459 tcInstType :: ([TyVar] -> TcM (TCvSubst, [TcTyVar]))
460 -- ^ How to instantiate the type variables
461 -> Id -- ^ Type to instantiate
462 -> TcM ([(Name, TcTyVar)], TcThetaType, TcType) -- ^ Result
463 -- (type vars, preds (incl equalities), rho)
464 tcInstType inst_tyvars id
465 = case tcSplitForAllTys (idType id) of
466 ([], rho) -> let -- There may be overloading despite no type variables;
467 -- (?x :: Int) => Int -> Int
468 (theta, tau) = tcSplitPhiTy rho
469 in
470 return ([], theta, tau)
471
472 (tyvars, rho) -> do { (subst, tyvars') <- inst_tyvars tyvars
473 ; let (theta, tau) = tcSplitPhiTy (substTyAddInScope subst rho)
474 tv_prs = map tyVarName tyvars `zip` tyvars'
475 ; return (tv_prs, theta, tau) }
476
477 tcSkolDFunType :: DFunId -> TcM ([TcTyVar], TcThetaType, TcType)
478 -- Instantiate a type signature with skolem constants.
479 -- We could give them fresh names, but no need to do so
480 tcSkolDFunType dfun
481 = do { (tv_prs, theta, tau) <- tcInstType tcInstSuperSkolTyVars dfun
482 ; 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
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)
494 where
495 kind = substTyUnchecked subst (tyVarKind tv)
496 new_tv = mkTcTyVar (tyVarName tv) kind superSkolemTv
497
498 -- | Given a list of @['TyVar']@, skolemize the type variables,
499 -- returning a substitution mapping the original tyvars to the
500 -- skolems, and the list of newly bound skolems. See also
501 -- tcInstSkolTyVars' for a precondition. The resulting
502 -- skolems are non-overlappable; see Note [Overlap and deriving]
503 -- for an example where this matters.
504 tcInstSkolTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
505 tcInstSkolTyVars = tcInstSkolTyVarsX emptyTCvSubst
506
507 tcInstSkolTyVarsX :: TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
508 tcInstSkolTyVarsX = tcInstSkolTyVars' False
509
510 tcInstSuperSkolTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
511 tcInstSuperSkolTyVars = tcInstSuperSkolTyVarsX emptyTCvSubst
512
513 tcInstSuperSkolTyVarsX :: TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
514 tcInstSuperSkolTyVarsX subst = tcInstSkolTyVars' True subst
515
516 tcInstSkolTyVars' :: Bool -> TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
517 -- Precondition: tyvars should be ordered (kind vars first)
518 -- 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 ; lvl <- getTcLevel
523 ; instSkolTyCoVarsX (mkTcSkolTyVar lvl loc overlappable) subst tvs }
524
525 mkTcSkolTyVar :: TcLevel -> SrcSpan -> Bool -> TcTyCoVarMaker gbl lcl
526 -- Allocates skolems whose level is ONE GREATER THAN the passed-in tc_lvl
527 -- See Note [Skolem level allocation]
528 mkTcSkolTyVar tc_lvl loc overlappable old_name kind
529 = do { uniq <- newUnique
530 ; let name = mkInternalName uniq (getOccName old_name) loc
531 ; return (mkTcTyVar name kind details) }
532 where
533 details = SkolemTv (pushTcLevel tc_lvl) overlappable
534 -- pushTcLevel: see Note [Skolem level allocation]
535
536 {- Note [Skolem level allocation]
537 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
538 We generally allocate skolems /before/ calling pushLevelAndCaptureConstraints.
539 So we want their level to the level of the soon-to-be-created implication,
540 which has a level one higher than the current level. Hence the pushTcLevel.
541 It feels like a slight hack. Applies also to vanillaSkolemTv.
542
543 -}
544
545 ------------------
546 freshenTyVarBndrs :: [TyVar] -> TcRnIf gbl lcl (TCvSubst, [TyVar])
547 -- ^ Give fresh uniques to a bunch of TyVars, but they stay
548 -- as TyVars, rather than becoming TcTyVars
549 -- Used in FamInst.newFamInst, and Inst.newClsInst
550 freshenTyVarBndrs = instSkolTyCoVars mk_tv
551 where
552 mk_tv old_name kind
553 = do { uniq <- newUnique
554 ; return (mkTyVar (setNameUnique old_name uniq) kind) }
555
556 freshenCoVarBndrsX :: TCvSubst -> [CoVar] -> TcRnIf gbl lcl (TCvSubst, [CoVar])
557 -- ^ Give fresh uniques to a bunch of CoVars
558 -- Used in FamInst.newFamInst
559 freshenCoVarBndrsX subst = instSkolTyCoVarsX mk_cv subst
560 where
561 mk_cv old_name kind
562 = do { uniq <- newUnique
563 ; return (mkCoVar (setNameUnique old_name uniq) kind) }
564
565 ------------------
566 type TcTyCoVarMaker gbl lcl = Name -> Kind -> TcRnIf gbl lcl TyCoVar
567 -- The TcTyCoVarMaker should make a fresh Name, based on the old one
568 -- Freshness is critical. See Note [Skolems in zonkSyntaxExpr] in TcHsSyn
569
570 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 -> TCvSubst -> [TyCoVar] -> TcRnIf gbl lcl (TCvSubst, [TyCoVar])
575 instSkolTyCoVarsX mk_tcv = mapAccumLM (instSkolTyCoVarX mk_tcv)
576
577 instSkolTyCoVarX :: TcTyCoVarMaker gbl lcl
578 -> TCvSubst -> TyCoVar -> TcRnIf gbl lcl (TCvSubst, TyCoVar)
579 instSkolTyCoVarX mk_tcv subst tycovar
580 = do { new_tcv <- mk_tcv old_name kind
581 ; let subst1 | isTyVar new_tcv
582 = extendTvSubstWithClone subst tycovar new_tcv
583 | otherwise
584 = extendCvSubstWithClone subst tycovar new_tcv
585 ; return (subst1, new_tcv) }
586 where
587 old_name = tyVarName tycovar
588 kind = substTyUnchecked subst (tyVarKind tycovar)
589
590 newFskTyVar :: TcType -> TcM TcTyVar
591 newFskTyVar fam_ty
592 = do { uniq <- newUnique
593 ; ref <- newMutVar Flexi
594 ; tclvl <- getTcLevel
595 ; let details = MetaTv { mtv_info = FlatSkolTv
596 , mtv_ref = ref
597 , mtv_tclvl = tclvl }
598 name = mkMetaTyVarName uniq (fsLit "fsk")
599 ; return (mkTcTyVar name (typeKind fam_ty) details) }
600
601 {-
602 Note [Kind substitution when instantiating]
603 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
604 When we instantiate a bunch of kind and type variables, first we
605 expect them to be topologically sorted.
606 Then we have to instantiate the kind variables, build a substitution
607 from old variables to the new variables, then instantiate the type
608 variables substituting the original kind.
609
610 Exemple: If we want to instantiate
611 [(k1 :: *), (k2 :: *), (a :: k1 -> k2), (b :: k1)]
612 we want
613 [(?k1 :: *), (?k2 :: *), (?a :: ?k1 -> ?k2), (?b :: ?k1)]
614 instead of the buggous
615 [(?k1 :: *), (?k2 :: *), (?a :: k1 -> k2), (?b :: k1)]
616
617
618 ************************************************************************
619 * *
620 MetaTvs (meta type variables; mutable)
621 * *
622 ************************************************************************
623 -}
624
625 -- a SigTv can unify with type *variables* only, including other SigTvs
626 -- and skolems. Sometimes, they can unify with type variables that the
627 -- user would rather keep distinct; see #11203 for an example.
628 -- So, any client of this
629 -- function needs to either allow the SigTvs to unify with each other
630 -- (say, for pattern-bound scoped type variables), or check that they
631 -- don't (say, with a call to findDubSigTvs).
632 newSigTyVar :: Name -> Kind -> TcM TcTyVar
633 newSigTyVar name kind
634 = do { details <- newMetaDetails SigTv
635 ; let tyvar = mkTcTyVar name kind details
636 ; traceTc "newSigTyVar" (ppr tyvar)
637 ; return tyvar }
638
639 -- makes a new skolem tv
640 newSkolemTyVar :: Name -> Kind -> TcM TcTyVar
641 newSkolemTyVar name kind = do { lvl <- getTcLevel
642 ; return (mkTcTyVar name kind (SkolemTv lvl False)) }
643
644 newFmvTyVar :: TcType -> TcM TcTyVar
645 -- Very like newMetaTyVar, except sets mtv_tclvl to one less
646 -- so that the fmv is untouchable.
647 newFmvTyVar fam_ty
648 = do { uniq <- newUnique
649 ; ref <- newMutVar Flexi
650 ; tclvl <- getTcLevel
651 ; let details = MetaTv { mtv_info = FlatMetaTv
652 , mtv_ref = ref
653 , mtv_tclvl = tclvl }
654 name = mkMetaTyVarName uniq (fsLit "s")
655 ; return (mkTcTyVar name (typeKind fam_ty) details) }
656
657 newMetaDetails :: MetaInfo -> TcM TcTyVarDetails
658 newMetaDetails info
659 = do { ref <- newMutVar Flexi
660 ; tclvl <- getTcLevel
661 ; return (MetaTv { mtv_info = info
662 , mtv_ref = ref
663 , mtv_tclvl = tclvl }) }
664
665 cloneMetaTyVar :: TcTyVar -> TcM TcTyVar
666 cloneMetaTyVar tv
667 = ASSERT( isTcTyVar tv )
668 do { uniq <- newUnique
669 ; ref <- newMutVar Flexi
670 ; let name' = setNameUnique (tyVarName tv) uniq
671 details' = case tcTyVarDetails tv of
672 details@(MetaTv {}) -> details { mtv_ref = ref }
673 _ -> pprPanic "cloneMetaTyVar" (ppr tv)
674 tyvar = mkTcTyVar name' (tyVarKind tv) details'
675 ; traceTc "cloneMetaTyVar" (ppr tyvar)
676 ; return tyvar }
677
678 -- Works for both type and kind variables
679 readMetaTyVar :: TyVar -> TcM MetaDetails
680 readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
681 readMutVar (metaTyVarRef tyvar)
682
683 isFilledMetaTyVar :: TyVar -> TcM Bool
684 -- True of a filled-in (Indirect) meta type variable
685 isFilledMetaTyVar tv
686 | MetaTv { mtv_ref = ref } <- tcTyVarDetails tv
687 = do { details <- readMutVar ref
688 ; return (isIndirect details) }
689 | otherwise = return False
690
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 = do { details <- readMutVar ref
696 ; return (isFlexi details) }
697 | otherwise = return False
698
699 --------------------
700 -- Works with both type and kind variables
701 writeMetaTyVar :: TcTyVar -> TcType -> TcM ()
702 -- Write into a currently-empty MetaTyVar
703
704 writeMetaTyVar tyvar ty
705 | not debugIsOn
706 = writeMetaTyVarRef tyvar (metaTyVarRef tyvar) ty
707
708 -- Everything from here on only happens if DEBUG is on
709 | not (isTcTyVar tyvar)
710 = WARN( True, text "Writing to non-tc tyvar" <+> ppr tyvar )
711 return ()
712
713 | MetaTv { mtv_ref = ref } <- tcTyVarDetails tyvar
714 = writeMetaTyVarRef tyvar ref ty
715
716 | otherwise
717 = 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 -- the ref cell must be for the same tyvar
724 writeMetaTyVarRef tyvar ref ty
725 | not debugIsOn
726 = do { traceTc "writeMetaTyVar" (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)
727 <+> text ":=" <+> ppr ty)
728 ; writeTcRef ref (Indirect ty) }
729
730 -- Everything from here on only happens if DEBUG is on
731 | otherwise
732 = do { meta_details <- readMutVar ref;
733 -- Zonk kinds to allow the error check to work
734 ; zonked_tv_kind <- zonkTcType tv_kind
735 ; zonked_ty <- zonkTcType ty
736 ; let zonked_ty_kind = typeKind zonked_ty -- need to zonk even before typeKind;
737 -- 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 kind_msg = hang (text "Ill-kinded update to meta tyvar")
744 2 ( ppr tyvar <+> text "::" <+> (ppr tv_kind $$ ppr zonked_tv_kind)
745 <+> text ":="
746 <+> ppr ty <+> text "::" <+> (ppr zonked_ty_kind) )
747
748 ; traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty)
749
750 -- Check for double updates
751 ; MASSERT2( isFlexi meta_details, double_upd_msg meta_details )
752
753 -- Check for level OK
754 -- See Note [Level check when unifying]
755 ; MASSERT2( level_check_ok, level_check_msg )
756
757 -- Check Kinds ok
758 ; MASSERT2( kind_check_ok, kind_msg )
759
760 -- Do the write
761 ; writeMutVar ref (Indirect ty) }
762 where
763 tv_kind = tyVarKind tyvar
764
765 tv_lvl = tcTyVarLevel tyvar
766 ty_lvl = tcTypeLevel ty
767
768 level_check_ok = not (ty_lvl `strictlyDeeperThan` tv_lvl)
769 level_check_msg = ppr ty_lvl $$ ppr tv_lvl $$ ppr tyvar $$ ppr ty
770
771 double_upd_msg details = hang (text "Double update of meta tyvar")
772 2 (ppr tyvar $$ ppr details)
773
774
775 {- Note [Level check when unifying]
776 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
777 When unifying
778 alpha:lvl := ty
779 we expect that the TcLevel of 'ty' will be <= lvl.
780 However, during unflatting we do
781 fuv:l := ty:(l+1)
782 which is usually wrong; hence the check isFmmvTyVar in level_check_ok.
783 See Note [TcLevel assignment] in TcType.
784 -}
785
786 {-
787 % Generating fresh variables for pattern match check
788 -}
789
790
791 {-
792 ************************************************************************
793 * *
794 MetaTvs: TauTvs
795 * *
796 ************************************************************************
797
798 Note [Never need to instantiate coercion variables]
799 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
800 With coercion variables sloshing around in types, it might seem that we
801 sometimes need to instantiate coercion variables. This would be problematic,
802 because coercion variables inhabit unboxed equality (~#), and the constraint
803 solver thinks in terms only of boxed equality (~). The solution is that
804 we never need to instantiate coercion variables in the first place.
805
806 The tyvars that we need to instantiate come from the types of functions,
807 data constructors, and patterns. These will never be quantified over
808 coercion variables, except for the special case of the promoted Eq#. But,
809 that can't ever appear in user code, so we're safe!
810 -}
811
812 mkMetaTyVarName :: Unique -> FastString -> Name
813 -- Makes a /System/ Name, which is eagerly eliminated by
814 -- the unifier; see TcUnify.nicer_to_update_tv1, and
815 -- TcCanonical.canEqTyVarTyVar (nicer_to_update_tv2)
816 mkMetaTyVarName uniq str = mkSystemName uniq (mkTyVarOccFS str)
817
818 newAnonMetaTyVar :: MetaInfo -> Kind -> TcM TcTyVar
819 -- Make a new meta tyvar out of thin air
820 newAnonMetaTyVar meta_info kind
821 = do { uniq <- newUnique
822 ; let name = mkMetaTyVarName uniq s
823 s = case meta_info of
824 TauTv -> fsLit "t"
825 FlatMetaTv -> fsLit "fmv"
826 FlatSkolTv -> fsLit "fsk"
827 SigTv -> fsLit "a"
828 ; details <- newMetaDetails meta_info
829 ; let tyvar = mkTcTyVar name kind details
830 ; traceTc "newAnonMetaTyVar" (ppr tyvar)
831 ; return tyvar }
832
833 cloneAnonMetaTyVar :: MetaInfo -> TyVar -> TcKind -> TcM TcTyVar
834 -- Same as newAnonMetaTyVar, but use a supplied TyVar as the source of the print-name
835 cloneAnonMetaTyVar info tv kind
836 = do { uniq <- newUnique
837 ; details <- newMetaDetails info
838 ; let name = mkSystemName uniq (getOccName tv)
839 -- See Note [Name of an instantiated type variable]
840 tyvar = mkTcTyVar name kind details
841 ; traceTc "cloneAnonMetaTyVar" (ppr tyvar)
842 ; return tyvar }
843
844 {- Note [Name of an instantiated type variable]
845 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
846 At the moment we give a unification variable a System Name, which
847 influences the way it is tidied; see TypeRep.tidyTyVarBndr.
848 -}
849
850 newFlexiTyVar :: Kind -> TcM TcTyVar
851 newFlexiTyVar kind = newAnonMetaTyVar TauTv kind
852
853 newFlexiTyVarTy :: Kind -> TcM TcType
854 newFlexiTyVarTy kind = do
855 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 newOpenTypeKind :: TcM TcKind
862 newOpenTypeKind
863 = do { rr <- newFlexiTyVarTy runtimeRepTy
864 ; return (tYPE rr) }
865
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 newOpenFlexiTyVarTy :: TcM TcType
869 newOpenFlexiTyVarTy
870 = do { kind <- newOpenTypeKind
871 ; newFlexiTyVarTy kind }
872
873 newMetaSigTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
874 newMetaSigTyVars = mapAccumLM newMetaSigTyVarX emptyTCvSubst
875
876 newMetaTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
877 -- Instantiate with META type variables
878 -- Note that this works for a sequence of kind, type, and coercion variables
879 -- variables. Eg [ (k:*), (a:k->k) ]
880 -- Gives [ (k7:*), (a8:k7->k7) ]
881 newMetaTyVars = mapAccumLM newMetaTyVarX emptyTCvSubst
882 -- emptyTCvSubst has an empty in-scope set, but that's fine here
883 -- Since the tyvars are freshly made, they cannot possibly be
884 -- captured by any existing for-alls.
885
886 newMetaTyVarX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
887 -- Make a new unification variable tyvar whose Name and Kind come from
888 -- an existing TyVar. We substitute kind variables in the kind.
889 newMetaTyVarX subst tyvar = new_meta_tv_x TauTv subst tyvar
890
891 newMetaTyVarsX :: TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
892 -- Just like newMetaTyVars, but start with an existing substitution.
893 newMetaTyVarsX subst = mapAccumLM newMetaTyVarX subst
894
895 newMetaSigTyVarX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
896 -- Just like newMetaTyVarX, but make a SigTv
897 newMetaSigTyVarX subst tyvar = new_meta_tv_x SigTv subst tyvar
898
899 newWildCardX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
900 newWildCardX subst tv
901 = do { new_tv <- newAnonMetaTyVar TauTv (substTy subst (tyVarKind tv))
902 ; return (extendTvSubstWithClone subst tv new_tv, new_tv) }
903
904 new_meta_tv_x :: MetaInfo -> TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
905 new_meta_tv_x info subst tv
906 = do { new_tv <- cloneAnonMetaTyVar info tv substd_kind
907 ; let subst1 = extendTvSubstWithClone subst tv new_tv
908 ; return (subst1, new_tv) }
909 where
910 substd_kind = substTyUnchecked subst (tyVarKind tv)
911 -- NOTE: Trac #12549 is fixed so we could use
912 -- substTy here, but the tc_infer_args problem
913 -- is not yet fixed so leaving as unchecked for now.
914 -- OLD NOTE:
915 -- Unchecked because we call newMetaTyVarX from
916 -- tcInstTyBinder, which is called from tcInferApps
917 -- which does not yet take enough trouble to ensure
918 -- the in-scope set is right; e.g. Trac #12785 trips
919 -- if we use substTy here
920
921 newMetaTyVarTyAtLevel :: TcLevel -> TcKind -> TcM TcType
922 newMetaTyVarTyAtLevel tc_lvl kind
923 = do { uniq <- newUnique
924 ; ref <- newMutVar Flexi
925 ; let name = mkMetaTyVarName uniq (fsLit "p")
926 details = MetaTv { mtv_info = TauTv
927 , mtv_ref = ref
928 , mtv_tclvl = tc_lvl }
929 ; return (mkTyVarTy (mkTcTyVar name kind details)) }
930
931 {- *********************************************************************
932 * *
933 Quantification
934 * *
935 ************************************************************************
936
937 Note [quantifyTyVars]
938 ~~~~~~~~~~~~~~~~~~~~~
939 quantifyTyVars is given the free vars of a type that we
940 are about to wrap in a forall.
941
942 It takes these free type/kind variables (partitioned into dependent and
943 non-dependent variables) and
944 1. Zonks them and remove globals and covars
945 2. Extends kvs1 with free kind vars in the kinds of tvs (removing globals)
946 3. Calls zonkQuantifiedTyVar on each
947
948 Step (2) is often unimportant, because the kind variable is often
949 also free in the type. Eg
950 Typeable k (a::k)
951 has free vars {k,a}. But the type (see Trac #7916)
952 (f::k->*) (a::k)
953 has free vars {f,a}, but we must add 'k' as well! Hence step (2).
954
955 * This function distinguishes between dependent and non-dependent
956 variables only to keep correct defaulting behavior with -XNoPolyKinds.
957 With -XPolyKinds, it treats both classes of variables identically.
958
959 * quantifyTyVars never quantifies over
960 - a coercion variable
961 - a runtime-rep variable
962
963 Note [quantifyTyVars determinism]
964 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
965 The results of quantifyTyVars are wrapped in a forall and can end up in the
966 interface file. One such example is inferred type signatures. They also affect
967 the results of optimizations, for example worker-wrapper. This means that to
968 get deterministic builds quantifyTyVars needs to be deterministic.
969
970 To achieve this CandidatesQTvs is backed by deterministic sets which allows them
971 to be later converted to a list in a deterministic order.
972
973 For more information about deterministic sets see
974 Note [Deterministic UniqFM] in UniqDFM.
975 -}
976
977 quantifyTyVars
978 :: 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 -- associated type declarations. Also accepts covars, but *never* returns any.
985
986 quantifyTyVars gbl_tvs dvs@(DV{ dv_kvs = dep_tkvs, dv_tvs = nondep_tkvs })
987 = do { traceTc "quantifyTyVars" (vcat [ppr dvs, ppr gbl_tvs])
988 ; let dep_kvs = dVarSetElemsWellScoped $
989 dep_tkvs `dVarSetMinusVarSet` gbl_tvs
990 -- dVarSetElemsWellScoped: put the kind variables into
991 -- well-scoped order.
992 -- E.g. [k, (a::k)] not the other way roud
993
994 nondep_tvs = dVarSetElems $
995 (nondep_tkvs `minusDVarSet` dep_tkvs)
996 `dVarSetMinusVarSet` gbl_tvs
997 -- See Note [Dependent type variables] in TcType
998 -- The `minus` dep_tkvs removes any kind-level vars
999 -- e.g. T k (a::k) Since k appear in a kind it'll
1000 -- be in dv_kvs, and is dependent. So remove it from
1001 -- dv_tvs which will also contain k
1002 -- No worry about dependent covars here;
1003 -- they are all in dep_tkvs
1004 -- No worry about scoping, because these are all
1005 -- type variables
1006 -- NB kinds of tvs are zonked by zonkTyCoVarsAndFV
1007
1008 -- In the non-PolyKinds case, default the kind variables
1009 -- to *, and zonk the tyvars as usual. Notice that this
1010 -- may make quantifyTyVars return a shorter list
1011 -- than it was passed, but that's ok
1012 ; poly_kinds <- xoptM LangExt.PolyKinds
1013 ; dep_kvs' <- mapMaybeM (zonk_quant (not poly_kinds)) dep_kvs
1014 ; nondep_tvs' <- mapMaybeM (zonk_quant False) nondep_tvs
1015 ; let final_qtvs = dep_kvs' ++ nondep_tvs'
1016 -- Because of the order, any kind variables
1017 -- mentioned in the kinds of the nondep_tvs'
1018 -- now refer to the dep_kvs'
1019
1020 ; traceTc "quantifyTyVars"
1021 (vcat [ text "globals:" <+> ppr gbl_tvs
1022 , text "nondep:" <+> pprTyVars nondep_tvs
1023 , text "dep:" <+> pprTyVars dep_kvs
1024 , text "dep_kvs'" <+> pprTyVars dep_kvs'
1025 , text "nondep_tvs'" <+> pprTyVars nondep_tvs' ])
1026
1027 -- We should never quantify over coercion variables; check this
1028 ; let co_vars = filter isCoVar final_qtvs
1029 ; MASSERT2( null co_vars, ppr co_vars )
1030
1031 ; return final_qtvs }
1032 where
1033 -- zonk_quant returns a tyvar if it should be quantified over;
1034 -- otherwise, it returns Nothing. The latter case happens for
1035 -- * Kind variables, with -XNoPolyKinds: don't quantify over these
1036 -- * RuntimeRep variables: we never quantify over these
1037 zonk_quant default_kind tkv
1038 | not (isTyVar tkv)
1039 = return Nothing -- this can happen for a covar that's associated with
1040 -- a coercion hole. Test case: typecheck/should_compile/T2494
1041
1042 | not (isTcTyVar tkv)
1043 = return (Just tkv) -- For associated types, we have the class variables
1044 -- in scope, and they are TyVars not TcTyVars
1045 | otherwise
1046 = do { deflt_done <- defaultTyVar default_kind tkv
1047 ; case deflt_done of
1048 True -> return Nothing
1049 False -> do { tv <- zonkQuantifiedTyVar tkv
1050 ; return (Just tv) } }
1051
1052 zonkQuantifiedTyVar :: TcTyVar -> TcM TcTyVar
1053 -- The quantified type variables often include meta type variables
1054 -- we want to freeze them into ordinary type variables
1055 -- The meta tyvar is updated to point to the new skolem TyVar. Now any
1056 -- bound occurrences of the original type variable will get zonked to
1057 -- the immutable version.
1058 --
1059 -- We leave skolem TyVars alone; they are immutable.
1060 --
1061 -- This function is called on both kind and type variables,
1062 -- but kind variables *only* if PolyKinds is on.
1063
1064 zonkQuantifiedTyVar tv
1065 = case tcTyVarDetails tv of
1066 SkolemTv {} -> do { kind <- zonkTcType (tyVarKind tv)
1067 ; return (setTyVarKind tv kind) }
1068 -- It might be a skolem type variable,
1069 -- for example from a user type signature
1070
1071 MetaTv {} -> skolemiseUnboundMetaTyVar tv
1072
1073 _other -> pprPanic "zonkQuantifiedTyVar" (ppr tv) -- RuntimeUnk
1074
1075 defaultTyVar :: Bool -- True <=> please default this kind variable to *
1076 -> TcTyVar -- If it's a MetaTyVar then it is unbound
1077 -> TcM Bool -- True <=> defaulted away altogether
1078
1079 defaultTyVar default_kind tv
1080 | not (isMetaTyVar tv)
1081 = return False
1082
1083 | isSigTyVar tv
1084 -- Do not default SigTvs. Doing so would violate the invariants
1085 -- on SigTvs; see Note [Signature skolems] in TcType.
1086 -- Trac #13343 is an example; #14555 is another
1087 -- See Note [Kind generalisation and SigTvs]
1088 = return False
1089
1090
1091 | isRuntimeRepVar tv -- Do not quantify over a RuntimeRep var
1092 -- unless it is a SigTv, handled earlier
1093 = do { traceTc "Defaulting a RuntimeRep var to LiftedRep" (ppr tv)
1094 ; writeMetaTyVar tv liftedRepTy
1095 ; return True }
1096
1097 | default_kind -- -XNoPolyKinds and this is a kind var
1098 = do { default_kind_var tv -- so default it to * if possible
1099 ; return True }
1100
1101 | otherwise
1102 = return False
1103
1104 where
1105 default_kind_var :: TyVar -> TcM ()
1106 -- defaultKindVar is used exclusively with -XNoPolyKinds
1107 -- See Note [Defaulting with -XNoPolyKinds]
1108 -- It takes an (unconstrained) meta tyvar and defaults it.
1109 -- Works only on vars of type *; for other kinds, it issues an error.
1110 default_kind_var kv
1111 | isLiftedTypeKind (tyVarKind kv)
1112 = do { traceTc "Defaulting a kind var to *" (ppr kv)
1113 ; writeMetaTyVar kv liftedTypeKind }
1114 | otherwise
1115 = addErr (vcat [ text "Cannot default kind variable" <+> quotes (ppr kv')
1116 , text "of kind:" <+> ppr (tyVarKind kv')
1117 , text "Perhaps enable PolyKinds or add a kind signature" ])
1118 where
1119 (_, kv') = tidyOpenTyCoVar emptyTidyEnv kv
1120
1121 skolemiseRuntimeUnk :: TcTyVar -> TcM TyVar
1122 skolemiseRuntimeUnk tv
1123 = skolemise_tv tv RuntimeUnk
1124
1125 skolemiseUnboundMetaTyVar :: TcTyVar -> TcM TyVar
1126 skolemiseUnboundMetaTyVar tv
1127 = skolemise_tv tv (SkolemTv (metaTyVarTcLevel tv) False)
1128
1129 skolemise_tv :: TcTyVar -> TcTyVarDetails -> TcM TyVar
1130 -- We have a Meta tyvar with a ref-cell inside it
1131 -- Skolemise it, so that
1132 -- we are totally out of Meta-tyvar-land
1133 -- We create a skolem TyVar, not a regular TyVar
1134 -- See Note [Zonking to Skolem]
1135 skolemise_tv tv details
1136 = ASSERT2( isMetaTyVar tv, ppr tv )
1137 do { when debugIsOn (check_empty tv)
1138 ; span <- getSrcSpanM -- Get the location from "here"
1139 -- ie where we are generalising
1140 ; kind <- zonkTcType (tyVarKind tv)
1141 ; let uniq = getUnique tv
1142 -- NB: Use same Unique as original tyvar. This is
1143 -- important for TcHsType.splitTelescopeTvs to work properly
1144
1145 tv_name = getOccName tv
1146 final_name = mkInternalName uniq tv_name span
1147 final_tv = mkTcTyVar final_name kind details
1148
1149 ; traceTc "Skolemising" (ppr tv <+> text ":=" <+> ppr final_tv)
1150 ; writeMetaTyVar tv (mkTyVarTy final_tv)
1151 ; return final_tv }
1152
1153 where
1154 check_empty tv -- [Sept 04] Check for non-empty.
1155 = when debugIsOn $ -- See note [Silly Type Synonym]
1156 do { cts <- readMetaTyVar tv
1157 ; case cts of
1158 Flexi -> return ()
1159 Indirect ty -> WARN( True, ppr tv $$ ppr ty )
1160 return () }
1161
1162 {- Note [Defaulting with -XNoPolyKinds]
1163 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1164 Consider
1165
1166 data Compose f g a = Mk (f (g a))
1167
1168 We infer
1169
1170 Compose :: forall k1 k2. (k2 -> *) -> (k1 -> k2) -> k1 -> *
1171 Mk :: forall k1 k2 (f :: k2 -> *) (g :: k1 -> k2) (a :: k1).
1172 f (g a) -> Compose k1 k2 f g a
1173
1174 Now, in another module, we have -XNoPolyKinds -XDataKinds in effect.
1175 What does 'Mk mean? Pre GHC-8.0 with -XNoPolyKinds,
1176 we just defaulted all kind variables to *. But that's no good here,
1177 because the kind variables in 'Mk aren't of kind *, so defaulting to *
1178 is ill-kinded.
1179
1180 After some debate on #11334, we decided to issue an error in this case.
1181 The code is in defaultKindVar.
1182
1183 Note [What is a meta variable?]
1184 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1185 A "meta type-variable", also know as a "unification variable" is a placeholder
1186 introduced by the typechecker for an as-yet-unknown monotype.
1187
1188 For example, when we see a call `reverse (f xs)`, we know that we calling
1189 reverse :: forall a. [a] -> [a]
1190 So we know that the argument `f xs` must be a "list of something". But what is
1191 the "something"? We don't know until we explore the `f xs` a bit more. So we set
1192 out what we do know at the call of `reverse` by instantiate its type with a fresh
1193 meta tyvar, `alpha` say. So now the type of the argument `f xs`, and of the
1194 result, is `[alpha]`. The unification variable `alpha` stands for the
1195 as-yet-unknown type of the elements of the list.
1196
1197 As type inference progresses we may learn more about `alpha`. For example, suppose
1198 `f` has the type
1199 f :: forall b. b -> [Maybe b]
1200 Then we instantiate `f`'s type with another fresh unification variable, say
1201 `beta`; and equate `f`'s result type with reverse's argument type, thus
1202 `[alpha] ~ [Maybe beta]`.
1203
1204 Now we can solve this equality to learn that `alpha ~ Maybe beta`, so we've
1205 refined our knowledge about `alpha`. And so on.
1206
1207 If you found this Note useful, you may also want to have a look at
1208 Section 5 of "Practical type inference for higher rank types" (Peyton Jones,
1209 Vytiniotis, Weirich and Shields. J. Functional Programming. 2011).
1210
1211 Note [What is zonking?]
1212 ~~~~~~~~~~~~~~~~~~~~~~~
1213 GHC relies heavily on mutability in the typechecker for efficient operation.
1214 For this reason, throughout much of the type checking process meta type
1215 variables (the MetaTv constructor of TcTyVarDetails) are represented by mutable
1216 variables (known as TcRefs).
1217
1218 Zonking is the process of ripping out these mutable variables and replacing them
1219 with a real Type. This involves traversing the entire type expression, but the
1220 interesting part of replacing the mutable variables occurs in zonkTyVarOcc.
1221
1222 There are two ways to zonk a Type:
1223
1224 * zonkTcTypeToType, which is intended to be used at the end of type-checking
1225 for the final zonk. It has to deal with unfilled metavars, either by filling
1226 it with a value like Any or failing (determined by the UnboundTyVarZonker
1227 used).
1228
1229 * zonkTcType, which will happily ignore unfilled metavars. This is the
1230 appropriate function to use while in the middle of type-checking.
1231
1232 Note [Zonking to Skolem]
1233 ~~~~~~~~~~~~~~~~~~~~~~~~
1234 We used to zonk quantified type variables to regular TyVars. However, this
1235 leads to problems. Consider this program from the regression test suite:
1236
1237 eval :: Int -> String -> String -> String
1238 eval 0 root actual = evalRHS 0 root actual
1239
1240 evalRHS :: Int -> a
1241 evalRHS 0 root actual = eval 0 root actual
1242
1243 It leads to the deferral of an equality (wrapped in an implication constraint)
1244
1245 forall a. () => ((String -> String -> String) ~ a)
1246
1247 which is propagated up to the toplevel (see TcSimplify.tcSimplifyInferCheck).
1248 In the meantime `a' is zonked and quantified to form `evalRHS's signature.
1249 This has the *side effect* of also zonking the `a' in the deferred equality
1250 (which at this point is being handed around wrapped in an implication
1251 constraint).
1252
1253 Finally, the equality (with the zonked `a') will be handed back to the
1254 simplifier by TcRnDriver.tcRnSrcDecls calling TcSimplify.tcSimplifyTop.
1255 If we zonk `a' with a regular type variable, we will have this regular type
1256 variable now floating around in the simplifier, which in many places assumes to
1257 only see proper TcTyVars.
1258
1259 We can avoid this problem by zonking with a skolem. The skolem is rigid
1260 (which we require for a quantified variable), but is still a TcTyVar that the
1261 simplifier knows how to deal with.
1262
1263 Note [Silly Type Synonyms]
1264 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1265 Consider this:
1266 type C u a = u -- Note 'a' unused
1267
1268 foo :: (forall a. C u a -> C u a) -> u
1269 foo x = ...
1270
1271 bar :: Num u => u
1272 bar = foo (\t -> t + t)
1273
1274 * From the (\t -> t+t) we get type {Num d} => d -> d
1275 where d is fresh.
1276
1277 * Now unify with type of foo's arg, and we get:
1278 {Num (C d a)} => C d a -> C d a
1279 where a is fresh.
1280
1281 * Now abstract over the 'a', but float out the Num (C d a) constraint
1282 because it does not 'really' mention a. (see exactTyVarsOfType)
1283 The arg to foo becomes
1284 \/\a -> \t -> t+t
1285
1286 * So we get a dict binding for Num (C d a), which is zonked to give
1287 a = ()
1288 [Note Sept 04: now that we are zonking quantified type variables
1289 on construction, the 'a' will be frozen as a regular tyvar on
1290 quantification, so the floated dict will still have type (C d a).
1291 Which renders this whole note moot; happily!]
1292
1293 * Then the \/\a abstraction has a zonked 'a' in it.
1294
1295 All very silly. I think its harmless to ignore the problem. We'll end up with
1296 a \/\a in the final result but all the occurrences of a will be zonked to ()
1297
1298 ************************************************************************
1299 * *
1300 Zonking types
1301 * *
1302 ************************************************************************
1303
1304 -}
1305
1306 -- | @tcGetGlobalTyCoVars@ returns a fully-zonked set of *scoped* tyvars free in
1307 -- the environment. To improve subsequent calls to the same function it writes
1308 -- the zonked set back into the environment. Note that this returns all
1309 -- variables free in anything (term-level or type-level) in scope. We thus
1310 -- don't have to worry about clashes with things that are not in scope, because
1311 -- if they are reachable, then they'll be returned here.
1312 tcGetGlobalTyCoVars :: TcM TcTyVarSet
1313 tcGetGlobalTyCoVars
1314 = do { (TcLclEnv {tcl_tyvars = gtv_var}) <- getLclEnv
1315 ; gbl_tvs <- readMutVar gtv_var
1316 ; gbl_tvs' <- zonkTyCoVarsAndFV gbl_tvs
1317 ; writeMutVar gtv_var gbl_tvs'
1318 ; return gbl_tvs' }
1319
1320 -- | Zonk a type without using the smart constructors; the result type
1321 -- is available for inspection within the type-checking knot.
1322 zonkTcTypeInKnot :: TcType -> TcM TcType
1323 zonkTcTypeInKnot = mapType (zonkTcTypeMapper { tcm_smart = False }) ()
1324
1325 zonkTcTypeAndFV :: TcType -> TcM DTyCoVarSet
1326 -- Zonk a type and take its free variables
1327 -- With kind polymorphism it can be essential to zonk *first*
1328 -- so that we find the right set of free variables. Eg
1329 -- forall k1. forall (a:k2). a
1330 -- where k2:=k1 is in the substitution. We don't want
1331 -- k2 to look free in this type!
1332 -- NB: This might be called from within the knot, so don't use
1333 -- smart constructors. See Note [Type-checking inside the knot] in TcHsType
1334 zonkTcTypeAndFV ty
1335 = tyCoVarsOfTypeDSet <$> zonkTcTypeInKnot ty
1336
1337 -- | Zonk a type and call 'candidateQTyVarsOfType' on it.
1338 -- Works within the knot.
1339 zonkTcTypeAndSplitDepVars :: TcType -> TcM CandidatesQTvs
1340 zonkTcTypeAndSplitDepVars ty
1341 = candidateQTyVarsOfType <$> zonkTcTypeInKnot ty
1342
1343 zonkTcTypesAndSplitDepVars :: [TcType] -> TcM CandidatesQTvs
1344 zonkTcTypesAndSplitDepVars tys
1345 = candidateQTyVarsOfTypes <$> mapM zonkTcTypeInKnot tys
1346
1347 zonkTyCoVar :: TyCoVar -> TcM TcType
1348 -- Works on TyVars and TcTyVars
1349 zonkTyCoVar tv | isTcTyVar tv = zonkTcTyVar tv
1350 | isTyVar tv = mkTyVarTy <$> zonkTyCoVarKind tv
1351 | otherwise = ASSERT2( isCoVar tv, ppr tv )
1352 mkCoercionTy . mkCoVarCo <$> zonkTyCoVarKind tv
1353 -- Hackily, when typechecking type and class decls
1354 -- we have TyVars in scopeadded (only) in
1355 -- TcHsType.tcTyClTyVars, but it seems
1356 -- painful to make them into TcTyVars there
1357
1358 zonkTyCoVarsAndFV :: TyCoVarSet -> TcM TyCoVarSet
1359 zonkTyCoVarsAndFV tycovars =
1360 tyCoVarsOfTypes <$> mapM zonkTyCoVar (nonDetEltsUniqSet tycovars)
1361 -- It's OK to use nonDetEltsUniqSet here because we immediately forget about
1362 -- the ordering by turning it into a nondeterministic set and the order
1363 -- of zonking doesn't matter for determinism.
1364
1365 -- Takes a list of TyCoVars, zonks them and returns a
1366 -- deterministically ordered list of their free variables.
1367 zonkTyCoVarsAndFVList :: [TyCoVar] -> TcM [TyCoVar]
1368 zonkTyCoVarsAndFVList tycovars =
1369 tyCoVarsOfTypesList <$> mapM zonkTyCoVar tycovars
1370
1371 zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
1372 zonkTcTyVars tyvars = mapM zonkTcTyVar tyvars
1373
1374 ----------------- Types
1375 zonkTyCoVarKind :: TyCoVar -> TcM TyCoVar
1376 zonkTyCoVarKind tv = do { kind' <- zonkTcType (tyVarKind tv)
1377 ; return (setTyVarKind tv kind') }
1378
1379 zonkTcTypes :: [TcType] -> TcM [TcType]
1380 zonkTcTypes tys = mapM zonkTcType tys
1381
1382 {-
1383 ************************************************************************
1384 * *
1385 Zonking constraints
1386 * *
1387 ************************************************************************
1388 -}
1389
1390 zonkImplication :: Implication -> TcM Implication
1391 zonkImplication implic@(Implic { ic_skols = skols
1392 , ic_given = given
1393 , ic_wanted = wanted
1394 , ic_info = info })
1395 = do { skols' <- mapM zonkTcTyCoVarBndr skols -- Need to zonk their kinds!
1396 -- as Trac #7230 showed
1397 ; given' <- mapM zonkEvVar given
1398 ; info' <- zonkSkolemInfo info
1399 ; wanted' <- zonkWCRec wanted
1400 ; return (implic { ic_skols = skols'
1401 , ic_given = given'
1402 , ic_wanted = wanted'
1403 , ic_info = info' }) }
1404
1405 zonkEvVar :: EvVar -> TcM EvVar
1406 zonkEvVar var = do { ty' <- zonkTcType (varType var)
1407 ; return (setVarType var ty') }
1408
1409
1410 zonkWC :: WantedConstraints -> TcM WantedConstraints
1411 zonkWC wc = zonkWCRec wc
1412
1413 zonkWCRec :: WantedConstraints -> TcM WantedConstraints
1414 zonkWCRec (WC { wc_simple = simple, wc_impl = implic })
1415 = do { simple' <- zonkSimples simple
1416 ; implic' <- mapBagM zonkImplication implic
1417 ; return (WC { wc_simple = simple', wc_impl = implic' }) }
1418
1419 zonkSimples :: Cts -> TcM Cts
1420 zonkSimples cts = do { cts' <- mapBagM zonkCt' cts
1421 ; traceTc "zonkSimples done:" (ppr cts')
1422 ; return cts' }
1423
1424 zonkCt' :: Ct -> TcM Ct
1425 zonkCt' ct = zonkCt ct
1426
1427 {- Note [zonkCt behaviour]
1428 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1429 zonkCt tries to maintain the canonical form of a Ct. For example,
1430 - a CDictCan should stay a CDictCan;
1431 - a CTyEqCan should stay a CTyEqCan (if the LHS stays as a variable.).
1432 - a CHoleCan should stay a CHoleCan
1433 - a CIrredCan should stay a CIrredCan with its cc_insol flag intact
1434
1435 Why?, for example:
1436 - For CDictCan, the @TcSimplify.expandSuperClasses@ step, which runs after the
1437 simple wanted and plugin loop, looks for @CDictCan@s. If a plugin is in use,
1438 constraints are zonked before being passed to the plugin. This means if we
1439 don't preserve a canonical form, @expandSuperClasses@ fails to expand
1440 superclasses. This is what happened in Trac #11525.
1441
1442 - For CHoleCan, once we forget that it's a hole, we can never recover that info.
1443
1444 - For CIrredCan we want to see if a constraint is insoluble with insolubleWC
1445
1446 NB: we do not expect to see any CFunEqCans, because zonkCt is only
1447 called on unflattened constraints.
1448
1449 NB: Constraints are always re-flattened etc by the canonicaliser in
1450 @TcCanonical@ even if they come in as CDictCan. Only canonical constraints that
1451 are actually in the inert set carry all the guarantees. So it is okay if zonkCt
1452 creates e.g. a CDictCan where the cc_tyars are /not/ function free.
1453 -}
1454
1455 zonkCt :: Ct -> TcM Ct
1456 zonkCt ct@(CHoleCan { cc_ev = ev })
1457 = do { ev' <- zonkCtEvidence ev
1458 ; return $ ct { cc_ev = ev' } }
1459
1460 zonkCt ct@(CDictCan { cc_ev = ev, cc_tyargs = args })
1461 = do { ev' <- zonkCtEvidence ev
1462 ; args' <- mapM zonkTcType args
1463 ; return $ ct { cc_ev = ev', cc_tyargs = args' } }
1464
1465 zonkCt ct@(CTyEqCan { cc_ev = ev, cc_tyvar = tv, cc_rhs = rhs })
1466 = do { ev' <- zonkCtEvidence ev
1467 ; tv_ty' <- zonkTcTyVar tv
1468 ; case getTyVar_maybe tv_ty' of
1469 Just tv' -> do { rhs' <- zonkTcType rhs
1470 ; return ct { cc_ev = ev'
1471 , cc_tyvar = tv'
1472 , cc_rhs = rhs' } }
1473 Nothing -> return (mkNonCanonical ev') }
1474
1475 zonkCt ct@(CIrredCan { cc_ev = ev }) -- Preserve the cc_insol flag
1476 = do { ev' <- zonkCtEvidence ev
1477 ; return (ct { cc_ev = ev' }) }
1478
1479 zonkCt ct
1480 = ASSERT( not (isCFunEqCan ct) )
1481 -- We do not expect to see any CFunEqCans, because zonkCt is only called on
1482 -- unflattened constraints.
1483 do { fl' <- zonkCtEvidence (ctEvidence ct)
1484 ; return (mkNonCanonical fl') }
1485
1486 zonkCtEvidence :: CtEvidence -> TcM CtEvidence
1487 zonkCtEvidence ctev@(CtGiven { ctev_pred = pred })
1488 = do { pred' <- zonkTcType pred
1489 ; return (ctev { ctev_pred = pred'}) }
1490 zonkCtEvidence ctev@(CtWanted { ctev_pred = pred, ctev_dest = dest })
1491 = do { pred' <- zonkTcType pred
1492 ; let dest' = case dest of
1493 EvVarDest ev -> EvVarDest $ setVarType ev pred'
1494 -- necessary in simplifyInfer
1495 HoleDest h -> HoleDest h
1496 ; return (ctev { ctev_pred = pred', ctev_dest = dest' }) }
1497 zonkCtEvidence ctev@(CtDerived { ctev_pred = pred })
1498 = do { pred' <- zonkTcType pred
1499 ; return (ctev { ctev_pred = pred' }) }
1500
1501 zonkSkolemInfo :: SkolemInfo -> TcM SkolemInfo
1502 zonkSkolemInfo (SigSkol cx ty tv_prs) = do { ty' <- zonkTcType ty
1503 ; return (SigSkol cx ty' tv_prs) }
1504 zonkSkolemInfo (InferSkol ntys) = do { ntys' <- mapM do_one ntys
1505 ; return (InferSkol ntys') }
1506 where
1507 do_one (n, ty) = do { ty' <- zonkTcType ty; return (n, ty') }
1508 zonkSkolemInfo skol_info = return skol_info
1509
1510 {-
1511 %************************************************************************
1512 %* *
1513 \subsection{Zonking -- the main work-horses: zonkTcType, zonkTcTyVar}
1514 * *
1515 * For internal use only! *
1516 * *
1517 ************************************************************************
1518
1519 -}
1520
1521 -- zonkId is used *during* typechecking just to zonk the Id's type
1522 zonkId :: TcId -> TcM TcId
1523 zonkId id
1524 = do { ty' <- zonkTcType (idType id)
1525 ; return (Id.setIdType id ty') }
1526
1527 zonkCoVar :: CoVar -> TcM CoVar
1528 zonkCoVar = zonkId
1529
1530 -- | A suitable TyCoMapper for zonking a type inside the knot, and
1531 -- before all metavars are filled in.
1532 zonkTcTypeMapper :: TyCoMapper () TcM
1533 zonkTcTypeMapper = TyCoMapper
1534 { tcm_smart = True
1535 , tcm_tyvar = const zonkTcTyVar
1536 , tcm_covar = const (\cv -> mkCoVarCo <$> zonkTyCoVarKind cv)
1537 , tcm_hole = hole
1538 , tcm_tybinder = \_env tv _vis -> ((), ) <$> zonkTcTyCoVarBndr tv }
1539 where
1540 hole :: () -> CoercionHole -> TcM Coercion
1541 hole _ hole@(CoercionHole { ch_ref = ref, ch_co_var = cv })
1542 = do { contents <- readTcRef ref
1543 ; case contents of
1544 Just co -> do { co' <- zonkCo co
1545 ; checkCoercionHole cv co' }
1546 Nothing -> do { cv' <- zonkCoVar cv
1547 ; return $ HoleCo (hole { ch_co_var = cv' }) } }
1548
1549
1550 -- For unbound, mutable tyvars, zonkType uses the function given to it
1551 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
1552 -- type variable and zonks the kind too
1553 zonkTcType :: TcType -> TcM TcType
1554 zonkTcType = mapType zonkTcTypeMapper ()
1555
1556 -- | "Zonk" a coercion -- really, just zonk any types in the coercion
1557 zonkCo :: Coercion -> TcM Coercion
1558 zonkCo = mapCoercion zonkTcTypeMapper ()
1559
1560 zonkTcTyCoVarBndr :: TcTyCoVar -> TcM TcTyCoVar
1561 -- A tyvar binder is never a unification variable (TauTv),
1562 -- rather it is always a skolem. It *might* be a SigTv.
1563 -- (Because non-CUSK type declarations use SigTvs.)
1564 -- Regardless, it may have a kind
1565 -- that has not yet been zonked, and may include kind
1566 -- unification variables.
1567 zonkTcTyCoVarBndr tyvar
1568 | isSigTyVar tyvar
1569 = tcGetTyVar "zonkTcTyCoVarBndr SigTv" <$> zonkTcTyVar tyvar
1570
1571 | otherwise
1572 -- can't use isCoVar, because it looks at a TyCon. Argh.
1573 = ASSERT2( isImmutableTyVar tyvar || (not $ isTyVar tyvar), pprTyVar tyvar )
1574 updateTyVarKindM zonkTcType tyvar
1575
1576 zonkTcTyVarBinder :: TyVarBndr TcTyVar vis -> TcM (TyVarBndr TcTyVar vis)
1577 zonkTcTyVarBinder (TvBndr tv vis)
1578 = do { tv' <- zonkTcTyCoVarBndr tv
1579 ; return (TvBndr tv' vis) }
1580
1581 zonkTcTyVar :: TcTyVar -> TcM TcType
1582 -- Simply look through all Flexis
1583 zonkTcTyVar tv
1584 | isTcTyVar tv
1585 = case tcTyVarDetails tv of
1586 SkolemTv {} -> zonk_kind_and_return
1587 RuntimeUnk {} -> zonk_kind_and_return
1588 MetaTv { mtv_ref = ref }
1589 -> do { cts <- readMutVar ref
1590 ; case cts of
1591 Flexi -> zonk_kind_and_return
1592 Indirect ty -> zonkTcType ty }
1593
1594 | otherwise -- coercion variable
1595 = zonk_kind_and_return
1596 where
1597 zonk_kind_and_return = do { z_tv <- zonkTyCoVarKind tv
1598 ; return (mkTyVarTy z_tv) }
1599
1600 -- Variant that assumes that any result of zonking is still a TyVar.
1601 -- Should be used only on skolems and SigTvs
1602 zonkTcTyVarToTyVar :: HasDebugCallStack => TcTyVar -> TcM TcTyVar
1603 zonkTcTyVarToTyVar tv
1604 = do { ty <- zonkTcTyVar tv
1605 ; let tv' = case tcGetTyVar_maybe ty of
1606 Just tv' -> tv'
1607 Nothing -> pprPanic "zonkTcTyVarToTyVar"
1608 (ppr tv $$ ppr ty)
1609 ; return tv' }
1610
1611 zonkSigTyVarPairs :: [(Name,TcTyVar)] -> TcM [(Name,TcTyVar)]
1612 zonkSigTyVarPairs prs
1613 = mapM do_one prs
1614 where
1615 do_one (nm, tv) = do { tv' <- zonkTcTyVarToTyVar tv
1616 ; return (nm, tv') }
1617
1618 {-
1619 %************************************************************************
1620 %* *
1621 Tidying
1622 * *
1623 ************************************************************************
1624 -}
1625
1626 zonkTidyTcType :: TidyEnv -> TcType -> TcM (TidyEnv, TcType)
1627 zonkTidyTcType env ty = do { ty' <- zonkTcType ty
1628 ; return (tidyOpenType env ty') }
1629
1630 zonkTidyTcTypes :: TidyEnv -> [TcType] -> TcM (TidyEnv, [TcType])
1631 zonkTidyTcTypes = zonkTidyTcTypes' []
1632 where zonkTidyTcTypes' zs env [] = return (env, reverse zs)
1633 zonkTidyTcTypes' zs env (ty:tys)
1634 = do { (env', ty') <- zonkTidyTcType env ty
1635 ; zonkTidyTcTypes' (ty':zs) env' tys }
1636
1637 zonkTidyOrigin :: TidyEnv -> CtOrigin -> TcM (TidyEnv, CtOrigin)
1638 zonkTidyOrigin env (GivenOrigin skol_info)
1639 = do { skol_info1 <- zonkSkolemInfo skol_info
1640 ; let skol_info2 = tidySkolemInfo env skol_info1
1641 ; return (env, GivenOrigin skol_info2) }
1642 zonkTidyOrigin env orig@(TypeEqOrigin { uo_actual = act
1643 , uo_expected = exp })
1644 = do { (env1, act') <- zonkTidyTcType env act
1645 ; (env2, exp') <- zonkTidyTcType env1 exp
1646 ; return ( env2, orig { uo_actual = act'
1647 , uo_expected = exp' }) }
1648 zonkTidyOrigin env (KindEqOrigin ty1 m_ty2 orig t_or_k)
1649 = do { (env1, ty1') <- zonkTidyTcType env ty1
1650 ; (env2, m_ty2') <- case m_ty2 of
1651 Just ty2 -> second Just <$> zonkTidyTcType env1 ty2
1652 Nothing -> return (env1, Nothing)
1653 ; (env3, orig') <- zonkTidyOrigin env2 orig
1654 ; return (env3, KindEqOrigin ty1' m_ty2' orig' t_or_k) }
1655 zonkTidyOrigin env (FunDepOrigin1 p1 l1 p2 l2)
1656 = do { (env1, p1') <- zonkTidyTcType env p1
1657 ; (env2, p2') <- zonkTidyTcType env1 p2
1658 ; return (env2, FunDepOrigin1 p1' l1 p2' l2) }
1659 zonkTidyOrigin env (FunDepOrigin2 p1 o1 p2 l2)
1660 = do { (env1, p1') <- zonkTidyTcType env p1
1661 ; (env2, p2') <- zonkTidyTcType env1 p2
1662 ; (env3, o1') <- zonkTidyOrigin env2 o1
1663 ; return (env3, FunDepOrigin2 p1' o1' p2' l2) }
1664 zonkTidyOrigin env orig = return (env, orig)
1665
1666 ----------------
1667 tidyCt :: TidyEnv -> Ct -> Ct
1668 -- Used only in error reporting
1669 -- Also converts it to non-canonical
1670 tidyCt env ct
1671 = case ct of
1672 CHoleCan { cc_ev = ev }
1673 -> ct { cc_ev = tidy_ev env ev }
1674 _ -> mkNonCanonical (tidy_ev env (ctEvidence ct))
1675 where
1676 tidy_ev :: TidyEnv -> CtEvidence -> CtEvidence
1677 -- NB: we do not tidy the ctev_evar field because we don't
1678 -- show it in error messages
1679 tidy_ev env ctev@(CtGiven { ctev_pred = pred })
1680 = ctev { ctev_pred = tidyType env pred }
1681 tidy_ev env ctev@(CtWanted { ctev_pred = pred })
1682 = ctev { ctev_pred = tidyType env pred }
1683 tidy_ev env ctev@(CtDerived { ctev_pred = pred })
1684 = ctev { ctev_pred = tidyType env pred }
1685
1686 ----------------
1687 tidyEvVar :: TidyEnv -> EvVar -> EvVar
1688 tidyEvVar env var = setVarType var (tidyType env (varType var))
1689
1690 ----------------
1691 tidySkolemInfo :: TidyEnv -> SkolemInfo -> SkolemInfo
1692 tidySkolemInfo env (DerivSkol ty) = DerivSkol (tidyType env ty)
1693 tidySkolemInfo env (SigSkol cx ty tv_prs) = tidySigSkol env cx ty tv_prs
1694 tidySkolemInfo env (InferSkol ids) = InferSkol (mapSnd (tidyType env) ids)
1695 tidySkolemInfo env (UnifyForAllSkol ty) = UnifyForAllSkol (tidyType env ty)
1696 tidySkolemInfo _ info = info
1697
1698 tidySigSkol :: TidyEnv -> UserTypeCtxt
1699 -> TcType -> [(Name,TcTyVar)] -> SkolemInfo
1700 -- We need to take special care when tidying SigSkol
1701 -- See Note [SigSkol SkolemInfo] in TcRnTypes
1702 tidySigSkol env cx ty tv_prs
1703 = SigSkol cx (tidy_ty env ty) tv_prs'
1704 where
1705 tv_prs' = mapSnd (tidyTyVarOcc env) tv_prs
1706 inst_env = mkNameEnv tv_prs'
1707
1708 tidy_ty env (ForAllTy (TvBndr tv vis) ty)
1709 = ForAllTy (TvBndr tv' vis) (tidy_ty env' ty)
1710 where
1711 (env', tv') = tidy_tv_bndr env tv
1712
1713 tidy_ty env (FunTy arg res)
1714 = FunTy (tidyType env arg) (tidy_ty env res)
1715
1716 tidy_ty env ty = tidyType env ty
1717
1718 tidy_tv_bndr :: TidyEnv -> TyVar -> (TidyEnv, TyVar)
1719 tidy_tv_bndr env@(occ_env, subst) tv
1720 | Just tv' <- lookupNameEnv inst_env (tyVarName tv)
1721 = ((occ_env, extendVarEnv subst tv tv'), tv')
1722
1723 | otherwise
1724 = tidyTyCoVarBndr env tv
1725
1726 -------------------------------------------------------------------------
1727 {-
1728 %************************************************************************
1729 %* *
1730 Levity polymorphism checks
1731 * *
1732 ************************************************************************
1733
1734 See Note [Levity polymorphism checking] in DsMonad
1735
1736 -}
1737
1738 -- | According to the rules around representation polymorphism
1739 -- (see https://ghc.haskell.org/trac/ghc/wiki/NoSubKinds), no binder
1740 -- can have a representation-polymorphic type. This check ensures
1741 -- that we respect this rule. It is a bit regrettable that this error
1742 -- occurs in zonking, after which we should have reported all errors.
1743 -- But it's hard to see where else to do it, because this can be discovered
1744 -- only after all solving is done. And, perhaps most importantly, this
1745 -- isn't really a compositional property of a type system, so it's
1746 -- not a terrible surprise that the check has to go in an awkward spot.
1747 ensureNotLevPoly :: Type -- its zonked type
1748 -> SDoc -- where this happened
1749 -> TcM ()
1750 ensureNotLevPoly ty doc
1751 = whenNoErrs $ -- sometimes we end up zonking bogus definitions of type
1752 -- forall a. a. See, for example, test ghci/scripts/T9140
1753 checkForLevPoly doc ty
1754
1755 -- See Note [Levity polymorphism checking] in DsMonad
1756 checkForLevPoly :: SDoc -> Type -> TcM ()
1757 checkForLevPoly = checkForLevPolyX addErr
1758
1759 checkForLevPolyX :: Monad m
1760 => (SDoc -> m ()) -- how to report an error
1761 -> SDoc -> Type -> m ()
1762 checkForLevPolyX add_err extra ty
1763 | isTypeLevPoly ty
1764 = add_err (formatLevPolyErr ty $$ extra)
1765 | otherwise
1766 = return ()
1767
1768 formatLevPolyErr :: Type -- levity-polymorphic type
1769 -> SDoc
1770 formatLevPolyErr ty
1771 = hang (text "A levity-polymorphic type is not allowed here:")
1772 2 (vcat [ text "Type:" <+> pprWithTYPE tidy_ty
1773 , text "Kind:" <+> pprWithTYPE tidy_ki ])
1774 where
1775 (tidy_env, tidy_ty) = tidyOpenType emptyTidyEnv ty
1776 tidy_ki = tidyType tidy_env (typeKind ty)