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