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