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