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