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