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