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