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