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