59dca2cb745da4a9a001dc4efd29fe4c747ea91c
[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 {-# OPTIONS -fno-warn-tabs #-}
13 -- The above warning supression flag is a temporary kludge.
14 -- While working on this module you are encouraged to remove it and
15 -- detab the module (please do the detabbing in a separate patch). See
16 --     http://ghc.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#TabsvsSpaces
17 -- for details
18
19 module TcMType (
20   TcTyVar, TcKind, TcType, TcTauType, TcThetaType, TcTyVarSet,
21
22   --------------------------------
23   -- Creating new mutable type variables
24   newFlexiTyVar,
25   newFlexiTyVarTy,              -- Kind -> TcM TcType
26   newFlexiTyVarTys,             -- Int -> Kind -> TcM [TcType]
27   newPolyFlexiTyVarTy,
28   newMetaKindVar, newMetaKindVars,
29   mkTcTyVarName, cloneMetaTyVar, 
30
31   newMetaTyVar, readMetaTyVar, writeMetaTyVar, writeMetaTyVarRef,
32   newMetaDetails, isFilledMetaTyVar, isFlexiMetaTyVar,
33
34   --------------------------------
35   -- Creating new evidence variables
36   newEvVar, newEvVars, newEq, newDict,
37   newWantedEvVar, newWantedEvVars,
38   newTcEvBinds, addTcEvBind,
39   newFlatWanted, newFlatWanteds,
40
41   --------------------------------
42   -- Instantiation
43   tcInstTyVars, tcInstSigTyVars, newSigTyVar,
44   tcInstType, 
45   tcInstSkolTyVars, tcInstSkolTyVarsLoc, tcInstSuperSkolTyVars,
46   tcInstSkolTyVarsX, tcInstSuperSkolTyVarsX,
47   tcInstSkolTyVar, tcInstSkolType,
48   tcSkolDFunType, tcSuperSkolTyVars,
49
50   --------------------------------
51   -- Zonking
52   zonkTcPredType, 
53   skolemiseSigTv, skolemiseUnboundMetaTyVar,
54   zonkTcTyVar, zonkTcTyVars, zonkTyVarsAndFV, zonkTcTypeAndFV,
55   zonkQuantifiedTyVar, quantifyTyVars,
56   zonkTcTyVarBndr, zonkTcType, zonkTcTypes, zonkTcThetaType, 
57
58   zonkTcKind, defaultKindVarToStar,
59   zonkEvVar, zonkWC, zonkId, zonkCt, zonkCts, zonkSkolemInfo,
60
61   tcGetGlobalTyVars, 
62   ) where
63
64 #include "HsVersions.h"
65
66 -- friends:
67 import TypeRep
68 import TcType
69 import TcEvidence
70 import Type
71 import Class
72 import TyCon
73 import Var
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 \end{code}
91
92
93 %************************************************************************
94 %*                                                                      *
95         Kind variables
96 %*                                                                      *
97 %************************************************************************
98
99 \begin{code}
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
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 \end{code}
116
117
118 %************************************************************************
119 %*                                                                      *
120      Evidence variables; range over constraints we can abstract over
121 %*                                                                      *
122 %************************************************************************
123
124 \begin{code}
125 newEvVars :: TcThetaType -> TcM [EvVar]
126 newEvVars theta = mapM newEvVar theta
127
128 newWantedEvVar :: TcPredType -> TcM EvVar 
129 newWantedEvVar = newEvVar
130
131 newWantedEvVars :: TcThetaType -> TcM [EvVar] 
132 newWantedEvVars theta = mapM newWantedEvVar theta 
133
134 --------------
135
136 newEvVar :: TcPredType -> TcM EvVar
137 -- Creates new *rigid* variables for predicates
138 newEvVar ty = do { name <- newSysName (predTypeOccName ty) 
139                  ; return (mkLocalId name ty) }
140
141 newEq :: TcType -> TcType -> TcM EvVar
142 newEq ty1 ty2
143   = do { name <- newSysName (mkVarOccFS (fsLit "cobox"))
144        ; return (mkLocalId name (mkTcEqPred ty1 ty2)) }
145
146 newDict :: Class -> [TcType] -> TcM DictId
147 newDict cls tys 
148   = do { name <- newSysName (mkDictOcc (getOccName cls))
149        ; return (mkLocalId name (mkClassPred cls tys)) }
150
151 predTypeOccName :: PredType -> OccName
152 predTypeOccName ty = case classifyPredType ty of
153     ClassPred cls _ -> mkDictOcc (getOccName cls)
154     EqPred _ _      -> mkVarOccFS (fsLit "cobox")
155     TuplePred _     -> mkVarOccFS (fsLit "tup")
156     IrredPred _     -> mkVarOccFS (fsLit "irred")
157 \end{code}
158
159 *********************************************************************************
160 *                                                                               * 
161 *                   Wanted constraints
162 *                                                                               *
163 *********************************************************************************
164
165 \begin{code}
166 newFlatWanted :: CtOrigin -> PredType -> TcM Ct
167 newFlatWanted orig pty
168   = do loc <- getCtLoc orig
169        v <- newWantedEvVar pty
170        return $ mkNonCanonical $
171             CtWanted { ctev_evar = v
172                      , ctev_pred = pty
173                      , ctev_loc = loc }
174
175 newFlatWanteds :: CtOrigin -> ThetaType -> TcM [Ct]
176 newFlatWanteds orig = mapM (newFlatWanted orig)
177 \end{code}
178
179 %************************************************************************
180 %*                                                                      *
181         SkolemTvs (immutable)
182 %*                                                                      *
183 %************************************************************************
184
185 \begin{code}
186 tcInstType :: ([TyVar] -> TcM (TvSubst, [TcTyVar]))     -- How to instantiate the type variables
187            -> TcType                                    -- Type to instantiate
188            -> TcM ([TcTyVar], TcThetaType, TcType)      -- Result
189                 -- (type vars (excl coercion vars), preds (incl equalities), rho)
190 tcInstType inst_tyvars ty
191   = case tcSplitForAllTys ty of
192         ([],     rho) -> let    -- There may be overloading despite no type variables;
193                                 --      (?x :: Int) => Int -> Int
194                            (theta, tau) = tcSplitPhiTy rho
195                          in
196                          return ([], theta, tau)
197
198         (tyvars, rho) -> do { (subst, tyvars') <- inst_tyvars tyvars
199                             ; let (theta, tau) = tcSplitPhiTy (substTy subst rho)
200                             ; return (tyvars', theta, tau) }
201
202 tcSkolDFunType :: Type -> TcM ([TcTyVar], TcThetaType, TcType)
203 -- Instantiate a type signature with skolem constants, but 
204 -- do *not* give them fresh names, because we want the name to
205 -- be in the type environment: it is lexically scoped.
206 tcSkolDFunType ty = tcInstType (\tvs -> return (tcSuperSkolTyVars tvs)) ty
207
208 tcSuperSkolTyVars :: [TyVar] -> (TvSubst, [TcTyVar])
209 -- Make skolem constants, but do *not* give them new names, as above
210 -- Moreover, make them "super skolems"; see comments with superSkolemTv
211 -- see Note [Kind substitution when instantiating]
212 -- Precondition: tyvars should be ordered (kind vars first)
213 tcSuperSkolTyVars = mapAccumL tcSuperSkolTyVar (mkTopTvSubst [])
214
215 tcSuperSkolTyVar :: TvSubst -> TyVar -> (TvSubst, TcTyVar)
216 tcSuperSkolTyVar subst tv
217   = (extendTvSubst subst tv (mkTyVarTy new_tv), new_tv)
218   where
219     kind   = substTy subst (tyVarKind tv)
220     new_tv = mkTcTyVar (tyVarName tv) kind superSkolemTv
221
222 tcInstSkolTyVar :: SrcSpan -> Bool -> TvSubst -> TyVar
223                 -> TcRnIf gbl lcl (TvSubst, TcTyVar)
224 -- Instantiate the tyvar, using 
225 --      * the occ-name and kind of the supplied tyvar, 
226 --      * the unique from the monad,
227 --      * the location either from the tyvar (skol_info = SigSkol)
228 --                     or from the monad (otherwise)
229 tcInstSkolTyVar loc overlappable subst tyvar
230   = do  { uniq <- newUnique
231         ; let new_name = mkInternalName uniq occ loc
232               new_tv   = mkTcTyVar new_name kind (SkolemTv overlappable)
233         ; return (extendTvSubst subst tyvar (mkTyVarTy new_tv), new_tv) }
234   where
235     old_name = tyVarName tyvar
236     occ      = nameOccName old_name
237     kind     = substTy subst (tyVarKind tyvar)
238
239 -- Wrappers
240 -- we need to be able to do this from outside the TcM monad:
241 tcInstSkolTyVarsLoc :: SrcSpan -> [TyVar] -> TcRnIf gbl lcl (TvSubst, [TcTyVar])
242 tcInstSkolTyVarsLoc loc = mapAccumLM (tcInstSkolTyVar loc False) (mkTopTvSubst [])
243
244 tcInstSkolTyVars :: [TyVar] -> TcM (TvSubst, [TcTyVar])
245 tcInstSkolTyVars = tcInstSkolTyVarsX (mkTopTvSubst [])
246
247 tcInstSuperSkolTyVars :: [TyVar] -> TcM [TcTyVar]
248 tcInstSuperSkolTyVars = fmap snd . tcInstSkolTyVars' True  (mkTopTvSubst [])
249
250 tcInstSkolTyVarsX, tcInstSuperSkolTyVarsX
251   :: TvSubst -> [TyVar] -> TcM (TvSubst, [TcTyVar])
252 tcInstSkolTyVarsX      subst = tcInstSkolTyVars' False subst
253 tcInstSuperSkolTyVarsX subst = tcInstSkolTyVars' True  subst
254
255 tcInstSkolTyVars' :: Bool -> TvSubst -> [TyVar] -> TcM (TvSubst, [TcTyVar])
256 -- Precondition: tyvars should be ordered (kind vars first)
257 -- see Note [Kind substitution when instantiating]
258 tcInstSkolTyVars' isSuperSkol subst tvs
259   = do { loc <- getSrcSpanM
260        ; mapAccumLM (tcInstSkolTyVar loc isSuperSkol) subst tvs }
261
262 tcInstSkolType :: TcType -> TcM ([TcTyVar], TcThetaType, TcType)
263 -- Instantiate a type with fresh skolem constants
264 -- Binding location comes from the monad
265 tcInstSkolType ty = tcInstType tcInstSkolTyVars ty
266
267 tcInstSigTyVars :: [TyVar] -> TcM (TvSubst, [TcTyVar])
268 -- Make meta SigTv type variables for patten-bound scoped type varaibles
269 -- We use SigTvs for them, so that they can't unify with arbitrary types
270 -- Precondition: tyvars should be ordered (kind vars first)
271 -- see Note [Kind substitution when instantiating]
272 tcInstSigTyVars = mapAccumLM tcInstSigTyVar (mkTopTvSubst [])
273         -- The tyvars are freshly made, by tcInstSigTyVar
274         -- So mkTopTvSubst [] is ok
275
276 tcInstSigTyVar :: TvSubst -> TyVar -> TcM (TvSubst, TcTyVar)
277 tcInstSigTyVar subst tv
278   = do { new_tv <- newSigTyVar (tyVarName tv) (substTy subst (tyVarKind tv))
279        ; return (extendTvSubst subst tv (mkTyVarTy new_tv), new_tv) }
280
281 newSigTyVar :: Name -> Kind -> TcM TcTyVar
282 newSigTyVar name kind
283   = do { uniq <- newUnique
284        ; let name' = setNameUnique name uniq
285                       -- Use the same OccName so that the tidy-er
286                       -- doesn't gratuitously rename 'a' to 'a0' etc
287        ; details <- newMetaDetails SigTv
288        ; return (mkTcTyVar name' kind details) }
289
290 newMetaDetails :: MetaInfo -> TcM TcTyVarDetails
291 newMetaDetails info 
292   = do { ref <- newMutVar Flexi
293        ; untch <- getUntouchables
294        ; return (MetaTv { mtv_info = info, mtv_ref = ref, mtv_untch = untch }) }
295 \end{code}
296
297 Note [Kind substitution when instantiating]
298 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
299 When we instantiate a bunch of kind and type variables, first we
300 expect them to be sorted (kind variables first, then type variables).
301 Then we have to instantiate the kind variables, build a substitution
302 from old variables to the new variables, then instantiate the type
303 variables substituting the original kind.
304
305 Exemple: If we want to instantiate
306   [(k1 :: BOX), (k2 :: BOX), (a :: k1 -> k2), (b :: k1)]
307 we want
308   [(?k1 :: BOX), (?k2 :: BOX), (?a :: ?k1 -> ?k2), (?b :: ?k1)]
309 instead of the buggous
310   [(?k1 :: BOX), (?k2 :: BOX), (?a :: k1 -> k2), (?b :: k1)]
311
312
313 %************************************************************************
314 %*                                                                      *
315         MetaTvs (meta type variables; mutable)
316 %*                                                                      *
317 %************************************************************************
318
319 \begin{code}
320 newMetaTyVar :: MetaInfo -> Kind -> TcM TcTyVar
321 -- Make a new meta tyvar out of thin air
322 newMetaTyVar meta_info kind
323   = do  { uniq <- newUnique
324         ; let name = mkTcTyVarName uniq s
325               s = case meta_info of
326                         PolyTv -> fsLit "s"
327                         TauTv  -> fsLit "t"
328                         SigTv  -> fsLit "a"
329         ; details <- newMetaDetails meta_info
330         ; return (mkTcTyVar name kind details) }
331
332 cloneMetaTyVar :: TcTyVar -> TcM TcTyVar
333 cloneMetaTyVar tv
334   = ASSERT( isTcTyVar tv )
335     do  { uniq <- newUnique
336         ; ref  <- newMutVar Flexi
337         ; let name'    = setNameUnique (tyVarName tv) uniq
338               details' = case tcTyVarDetails tv of 
339                            details@(MetaTv {}) -> details { mtv_ref = ref }
340                            _ -> pprPanic "cloneMetaTyVar" (ppr tv)
341         ; return (mkTcTyVar name' (tyVarKind tv) details') }
342
343 mkTcTyVarName :: Unique -> FastString -> Name
344 -- Make sure that fresh TcTyVar names finish with a digit
345 -- leaving the un-cluttered names free for user names
346 mkTcTyVarName uniq str = mkSysTvName uniq str
347
348 -- Works for both type and kind variables
349 readMetaTyVar :: TyVar -> TcM MetaDetails
350 readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
351                       readMutVar (metaTvRef tyvar)
352
353 isFilledMetaTyVar :: TyVar -> TcM Bool
354 -- True of a filled-in (Indirect) meta type variable
355 isFilledMetaTyVar tv
356   | not (isTcTyVar tv) = return False
357   | MetaTv { mtv_ref = ref } <- tcTyVarDetails tv
358   = do  { details <- readMutVar ref
359         ; return (isIndirect details) }
360   | otherwise = return False
361
362 isFlexiMetaTyVar :: TyVar -> TcM Bool
363 -- True of a un-filled-in (Flexi) meta type variable
364 isFlexiMetaTyVar tv
365   | not (isTcTyVar tv) = return False
366   | MetaTv { mtv_ref = ref } <- tcTyVarDetails tv
367   = do  { details <- readMutVar ref
368         ; return (isFlexi details) }
369   | otherwise = return False
370
371 --------------------
372 -- Works with both type and kind variables
373 writeMetaTyVar :: TcTyVar -> TcType -> TcM ()
374 -- Write into a currently-empty MetaTyVar
375
376 writeMetaTyVar tyvar ty
377   | not debugIsOn 
378   = writeMetaTyVarRef tyvar (metaTvRef tyvar) ty
379
380 -- Everything from here on only happens if DEBUG is on
381   | not (isTcTyVar tyvar)
382   = WARN( True, text "Writing to non-tc tyvar" <+> ppr tyvar )
383     return ()
384
385   | MetaTv { mtv_ref = ref } <- tcTyVarDetails tyvar
386   = writeMetaTyVarRef tyvar ref ty
387
388   | otherwise
389   = WARN( True, text "Writing to non-meta tyvar" <+> ppr tyvar )
390     return ()
391
392 --------------------
393 writeMetaTyVarRef :: TcTyVar -> TcRef MetaDetails -> TcType -> TcM ()
394 -- Here the tyvar is for error checking only; 
395 -- the ref cell must be for the same tyvar
396 writeMetaTyVarRef tyvar ref ty
397   | not debugIsOn 
398   = do { traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty)
399        ; writeMutVar ref (Indirect ty) }
400
401 -- Everything from here on only happens if DEBUG is on
402   | otherwise
403   = do { meta_details <- readMutVar ref; 
404        -- Zonk kinds to allow the error check to work
405        ; zonked_tv_kind <- zonkTcKind tv_kind 
406        ; zonked_ty_kind <- zonkTcKind ty_kind
407
408        -- Check for double updates
409        ; ASSERT2( isFlexi meta_details, 
410                   hang (text "Double update of meta tyvar")
411                    2 (ppr tyvar $$ ppr meta_details) )
412
413          traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty)
414        ; writeMutVar ref (Indirect ty) 
415        ; when (   not (isPredTy tv_kind) 
416                     -- Don't check kinds for updates to coercion variables
417                && not (zonked_ty_kind `tcIsSubKind` zonked_tv_kind))
418        $ WARN( True, hang (text "Ill-kinded update to meta tyvar")
419                         2 (    ppr tyvar <+> text "::" <+> ppr tv_kind 
420                            <+> text ":=" 
421                            <+> ppr ty    <+> text "::" <+> ppr ty_kind) )
422          (return ()) }
423   where
424     tv_kind = tyVarKind tyvar
425     ty_kind = typeKind ty
426 \end{code}
427
428
429 %************************************************************************
430 %*                                                                      *
431         MetaTvs: TauTvs
432 %*                                                                      *
433 %************************************************************************
434
435 \begin{code}
436 newFlexiTyVar :: Kind -> TcM TcTyVar
437 newFlexiTyVar kind = newMetaTyVar TauTv kind
438
439 newFlexiTyVarTy  :: Kind -> TcM TcType
440 newFlexiTyVarTy kind = do
441     tc_tyvar <- newFlexiTyVar kind
442     return (TyVarTy tc_tyvar)
443
444 newFlexiTyVarTys :: Int -> Kind -> TcM [TcType]
445 newFlexiTyVarTys n kind = mapM newFlexiTyVarTy (nOfThem n kind)
446
447 newPolyFlexiTyVarTy :: TcM TcType
448 newPolyFlexiTyVarTy = do { tv <- newMetaTyVar PolyTv liftedTypeKind
449                          ; return (TyVarTy tv) }
450
451 tcInstTyVars :: [TKVar] -> TcM ([TcTyVar], [TcType], TvSubst)
452 -- Instantiate with META type variables
453 -- Note that this works for a sequence of kind and type
454 -- variables.  Eg    [ (k:BOX), (a:k->k) ]
455 --             Gives [ (k7:BOX), (a8:k7->k7) ]
456 tcInstTyVars tyvars = tcInstTyVarsX emptyTvSubst tyvars
457     -- emptyTvSubst has an empty in-scope set, but that's fine here
458     -- Since the tyvars are freshly made, they cannot possibly be
459     -- captured by any existing for-alls.
460
461 tcInstTyVarsX :: TvSubst -> [TKVar] -> TcM ([TcTyVar], [TcType], TvSubst)
462 -- The "X" part is because of extending the substitution
463 tcInstTyVarsX subst tyvars =
464   do { (subst', tyvars') <- mapAccumLM tcInstTyVarX subst tyvars
465      ; return (tyvars', mkTyVarTys tyvars', subst') }
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
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 \end{code}
478
479
480 %************************************************************************
481 %*                                                                      *
482              Quantification
483 %*                                                                      *
484 %************************************************************************
485
486 Note [quantifyTyVars]
487 ~~~~~~~~~~~~~~~~~~~~~
488 quantifyTyVars is give the free vars of a type that we
489 are about to wrap in a forall.
490
491 It takes these free type/kind variables and 
492   1. Zonks them and remove globals
493   2. Partitions into type and kind variables (kvs1, tvs)
494   3. Extends kvs1 with free kind vars in the kinds of tvs (removing globals)
495   4. Calls zonkQuantifiedTyVar on each
496
497 Step (3) is often unimportant, because the kind variable is often
498 also free in the type.  Eg
499      Typeable k (a::k)
500 has free vars {k,a}.  But the type (see Trac #7916)
501     (f::k->*) (a::k)
502 has free vars {f,a}, but we must add 'k' as well! Hence step (3).
503
504 \begin{code}
505 quantifyTyVars :: TcTyVarSet -> TcTyVarSet -> TcM [TcTyVar]
506 -- See Note [quantifyTyVars]
507 -- The input is a mixture of type and kind variables; a kind variable k 
508 --   may occur *after* a tyvar mentioning k in its kind
509 -- Can be given a mixture of TcTyVars and TyVars, in the case of
510 --   associated type declarations
511
512 quantifyTyVars gbl_tvs tkvs
513   = do { tkvs    <- zonkTyVarsAndFV tkvs
514        ; gbl_tvs <- zonkTyVarsAndFV gbl_tvs
515        ; let (kvs, tvs) = partitionVarSet isKindVar (closeOverKinds tkvs `minusVarSet` gbl_tvs)
516                               -- NB kinds of tvs are zonked by zonkTyVarsAndFV
517              kvs2 = varSetElems kvs
518              qtvs = varSetElems tvs                       
519
520              -- In the non-PolyKinds case, default the kind variables
521              -- to *, and zonk the tyvars as usual.  Notice that this
522              -- may make quantifyTyVars return a shorter list
523              -- than it was passed, but that's ok
524        ; poly_kinds <- xoptM Opt_PolyKinds
525        ; qkvs <- if poly_kinds
526                  then return kvs2
527                  else do { let (meta_kvs, skolem_kvs) = partition is_meta kvs2
528                                is_meta kv = isTcTyVar kv && isMetaTyVar kv
529                          ; mapM_ defaultKindVarToStar meta_kvs
530                          ; return skolem_kvs }  -- should be empty
531
532        ; mapM zonk_quant (qkvs ++ qtvs) } 
533            -- Because of the order, any kind variables
534            -- mentioned in the kinds of the type variables refer to
535            -- the now-quantified versions
536   where
537     zonk_quant tkv
538       | isTcTyVar tkv = zonkQuantifiedTyVar tkv
539       | otherwise     = return tkv
540       -- For associated types, we have the class variables 
541       -- in scope, and they are TyVars not TcTyVars
542
543 zonkQuantifiedTyVar :: TcTyVar -> TcM TcTyVar
544 -- The quantified type variables often include meta type variables
545 -- we want to freeze them into ordinary type variables, and
546 -- default their kind (e.g. from OpenTypeKind to TypeKind)
547 --                      -- see notes with Kind.defaultKind
548 -- The meta tyvar is updated to point to the new skolem TyVar.  Now any 
549 -- bound occurences of the original type variable will get zonked to 
550 -- the immutable version.
551 --
552 -- We leave skolem TyVars alone; they are immutable.
553 --
554 -- This function is called on both kind and type variables,
555 -- but kind variables *only* if PolyKinds is on.
556 zonkQuantifiedTyVar tv
557   = ASSERT2( isTcTyVar tv, ppr tv ) 
558     case tcTyVarDetails tv of
559       SkolemTv {} -> do { kind <- zonkTcKind (tyVarKind tv)
560                         ; return $ setTyVarKind tv kind }
561         -- It might be a skolem type variable, 
562         -- for example from a user type signature
563
564       MetaTv { mtv_ref = ref } ->
565           do when debugIsOn $ do
566                  -- [Sept 04] Check for non-empty.
567                  -- See note [Silly Type Synonym]
568                  cts <- readMutVar ref
569                  case cts of
570                      Flexi -> return ()
571                      Indirect ty -> WARN( True, ppr tv $$ ppr ty )
572                                     return ()
573              skolemiseUnboundMetaTyVar tv vanillaSkolemTv
574       _other -> pprPanic "zonkQuantifiedTyVar" (ppr tv) -- FlatSkol, RuntimeUnk
575
576 defaultKindVarToStar :: TcTyVar -> TcM Kind
577 -- We have a meta-kind: unify it with '*'
578 defaultKindVarToStar kv 
579   = do { ASSERT( isKindVar kv && isMetaTyVar kv )
580          writeMetaTyVar kv liftedTypeKind
581        ; return liftedTypeKind }
582
583 skolemiseUnboundMetaTyVar :: TcTyVar -> TcTyVarDetails -> TcM TyVar
584 -- We have a Meta tyvar with a ref-cell inside it
585 -- Skolemise it, including giving it a new Name, so that
586 --   we are totally out of Meta-tyvar-land
587 -- We create a skolem TyVar, not a regular TyVar
588 --   See Note [Zonking to Skolem]
589 skolemiseUnboundMetaTyVar tv details
590   = ASSERT2( isMetaTyVar tv, ppr tv ) 
591     do  { span <- getSrcSpanM    -- Get the location from "here"
592                                  -- ie where we are generalising
593         ; uniq <- newUnique      -- Remove it from TcMetaTyVar unique land
594         ; kind <- zonkTcKind (tyVarKind tv)
595         ; let final_kind = defaultKind kind
596               final_name = mkInternalName uniq (getOccName tv) span
597               final_tv   = mkTcTyVar final_name final_kind details
598
599         ; writeMetaTyVar tv (mkTyVarTy final_tv)
600         ; return final_tv }
601
602 skolemiseSigTv :: TcTyVar -> TcM TcTyVar
603 -- In TcBinds we create SigTvs for type signatures
604 -- but for singleton groups we want them to really be skolems
605 -- which do not unify with each other
606 skolemiseSigTv tv  
607   = ASSERT2( isSigTyVar tv, ppr tv )
608     do { writeMetaTyVarRef tv (metaTvRef tv) (mkTyVarTy skol_tv)
609        ; return skol_tv }
610   where
611     skol_tv = setTcTyVarDetails tv (SkolemTv False)
612 \end{code}
613
614 Note [Zonking to Skolem]
615 ~~~~~~~~~~~~~~~~~~~~~~~~
616 We used to zonk quantified type variables to regular TyVars.  However, this
617 leads to problems.  Consider this program from the regression test suite:
618
619   eval :: Int -> String -> String -> String
620   eval 0 root actual = evalRHS 0 root actual
621
622   evalRHS :: Int -> a
623   evalRHS 0 root actual = eval 0 root actual
624
625 It leads to the deferral of an equality (wrapped in an implication constraint)
626
627   forall a. () => ((String -> String -> String) ~ a)
628
629 which is propagated up to the toplevel (see TcSimplify.tcSimplifyInferCheck).
630 In the meantime `a' is zonked and quantified to form `evalRHS's signature.
631 This has the *side effect* of also zonking the `a' in the deferred equality
632 (which at this point is being handed around wrapped in an implication
633 constraint).
634
635 Finally, the equality (with the zonked `a') will be handed back to the
636 simplifier by TcRnDriver.tcRnSrcDecls calling TcSimplify.tcSimplifyTop.
637 If we zonk `a' with a regular type variable, we will have this regular type
638 variable now floating around in the simplifier, which in many places assumes to
639 only see proper TcTyVars.
640
641 We can avoid this problem by zonking with a skolem.  The skolem is rigid
642 (which we require for a quantified variable), but is still a TcTyVar that the
643 simplifier knows how to deal with.
644
645 Note [Silly Type Synonyms]
646 ~~~~~~~~~~~~~~~~~~~~~~~~~~
647 Consider this:
648         type C u a = u  -- Note 'a' unused
649
650         foo :: (forall a. C u a -> C u a) -> u
651         foo x = ...
652
653         bar :: Num u => u
654         bar = foo (\t -> t + t)
655
656 * From the (\t -> t+t) we get type  {Num d} =>  d -> d
657   where d is fresh.
658
659 * Now unify with type of foo's arg, and we get:
660         {Num (C d a)} =>  C d a -> C d a
661   where a is fresh.
662
663 * Now abstract over the 'a', but float out the Num (C d a) constraint
664   because it does not 'really' mention a.  (see exactTyVarsOfType)
665   The arg to foo becomes
666         \/\a -> \t -> t+t
667
668 * So we get a dict binding for Num (C d a), which is zonked to give
669         a = ()
670   [Note Sept 04: now that we are zonking quantified type variables
671   on construction, the 'a' will be frozen as a regular tyvar on
672   quantification, so the floated dict will still have type (C d a).
673   Which renders this whole note moot; happily!]
674
675 * Then the \/\a abstraction has a zonked 'a' in it.
676
677 All very silly.   I think its harmless to ignore the problem.  We'll end up with
678 a \/\a in the final result but all the occurrences of a will be zonked to ()
679
680 %************************************************************************
681 %*                                                                      *
682               Zonking
683 %*                                                                      *
684 %************************************************************************
685
686 @tcGetGlobalTyVars@ returns a fully-zonked set of tyvars free in the environment.
687 To improve subsequent calls to the same function it writes the zonked set back into
688 the environment.
689
690 \begin{code}
691 tcGetGlobalTyVars :: TcM TcTyVarSet
692 tcGetGlobalTyVars
693   = do { (TcLclEnv {tcl_tyvars = gtv_var}) <- getLclEnv
694        ; gbl_tvs  <- readMutVar gtv_var
695        ; gbl_tvs' <- zonkTyVarsAndFV gbl_tvs
696        ; writeMutVar gtv_var gbl_tvs'
697        ; return gbl_tvs' }
698   where
699 \end{code}
700
701 -----------------  Type variables
702
703 \begin{code}
704 zonkTcTypeAndFV :: TcType -> TcM TyVarSet
705 -- Zonk a type and take its free variables
706 -- With kind polymorphism it can be essential to zonk *first*
707 -- so that we find the right set of free variables.  Eg
708 --    forall k1. forall (a:k2). a
709 -- where k2:=k1 is in the substitution.  We don't want
710 -- k2 to look free in this type!
711 zonkTcTypeAndFV ty = do { ty <- zonkTcType ty; return (tyVarsOfType ty) }
712
713 zonkTyVar :: TyVar -> TcM TcType
714 -- Works on TyVars and TcTyVars
715 zonkTyVar tv | isTcTyVar tv = zonkTcTyVar tv
716              | otherwise    = return (mkTyVarTy tv)
717    -- Hackily, when typechecking type and class decls
718    -- we have TyVars in scopeadded (only) in 
719    -- TcHsType.tcTyClTyVars, but it seems
720    -- painful to make them into TcTyVars there
721
722 zonkTyVarsAndFV :: TyVarSet -> TcM TyVarSet
723 zonkTyVarsAndFV tyvars = tyVarsOfTypes <$> mapM zonkTyVar (varSetElems tyvars)
724
725 zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
726 zonkTcTyVars tyvars = mapM zonkTcTyVar tyvars
727
728 -----------------  Types
729 zonkTyVarKind :: TyVar -> TcM TyVar
730 zonkTyVarKind tv = do { kind' <- zonkTcKind (tyVarKind tv)
731                       ; return (setTyVarKind tv kind') }
732
733 zonkTcTypes :: [TcType] -> TcM [TcType]
734 zonkTcTypes tys = mapM zonkTcType tys
735
736 zonkTcThetaType :: TcThetaType -> TcM TcThetaType
737 zonkTcThetaType theta = mapM zonkTcPredType theta
738
739 zonkTcPredType :: TcPredType -> TcM TcPredType
740 zonkTcPredType = zonkTcType
741 \end{code}
742
743 ---------------  Constraints
744
745 \begin{code}
746 zonkImplication :: Implication -> TcM (Bag Implication)
747 zonkImplication implic@(Implic { ic_untch  = untch
748                                , ic_binds  = binds_var
749                                , ic_skols  = skols
750                                , ic_given  = given
751                                , ic_wanted = wanted
752                                , ic_info   = info })
753   = do { skols'  <- mapM zonkTcTyVarBndr skols  -- Need to zonk their kinds!
754                                                 -- as Trac #7230 showed
755        ; given'  <- mapM zonkEvVar given
756        ; info'   <- zonkSkolemInfo info
757        ; wanted' <- zonkWCRec binds_var untch wanted
758        ; if isEmptyWC wanted' 
759          then return emptyBag
760          else return $ unitBag $
761               implic { ic_fsks   = []  -- Zonking removes all FlatSkol tyvars
762                      , ic_skols  = skols'
763                      , ic_given  = given'
764                      , ic_wanted = wanted'
765                      , ic_info   = info' } }
766
767 zonkEvVar :: EvVar -> TcM EvVar
768 zonkEvVar var = do { ty' <- zonkTcType (varType var)
769                    ; return (setVarType var ty') }
770
771
772 zonkWC :: EvBindsVar -- May add new bindings for wanted family equalities in here
773        -> WantedConstraints -> TcM WantedConstraints
774 zonkWC binds_var wc
775   = do { untch <- getUntouchables
776        ; zonkWCRec binds_var untch wc }
777
778 zonkWCRec :: EvBindsVar
779           -> Untouchables
780           -> WantedConstraints -> TcM WantedConstraints
781 zonkWCRec binds_var untch (WC { wc_flat = flat, wc_impl = implic, wc_insol = insol })
782   = do { flat'   <- zonkFlats binds_var untch flat
783        ; implic' <- flatMapBagM zonkImplication implic
784        ; insol'  <- zonkCts insol -- No need to do the more elaborate zonkFlats thing
785        ; return (WC { wc_flat = flat', wc_impl = implic', wc_insol = insol' }) }
786
787 zonkFlats :: EvBindsVar -> Untouchables -> Cts -> TcM Cts
788 -- This zonks and unflattens a bunch of flat constraints
789 -- See Note [Unflattening while zonking]
790 zonkFlats binds_var untch cts
791   = do { -- See Note [How to unflatten]
792          cts <- foldrBagM unflatten_one emptyCts cts
793        ; zonkCts cts }
794   where
795     unflatten_one orig_ct cts
796       = do { zct <- zonkCt orig_ct                -- First we need to fully zonk 
797            ; mct <- try_zonk_fun_eq orig_ct zct   -- Then try to solve if family equation
798            ; return $ maybe cts (`consBag` cts) mct }
799
800     try_zonk_fun_eq orig_ct zct   -- See Note [How to unflatten]
801       | EqPred ty_lhs ty_rhs <- classifyPredType (ctPred zct)
802           -- NB: zonking de-classifies the constraint,
803           --     so we can't look for CFunEqCan
804       , Just tv <- getTyVar_maybe ty_rhs
805       , ASSERT2( not (isFloatedTouchableMetaTyVar untch tv), ppr tv )
806         isTouchableMetaTyVar untch tv
807       , not (isSigTyVar tv) || isTyVarTy ty_lhs     -- Never unify a SigTyVar with a non-tyvar
808       , typeKind ty_lhs `tcIsSubKind` tyVarKind tv  -- c.f. TcInteract.trySpontaneousEqOneWay
809       , not (tv `elemVarSet` tyVarsOfType ty_lhs)   -- Do not construct an infinite type
810       = ASSERT2( case tcSplitTyConApp_maybe ty_lhs of { Just (tc,_) -> isSynFamilyTyCon tc; _ -> False }, ppr orig_ct )
811         do { writeMetaTyVar tv ty_lhs
812            ; let evterm = EvCoercion (mkTcNomReflCo ty_lhs)
813                  evvar  = ctev_evar (cc_ev zct)
814            ; when (isWantedCt orig_ct) $         -- Can be derived (Trac #8129)
815              addTcEvBind binds_var evvar evterm
816            ; traceTc "zonkFlats/unflattening" $
817              vcat [ text "zct = " <+> ppr zct,
818                     text "binds_var = " <+> ppr binds_var ]
819            ; return Nothing }
820       | otherwise
821       = return (Just zct)
822 \end{code}
823
824 Note [Unflattening while zonking]
825 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
826 A bunch of wanted constraints could contain wanted equations of the form
827 (F taus ~ alpha) where alpha is either an ordinary unification variable, or
828 a flatten unification variable.
829
830 These are ordinary wanted constraints and can/should be solved by
831 ordinary unification alpha := F taus. However the constraint solving
832 algorithm does not do that, as their 'inert' form is F taus ~ alpha.
833
834 Hence, we need an extra step to 'unflatten' these equations by
835 performing unification. This unification, if it happens at the end of
836 constraint solving, cannot produce any more interactions in the
837 constraint solver so it is safe to do it as the very very last step.
838
839 We choose therefore to do it during zonking, in the function
840 zonkFlats. This is in analogy to the zonking of given "flatten skolems"
841 which are eliminated in favor of the underlying type that they are
842 equal to.
843
844 Note that, because we now have to affect *evidence* while zonking
845 (setting some evidence binds to identities), we have to pass to the
846 zonkWC function an evidence variable to collect all the extra
847 variables.
848
849 Note [How to unflatten]
850 ~~~~~~~~~~~~~~~~~~~~~~~
851 How do we unflatten during zonking.  Consider a bunch of flat constraints.
852 Consider them one by one.  For each such constraint C
853   * Zonk C (to apply current substitution)
854   * If C is of form F tys ~ alpha, 
855        where alpha is touchable
856        and   alpha is not mentioned in tys
857     then unify alpha := F tys
858          and discard C
859
860 After processing all the flat constraints, zonk them again to propagate
861 the inforamtion from later ones to earlier ones.  Eg
862   Start:  (F alpha ~ beta, G Int ~ alpha)
863   Then we get beta := F alpha
864               alpha := G Int
865   but we must apply the second unification to the first constraint.
866
867
868 \begin{code}
869 zonkCts :: Cts -> TcM Cts
870 zonkCts = mapBagM zonkCt
871
872 zonkCt :: Ct -> TcM Ct
873 zonkCt ct@(CHoleCan { cc_ev = ev })
874   = do { ev' <- zonkCtEvidence ev
875        ; return $ ct { cc_ev = ev' } }
876 zonkCt ct
877   = do { fl' <- zonkCtEvidence (cc_ev ct)
878        ; return (mkNonCanonical fl') }
879
880 zonkCtEvidence :: CtEvidence -> TcM CtEvidence
881 zonkCtEvidence ctev@(CtGiven { ctev_pred = pred }) 
882   = do { pred' <- zonkTcType pred
883        ; return (ctev { ctev_pred = pred'}) }
884 zonkCtEvidence ctev@(CtWanted { ctev_pred = pred })
885   = do { pred' <- zonkTcType pred
886        ; return (ctev { ctev_pred = pred' }) }
887 zonkCtEvidence ctev@(CtDerived { ctev_pred = pred })
888   = do { pred' <- zonkTcType pred
889        ; return (ctev { ctev_pred = pred' }) }
890
891 zonkSkolemInfo :: SkolemInfo -> TcM SkolemInfo
892 zonkSkolemInfo (SigSkol cx ty)  = do { ty' <- zonkTcType ty
893                                      ; return (SigSkol cx ty') }
894 zonkSkolemInfo (InferSkol ntys) = do { ntys' <- mapM do_one ntys
895                                      ; return (InferSkol ntys') }
896   where
897     do_one (n, ty) = do { ty' <- zonkTcType ty; return (n, ty') }
898 zonkSkolemInfo skol_info = return skol_info
899 \end{code}
900
901
902
903 %************************************************************************
904 %*                                                                      *
905 \subsection{Zonking -- the main work-horses: zonkTcType, zonkTcTyVar}
906 %*                                                                      *
907 %*              For internal use only!                                  *
908 %*                                                                      *
909 %************************************************************************
910
911 \begin{code}
912 -- zonkId is used *during* typechecking just to zonk the Id's type
913 zonkId :: TcId -> TcM TcId
914 zonkId id
915   = do { ty' <- zonkTcType (idType id)
916        ; return (Id.setIdType id ty') }
917
918 -- For unbound, mutable tyvars, zonkType uses the function given to it
919 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
920 --      type variable and zonks the kind too
921
922 zonkTcType :: TcType -> TcM TcType
923 zonkTcType ty
924   = go ty
925   where
926     go (TyConApp tc tys) = do tys' <- mapM go tys
927                               return (TyConApp tc tys')
928                 -- Do NOT establish Type invariants, because
929                 -- doing so is strict in the TyCOn.
930                 -- See Note [Zonking inside the knot] in TcHsType
931
932     go (LitTy n)         = return (LitTy n)
933
934     go (FunTy arg res)   = do arg' <- go arg
935                               res' <- go res
936                               return (FunTy arg' res')
937
938     go (AppTy fun arg)   = do fun' <- go fun
939                               arg' <- go arg
940                               return (mkAppTy fun' arg')
941                 -- NB the mkAppTy; we might have instantiated a
942                 -- type variable to a type constructor, so we need
943                 -- to pull the TyConApp to the top.
944                 -- OK to do this because only strict in the structure
945                 -- not in the TyCon.
946                 -- See Note [Zonking inside the knot] in TcHsType
947
948         -- The two interesting cases!
949     go (TyVarTy tyvar) | isTcTyVar tyvar = zonkTcTyVar tyvar
950                        | otherwise       = TyVarTy <$> updateTyVarKindM go tyvar
951                 -- Ordinary (non Tc) tyvars occur inside quantified types
952
953     go (ForAllTy tv ty) = do { tv' <- zonkTcTyVarBndr tv
954                              ; ty' <- go ty
955                              ; return (ForAllTy tv' ty') }
956
957 zonkTcTyVarBndr :: TcTyVar -> TcM TcTyVar
958 -- A tyvar binder is never a unification variable (MetaTv),
959 -- rather it is always a skolems.  BUT it may have a kind 
960 -- that has not yet been zonked, and may include kind
961 -- unification variables.
962 zonkTcTyVarBndr tyvar
963   = ASSERT2( isImmutableTyVar tyvar, ppr tyvar ) do
964     updateTyVarKindM zonkTcType tyvar
965
966 zonkTcTyVar :: TcTyVar -> TcM TcType
967 -- Simply look through all Flexis
968 zonkTcTyVar tv
969   = ASSERT2( isTcTyVar tv, ppr tv ) do
970     case tcTyVarDetails tv of
971       SkolemTv {}   -> zonk_kind_and_return
972       RuntimeUnk {} -> zonk_kind_and_return
973       FlatSkol ty   -> zonkTcType ty
974       MetaTv { mtv_ref = ref }
975          -> do { cts <- readMutVar ref
976                ; case cts of
977                     Flexi       -> zonk_kind_and_return
978                     Indirect ty -> zonkTcType ty }
979   where
980     zonk_kind_and_return = do { z_tv <- zonkTyVarKind tv
981                               ; return (TyVarTy z_tv) }
982 \end{code}
983
984
985
986 %************************************************************************
987 %*                                                                      *
988                         Zonking kinds
989 %*                                                                      *
990 %************************************************************************
991
992 \begin{code}
993 zonkTcKind :: TcKind -> TcM TcKind
994 zonkTcKind k = zonkTcType k
995 \end{code}
996     
997
998