4bf725f35cc0f6124f1ce488412ca0ea3f0ffb4f
[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 #-}
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 newReturnTyVar, newReturnTyVarTy,
23 newMetaKindVar, newMetaKindVars,
24 mkTcTyVarName, cloneMetaTyVar,
25
26 newMetaTyVar, readMetaTyVar, writeMetaTyVar, writeMetaTyVarRef,
27 newMetaDetails, isFilledMetaTyVar, isUnfilledMetaTyVar,
28
29 --------------------------------
30 -- Creating new evidence variables
31 newEvVar, newEvVars, newEq, newDict,
32 newTcEvBinds, addTcEvBind,
33
34 --------------------------------
35 -- Instantiation
36 tcInstTyVars, tcInstTyVarX, newSigTyVar,
37 tcInstType,
38 tcInstSkolTyVars, tcInstSuperSkolTyVarsX,
39 tcInstSigTyVarsLoc, tcInstSigTyVars,
40 tcInstSkolType,
41 tcSkolDFunType, tcSuperSkolTyVars,
42
43 instSkolTyVars, freshenTyVarBndrs,
44
45 --------------------------------
46 -- Zonking and tidying
47 zonkTcPredType, zonkTidyTcType, zonkTidyOrigin,
48 tidyEvVar, tidyCt, tidySkolemInfo,
49 skolemiseUnboundMetaTyVar,
50 zonkTcTyVar, zonkTcTyVars, zonkTyVarsAndFV, zonkTcTypeAndFV,
51 zonkQuantifiedTyVar, quantifyTyVars,
52 zonkTcTyVarBndr, zonkTcType, zonkTcTypes, zonkTcThetaType,
53
54 zonkTcKind, defaultKindVarToStar,
55 zonkEvVar, zonkWC, zonkSimples, zonkId, zonkCt, zonkSkolemInfo,
56
57 tcGetGlobalTyVars,
58
59 --------------------------------
60 -- (Named) Wildcards
61 newWildcardVar, newWildcardVarMetaKind
62 ) where
63
64 #include "HsVersions.h"
65
66 -- friends:
67 import TypeRep
68 import TcType
69 import Type
70 import Kind ( isOpenTypeKind )
71 import Class
72 import Var
73 import VarEnv
74
75 -- others:
76 import TcRnMonad -- TcType, amongst others
77 import Id
78 import Name
79 import VarSet
80 import PrelNames
81 import DynFlags
82 import Util
83 import Outputable
84 import FastString
85 import SrcLoc
86 import Bag
87
88 import Control.Monad
89 import Data.List ( partition, mapAccumL )
90
91 {-
92 ************************************************************************
93 * *
94 Kind variables
95 * *
96 ************************************************************************
97 -}
98
99 mkKindName :: Unique -> Name
100 mkKindName unique = mkSystemName unique kind_var_occ
101
102 kind_var_occ :: OccName -- Just one for all MetaKindVars
103 -- They may be jiggled by tidying
104 kind_var_occ = mkOccName tvName "k"
105
106 newMetaKindVar :: TcM TcKind
107 newMetaKindVar = do { uniq <- newUnique
108 ; details <- newMetaDetails (TauTv VanillaTau)
109 ; let kv = mkTcTyVar (mkKindName uniq) superKind details
110 ; return (mkTyVarTy kv) }
111
112 newMetaKindVars :: Int -> TcM [TcKind]
113 newMetaKindVars n = mapM (\ _ -> newMetaKindVar) (nOfThem n ())
114
115 {-
116 ************************************************************************
117 * *
118 Evidence variables; range over constraints we can abstract over
119 * *
120 ************************************************************************
121 -}
122
123 newEvVars :: TcThetaType -> TcM [EvVar]
124 newEvVars theta = mapM newEvVar theta
125
126 --------------
127
128 newEvVar :: TcPredType -> TcM EvVar
129 -- Creates new *rigid* variables for predicates
130 newEvVar ty = do { name <- newSysName (predTypeOccName ty)
131 ; return (mkLocalId name ty NoSigId) }
132
133 newEq :: TcType -> TcType -> TcM EvVar
134 newEq ty1 ty2
135 = do { name <- newSysName (mkVarOccFS (fsLit "cobox"))
136 ; return (mkLocalId name (mkTcEqPred ty1 ty2) NoSigId) }
137
138 newDict :: Class -> [TcType] -> TcM DictId
139 newDict cls tys
140 = do { name <- newSysName (mkDictOcc (getOccName cls))
141 ; return (mkLocalId name (mkClassPred cls tys) NoSigId) }
142
143 predTypeOccName :: PredType -> OccName
144 predTypeOccName ty = case classifyPredType ty of
145 ClassPred cls _ -> mkDictOcc (getOccName cls)
146 EqPred _ _ _ -> mkVarOccFS (fsLit "cobox")
147 IrredPred _ -> mkVarOccFS (fsLit "irred")
148
149
150 {-
151 ************************************************************************
152 * *
153 SkolemTvs (immutable)
154 * *
155 ************************************************************************
156 -}
157
158 tcInstType :: ([TyVar] -> TcM (TvSubst, [TcTyVar])) -- How to instantiate the type variables
159 -> TcType -- Type to instantiate
160 -> TcM ([TcTyVar], TcThetaType, TcType) -- Result
161 -- (type vars (excl coercion vars), preds (incl equalities), rho)
162 tcInstType inst_tyvars ty
163 = case tcSplitForAllTys ty of
164 ([], rho) -> let -- There may be overloading despite no type variables;
165 -- (?x :: Int) => Int -> Int
166 (theta, tau) = tcSplitPhiTy rho
167 in
168 return ([], theta, tau)
169
170 (tyvars, rho) -> do { (subst, tyvars') <- inst_tyvars tyvars
171 ; let (theta, tau) = tcSplitPhiTy (substTy subst rho)
172 ; return (tyvars', theta, tau) }
173
174 tcSkolDFunType :: Type -> TcM ([TcTyVar], TcThetaType, TcType)
175 -- Instantiate a type signature with skolem constants.
176 -- We could give them fresh names, but no need to do so
177 tcSkolDFunType ty = tcInstType tcInstSuperSkolTyVars ty
178
179 tcSuperSkolTyVars :: [TyVar] -> (TvSubst, [TcTyVar])
180 -- Make skolem constants, but do *not* give them new names, as above
181 -- Moreover, make them "super skolems"; see comments with superSkolemTv
182 -- see Note [Kind substitution when instantiating]
183 -- Precondition: tyvars should be ordered (kind vars first)
184 tcSuperSkolTyVars = mapAccumL tcSuperSkolTyVar (mkTopTvSubst [])
185
186 tcSuperSkolTyVar :: TvSubst -> TyVar -> (TvSubst, TcTyVar)
187 tcSuperSkolTyVar subst tv
188 = (extendTvSubst subst tv (mkTyVarTy new_tv), new_tv)
189 where
190 kind = substTy subst (tyVarKind tv)
191 new_tv = mkTcTyVar (tyVarName tv) kind superSkolemTv
192
193 tcInstSkolTyVars :: [TyVar] -> TcM (TvSubst, [TcTyVar])
194 tcInstSkolTyVars = tcInstSkolTyVars' False emptyTvSubst
195
196 tcInstSuperSkolTyVars :: [TyVar] -> TcM (TvSubst, [TcTyVar])
197 tcInstSuperSkolTyVars = tcInstSuperSkolTyVarsX emptyTvSubst
198
199 tcInstSuperSkolTyVarsX :: TvSubst -> [TyVar] -> TcM (TvSubst, [TcTyVar])
200 tcInstSuperSkolTyVarsX subst = tcInstSkolTyVars' True subst
201
202 tcInstSkolTyVars' :: Bool -> TvSubst -> [TyVar] -> TcM (TvSubst, [TcTyVar])
203 -- Precondition: tyvars should be ordered (kind vars first)
204 -- see Note [Kind substitution when instantiating]
205 -- Get the location from the monad; this is a complete freshening operation
206 tcInstSkolTyVars' overlappable subst tvs
207 = do { loc <- getSrcSpanM
208 ; instSkolTyVarsX (mkTcSkolTyVar loc overlappable) subst tvs }
209
210 mkTcSkolTyVar :: SrcSpan -> Bool -> Unique -> Name -> Kind -> TcTyVar
211 mkTcSkolTyVar loc overlappable uniq old_name kind
212 = mkTcTyVar (mkInternalName uniq (getOccName old_name) loc)
213 kind
214 (SkolemTv overlappable)
215
216 tcInstSigTyVarsLoc :: SrcSpan -> [TyVar] -> TcRnIf gbl lcl (TvSubst, [TcTyVar])
217 -- We specify the location
218 tcInstSigTyVarsLoc loc = instSkolTyVars (mkTcSkolTyVar loc False)
219
220 tcInstSigTyVars :: [TyVar] -> TcRnIf gbl lcl (TvSubst, [TcTyVar])
221 -- Get the location from the TyVar itself, not the monad
222 tcInstSigTyVars
223 = instSkolTyVars mk_tv
224 where
225 mk_tv uniq old_name kind
226 = mkTcTyVar (setNameUnique old_name uniq) kind (SkolemTv False)
227
228 tcInstSkolType :: TcType -> TcM ([TcTyVar], TcThetaType, TcType)
229 -- Instantiate a type with fresh skolem constants
230 -- Binding location comes from the monad
231 tcInstSkolType ty = tcInstType tcInstSkolTyVars ty
232
233 ------------------
234 freshenTyVarBndrs :: [TyVar] -> TcRnIf gbl lcl (TvSubst, [TyVar])
235 -- ^ Give fresh uniques to a bunch of TyVars, but they stay
236 -- as TyVars, rather than becoming TcTyVars
237 -- Used in FamInst.newFamInst, and Inst.newClsInst
238 freshenTyVarBndrs = instSkolTyVars mk_tv
239 where
240 mk_tv uniq old_name kind = mkTyVar (setNameUnique old_name uniq) kind
241
242 ------------------
243 instSkolTyVars :: (Unique -> Name -> Kind -> TyVar)
244 -> [TyVar] -> TcRnIf gbl lcl (TvSubst, [TyVar])
245 instSkolTyVars mk_tv = instSkolTyVarsX mk_tv emptyTvSubst
246
247 instSkolTyVarsX :: (Unique -> Name -> Kind -> TyVar)
248 -> TvSubst -> [TyVar] -> TcRnIf gbl lcl (TvSubst, [TyVar])
249 instSkolTyVarsX mk_tv = mapAccumLM (instSkolTyVarX mk_tv)
250
251 instSkolTyVarX :: (Unique -> Name -> Kind -> TyVar)
252 -> TvSubst -> TyVar -> TcRnIf gbl lcl (TvSubst, TyVar)
253 instSkolTyVarX mk_tv subst tyvar
254 = do { uniq <- newUnique
255 ; let new_tv = mk_tv uniq old_name kind
256 ; return (extendTvSubst subst tyvar (mkTyVarTy new_tv), new_tv) }
257 where
258 old_name = tyVarName tyvar
259 kind = substTy subst (tyVarKind tyvar)
260
261 {-
262 Note [Kind substitution when instantiating]
263 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
264 When we instantiate a bunch of kind and type variables, first we
265 expect them to be sorted (kind variables first, then type variables).
266 Then we have to instantiate the kind variables, build a substitution
267 from old variables to the new variables, then instantiate the type
268 variables substituting the original kind.
269
270 Exemple: If we want to instantiate
271 [(k1 :: BOX), (k2 :: BOX), (a :: k1 -> k2), (b :: k1)]
272 we want
273 [(?k1 :: BOX), (?k2 :: BOX), (?a :: ?k1 -> ?k2), (?b :: ?k1)]
274 instead of the buggous
275 [(?k1 :: BOX), (?k2 :: BOX), (?a :: k1 -> k2), (?b :: k1)]
276
277
278 ************************************************************************
279 * *
280 MetaTvs (meta type variables; mutable)
281 * *
282 ************************************************************************
283 -}
284
285 newMetaTyVar :: MetaInfo -> Kind -> TcM TcTyVar
286 -- Make a new meta tyvar out of thin air
287 newMetaTyVar meta_info kind
288 = do { uniq <- newUnique
289 ; let name = mkTcTyVarName uniq s
290 s = case meta_info of
291 ReturnTv -> fsLit "r"
292 TauTv WildcardTau -> fsLit "w"
293 TauTv VanillaTau -> fsLit "t"
294 FlatMetaTv -> fsLit "fmv"
295 SigTv -> fsLit "a"
296 ; details <- newMetaDetails meta_info
297 ; return (mkTcTyVar name kind details) }
298
299 newNamedMetaTyVar :: Name -> MetaInfo -> Kind -> TcM TcTyVar
300 -- Make a new meta tyvar out of thin air
301 newNamedMetaTyVar name meta_info kind
302 = do { details <- newMetaDetails meta_info
303 ; return (mkTcTyVar name kind details) }
304
305 newSigTyVar :: Name -> Kind -> TcM TcTyVar
306 newSigTyVar name kind
307 = do { uniq <- newUnique
308 ; let name' = setNameUnique name uniq
309 -- Use the same OccName so that the tidy-er
310 -- doesn't gratuitously rename 'a' to 'a0' etc
311 ; details <- newMetaDetails SigTv
312 ; return (mkTcTyVar name' kind details) }
313
314 newMetaDetails :: MetaInfo -> TcM TcTyVarDetails
315 newMetaDetails info
316 = do { ref <- newMutVar Flexi
317 ; tclvl <- getTcLevel
318 ; return (MetaTv { mtv_info = info, mtv_ref = ref, mtv_tclvl = tclvl }) }
319
320 cloneMetaTyVar :: TcTyVar -> TcM TcTyVar
321 cloneMetaTyVar tv
322 = ASSERT( isTcTyVar tv )
323 do { uniq <- newUnique
324 ; ref <- newMutVar Flexi
325 ; let name' = setNameUnique (tyVarName tv) uniq
326 details' = case tcTyVarDetails tv of
327 details@(MetaTv {}) -> details { mtv_ref = ref }
328 _ -> pprPanic "cloneMetaTyVar" (ppr tv)
329 ; return (mkTcTyVar name' (tyVarKind tv) details') }
330
331 mkTcTyVarName :: Unique -> FastString -> Name
332 mkTcTyVarName uniq str = mkSysTvName uniq str
333
334 -- Works for both type and kind variables
335 readMetaTyVar :: TyVar -> TcM MetaDetails
336 readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
337 readMutVar (metaTvRef tyvar)
338
339 isFilledMetaTyVar :: TyVar -> TcM Bool
340 -- True of a filled-in (Indirect) meta type variable
341 isFilledMetaTyVar tv
342 | not (isTcTyVar tv) = return False
343 | MetaTv { mtv_ref = ref } <- tcTyVarDetails tv
344 = do { details <- readMutVar ref
345 ; return (isIndirect details) }
346 | otherwise = return False
347
348 isUnfilledMetaTyVar :: TyVar -> TcM Bool
349 -- True of a un-filled-in (Flexi) meta type variable
350 isUnfilledMetaTyVar tv
351 | not (isTcTyVar tv) = return False
352 | MetaTv { mtv_ref = ref } <- tcTyVarDetails tv
353 = do { details <- readMutVar ref
354 ; return (isFlexi details) }
355 | otherwise = return False
356
357 --------------------
358 -- Works with both type and kind variables
359 writeMetaTyVar :: TcTyVar -> TcType -> TcM ()
360 -- Write into a currently-empty MetaTyVar
361
362 writeMetaTyVar tyvar ty
363 | not debugIsOn
364 = writeMetaTyVarRef tyvar (metaTvRef tyvar) ty
365
366 -- Everything from here on only happens if DEBUG is on
367 | not (isTcTyVar tyvar)
368 = WARN( True, text "Writing to non-tc tyvar" <+> ppr tyvar )
369 return ()
370
371 | MetaTv { mtv_ref = ref } <- tcTyVarDetails tyvar
372 = writeMetaTyVarRef tyvar ref ty
373
374 | otherwise
375 = WARN( True, text "Writing to non-meta tyvar" <+> ppr tyvar )
376 return ()
377
378 --------------------
379 writeMetaTyVarRef :: TcTyVar -> TcRef MetaDetails -> TcType -> TcM ()
380 -- Here the tyvar is for error checking only;
381 -- the ref cell must be for the same tyvar
382 writeMetaTyVarRef tyvar ref ty
383 | not debugIsOn
384 = do { traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty)
385 ; writeMutVar ref (Indirect ty) }
386
387 -- Everything from here on only happens if DEBUG is on
388 | otherwise
389 = do { meta_details <- readMutVar ref;
390 -- Zonk kinds to allow the error check to work
391 ; zonked_tv_kind <- zonkTcKind tv_kind
392 ; zonked_ty_kind <- zonkTcKind ty_kind
393
394 -- Check for double updates
395 ; ASSERT2( isFlexi meta_details,
396 hang (text "Double update of meta tyvar")
397 2 (ppr tyvar $$ ppr meta_details) )
398
399 traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty)
400 ; writeMutVar ref (Indirect ty)
401 ; when ( not (isPredTy tv_kind)
402 -- Don't check kinds for updates to coercion variables
403 && not (zonked_ty_kind `tcIsSubKind` zonked_tv_kind))
404 $ WARN( True, hang (text "Ill-kinded update to meta tyvar")
405 2 ( ppr tyvar <+> text "::" <+> (ppr tv_kind $$ ppr zonked_tv_kind)
406 <+> text ":="
407 <+> ppr ty <+> text "::" <+> (ppr ty_kind $$ ppr zonked_ty_kind) ) )
408 (return ()) }
409 where
410 tv_kind = tyVarKind tyvar
411 ty_kind = typeKind ty
412
413 {-
414 ************************************************************************
415 * *
416 MetaTvs: TauTvs
417 * *
418 ************************************************************************
419 -}
420
421 newFlexiTyVar :: Kind -> TcM TcTyVar
422 newFlexiTyVar kind = newMetaTyVar (TauTv VanillaTau) kind
423
424 newFlexiTyVarTy :: Kind -> TcM TcType
425 newFlexiTyVarTy kind = do
426 tc_tyvar <- newFlexiTyVar kind
427 return (TyVarTy tc_tyvar)
428
429 newFlexiTyVarTys :: Int -> Kind -> TcM [TcType]
430 newFlexiTyVarTys n kind = mapM newFlexiTyVarTy (nOfThem n kind)
431
432 newReturnTyVar :: Kind -> TcM TcTyVar
433 newReturnTyVar kind = newMetaTyVar ReturnTv kind
434
435 newReturnTyVarTy :: Kind -> TcM TcType
436 newReturnTyVarTy kind = TyVarTy <$> newReturnTyVar kind
437
438 tcInstTyVars :: [TKVar] -> TcM (TvSubst, [TcTyVar])
439 -- Instantiate with META type variables
440 -- Note that this works for a sequence of kind and type
441 -- variables. Eg [ (k:BOX), (a:k->k) ]
442 -- Gives [ (k7:BOX), (a8:k7->k7) ]
443 tcInstTyVars tyvars = mapAccumLM tcInstTyVarX emptyTvSubst tyvars
444 -- emptyTvSubst has an empty in-scope set, but that's fine here
445 -- Since the tyvars are freshly made, they cannot possibly be
446 -- captured by any existing for-alls.
447
448 tcInstTyVarX :: TvSubst -> TKVar -> TcM (TvSubst, TcTyVar)
449 -- Make a new unification variable tyvar whose Name and Kind come from
450 -- an existing TyVar. We substitute kind variables in the kind.
451 tcInstTyVarX subst tyvar
452 = do { uniq <- newUnique
453 ; let info | isOpenTypeKind (tyVarKind tyvar) = ReturnTv
454 -- See Note [OpenTypeKind accepts foralls]
455 | otherwise = TauTv VanillaTau
456 ; details <- newMetaDetails info
457 ; let name = mkSystemName uniq (getOccName tyvar)
458 -- See Note [Name of an instantiated type variable]
459 kind = substTy subst (tyVarKind tyvar)
460 new_tv = mkTcTyVar name kind details
461 ; return (extendTvSubst subst tyvar (mkTyVarTy new_tv), new_tv) }
462
463 {- Note [Name of an instantiated type variable]
464 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
465 At the moment we give a unification variable a System Name, which
466 influences the way it is tidied; see TypeRep.tidyTyVarBndr.
467
468 Note [OpenTypeKind accepts foralls]
469 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
470 Here is a common paradigm:
471 foo :: (forall a. a -> a) -> Int
472 foo = error "urk"
473 To make this work we need to instantiate 'error' with a polytype.
474 A similar case is
475 bar :: Bool -> (forall a. a->a) -> Int
476 bar True = \x. (x 3)
477 bar False = error "urk"
478 Here we need to instantiate 'error' with a polytype.
479
480 But 'error' has an OpenTypeKind type variable, precisely so that
481 we can instantiate it with Int#. So we also allow such type variables
482 to be instantiated with a ReturnTv, which can unify with foralls.
483 It's a bit of a hack, but seems straightforward.
484
485
486 ************************************************************************
487 * *
488 Quantification
489 * *
490 ************************************************************************
491
492 Note [quantifyTyVars]
493 ~~~~~~~~~~~~~~~~~~~~~
494 quantifyTyVars is give the free vars of a type that we
495 are about to wrap in a forall.
496
497 It takes these free type/kind variables and
498 1. Zonks them and remove globals
499 2. Partitions into type and kind variables (kvs1, tvs)
500 3. Extends kvs1 with free kind vars in the kinds of tvs (removing globals)
501 4. Calls zonkQuantifiedTyVar on each
502
503 Step (3) is often unimportant, because the kind variable is often
504 also free in the type. Eg
505 Typeable k (a::k)
506 has free vars {k,a}. But the type (see Trac #7916)
507 (f::k->*) (a::k)
508 has free vars {f,a}, but we must add 'k' as well! Hence step (3).
509 -}
510
511 quantifyTyVars :: TcTyVarSet -> TcTyVarSet -> TcM [TcTyVar]
512 -- See Note [quantifyTyVars]
513 -- The input is a mixture of type and kind variables; a kind variable k
514 -- may occur *after* a tyvar mentioning k in its kind
515 -- Can be given a mixture of TcTyVars and TyVars, in the case of
516 -- associated type declarations
517
518 quantifyTyVars gbl_tvs tkvs
519 = do { tkvs <- zonkTyVarsAndFV tkvs
520 ; gbl_tvs <- zonkTyVarsAndFV gbl_tvs
521 ; let (kvs, tvs) = partitionVarSet isKindVar (closeOverKinds tkvs `minusVarSet` gbl_tvs)
522 -- NB kinds of tvs are zonked by zonkTyVarsAndFV
523 kvs2 = varSetElems kvs
524 qtvs = varSetElems tvs
525
526 -- In the non-PolyKinds case, default the kind variables
527 -- to *, and zonk the tyvars as usual. Notice that this
528 -- may make quantifyTyVars return a shorter list
529 -- than it was passed, but that's ok
530 ; poly_kinds <- xoptM Opt_PolyKinds
531 ; qkvs <- if poly_kinds
532 then return kvs2
533 else do { let (meta_kvs, skolem_kvs) = partition is_meta kvs2
534 is_meta kv = isTcTyVar kv && isMetaTyVar kv
535 ; mapM_ defaultKindVarToStar meta_kvs
536 ; return skolem_kvs } -- should be empty
537
538 ; mapM zonk_quant (qkvs ++ qtvs) }
539 -- Because of the order, any kind variables
540 -- mentioned in the kinds of the type variables refer to
541 -- the now-quantified versions
542 where
543 zonk_quant tkv
544 | isTcTyVar tkv = zonkQuantifiedTyVar tkv
545 | otherwise = return tkv
546 -- For associated types, we have the class variables
547 -- in scope, and they are TyVars not TcTyVars
548
549 zonkQuantifiedTyVar :: TcTyVar -> TcM TcTyVar
550 -- The quantified type variables often include meta type variables
551 -- we want to freeze them into ordinary type variables, and
552 -- default their kind (e.g. from OpenTypeKind to TypeKind)
553 -- -- see notes with Kind.defaultKind
554 -- The meta tyvar is updated to point to the new skolem TyVar. Now any
555 -- bound occurrences of the original type variable will get zonked to
556 -- the immutable version.
557 --
558 -- We leave skolem TyVars alone; they are immutable.
559 --
560 -- This function is called on both kind and type variables,
561 -- but kind variables *only* if PolyKinds is on.
562 zonkQuantifiedTyVar tv
563 = ASSERT2( isTcTyVar tv, ppr tv )
564 case tcTyVarDetails tv of
565 SkolemTv {} -> do { kind <- zonkTcKind (tyVarKind tv)
566 ; return $ setTyVarKind tv kind }
567 -- It might be a skolem type variable,
568 -- for example from a user type signature
569
570 MetaTv { mtv_ref = ref } ->
571 do when debugIsOn $ do
572 -- [Sept 04] Check for non-empty.
573 -- See note [Silly Type Synonym]
574 cts <- readMutVar ref
575 case cts of
576 Flexi -> return ()
577 Indirect ty -> WARN( True, ppr tv $$ ppr ty )
578 return ()
579 skolemiseUnboundMetaTyVar tv vanillaSkolemTv
580 _other -> pprPanic "zonkQuantifiedTyVar" (ppr tv) -- FlatSkol, RuntimeUnk
581
582 defaultKindVarToStar :: TcTyVar -> TcM Kind
583 -- We have a meta-kind: unify it with '*'
584 defaultKindVarToStar kv
585 = do { ASSERT( isKindVar kv && isMetaTyVar kv )
586 writeMetaTyVar kv liftedTypeKind
587 ; return liftedTypeKind }
588
589 skolemiseUnboundMetaTyVar :: TcTyVar -> TcTyVarDetails -> TcM TyVar
590 -- We have a Meta tyvar with a ref-cell inside it
591 -- Skolemise it, including giving it a new Name, so that
592 -- we are totally out of Meta-tyvar-land
593 -- We create a skolem TyVar, not a regular TyVar
594 -- See Note [Zonking to Skolem]
595 skolemiseUnboundMetaTyVar tv details
596 = ASSERT2( isMetaTyVar tv, ppr tv )
597 do { span <- getSrcSpanM -- Get the location from "here"
598 -- ie where we are generalising
599 ; uniq <- newUnique -- Remove it from TcMetaTyVar unique land
600 ; kind <- zonkTcKind (tyVarKind tv)
601 ; let tv_name = getOccName tv
602 new_tv_name = if isWildcardVar tv
603 then generaliseWildcardVarName tv_name
604 else tv_name
605 -- NB: make a System name. See Note [Visible type application]
606 -- in TcExpr
607 final_name = mkSystemNameAt uniq new_tv_name span
608 final_kind = defaultKind kind
609 final_tv = mkTcTyVar final_name final_kind details
610
611 ; traceTc "Skolemising" (ppr tv <+> ptext (sLit ":=") <+> ppr final_tv)
612 ; writeMetaTyVar tv (mkTyVarTy final_tv)
613 ; return final_tv }
614 where
615 -- If a wildcard type called _a is generalised, we rename it to w_a
616 generaliseWildcardVarName :: OccName -> OccName
617 generaliseWildcardVarName name | startsWithUnderscore name
618 = mkOccNameFS (occNameSpace name) (appendFS (fsLit "w") (occNameFS name))
619 generaliseWildcardVarName name = name
620
621 {-
622 Note [Zonking to Skolem]
623 ~~~~~~~~~~~~~~~~~~~~~~~~
624 We used to zonk quantified type variables to regular TyVars. However, this
625 leads to problems. Consider this program from the regression test suite:
626
627 eval :: Int -> String -> String -> String
628 eval 0 root actual = evalRHS 0 root actual
629
630 evalRHS :: Int -> a
631 evalRHS 0 root actual = eval 0 root actual
632
633 It leads to the deferral of an equality (wrapped in an implication constraint)
634
635 forall a. () => ((String -> String -> String) ~ a)
636
637 which is propagated up to the toplevel (see TcSimplify.tcSimplifyInferCheck).
638 In the meantime `a' is zonked and quantified to form `evalRHS's signature.
639 This has the *side effect* of also zonking the `a' in the deferred equality
640 (which at this point is being handed around wrapped in an implication
641 constraint).
642
643 Finally, the equality (with the zonked `a') will be handed back to the
644 simplifier by TcRnDriver.tcRnSrcDecls calling TcSimplify.tcSimplifyTop.
645 If we zonk `a' with a regular type variable, we will have this regular type
646 variable now floating around in the simplifier, which in many places assumes to
647 only see proper TcTyVars.
648
649 We can avoid this problem by zonking with a skolem. The skolem is rigid
650 (which we require for a quantified variable), but is still a TcTyVar that the
651 simplifier knows how to deal with.
652
653 Note [Silly Type Synonyms]
654 ~~~~~~~~~~~~~~~~~~~~~~~~~~
655 Consider this:
656 type C u a = u -- Note 'a' unused
657
658 foo :: (forall a. C u a -> C u a) -> u
659 foo x = ...
660
661 bar :: Num u => u
662 bar = foo (\t -> t + t)
663
664 * From the (\t -> t+t) we get type {Num d} => d -> d
665 where d is fresh.
666
667 * Now unify with type of foo's arg, and we get:
668 {Num (C d a)} => C d a -> C d a
669 where a is fresh.
670
671 * Now abstract over the 'a', but float out the Num (C d a) constraint
672 because it does not 'really' mention a. (see exactTyVarsOfType)
673 The arg to foo becomes
674 \/\a -> \t -> t+t
675
676 * So we get a dict binding for Num (C d a), which is zonked to give
677 a = ()
678 [Note Sept 04: now that we are zonking quantified type variables
679 on construction, the 'a' will be frozen as a regular tyvar on
680 quantification, so the floated dict will still have type (C d a).
681 Which renders this whole note moot; happily!]
682
683 * Then the \/\a abstraction has a zonked 'a' in it.
684
685 All very silly. I think its harmless to ignore the problem. We'll end up with
686 a \/\a in the final result but all the occurrences of a will be zonked to ()
687
688 ************************************************************************
689 * *
690 Zonking types
691 * *
692 ************************************************************************
693
694 @tcGetGlobalTyVars@ returns a fully-zonked set of tyvars free in the environment.
695 To improve subsequent calls to the same function it writes the zonked set back into
696 the environment.
697 -}
698
699 tcGetGlobalTyVars :: TcM TcTyVarSet
700 tcGetGlobalTyVars
701 = do { (TcLclEnv {tcl_tyvars = gtv_var}) <- getLclEnv
702 ; gbl_tvs <- readMutVar gtv_var
703 ; gbl_tvs' <- zonkTyVarsAndFV gbl_tvs
704 ; writeMutVar gtv_var gbl_tvs'
705 ; return gbl_tvs' }
706 where
707
708 zonkTcTypeAndFV :: TcType -> TcM TyVarSet
709 -- Zonk a type and take its free variables
710 -- With kind polymorphism it can be essential to zonk *first*
711 -- so that we find the right set of free variables. Eg
712 -- forall k1. forall (a:k2). a
713 -- where k2:=k1 is in the substitution. We don't want
714 -- k2 to look free in this type!
715 zonkTcTypeAndFV ty = do { ty <- zonkTcType ty; return (tyVarsOfType ty) }
716
717 zonkTyVar :: TyVar -> TcM TcType
718 -- Works on TyVars and TcTyVars
719 zonkTyVar tv | isTcTyVar tv = zonkTcTyVar tv
720 | otherwise = return (mkTyVarTy tv)
721 -- Hackily, when typechecking type and class decls
722 -- we have TyVars in scopeadded (only) in
723 -- TcHsType.tcTyClTyVars, but it seems
724 -- painful to make them into TcTyVars there
725
726 zonkTyVarsAndFV :: TyVarSet -> TcM TyVarSet
727 zonkTyVarsAndFV tyvars = tyVarsOfTypes <$> mapM zonkTyVar (varSetElems tyvars)
728
729 zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
730 zonkTcTyVars tyvars = mapM zonkTcTyVar tyvars
731
732 ----------------- Types
733 zonkTyVarKind :: TyVar -> TcM TyVar
734 zonkTyVarKind tv = do { kind' <- zonkTcKind (tyVarKind tv)
735 ; return (setTyVarKind tv kind') }
736
737 zonkTcTypes :: [TcType] -> TcM [TcType]
738 zonkTcTypes tys = mapM zonkTcType tys
739
740 zonkTcThetaType :: TcThetaType -> TcM TcThetaType
741 zonkTcThetaType theta = mapM zonkTcPredType theta
742
743 zonkTcPredType :: TcPredType -> TcM TcPredType
744 zonkTcPredType = zonkTcType
745
746 {-
747 ************************************************************************
748 * *
749 Zonking constraints
750 * *
751 ************************************************************************
752 -}
753
754 zonkImplication :: Implication -> TcM Implication
755 zonkImplication implic@(Implic { ic_skols = skols
756 , ic_given = given
757 , ic_wanted = wanted
758 , ic_info = info })
759 = do { skols' <- mapM zonkTcTyVarBndr skols -- Need to zonk their kinds!
760 -- as Trac #7230 showed
761 ; given' <- mapM zonkEvVar given
762 ; info' <- zonkSkolemInfo info
763 ; wanted' <- zonkWCRec wanted
764 ; return (implic { ic_skols = skols'
765 , ic_given = given'
766 , ic_wanted = wanted'
767 , ic_info = info' }) }
768
769 zonkEvVar :: EvVar -> TcM EvVar
770 zonkEvVar var = do { ty' <- zonkTcType (varType var)
771 ; return (setVarType var ty') }
772
773
774 zonkWC :: WantedConstraints -> TcM WantedConstraints
775 zonkWC wc = zonkWCRec wc
776
777 zonkWCRec :: WantedConstraints -> TcM WantedConstraints
778 zonkWCRec (WC { wc_simple = simple, wc_impl = implic, wc_insol = insol })
779 = do { simple' <- zonkSimples simple
780 ; implic' <- mapBagM zonkImplication implic
781 ; insol' <- zonkSimples insol
782 ; return (WC { wc_simple = simple', wc_impl = implic', wc_insol = insol' }) }
783
784 zonkSimples :: Cts -> TcM Cts
785 zonkSimples cts = do { cts' <- mapBagM zonkCt' cts
786 ; traceTc "zonkSimples done:" (ppr cts')
787 ; return cts' }
788
789 zonkCt' :: Ct -> TcM Ct
790 zonkCt' ct = zonkCt ct
791
792 zonkCt :: Ct -> TcM Ct
793 zonkCt ct@(CHoleCan { cc_ev = ev })
794 = do { ev' <- zonkCtEvidence ev
795 ; return $ ct { cc_ev = ev' } }
796 zonkCt ct
797 = do { fl' <- zonkCtEvidence (cc_ev ct)
798 ; return (mkNonCanonical fl') }
799
800 zonkCtEvidence :: CtEvidence -> TcM CtEvidence
801 zonkCtEvidence ctev@(CtGiven { ctev_pred = pred })
802 = do { pred' <- zonkTcType pred
803 ; return (ctev { ctev_pred = pred'}) }
804 zonkCtEvidence ctev@(CtWanted { ctev_pred = pred })
805 = do { pred' <- zonkTcType pred
806 ; return (ctev { ctev_pred = pred' }) }
807 zonkCtEvidence ctev@(CtDerived { ctev_pred = pred })
808 = do { pred' <- zonkTcType pred
809 ; return (ctev { ctev_pred = pred' }) }
810
811 zonkSkolemInfo :: SkolemInfo -> TcM SkolemInfo
812 zonkSkolemInfo (SigSkol cx ty) = do { ty' <- zonkTcType ty
813 ; return (SigSkol cx ty') }
814 zonkSkolemInfo (InferSkol ntys) = do { ntys' <- mapM do_one ntys
815 ; return (InferSkol ntys') }
816 where
817 do_one (n, ty) = do { ty' <- zonkTcType ty; return (n, ty') }
818 zonkSkolemInfo skol_info = return skol_info
819
820 {-
821 ************************************************************************
822 * *
823 \subsection{Zonking -- the main work-horses: zonkTcType, zonkTcTyVar}
824 * *
825 * For internal use only! *
826 * *
827 ************************************************************************
828 -}
829
830 -- zonkId is used *during* typechecking just to zonk the Id's type
831 zonkId :: TcId -> TcM TcId
832 zonkId id
833 = do { ty' <- zonkTcType (idType id)
834 ; return (Id.setIdType id ty') }
835
836 -- For unbound, mutable tyvars, zonkType uses the function given to it
837 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
838 -- type variable and zonks the kind too
839
840 zonkTcType :: TcType -> TcM TcType
841 zonkTcType ty
842 = go ty
843 where
844 go (TyConApp tc tys) = do tys' <- mapM go tys
845 return (TyConApp tc tys')
846 -- Do NOT establish Type invariants, because
847 -- doing so is strict in the TyCOn.
848 -- See Note [Zonking inside the knot] in TcHsType
849
850 go (LitTy n) = return (LitTy n)
851
852 go (FunTy arg res) = do arg' <- go arg
853 res' <- go res
854 return (FunTy arg' res')
855
856 go (AppTy fun arg) = do fun' <- go fun
857 arg' <- go arg
858 return (mkAppTy fun' arg')
859 -- NB the mkAppTy; we might have instantiated a
860 -- type variable to a type constructor, so we need
861 -- to pull the TyConApp to the top.
862 -- OK to do this because only strict in the structure
863 -- not in the TyCon.
864 -- See Note [Zonking inside the knot] in TcHsType
865
866 -- The two interesting cases!
867 go (TyVarTy tyvar) | isTcTyVar tyvar = zonkTcTyVar tyvar
868 | otherwise = TyVarTy <$> updateTyVarKindM go tyvar
869 -- Ordinary (non Tc) tyvars occur inside quantified types
870
871 go (ForAllTy tv ty) = do { tv' <- zonkTcTyVarBndr tv
872 ; ty' <- go ty
873 ; return (ForAllTy tv' ty') }
874
875 zonkTcTyVarBndr :: TcTyVar -> TcM TcTyVar
876 -- A tyvar binder is never a unification variable (MetaTv),
877 -- rather it is always a skolems. BUT it may have a kind
878 -- that has not yet been zonked, and may include kind
879 -- unification variables.
880 zonkTcTyVarBndr tyvar
881 = ASSERT2( isImmutableTyVar tyvar, ppr tyvar ) do
882 updateTyVarKindM zonkTcType tyvar
883
884 zonkTcTyVar :: TcTyVar -> TcM TcType
885 -- Simply look through all Flexis
886 zonkTcTyVar tv
887 = ASSERT2( isTcTyVar tv, ppr tv ) do
888 case tcTyVarDetails tv of
889 SkolemTv {} -> zonk_kind_and_return
890 RuntimeUnk {} -> zonk_kind_and_return
891 FlatSkol ty -> zonkTcType ty
892 MetaTv { mtv_ref = ref }
893 -> do { cts <- readMutVar ref
894 ; case cts of
895 Flexi -> zonk_kind_and_return
896 Indirect ty -> zonkTcType ty }
897 where
898 zonk_kind_and_return = do { z_tv <- zonkTyVarKind tv
899 ; return (TyVarTy z_tv) }
900
901 {-
902 ************************************************************************
903 * *
904 Zonking kinds
905 * *
906 ************************************************************************
907 -}
908
909 zonkTcKind :: TcKind -> TcM TcKind
910 zonkTcKind k = zonkTcType k
911
912 {-
913 ************************************************************************
914 * *
915 Tidying
916 * *
917 ************************************************************************
918 -}
919
920 zonkTidyTcType :: TidyEnv -> TcType -> TcM (TidyEnv, TcType)
921 zonkTidyTcType env ty = do { ty' <- zonkTcType ty
922 ; return (tidyOpenType env ty') }
923
924 zonkTidyOrigin :: TidyEnv -> CtOrigin -> TcM (TidyEnv, CtOrigin)
925 zonkTidyOrigin env (GivenOrigin skol_info)
926 = do { skol_info1 <- zonkSkolemInfo skol_info
927 ; let (env1, skol_info2) = tidySkolemInfo env skol_info1
928 ; return (env1, GivenOrigin skol_info2) }
929 zonkTidyOrigin env (TypeEqOrigin { uo_actual = act, uo_expected = exp })
930 = do { (env1, act') <- zonkTidyTcType env act
931 ; (env2, exp') <- zonkTidyTcType env1 exp
932 ; return ( env2, TypeEqOrigin { uo_actual = act', uo_expected = exp' }) }
933 zonkTidyOrigin env (KindEqOrigin ty1 ty2 orig)
934 = do { (env1, ty1') <- zonkTidyTcType env ty1
935 ; (env2, ty2') <- zonkTidyTcType env1 ty2
936 ; (env3, orig') <- zonkTidyOrigin env2 orig
937 ; return (env3, KindEqOrigin ty1' ty2' orig') }
938 zonkTidyOrigin env (FunDepOrigin1 p1 l1 p2 l2)
939 = do { (env1, p1') <- zonkTidyTcType env p1
940 ; (env2, p2') <- zonkTidyTcType env1 p2
941 ; return (env2, FunDepOrigin1 p1' l1 p2' l2) }
942 zonkTidyOrigin env (FunDepOrigin2 p1 o1 p2 l2)
943 = do { (env1, p1') <- zonkTidyTcType env p1
944 ; (env2, p2') <- zonkTidyTcType env1 p2
945 ; (env3, o1') <- zonkTidyOrigin env2 o1
946 ; return (env3, FunDepOrigin2 p1' o1' p2' l2) }
947 zonkTidyOrigin env orig = return (env, orig)
948
949 ----------------
950 tidyCt :: TidyEnv -> Ct -> Ct
951 -- Used only in error reporting
952 -- Also converts it to non-canonical
953 tidyCt env ct
954 = case ct of
955 CHoleCan { cc_ev = ev }
956 -> ct { cc_ev = tidy_ev env ev }
957 _ -> mkNonCanonical (tidy_ev env (ctEvidence ct))
958 where
959 tidy_ev :: TidyEnv -> CtEvidence -> CtEvidence
960 -- NB: we do not tidy the ctev_evar field because we don't
961 -- show it in error messages
962 tidy_ev env ctev@(CtGiven { ctev_pred = pred })
963 = ctev { ctev_pred = tidyType env pred }
964 tidy_ev env ctev@(CtWanted { ctev_pred = pred })
965 = ctev { ctev_pred = tidyType env pred }
966 tidy_ev env ctev@(CtDerived { ctev_pred = pred })
967 = ctev { ctev_pred = tidyType env pred }
968
969 ----------------
970 tidyEvVar :: TidyEnv -> EvVar -> EvVar
971 tidyEvVar env var = setVarType var (tidyType env (varType var))
972
973 ----------------
974 tidySkolemInfo :: TidyEnv -> SkolemInfo -> (TidyEnv, SkolemInfo)
975 tidySkolemInfo env (SigSkol cx ty)
976 = (env', SigSkol cx ty')
977 where
978 (env', ty') = tidyOpenType env ty
979
980 tidySkolemInfo env (InferSkol ids)
981 = (env', InferSkol ids')
982 where
983 (env', ids') = mapAccumL do_one env ids
984 do_one env (name, ty) = (env', (name, ty'))
985 where
986 (env', ty') = tidyOpenType env ty
987
988 tidySkolemInfo env (UnifyForAllSkol skol_tvs ty)
989 = (env1, UnifyForAllSkol skol_tvs' ty')
990 where
991 env1 = tidyFreeTyVars env (tyVarsOfType ty `delVarSetList` skol_tvs)
992 (env2, skol_tvs') = tidyTyVarBndrs env1 skol_tvs
993 ty' = tidyType env2 ty
994
995 tidySkolemInfo env info = (env, info)
996
997 {-
998 ************************************************************************
999 * *
1000 (Named) Wildcards
1001 * *
1002 ************************************************************************
1003 -}
1004
1005 -- | Create a new meta var with the given kind. This meta var should be used
1006 -- to replace a wildcard in a type. Such a wildcard meta var can be
1007 -- distinguished from other meta vars with the 'isWildcardVar' function.
1008 newWildcardVar :: Name -> Kind -> TcM TcTyVar
1009 newWildcardVar name kind = newNamedMetaTyVar name (TauTv WildcardTau) kind
1010
1011 -- | Create a new meta var (which can unify with a type of any kind). This
1012 -- meta var should be used to replace a wildcard in a type. Such a wildcard
1013 -- meta var can be distinguished from other meta vars with the 'isWildcardVar'
1014 -- function.
1015 newWildcardVarMetaKind :: Name -> TcM TcTyVar
1016 newWildcardVarMetaKind name = do kind <- newMetaKindVar
1017 newWildcardVar name kind
1018
1019 -- | Return 'True' if the argument is a meta var created for a wildcard (by
1020 -- 'newWildcardVar' or 'newWildcardVarMetaKind').
1021 isWildcardVar :: TcTyVar -> Bool
1022 isWildcardVar tv | isTcTyVar tv, MetaTv (TauTv WildcardTau) _ _ <- tcTyVarDetails tv = True
1023 isWildcardVar _ = False