(Another) minor refactoring of substitutions
[ghc.git] / compiler / typecheck / TcMType.hs
1 {-
2 (c) The University of Glasgow 2006
3 (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4
5
6 Monadic type operations
7
8 This module contains monadic operations over types that contain
9 mutable type variables
10 -}
11
12 {-# LANGUAGE CPP, TupleSections, MultiWayIf #-}
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 newOpenFlexiTyVarTy,
23 newMetaKindVar, newMetaKindVars,
24 cloneMetaTyVar,
25 newFmvTyVar, newFskTyVar,
26
27 readMetaTyVar, writeMetaTyVar, writeMetaTyVarRef,
28 newMetaDetails, isFilledMetaTyVar, isUnfilledMetaTyVar,
29
30 --------------------------------
31 -- Expected types
32 ExpType(..), ExpSigmaType, ExpRhoType,
33 mkCheckExpType, newOpenInferExpType, readExpType, readExpType_maybe,
34 writeExpType, expTypeToType, checkingExpType_maybe, checkingExpType,
35 tauifyExpType,
36
37 --------------------------------
38 -- Creating fresh type variables for pm checking
39 genInstSkolTyVarsX,
40
41 --------------------------------
42 -- Creating new evidence variables
43 newEvVar, newEvVars, newDict,
44 newWanted, newWanteds,
45 emitWanted, emitWantedEq, emitWantedEvVar, emitWantedEvVars,
46 newTcEvBinds, addTcEvBind,
47
48 newCoercionHole, fillCoercionHole, isFilledCoercionHole,
49 unpackCoercionHole, unpackCoercionHole_maybe,
50 checkCoercionHole,
51
52 --------------------------------
53 -- Instantiation
54 newMetaTyVars, newMetaTyVarX, newMetaSigTyVars,
55 newSigTyVar,
56 tcInstType,
57 tcInstSkolTyVars, tcInstSkolTyVarsLoc, tcInstSuperSkolTyVarsX,
58 tcInstSigTyVarsLoc, tcInstSigTyVars,
59 tcInstSkolType,
60 tcSkolDFunType, tcSuperSkolTyVars,
61
62 instSkolTyCoVars, freshenTyVarBndrs, freshenCoVarBndrsX,
63
64 --------------------------------
65 -- Zonking and tidying
66 zonkTidyTcType, zonkTidyOrigin,
67 mkTypeErrorThing, mkTypeErrorThingArgs,
68 tidyEvVar, tidyCt, tidySkolemInfo,
69 skolemiseUnboundMetaTyVar,
70 zonkTcTyVar, zonkTcTyVars, zonkTyCoVarsAndFV, zonkTcTypeAndFV,
71 zonkQuantifiedTyVar, zonkQuantifiedTyVarOrType, quantifyTyVars,
72 defaultKindVar,
73 zonkTcTyCoVarBndr, zonkTcType, zonkTcTypes, zonkCo,
74 zonkTyCoVarKind, zonkTcTypeMapper,
75
76 zonkEvVar, zonkWC, zonkSimples, zonkId, zonkCt, zonkSkolemInfo,
77
78 tcGetGlobalTyCoVars
79 ) where
80
81 #include "HsVersions.h"
82
83 -- friends:
84 import TyCoRep
85 import TcType
86 import Type
87 import Coercion
88 import Class
89 import Var
90
91 -- others:
92 import TcRnMonad -- TcType, amongst others
93 import TcEvidence
94 import Id
95 import Name
96 import VarSet
97 import TysWiredIn
98 import TysPrim
99 import VarEnv
100 import PrelNames
101 import Util
102 import Outputable
103 import FastString
104 import SrcLoc
105 import Bag
106 import Pair
107 import qualified GHC.LanguageExtensions as LangExt
108
109 import Control.Monad
110 import Maybes
111 import Data.List ( mapAccumL, partition )
112 import Control.Arrow ( second )
113
114 {-
115 ************************************************************************
116 * *
117 Kind variables
118 * *
119 ************************************************************************
120 -}
121
122 mkKindName :: Unique -> Name
123 mkKindName unique = mkSystemName unique kind_var_occ
124
125 kind_var_occ :: OccName -- Just one for all MetaKindVars
126 -- They may be jiggled by tidying
127 kind_var_occ = mkOccName tvName "k"
128
129 newMetaKindVar :: TcM TcKind
130 newMetaKindVar = do { uniq <- newUnique
131 ; details <- newMetaDetails TauTv
132 ; let kv = mkTcTyVar (mkKindName uniq) liftedTypeKind details
133 ; return (mkTyVarTy kv) }
134
135 newMetaKindVars :: Int -> TcM [TcKind]
136 newMetaKindVars n = mapM (\ _ -> newMetaKindVar) (nOfThem n ())
137
138 {-
139 ************************************************************************
140 * *
141 Evidence variables; range over constraints we can abstract over
142 * *
143 ************************************************************************
144 -}
145
146 newEvVars :: TcThetaType -> TcM [EvVar]
147 newEvVars theta = mapM newEvVar theta
148
149 --------------
150
151 newEvVar :: TcPredType -> TcRnIf gbl lcl EvVar
152 -- Creates new *rigid* variables for predicates
153 newEvVar ty = do { name <- newSysName (predTypeOccName ty)
154 ; return (mkLocalIdOrCoVar name ty) }
155
156 newWanted :: CtOrigin -> Maybe TypeOrKind -> PredType -> TcM CtEvidence
157 -- Deals with both equality and non-equality predicates
158 newWanted orig t_or_k pty
159 = do loc <- getCtLocM orig t_or_k
160 d <- if isEqPred pty then HoleDest <$> newCoercionHole
161 else EvVarDest <$> newEvVar pty
162 return $ CtWanted { ctev_dest = d
163 , ctev_pred = pty
164 , ctev_loc = loc }
165
166 newWanteds :: CtOrigin -> ThetaType -> TcM [CtEvidence]
167 newWanteds orig = mapM (newWanted orig Nothing)
168
169 -- | Emits a new Wanted. Deals with both equalities and non-equalities.
170 emitWanted :: CtOrigin -> TcPredType -> TcM EvTerm
171 emitWanted origin pty
172 = do { ev <- newWanted origin Nothing pty
173 ; emitSimple $ mkNonCanonical ev
174 ; return $ ctEvTerm ev }
175
176 -- | Emits a new equality constraint
177 emitWantedEq :: CtOrigin -> TypeOrKind -> Role -> TcType -> TcType -> TcM Coercion
178 emitWantedEq origin t_or_k role ty1 ty2
179 = do { hole <- newCoercionHole
180 ; loc <- getCtLocM origin (Just t_or_k)
181 ; emitSimple $ mkNonCanonical $
182 CtWanted { ctev_pred = pty, ctev_dest = HoleDest hole, ctev_loc = loc }
183 ; return (mkHoleCo hole role ty1 ty2) }
184 where
185 pty = mkPrimEqPredRole role ty1 ty2
186
187 -- | Creates a new EvVar and immediately emits it as a Wanted.
188 -- No equality predicates here.
189 emitWantedEvVar :: CtOrigin -> TcPredType -> TcM EvVar
190 emitWantedEvVar origin ty
191 = do { new_cv <- newEvVar ty
192 ; loc <- getCtLocM origin Nothing
193 ; let ctev = CtWanted { ctev_dest = EvVarDest new_cv
194 , ctev_pred = ty
195 , ctev_loc = loc }
196 ; emitSimple $ mkNonCanonical ctev
197 ; return new_cv }
198
199 emitWantedEvVars :: CtOrigin -> [TcPredType] -> TcM [EvVar]
200 emitWantedEvVars orig = mapM (emitWantedEvVar orig)
201
202 newDict :: Class -> [TcType] -> TcM DictId
203 newDict cls tys
204 = do { name <- newSysName (mkDictOcc (getOccName cls))
205 ; return (mkLocalId name (mkClassPred cls tys)) }
206
207 predTypeOccName :: PredType -> OccName
208 predTypeOccName ty = case classifyPredType ty of
209 ClassPred cls _ -> mkDictOcc (getOccName cls)
210 EqPred _ _ _ -> mkVarOccFS (fsLit "cobox")
211 IrredPred _ -> mkVarOccFS (fsLit "irred")
212
213 {-
214 ************************************************************************
215 * *
216 Coercion holes
217 * *
218 ************************************************************************
219 -}
220
221 newCoercionHole :: TcM CoercionHole
222 newCoercionHole
223 = do { u <- newUnique
224 ; traceTc "New coercion hole:" (ppr u)
225 ; ref <- newMutVar Nothing
226 ; return $ CoercionHole u ref }
227
228 -- | Put a value in a coercion hole
229 fillCoercionHole :: CoercionHole -> Coercion -> TcM ()
230 fillCoercionHole (CoercionHole u ref) co
231 = do {
232 #ifdef DEBUG
233 ; cts <- readTcRef ref
234 ; whenIsJust cts $ \old_co ->
235 pprPanic "Filling a filled coercion hole" (ppr u $$ ppr co $$ ppr old_co)
236 #endif
237 ; traceTc "Filling coercion hole" (ppr u <+> text ":=" <+> ppr co)
238 ; writeTcRef ref (Just co) }
239
240 -- | Is a coercion hole filled in?
241 isFilledCoercionHole :: CoercionHole -> TcM Bool
242 isFilledCoercionHole (CoercionHole _ ref) = isJust <$> readTcRef ref
243
244 -- | Retrieve the contents of a coercion hole. Panics if the hole
245 -- is unfilled
246 unpackCoercionHole :: CoercionHole -> TcM Coercion
247 unpackCoercionHole hole
248 = do { contents <- unpackCoercionHole_maybe hole
249 ; case contents of
250 Just co -> return co
251 Nothing -> pprPanic "Unfilled coercion hole" (ppr hole) }
252
253 -- | Retrieve the contents of a coercion hole, if it is filled
254 unpackCoercionHole_maybe :: CoercionHole -> TcM (Maybe Coercion)
255 unpackCoercionHole_maybe (CoercionHole _ ref) = readTcRef ref
256
257 -- | Check that a coercion is appropriate for filling a hole. (The hole
258 -- itself is needed only for printing. NB: This must be /lazy/ in the coercion,
259 -- as it's used in TcHsSyn in the presence of knots.
260 -- Always returns the checked coercion, but this return value is necessary
261 -- so that the input coercion is forced only when the output is forced.
262 checkCoercionHole :: Coercion -> CoercionHole -> Role -> Type -> Type -> TcM Coercion
263 checkCoercionHole co h r t1 t2
264 -- co is already zonked, but t1 and t2 might not be
265 | debugIsOn
266 = do { t1 <- zonkTcType t1
267 ; t2 <- zonkTcType t2
268 ; let (Pair _t1 _t2, _role) = coercionKindRole co
269 ; return $
270 ASSERT2( t1 `eqType` _t1 && t2 `eqType` _t2 && r == _role
271 , (text "Bad coercion hole" <+>
272 ppr h <> colon <+> vcat [ ppr _t1, ppr _t2, ppr _role
273 , ppr co, ppr t1, ppr t2
274 , ppr r ]) )
275 co }
276 | otherwise
277 = return co
278
279 {-
280 ************************************************************************
281 *
282 Expected types
283 *
284 ************************************************************************
285
286 Note [ExpType]
287 ~~~~~~~~~~~~~~
288
289 An ExpType is used as the "expected type" when type-checking an expression.
290 An ExpType can hold a "hole" that can be filled in by the type-checker.
291 This allows us to have one tcExpr that works in both checking mode and
292 synthesis mode (that is, bidirectional type-checking). Previously, this
293 was achieved by using ordinary unification variables, but we don't need
294 or want that generality. (For example, #11397 was caused by doing the
295 wrong thing with unification variables.) Instead, we observe that these
296 holes should
297
298 1. never be nested
299 2. never appear as the type of a variable
300 3. be used linearly (never be duplicated)
301
302 By defining ExpType, separately from Type, we can achieve goals 1 and 2
303 statically.
304
305 See also [wiki:Typechecking]
306
307 Note [TcLevel of ExpType]
308 ~~~~~~~~~~~~~~~~~~~~~~~~~
309 Consider
310
311 data G a where
312 MkG :: G Bool
313
314 foo MkG = True
315
316 This is a classic untouchable-variable / ambiguous GADT return type
317 scenario. But, with ExpTypes, we'll be inferring the type of the RHS.
318 And, because there is only one branch of the case, we won't trigger
319 Note [Case branches must never infer a non-tau type] of TcMatches.
320 We thus must track a TcLevel in an Inferring ExpType. If we try to
321 fill the ExpType and find that the TcLevels don't work out, we
322 fill the ExpType with a tau-tv at the low TcLevel, hopefully to
323 be worked out later by some means. This is triggered in
324 test gadt/gadt-escape1.
325
326 -}
327
328 -- actual data definition is in TcType
329
330 -- | Make an 'ExpType' suitable for inferring a type of kind * or #.
331 newOpenInferExpType :: TcM ExpType
332 newOpenInferExpType
333 = do { lev <- newFlexiTyVarTy levityTy
334 ; u <- newUnique
335 ; tclvl <- getTcLevel
336 ; let ki = tYPE lev
337 ; traceTc "newOpenInferExpType" (ppr u <+> dcolon <+> ppr ki)
338 ; ref <- newMutVar Nothing
339 ; return (Infer u tclvl ki ref) }
340
341 -- | Extract a type out of an ExpType, if one exists. But one should always
342 -- exist. Unless you're quite sure you know what you're doing.
343 readExpType_maybe :: ExpType -> TcM (Maybe TcType)
344 readExpType_maybe (Check ty) = return (Just ty)
345 readExpType_maybe (Infer _ _ _ ref) = readMutVar ref
346
347 -- | Extract a type out of an ExpType. Otherwise, panics.
348 readExpType :: ExpType -> TcM TcType
349 readExpType exp_ty
350 = do { mb_ty <- readExpType_maybe exp_ty
351 ; case mb_ty of
352 Just ty -> return ty
353 Nothing -> pprPanic "Unknown expected type" (ppr exp_ty) }
354
355 -- | Write into an 'ExpType'. It must be an 'Infer'.
356 writeExpType :: ExpType -> TcType -> TcM ()
357 writeExpType (Infer u tc_lvl ki ref) ty
358 | debugIsOn
359 = do { ki1 <- zonkTcType (typeKind ty)
360 ; ki2 <- zonkTcType ki
361 ; MASSERT2( ki1 `eqType` ki2, ppr ki1 $$ ppr ki2 $$ ppr u )
362 ; lvl_now <- getTcLevel
363 ; MASSERT2( tc_lvl == lvl_now, ppr u $$ ppr tc_lvl $$ ppr lvl_now )
364 ; cts <- readTcRef ref
365 ; case cts of
366 Just already_there -> pprPanic "writeExpType"
367 (vcat [ ppr u
368 , ppr ty
369 , ppr already_there ])
370 Nothing -> write }
371 | otherwise
372 = write
373 where
374 write = do { traceTc "Filling ExpType" $
375 ppr u <+> text ":=" <+> ppr ty
376 ; writeTcRef ref (Just ty) }
377 writeExpType (Check ty1) ty2 = pprPanic "writeExpType" (ppr ty1 $$ ppr ty2)
378
379 -- | Returns the expected type when in checking mode.
380 checkingExpType_maybe :: ExpType -> Maybe TcType
381 checkingExpType_maybe (Check ty) = Just ty
382 checkingExpType_maybe _ = Nothing
383
384 -- | Returns the expected type when in checking mode. Panics if in inference
385 -- mode.
386 checkingExpType :: String -> ExpType -> TcType
387 checkingExpType _ (Check ty) = ty
388 checkingExpType err et = pprPanic "checkingExpType" (text err $$ ppr et)
389
390 tauifyExpType :: ExpType -> TcM ExpType
391 -- ^ Turn a (Infer hole) type into a (Check alpha),
392 -- where alpha is a fresh unificaiton variable
393 tauifyExpType exp_ty = do { ty <- expTypeToType exp_ty
394 ; return (Check ty) }
395
396 -- | Extracts the expected type if there is one, or generates a new
397 -- TauTv if there isn't.
398 expTypeToType :: ExpType -> TcM TcType
399 expTypeToType (Check ty) = return ty
400 expTypeToType (Infer u tc_lvl ki ref)
401 = do { uniq <- newUnique
402 ; tv_ref <- newMutVar Flexi
403 ; let details = MetaTv { mtv_info = TauTv
404 , mtv_ref = tv_ref
405 , mtv_tclvl = tc_lvl }
406 name = mkMetaTyVarName uniq (fsLit "t")
407 tau_tv = mkTcTyVar name ki details
408 tau = mkTyVarTy tau_tv
409 -- can't use newFlexiTyVarTy because we need to set the tc_lvl
410 -- See also Note [TcLevel of ExpType]
411
412 ; writeMutVar ref (Just tau)
413 ; traceTc "Forcing ExpType to be monomorphic:"
414 (ppr u <+> dcolon <+> ppr ki <+> text ":=" <+> ppr tau)
415 ; return tau }
416
417 {-
418 ************************************************************************
419 * *
420 SkolemTvs (immutable)
421 * *
422 ************************************************************************
423 -}
424
425 tcInstType :: ([TyVar] -> TcM (TCvSubst, [TcTyVar]))
426 -- ^ How to instantiate the type variables
427 -> TcType -- ^ Type to instantiate
428 -> TcM ([TcTyVar], TcThetaType, TcType) -- ^ Result
429 -- (type vars, preds (incl equalities), rho)
430 tcInstType inst_tyvars ty
431 = case tcSplitForAllTys ty of
432 ([], rho) -> let -- There may be overloading despite no type variables;
433 -- (?x :: Int) => Int -> Int
434 (theta, tau) = tcSplitPhiTy rho
435 in
436 return ([], theta, tau)
437
438 (tyvars, rho) -> do { (subst, tyvars') <- inst_tyvars tyvars
439 ; let (theta, tau) = tcSplitPhiTy (substTyUnchecked subst rho)
440 ; return (tyvars', theta, tau) }
441
442 tcSkolDFunType :: Type -> TcM ([TcTyVar], TcThetaType, TcType)
443 -- Instantiate a type signature with skolem constants.
444 -- We could give them fresh names, but no need to do so
445 tcSkolDFunType ty = tcInstType tcInstSuperSkolTyVars ty
446
447 tcSuperSkolTyVars :: [TyVar] -> (TCvSubst, [TcTyVar])
448 -- Make skolem constants, but do *not* give them new names, as above
449 -- Moreover, make them "super skolems"; see comments with superSkolemTv
450 -- see Note [Kind substitution when instantiating]
451 -- Precondition: tyvars should be ordered by scoping
452 tcSuperSkolTyVars = mapAccumL tcSuperSkolTyVar emptyTCvSubst
453
454 tcSuperSkolTyVar :: TCvSubst -> TyVar -> (TCvSubst, TcTyVar)
455 tcSuperSkolTyVar subst tv
456 = (extendTvSubstWithClone subst tv new_tv, new_tv)
457 where
458 kind = substTyUnchecked subst (tyVarKind tv)
459 new_tv = mkTcTyVar (tyVarName tv) kind superSkolemTv
460
461 -- Wrappers
462 -- we need to be able to do this from outside the TcM monad:
463 tcInstSkolTyVarsLoc :: SrcSpan -> [TyVar] -> TcRnIf gbl lcl (TCvSubst, [TcTyVar])
464 tcInstSkolTyVarsLoc loc = instSkolTyCoVars (mkTcSkolTyVar loc False)
465
466 tcInstSkolTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
467 tcInstSkolTyVars = tcInstSkolTyVars' False emptyTCvSubst
468
469 tcInstSuperSkolTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
470 tcInstSuperSkolTyVars = tcInstSuperSkolTyVarsX emptyTCvSubst
471
472 tcInstSuperSkolTyVarsX :: TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
473 tcInstSuperSkolTyVarsX subst = tcInstSkolTyVars' True subst
474
475 tcInstSkolTyVars' :: Bool -> TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
476 -- Precondition: tyvars should be ordered (kind vars first)
477 -- see Note [Kind substitution when instantiating]
478 -- Get the location from the monad; this is a complete freshening operation
479 tcInstSkolTyVars' overlappable subst tvs
480 = do { loc <- getSrcSpanM
481 ; instSkolTyCoVarsX (mkTcSkolTyVar loc overlappable) subst tvs }
482
483 mkTcSkolTyVar :: SrcSpan -> Bool -> Unique -> Name -> Kind -> TcTyVar
484 mkTcSkolTyVar loc overlappable uniq old_name kind
485 = mkTcTyVar (mkInternalName uniq (getOccName old_name) loc)
486 kind
487 (SkolemTv overlappable)
488
489 tcInstSigTyVarsLoc :: SrcSpan -> [TyVar]
490 -> TcRnIf gbl lcl (TCvSubst, [TcTyVar])
491 -- We specify the location
492 tcInstSigTyVarsLoc loc = instSkolTyCoVars (mkTcSkolTyVar loc False)
493
494 tcInstSigTyVars :: [TyVar] -> TcRnIf gbl lcl (TCvSubst, [TcTyVar])
495 -- Get the location from the TyVar itself, not the monad
496 tcInstSigTyVars
497 = instSkolTyCoVars mk_tv
498 where
499 mk_tv uniq old_name kind
500 = mkTcTyVar (setNameUnique old_name uniq) kind (SkolemTv False)
501
502 tcInstSkolType :: TcType -> TcM ([TcTyVar], TcThetaType, TcType)
503 -- Instantiate a type with fresh skolem constants
504 -- Binding location comes from the monad
505 tcInstSkolType ty = tcInstType tcInstSkolTyVars ty
506
507 ------------------
508 freshenTyVarBndrs :: [TyVar] -> TcRnIf gbl lcl (TCvSubst, [TyVar])
509 -- ^ Give fresh uniques to a bunch of TyVars, but they stay
510 -- as TyVars, rather than becoming TcTyVars
511 -- Used in FamInst.newFamInst, and Inst.newClsInst
512 freshenTyVarBndrs = instSkolTyCoVars mk_tv
513 where
514 mk_tv uniq old_name kind = mkTyVar (setNameUnique old_name uniq) kind
515
516 freshenCoVarBndrsX :: TCvSubst -> [CoVar] -> TcRnIf gbl lcl (TCvSubst, [CoVar])
517 -- ^ Give fresh uniques to a bunch of CoVars
518 -- Used in FamInst.newFamInst
519 freshenCoVarBndrsX subst = instSkolTyCoVarsX mk_cv subst
520 where
521 mk_cv uniq old_name kind = mkCoVar (setNameUnique old_name uniq) kind
522
523 ------------------
524 instSkolTyCoVars :: (Unique -> Name -> Kind -> TyCoVar)
525 -> [TyVar] -> TcRnIf gbl lcl (TCvSubst, [TyCoVar])
526 instSkolTyCoVars mk_tcv = instSkolTyCoVarsX mk_tcv emptyTCvSubst
527
528 instSkolTyCoVarsX :: (Unique -> Name -> Kind -> TyCoVar)
529 -> TCvSubst -> [TyCoVar] -> TcRnIf gbl lcl (TCvSubst, [TyCoVar])
530 instSkolTyCoVarsX mk_tcv = mapAccumLM (instSkolTyCoVarX mk_tcv)
531
532 instSkolTyCoVarX :: (Unique -> Name -> Kind -> TyCoVar)
533 -> TCvSubst -> TyCoVar -> TcRnIf gbl lcl (TCvSubst, TyCoVar)
534 instSkolTyCoVarX mk_tcv subst tycovar
535 = do { uniq <- newUnique -- using a new unique is critical. See
536 -- Note [Skolems in zonkSyntaxExpr] in TcHsSyn
537 ; let new_tcv = mk_tcv uniq old_name kind
538 subst1 | isTyVar new_tcv
539 = extendTvSubstWithClone subst tycovar new_tcv
540 | otherwise
541 = extendCvSubstWithClone subst tycovar new_tcv
542 ; return (subst1, new_tcv) }
543 where
544 old_name = tyVarName tycovar
545 kind = substTyUnchecked subst (tyVarKind tycovar)
546
547 newFskTyVar :: TcType -> TcM TcTyVar
548 newFskTyVar fam_ty
549 = do { uniq <- newUnique
550 ; let name = mkSysTvName uniq (fsLit "fsk")
551 ; return (mkTcTyVar name (typeKind fam_ty) (FlatSkol fam_ty)) }
552
553 {-
554 Note [Kind substitution when instantiating]
555 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
556 When we instantiate a bunch of kind and type variables, first we
557 expect them to be topologically sorted.
558 Then we have to instantiate the kind variables, build a substitution
559 from old variables to the new variables, then instantiate the type
560 variables substituting the original kind.
561
562 Exemple: If we want to instantiate
563 [(k1 :: *), (k2 :: *), (a :: k1 -> k2), (b :: k1)]
564 we want
565 [(?k1 :: *), (?k2 :: *), (?a :: ?k1 -> ?k2), (?b :: ?k1)]
566 instead of the buggous
567 [(?k1 :: *), (?k2 :: *), (?a :: k1 -> k2), (?b :: k1)]
568
569
570 ************************************************************************
571 * *
572 MetaTvs (meta type variables; mutable)
573 * *
574 ************************************************************************
575 -}
576
577 mkMetaTyVarName :: Unique -> FastString -> Name
578 -- Makes a /System/ Name, which is eagerly eliminated by
579 -- the unifier; see TcUnify.nicer_to_update_tv1, and
580 -- TcCanonical.canEqTyVarTyVar (nicer_to_update_tv2)
581 mkMetaTyVarName uniq str = mkSysTvName uniq str
582
583 newSigTyVar :: Name -> Kind -> TcM TcTyVar
584 newSigTyVar name kind
585 = do { details <- newMetaDetails SigTv
586 ; return (mkTcTyVar name kind details) }
587
588 newFmvTyVar :: TcType -> TcM TcTyVar
589 -- Very like newMetaTyVar, except sets mtv_tclvl to one less
590 -- so that the fmv is untouchable.
591 newFmvTyVar fam_ty
592 = do { uniq <- newUnique
593 ; ref <- newMutVar Flexi
594 ; cur_lvl <- getTcLevel
595 ; let details = MetaTv { mtv_info = FlatMetaTv
596 , mtv_ref = ref
597 , mtv_tclvl = fmvTcLevel cur_lvl }
598 name = mkMetaTyVarName uniq (fsLit "s")
599 ; return (mkTcTyVar name (typeKind fam_ty) details) }
600
601 newMetaDetails :: MetaInfo -> TcM TcTyVarDetails
602 newMetaDetails info
603 = do { ref <- newMutVar Flexi
604 ; tclvl <- getTcLevel
605 ; return (MetaTv { mtv_info = info
606 , mtv_ref = ref
607 , mtv_tclvl = tclvl }) }
608
609 cloneMetaTyVar :: TcTyVar -> TcM TcTyVar
610 cloneMetaTyVar tv
611 = ASSERT( isTcTyVar tv )
612 do { uniq <- newUnique
613 ; ref <- newMutVar Flexi
614 ; let name' = setNameUnique (tyVarName tv) uniq
615 details' = case tcTyVarDetails tv of
616 details@(MetaTv {}) -> details { mtv_ref = ref }
617 _ -> pprPanic "cloneMetaTyVar" (ppr tv)
618 ; return (mkTcTyVar name' (tyVarKind tv) details') }
619
620 -- Works for both type and kind variables
621 readMetaTyVar :: TyVar -> TcM MetaDetails
622 readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
623 readMutVar (metaTvRef tyvar)
624
625 isFilledMetaTyVar :: TyVar -> TcM Bool
626 -- True of a filled-in (Indirect) meta type variable
627 isFilledMetaTyVar tv
628 | MetaTv { mtv_ref = ref } <- tcTyVarDetails tv
629 = do { details <- readMutVar ref
630 ; return (isIndirect details) }
631 | otherwise = return False
632
633 isUnfilledMetaTyVar :: TyVar -> TcM Bool
634 -- True of a un-filled-in (Flexi) meta type variable
635 isUnfilledMetaTyVar tv
636 | MetaTv { mtv_ref = ref } <- tcTyVarDetails tv
637 = do { details <- readMutVar ref
638 ; return (isFlexi details) }
639 | otherwise = return False
640
641 --------------------
642 -- Works with both type and kind variables
643 writeMetaTyVar :: TcTyVar -> TcType -> TcM ()
644 -- Write into a currently-empty MetaTyVar
645
646 writeMetaTyVar tyvar ty
647 | not debugIsOn
648 = writeMetaTyVarRef tyvar (metaTvRef tyvar) ty
649
650 -- Everything from here on only happens if DEBUG is on
651 | not (isTcTyVar tyvar)
652 = WARN( True, text "Writing to non-tc tyvar" <+> ppr tyvar )
653 return ()
654
655 | MetaTv { mtv_ref = ref } <- tcTyVarDetails tyvar
656 = writeMetaTyVarRef tyvar ref ty
657
658 | otherwise
659 = WARN( True, text "Writing to non-meta tyvar" <+> ppr tyvar )
660 return ()
661
662 --------------------
663 writeMetaTyVarRef :: TcTyVar -> TcRef MetaDetails -> TcType -> TcM ()
664 -- Here the tyvar is for error checking only;
665 -- the ref cell must be for the same tyvar
666 writeMetaTyVarRef tyvar ref ty
667 | not debugIsOn
668 = do { traceTc "writeMetaTyVar" (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)
669 <+> text ":=" <+> ppr ty)
670 ; writeTcRef ref (Indirect ty) }
671
672 -- Everything from here on only happens if DEBUG is on
673 | otherwise
674 = do { meta_details <- readMutVar ref;
675 -- Zonk kinds to allow the error check to work
676 ; zonked_tv_kind <- zonkTcType tv_kind
677 ; zonked_ty_kind <- zonkTcType ty_kind
678
679 -- Check for double updates
680 ; ASSERT2( isFlexi meta_details,
681 hang (text "Double update of meta tyvar")
682 2 (ppr tyvar $$ ppr meta_details) )
683
684 traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty)
685 ; writeMutVar ref (Indirect ty)
686 ; when ( not (isPredTy tv_kind)
687 -- Don't check kinds for updates to coercion variables
688 && not (zonked_ty_kind `tcEqKind` zonked_tv_kind))
689 $ WARN( True, hang (text "Ill-kinded update to meta tyvar")
690 2 ( ppr tyvar <+> text "::" <+> (ppr tv_kind $$ ppr zonked_tv_kind)
691 <+> text ":="
692 <+> ppr ty <+> text "::" <+> (ppr ty_kind $$ ppr zonked_ty_kind) ) )
693 (return ()) }
694 where
695 tv_kind = tyVarKind tyvar
696 ty_kind = typeKind ty
697
698 {-
699 % Generating fresh variables for pattern match check
700 -}
701
702 -- UNINSTANTIATED VERSION OF tcInstSkolTyCoVars
703 genInstSkolTyVarsX :: SrcSpan -> TCvSubst -> [TyVar]
704 -> TcRnIf gbl lcl (TCvSubst, [TcTyVar])
705 -- Precondition: tyvars should be scoping-ordered
706 -- see Note [Kind substitution when instantiating]
707 -- Get the location from the monad; this is a complete freshening operation
708 genInstSkolTyVarsX loc subst tvs = instSkolTyCoVarsX (mkTcSkolTyVar loc False) subst tvs
709
710 {-
711 ************************************************************************
712 * *
713 MetaTvs: TauTvs
714 * *
715 ************************************************************************
716
717 Note [Never need to instantiate coercion variables]
718 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
719 With coercion variables sloshing around in types, it might seem that we
720 sometimes need to instantiate coercion variables. This would be problematic,
721 because coercion variables inhabit unboxed equality (~#), and the constraint
722 solver thinks in terms only of boxed equality (~). The solution is that
723 we never need to instantiate coercion variables in the first place.
724
725 The tyvars that we need to instantiate come from the types of functions,
726 data constructors, and patterns. These will never be quantified over
727 coercion variables, except for the special case of the promoted Eq#. But,
728 that can't ever appear in user code, so we're safe!
729 -}
730
731 newAnonMetaTyVar :: MetaInfo -> Kind -> TcM TcTyVar
732 -- Make a new meta tyvar out of thin air
733 newAnonMetaTyVar meta_info kind
734 = do { uniq <- newUnique
735 ; let name = mkMetaTyVarName uniq s
736 s = case meta_info of
737 TauTv -> fsLit "t"
738 FlatMetaTv -> fsLit "fmv"
739 SigTv -> fsLit "a"
740 ; details <- newMetaDetails meta_info
741 ; return (mkTcTyVar name kind details) }
742
743 newFlexiTyVar :: Kind -> TcM TcTyVar
744 newFlexiTyVar kind = newAnonMetaTyVar TauTv kind
745
746 newFlexiTyVarTy :: Kind -> TcM TcType
747 newFlexiTyVarTy kind = do
748 tc_tyvar <- newFlexiTyVar kind
749 return (mkTyVarTy tc_tyvar)
750
751 newFlexiTyVarTys :: Int -> Kind -> TcM [TcType]
752 newFlexiTyVarTys n kind = mapM newFlexiTyVarTy (nOfThem n kind)
753
754 -- | Create a tyvar that can be a lifted or unlifted type.
755 newOpenFlexiTyVarTy :: TcM TcType
756 newOpenFlexiTyVarTy
757 = do { lev <- newFlexiTyVarTy levityTy
758 ; newFlexiTyVarTy (tYPE lev) }
759
760 newMetaSigTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
761 newMetaSigTyVars = mapAccumLM newMetaSigTyVarX emptyTCvSubst
762
763 newMetaTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
764 -- Instantiate with META type variables
765 -- Note that this works for a sequence of kind, type, and coercion variables
766 -- variables. Eg [ (k:*), (a:k->k) ]
767 -- Gives [ (k7:*), (a8:k7->k7) ]
768 newMetaTyVars = mapAccumLM newMetaTyVarX emptyTCvSubst
769 -- emptyTCvSubst has an empty in-scope set, but that's fine here
770 -- Since the tyvars are freshly made, they cannot possibly be
771 -- captured by any existing for-alls.
772
773 newMetaTyVarX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
774 -- Make a new unification variable tyvar whose Name and Kind come from
775 -- an existing TyVar. We substitute kind variables in the kind.
776 newMetaTyVarX subst tyvar = new_meta_tv_x TauTv subst tyvar
777
778 newMetaSigTyVarX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
779 -- Just like newMetaTyVarX, but make a SigTv
780 newMetaSigTyVarX subst tyvar = new_meta_tv_x SigTv subst tyvar
781
782 new_meta_tv_x :: MetaInfo -> TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
783 new_meta_tv_x info subst tyvar
784 = do { uniq <- newUnique
785 ; details <- newMetaDetails info
786 ; let name = mkSystemName uniq (getOccName tyvar)
787 -- See Note [Name of an instantiated type variable]
788 kind = substTyUnchecked subst (tyVarKind tyvar)
789 new_tv = mkTcTyVar name kind details
790 subst1 = extendTvSubstWithClone subst tyvar new_tv
791 ; return (subst1, new_tv) }
792
793 {- Note [Name of an instantiated type variable]
794 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
795 At the moment we give a unification variable a System Name, which
796 influences the way it is tidied; see TypeRep.tidyTyVarBndr.
797
798 ************************************************************************
799 * *
800 Quantification
801 * *
802 ************************************************************************
803
804 Note [quantifyTyVars]
805 ~~~~~~~~~~~~~~~~~~~~~
806 quantifyTyVars is given the free vars of a type that we
807 are about to wrap in a forall.
808
809 It takes these free type/kind variables (partitioned into dependent and
810 non-dependent variables) and
811 1. Zonks them and remove globals and covars
812 2. Extends kvs1 with free kind vars in the kinds of tvs (removing globals)
813 3. Calls zonkQuantifiedTyVar on each
814
815 Step (2) is often unimportant, because the kind variable is often
816 also free in the type. Eg
817 Typeable k (a::k)
818 has free vars {k,a}. But the type (see Trac #7916)
819 (f::k->*) (a::k)
820 has free vars {f,a}, but we must add 'k' as well! Hence step (3).
821
822 This function bothers to distinguish between dependent and non-dependent
823 variables only to keep correct defaulting behavior with -XNoPolyKinds.
824 With -XPolyKinds, it treats both classes of variables identically.
825
826 Note that this function can accept covars, but will never return them.
827 This is because we never want to infer a quantified covar!
828 -}
829
830 quantifyTyVars :: TcTyCoVarSet -- global tvs
831 -> Pair TcTyCoVarSet -- dependent tvs We only distinguish
832 -- nondependent tvs between these for
833 -- -XNoPolyKinds
834 -> TcM [TcTyVar]
835 -- See Note [quantifyTyVars]
836 -- Can be given a mixture of TcTyVars and TyVars, in the case of
837 -- associated type declarations. Also accepts covars, but *never* returns any.
838
839 quantifyTyVars gbl_tvs (Pair dep_tkvs nondep_tkvs)
840 = do { dep_tkvs <- zonkTyCoVarsAndFV dep_tkvs
841 ; nondep_tkvs <- (`minusVarSet` dep_tkvs) <$>
842 zonkTyCoVarsAndFV nondep_tkvs
843 ; gbl_tvs <- zonkTyCoVarsAndFV gbl_tvs
844
845 ; let all_cvs = filterVarSet isCoVar $
846 dep_tkvs `unionVarSet` nondep_tkvs `minusVarSet` gbl_tvs
847 dep_kvs = varSetElemsWellScoped $
848 dep_tkvs `minusVarSet` gbl_tvs
849 `minusVarSet` (closeOverKinds all_cvs)
850 -- remove any tvs that a covar depends on
851
852 nondep_tvs = varSetElemsWellScoped $
853 nondep_tkvs `minusVarSet` gbl_tvs
854 -- no worry about dependent cvs here, as these vars
855 -- are non-dependent
856
857 -- NB kinds of tvs are zonked by zonkTyCoVarsAndFV
858
859 -- In the non-PolyKinds case, default the kind variables
860 -- to *, and zonk the tyvars as usual. Notice that this
861 -- may make quantifyTyVars return a shorter list
862 -- than it was passed, but that's ok
863 ; poly_kinds <- xoptM LangExt.PolyKinds
864 ; dep_vars2 <- if poly_kinds
865 then return dep_kvs
866 else do { let (meta_kvs, skolem_kvs) = partition is_meta dep_kvs
867 is_meta kv = isTcTyVar kv && isMetaTyVar kv
868
869 ; mapM_ defaultKindVar meta_kvs
870 ; return skolem_kvs } -- should be empty
871
872 ; let quant_vars = dep_vars2 ++ nondep_tvs
873
874 ; traceTc "quantifyTyVars"
875 (vcat [ text "globals:" <+> ppr gbl_tvs
876 , text "nondep:" <+> ppr nondep_tvs
877 , text "dep:" <+> ppr dep_kvs
878 , text "dep2:" <+> ppr dep_vars2
879 , text "quant_vars:" <+> ppr quant_vars ])
880
881 ; mapMaybeM zonk_quant quant_vars }
882 -- Because of the order, any kind variables
883 -- mentioned in the kinds of the type variables refer to
884 -- the now-quantified versions
885 where
886 zonk_quant tkv
887 | isTcTyVar tkv = zonkQuantifiedTyVar tkv
888 | otherwise = return $ Just tkv
889 -- For associated types, we have the class variables
890 -- in scope, and they are TyVars not TcTyVars
891
892 zonkQuantifiedTyVar :: TcTyVar -> TcM (Maybe TcTyVar)
893 -- The quantified type variables often include meta type variables
894 -- we want to freeze them into ordinary type variables, and
895 -- default their kind (e.g. from TYPE v to TYPE Lifted)
896 -- The meta tyvar is updated to point to the new skolem TyVar. Now any
897 -- bound occurrences of the original type variable will get zonked to
898 -- the immutable version.
899 --
900 -- We leave skolem TyVars alone; they are immutable.
901 --
902 -- This function is called on both kind and type variables,
903 -- but kind variables *only* if PolyKinds is on.
904 --
905 -- This returns a tyvar if it should be quantified over; otherwise,
906 -- it returns Nothing. Nothing is
907 -- returned only if zonkQuantifiedTyVar is passed a Levity meta-tyvar,
908 -- in order to default to Lifted.
909 zonkQuantifiedTyVar tv = left_only `liftM` zonkQuantifiedTyVarOrType tv
910 where left_only :: Either a b -> Maybe a
911 left_only (Left x) = Just x
912 left_only (Right _) = Nothing
913
914 -- | Like zonkQuantifiedTyVar, but if zonking reveals that the tyvar
915 -- should become a type (when defaulting a levity var to Lifted), it
916 -- returns the type instead.
917 zonkQuantifiedTyVarOrType :: TcTyVar -> TcM (Either TcTyVar TcType)
918 zonkQuantifiedTyVarOrType tv
919 = case tcTyVarDetails tv of
920 SkolemTv {} -> do { kind <- zonkTcType (tyVarKind tv)
921 ; return $ Left $ setTyVarKind tv kind }
922 -- It might be a skolem type variable,
923 -- for example from a user type signature
924
925 MetaTv { mtv_ref = ref } ->
926 do when debugIsOn $ do
927 -- [Sept 04] Check for non-empty.
928 -- See note [Silly Type Synonym]
929 cts <- readMutVar ref
930 case cts of
931 Flexi -> return ()
932 Indirect ty -> WARN( True, ppr tv $$ ppr ty )
933 return ()
934 if isLevityVar tv
935 then do { writeMetaTyVar tv liftedDataConTy
936 ; return (Right liftedDataConTy) }
937 else Left `liftM` skolemiseUnboundMetaTyVar tv vanillaSkolemTv
938 _other -> pprPanic "zonkQuantifiedTyVar" (ppr tv) -- FlatSkol, RuntimeUnk
939
940 -- | Take an (unconstrained) meta tyvar and default it. Works only for
941 -- kind vars (of type BOX) and levity vars (of type Levity).
942 defaultKindVar :: TcTyVar -> TcM Kind
943 defaultKindVar kv
944 | ASSERT( isMetaTyVar kv )
945 isLevityVar kv
946 = writeMetaTyVar kv liftedDataConTy >> return liftedDataConTy
947 | otherwise
948 = writeMetaTyVar kv liftedTypeKind >> return liftedTypeKind
949
950 skolemiseUnboundMetaTyVar :: TcTyVar -> TcTyVarDetails -> TcM TyVar
951 -- We have a Meta tyvar with a ref-cell inside it
952 -- Skolemise it, so that
953 -- we are totally out of Meta-tyvar-land
954 -- We create a skolem TyVar, not a regular TyVar
955 -- See Note [Zonking to Skolem]
956 skolemiseUnboundMetaTyVar tv details
957 = ASSERT2( isMetaTyVar tv, ppr tv )
958 do { span <- getSrcSpanM -- Get the location from "here"
959 -- ie where we are generalising
960 ; kind <- zonkTcType (tyVarKind tv)
961 ; let uniq = getUnique tv
962 -- NB: Use same Unique as original tyvar. This is
963 -- important for TcHsType.splitTelescopeTvs to work properly
964
965 tv_name = getOccName tv
966 final_name = mkInternalName uniq tv_name span
967 final_tv = mkTcTyVar final_name kind details
968
969 ; traceTc "Skolemising" (ppr tv <+> text ":=" <+> ppr final_tv)
970 ; writeMetaTyVar tv (mkTyVarTy final_tv)
971 ; return final_tv }
972
973 {-
974 Note [What is a meta variable?]
975 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
976 A "meta type-variable", also know as a "unification variable" is a placeholder
977 introduced by the typechecker for an as-yet-unknown monotype.
978
979 For example, when we see a call `reverse (f xs)`, we know that we calling
980 reverse :: forall a. [a] -> [a]
981 So we know that the argument `f xs` must be a "list of something". But what is
982 the "something"? We don't know until we explore the `f xs` a bit more. So we set
983 out what we do know at the call of `reverse` by instantiate its type with a fresh
984 meta tyvar, `alpha` say. So now the type of the argument `f xs`, and of the
985 result, is `[alpha]`. The unification variable `alpha` stands for the
986 as-yet-unknown type of the elements of the list.
987
988 As type inference progresses we may learn more about `alpha`. For example, suppose
989 `f` has the type
990 f :: forall b. b -> [Maybe b]
991 Then we instantiate `f`'s type with another fresh unification variable, say
992 `beta`; and equate `f`'s result type with reverse's argument type, thus
993 `[alpha] ~ [Maybe beta]`.
994
995 Now we can solve this equality to learn that `alpha ~ Maybe beta`, so we've
996 refined our knowledge about `alpha`. And so on.
997
998 If you found this Note useful, you may also want to have a look at
999 Section 5 of "Practical type inference for higher rank types" (Peyton Jones,
1000 Vytiniotis, Weirich and Shields. J. Functional Programming. 2011).
1001
1002 Note [What is zonking?]
1003 ~~~~~~~~~~~~~~~~~~~~~~~
1004 GHC relies heavily on mutability in the typechecker for efficient operation.
1005 For this reason, throughout much of the type checking process meta type
1006 variables (the MetaTv constructor of TcTyVarDetails) are represented by mutable
1007 variables (known as TcRefs).
1008
1009 Zonking is the process of ripping out these mutable variables and replacing them
1010 with a real TcType. This involves traversing the entire type expression, but the
1011 interesting part of replacing the mutable variables occurs in zonkTyVarOcc.
1012
1013 There are two ways to zonk a Type:
1014
1015 * zonkTcTypeToType, which is intended to be used at the end of type-checking
1016 for the final zonk. It has to deal with unfilled metavars, either by filling
1017 it with a value like Any or failing (determined by the UnboundTyVarZonker
1018 used).
1019
1020 * zonkTcType, which will happily ignore unfilled metavars. This is the
1021 appropriate function to use while in the middle of type-checking.
1022
1023 Note [Zonking to Skolem]
1024 ~~~~~~~~~~~~~~~~~~~~~~~~
1025 We used to zonk quantified type variables to regular TyVars. However, this
1026 leads to problems. Consider this program from the regression test suite:
1027
1028 eval :: Int -> String -> String -> String
1029 eval 0 root actual = evalRHS 0 root actual
1030
1031 evalRHS :: Int -> a
1032 evalRHS 0 root actual = eval 0 root actual
1033
1034 It leads to the deferral of an equality (wrapped in an implication constraint)
1035
1036 forall a. () => ((String -> String -> String) ~ a)
1037
1038 which is propagated up to the toplevel (see TcSimplify.tcSimplifyInferCheck).
1039 In the meantime `a' is zonked and quantified to form `evalRHS's signature.
1040 This has the *side effect* of also zonking the `a' in the deferred equality
1041 (which at this point is being handed around wrapped in an implication
1042 constraint).
1043
1044 Finally, the equality (with the zonked `a') will be handed back to the
1045 simplifier by TcRnDriver.tcRnSrcDecls calling TcSimplify.tcSimplifyTop.
1046 If we zonk `a' with a regular type variable, we will have this regular type
1047 variable now floating around in the simplifier, which in many places assumes to
1048 only see proper TcTyVars.
1049
1050 We can avoid this problem by zonking with a skolem. The skolem is rigid
1051 (which we require for a quantified variable), but is still a TcTyVar that the
1052 simplifier knows how to deal with.
1053
1054 Note [Silly Type Synonyms]
1055 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1056 Consider this:
1057 type C u a = u -- Note 'a' unused
1058
1059 foo :: (forall a. C u a -> C u a) -> u
1060 foo x = ...
1061
1062 bar :: Num u => u
1063 bar = foo (\t -> t + t)
1064
1065 * From the (\t -> t+t) we get type {Num d} => d -> d
1066 where d is fresh.
1067
1068 * Now unify with type of foo's arg, and we get:
1069 {Num (C d a)} => C d a -> C d a
1070 where a is fresh.
1071
1072 * Now abstract over the 'a', but float out the Num (C d a) constraint
1073 because it does not 'really' mention a. (see exactTyVarsOfType)
1074 The arg to foo becomes
1075 \/\a -> \t -> t+t
1076
1077 * So we get a dict binding for Num (C d a), which is zonked to give
1078 a = ()
1079 [Note Sept 04: now that we are zonking quantified type variables
1080 on construction, the 'a' will be frozen as a regular tyvar on
1081 quantification, so the floated dict will still have type (C d a).
1082 Which renders this whole note moot; happily!]
1083
1084 * Then the \/\a abstraction has a zonked 'a' in it.
1085
1086 All very silly. I think its harmless to ignore the problem. We'll end up with
1087 a \/\a in the final result but all the occurrences of a will be zonked to ()
1088
1089 ************************************************************************
1090 * *
1091 Zonking types
1092 * *
1093 ************************************************************************
1094
1095 -}
1096
1097 -- | @tcGetGlobalTyCoVars@ returns a fully-zonked set of *scoped* tyvars free in
1098 -- the environment. To improve subsequent calls to the same function it writes
1099 -- the zonked set back into the environment. Note that this returns all
1100 -- variables free in anything (term-level or type-level) in scope. We thus
1101 -- don't have to worry about clashes with things that are not in scope, because
1102 -- if they are reachable, then they'll be returned here.
1103 tcGetGlobalTyCoVars :: TcM TcTyVarSet
1104 tcGetGlobalTyCoVars
1105 = do { (TcLclEnv {tcl_tyvars = gtv_var}) <- getLclEnv
1106 ; gbl_tvs <- readMutVar gtv_var
1107 ; gbl_tvs' <- zonkTyCoVarsAndFV gbl_tvs
1108 ; writeMutVar gtv_var gbl_tvs'
1109 ; return gbl_tvs' }
1110
1111 zonkTcTypeAndFV :: TcType -> TcM TyCoVarSet
1112 -- Zonk a type and take its free variables
1113 -- With kind polymorphism it can be essential to zonk *first*
1114 -- so that we find the right set of free variables. Eg
1115 -- forall k1. forall (a:k2). a
1116 -- where k2:=k1 is in the substitution. We don't want
1117 -- k2 to look free in this type!
1118 -- NB: This might be called from within the knot, so don't use
1119 -- smart constructors. See Note [Zonking within the knot] in TcHsType
1120 zonkTcTypeAndFV ty
1121 = tyCoVarsOfType <$> mapType (zonkTcTypeMapper { tcm_smart = False }) () ty
1122
1123 zonkTyCoVar :: TyCoVar -> TcM TcType
1124 -- Works on TyVars and TcTyVars
1125 zonkTyCoVar tv | isTcTyVar tv = zonkTcTyVar tv
1126 | isTyVar tv = mkTyVarTy <$> zonkTyCoVarKind tv
1127 | otherwise = ASSERT2( isCoVar tv, ppr tv )
1128 mkCoercionTy . mkCoVarCo <$> zonkTyCoVarKind tv
1129 -- Hackily, when typechecking type and class decls
1130 -- we have TyVars in scopeadded (only) in
1131 -- TcHsType.tcTyClTyVars, but it seems
1132 -- painful to make them into TcTyVars there
1133
1134 zonkTyCoVarsAndFV :: TyCoVarSet -> TcM TyCoVarSet
1135 zonkTyCoVarsAndFV tycovars = tyCoVarsOfTypes <$> mapM zonkTyCoVar (varSetElems tycovars)
1136
1137 zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
1138 zonkTcTyVars tyvars = mapM zonkTcTyVar tyvars
1139
1140 ----------------- Types
1141 zonkTyCoVarKind :: TyCoVar -> TcM TyCoVar
1142 zonkTyCoVarKind tv = do { kind' <- zonkTcType (tyVarKind tv)
1143 ; return (setTyVarKind tv kind') }
1144
1145 zonkTcTypes :: [TcType] -> TcM [TcType]
1146 zonkTcTypes tys = mapM zonkTcType tys
1147
1148 {-
1149 ************************************************************************
1150 * *
1151 Zonking constraints
1152 * *
1153 ************************************************************************
1154 -}
1155
1156 zonkImplication :: Implication -> TcM Implication
1157 zonkImplication implic@(Implic { ic_skols = skols
1158 , ic_given = given
1159 , ic_wanted = wanted
1160 , ic_info = info })
1161 = do { skols' <- mapM zonkTcTyCoVarBndr skols -- Need to zonk their kinds!
1162 -- as Trac #7230 showed
1163 ; given' <- mapM zonkEvVar given
1164 ; info' <- zonkSkolemInfo info
1165 ; wanted' <- zonkWCRec wanted
1166 ; return (implic { ic_skols = skols'
1167 , ic_given = given'
1168 , ic_wanted = wanted'
1169 , ic_info = info' }) }
1170
1171 zonkEvVar :: EvVar -> TcM EvVar
1172 zonkEvVar var = do { ty' <- zonkTcType (varType var)
1173 ; return (setVarType var ty') }
1174
1175
1176 zonkWC :: WantedConstraints -> TcM WantedConstraints
1177 zonkWC wc = zonkWCRec wc
1178
1179 zonkWCRec :: WantedConstraints -> TcM WantedConstraints
1180 zonkWCRec (WC { wc_simple = simple, wc_impl = implic, wc_insol = insol })
1181 = do { simple' <- zonkSimples simple
1182 ; implic' <- mapBagM zonkImplication implic
1183 ; insol' <- zonkSimples insol
1184 ; return (WC { wc_simple = simple', wc_impl = implic', wc_insol = insol' }) }
1185
1186 zonkSimples :: Cts -> TcM Cts
1187 zonkSimples cts = do { cts' <- mapBagM zonkCt' cts
1188 ; traceTc "zonkSimples done:" (ppr cts')
1189 ; return cts' }
1190
1191 zonkCt' :: Ct -> TcM Ct
1192 zonkCt' ct = zonkCt ct
1193
1194 zonkCt :: Ct -> TcM Ct
1195 zonkCt ct@(CHoleCan { cc_ev = ev })
1196 = do { ev' <- zonkCtEvidence ev
1197 ; return $ ct { cc_ev = ev' } }
1198 zonkCt ct
1199 = do { fl' <- zonkCtEvidence (cc_ev ct)
1200 ; return (mkNonCanonical fl') }
1201
1202 zonkCtEvidence :: CtEvidence -> TcM CtEvidence
1203 zonkCtEvidence ctev@(CtGiven { ctev_pred = pred })
1204 = do { pred' <- zonkTcType pred
1205 ; return (ctev { ctev_pred = pred'}) }
1206 zonkCtEvidence ctev@(CtWanted { ctev_pred = pred, ctev_dest = dest })
1207 = do { pred' <- zonkTcType pred
1208 ; let dest' = case dest of
1209 EvVarDest ev -> EvVarDest $ setVarType ev pred'
1210 -- necessary in simplifyInfer
1211 HoleDest h -> HoleDest h
1212 ; return (ctev { ctev_pred = pred', ctev_dest = dest' }) }
1213 zonkCtEvidence ctev@(CtDerived { ctev_pred = pred })
1214 = do { pred' <- zonkTcType pred
1215 ; return (ctev { ctev_pred = pred' }) }
1216
1217 zonkSkolemInfo :: SkolemInfo -> TcM SkolemInfo
1218 zonkSkolemInfo (SigSkol cx ty) = do { ty <- readExpType ty
1219 ; ty' <- zonkTcType ty
1220 ; return (SigSkol cx (mkCheckExpType ty')) }
1221 zonkSkolemInfo (InferSkol ntys) = do { ntys' <- mapM do_one ntys
1222 ; return (InferSkol ntys') }
1223 where
1224 do_one (n, ty) = do { ty' <- zonkTcType ty; return (n, ty') }
1225 zonkSkolemInfo skol_info = return skol_info
1226
1227 {-
1228 %************************************************************************
1229 %* *
1230 \subsection{Zonking -- the main work-horses: zonkTcType, zonkTcTyVar}
1231 * *
1232 * For internal use only! *
1233 * *
1234 ************************************************************************
1235
1236 -}
1237
1238 -- zonkId is used *during* typechecking just to zonk the Id's type
1239 zonkId :: TcId -> TcM TcId
1240 zonkId id
1241 = do { ty' <- zonkTcType (idType id)
1242 ; return (Id.setIdType id ty') }
1243
1244 -- | A suitable TyCoMapper for zonking a type inside the knot, and
1245 -- before all metavars are filled in.
1246 zonkTcTypeMapper :: TyCoMapper () TcM
1247 zonkTcTypeMapper = TyCoMapper
1248 { tcm_smart = True
1249 , tcm_tyvar = const zonkTcTyVar
1250 , tcm_covar = const (\cv -> mkCoVarCo <$> zonkTyCoVarKind cv)
1251 , tcm_hole = hole
1252 , tcm_tybinder = \_env tv _vis -> ((), ) <$> zonkTcTyCoVarBndr tv }
1253 where
1254 hole :: () -> CoercionHole -> Role -> Type -> Type
1255 -> TcM Coercion
1256 hole _ h r t1 t2
1257 = do { contents <- unpackCoercionHole_maybe h
1258 ; case contents of
1259 Just co -> do { co <- zonkCo co
1260 ; checkCoercionHole co h r t1 t2 }
1261 Nothing -> do { t1 <- zonkTcType t1
1262 ; t2 <- zonkTcType t2
1263 ; return $ mkHoleCo h r t1 t2 } }
1264
1265
1266 -- For unbound, mutable tyvars, zonkType uses the function given to it
1267 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
1268 -- type variable and zonks the kind too
1269 zonkTcType :: TcType -> TcM TcType
1270 zonkTcType = mapType zonkTcTypeMapper ()
1271
1272 -- | "Zonk" a coercion -- really, just zonk any types in the coercion
1273 zonkCo :: Coercion -> TcM Coercion
1274 zonkCo = mapCoercion zonkTcTypeMapper ()
1275
1276 zonkTcTyCoVarBndr :: TcTyCoVar -> TcM TcTyCoVar
1277 -- A tyvar binder is never a unification variable (MetaTv),
1278 -- rather it is always a skolems. BUT it may have a kind
1279 -- that has not yet been zonked, and may include kind
1280 -- unification variables.
1281 zonkTcTyCoVarBndr tyvar
1282 -- can't use isCoVar, because it looks at a TyCon. Argh.
1283 = ASSERT2( isImmutableTyVar tyvar || (not $ isTyVar tyvar), ppr tyvar ) do
1284 updateTyVarKindM zonkTcType tyvar
1285
1286 zonkTcTyVar :: TcTyVar -> TcM TcType
1287 -- Simply look through all Flexis
1288 zonkTcTyVar tv
1289 | isTcTyVar tv
1290 = case tcTyVarDetails tv of
1291 SkolemTv {} -> zonk_kind_and_return
1292 RuntimeUnk {} -> zonk_kind_and_return
1293 FlatSkol ty -> zonkTcType ty
1294 MetaTv { mtv_ref = ref }
1295 -> do { cts <- readMutVar ref
1296 ; case cts of
1297 Flexi -> zonk_kind_and_return
1298 Indirect ty -> zonkTcType ty }
1299
1300 | otherwise -- coercion variable
1301 = zonk_kind_and_return
1302 where
1303 zonk_kind_and_return = do { z_tv <- zonkTyCoVarKind tv
1304 ; return (mkTyVarTy z_tv) }
1305
1306 {-
1307 %************************************************************************
1308 %* *
1309 Tidying
1310 * *
1311 ************************************************************************
1312 -}
1313
1314 zonkTidyTcType :: TidyEnv -> TcType -> TcM (TidyEnv, TcType)
1315 zonkTidyTcType env ty = do { ty' <- zonkTcType ty
1316 ; return (tidyOpenType env ty') }
1317
1318 -- | Make an 'ErrorThing' storing a type.
1319 mkTypeErrorThing :: TcType -> ErrorThing
1320 mkTypeErrorThing ty = ErrorThing ty (Just $ length $ snd $ repSplitAppTys ty)
1321 zonkTidyTcType
1322 -- NB: Use *rep*splitAppTys, else we get #11313
1323
1324 -- | Make an 'ErrorThing' storing a type, with some extra args known about
1325 mkTypeErrorThingArgs :: TcType -> Int -> ErrorThing
1326 mkTypeErrorThingArgs ty num_args
1327 = ErrorThing ty (Just $ (length $ snd $ repSplitAppTys ty) + num_args)
1328 zonkTidyTcType
1329
1330 zonkTidyOrigin :: TidyEnv -> CtOrigin -> TcM (TidyEnv, CtOrigin)
1331 zonkTidyOrigin env (GivenOrigin skol_info)
1332 = do { skol_info1 <- zonkSkolemInfo skol_info
1333 ; let skol_info2 = tidySkolemInfo env skol_info1
1334 ; return (env, GivenOrigin skol_info2) }
1335 zonkTidyOrigin env orig@(TypeEqOrigin { uo_actual = act
1336 , uo_expected = exp
1337 , uo_thing = m_thing })
1338 = do { (env1, act') <- zonkTidyTcType env act
1339 ; mb_exp <- readExpType_maybe exp -- it really should be filled in.
1340 -- unless we're debugging.
1341 ; (env2, exp') <- case mb_exp of
1342 Just ty -> second mkCheckExpType <$> zonkTidyTcType env1 ty
1343 Nothing -> return (env1, exp)
1344 ; (env3, m_thing') <- zonkTidyErrorThing env2 m_thing
1345 ; return ( env3, orig { uo_actual = act'
1346 , uo_expected = exp'
1347 , uo_thing = m_thing' }) }
1348 zonkTidyOrigin env (KindEqOrigin ty1 m_ty2 orig t_or_k)
1349 = do { (env1, ty1') <- zonkTidyTcType env ty1
1350 ; (env2, m_ty2') <- case m_ty2 of
1351 Just ty2 -> second Just <$> zonkTidyTcType env1 ty2
1352 Nothing -> return (env1, Nothing)
1353 ; (env3, orig') <- zonkTidyOrigin env2 orig
1354 ; return (env3, KindEqOrigin ty1' m_ty2' orig' t_or_k) }
1355 zonkTidyOrigin env (FunDepOrigin1 p1 l1 p2 l2)
1356 = do { (env1, p1') <- zonkTidyTcType env p1
1357 ; (env2, p2') <- zonkTidyTcType env1 p2
1358 ; return (env2, FunDepOrigin1 p1' l1 p2' l2) }
1359 zonkTidyOrigin env (FunDepOrigin2 p1 o1 p2 l2)
1360 = do { (env1, p1') <- zonkTidyTcType env p1
1361 ; (env2, p2') <- zonkTidyTcType env1 p2
1362 ; (env3, o1') <- zonkTidyOrigin env2 o1
1363 ; return (env3, FunDepOrigin2 p1' o1' p2' l2) }
1364 zonkTidyOrigin env orig = return (env, orig)
1365
1366 zonkTidyErrorThing :: TidyEnv -> Maybe ErrorThing
1367 -> TcM (TidyEnv, Maybe ErrorThing)
1368 zonkTidyErrorThing env (Just (ErrorThing thing n_args zonker))
1369 = do { (env', thing') <- zonker env thing
1370 ; return (env', Just $ ErrorThing thing' n_args zonker) }
1371 zonkTidyErrorThing env Nothing
1372 = return (env, Nothing)
1373
1374 ----------------
1375 tidyCt :: TidyEnv -> Ct -> Ct
1376 -- Used only in error reporting
1377 -- Also converts it to non-canonical
1378 tidyCt env ct
1379 = case ct of
1380 CHoleCan { cc_ev = ev }
1381 -> ct { cc_ev = tidy_ev env ev }
1382 _ -> mkNonCanonical (tidy_ev env (ctEvidence ct))
1383 where
1384 tidy_ev :: TidyEnv -> CtEvidence -> CtEvidence
1385 -- NB: we do not tidy the ctev_evar field because we don't
1386 -- show it in error messages
1387 tidy_ev env ctev@(CtGiven { ctev_pred = pred })
1388 = ctev { ctev_pred = tidyType env pred }
1389 tidy_ev env ctev@(CtWanted { ctev_pred = pred })
1390 = ctev { ctev_pred = tidyType env pred }
1391 tidy_ev env ctev@(CtDerived { ctev_pred = pred })
1392 = ctev { ctev_pred = tidyType env pred }
1393
1394 ----------------
1395 tidyEvVar :: TidyEnv -> EvVar -> EvVar
1396 tidyEvVar env var = setVarType var (tidyType env (varType var))
1397
1398 ----------------
1399 tidySkolemInfo :: TidyEnv -> SkolemInfo -> SkolemInfo
1400 tidySkolemInfo env (DerivSkol ty) = DerivSkol (tidyType env ty)
1401 tidySkolemInfo env (SigSkol cx ty) = SigSkol cx (mkCheckExpType $
1402 tidyType env $
1403 checkingExpType "tidySkolemInfo" ty)
1404 tidySkolemInfo env (InferSkol ids) = InferSkol (mapSnd (tidyType env) ids)
1405 tidySkolemInfo env (UnifyForAllSkol ty) = UnifyForAllSkol (tidyType env ty)
1406 tidySkolemInfo _ info = info