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