Address #11471 by putting RuntimeRep in kinds.
[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, zonkTcTyBinder, 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 { rr <- newFlexiTyVarTy runtimeRepTy
334 ; u <- newUnique
335 ; tclvl <- getTcLevel
336 ; let ki = tYPE rr
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 Note [Kind substitution when instantiating]
554 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
555 When we instantiate a bunch of kind and type variables, first we
556 expect them to be topologically sorted.
557 Then we have to instantiate the kind variables, build a substitution
558 from old variables to the new variables, then instantiate the type
559 variables substituting the original kind.
560
561 Exemple: If we want to instantiate
562 [(k1 :: *), (k2 :: *), (a :: k1 -> k2), (b :: k1)]
563 we want
564 [(?k1 :: *), (?k2 :: *), (?a :: ?k1 -> ?k2), (?b :: ?k1)]
565 instead of the buggous
566 [(?k1 :: *), (?k2 :: *), (?a :: k1 -> k2), (?b :: k1)]
567
568
569 ************************************************************************
570 * *
571 MetaTvs (meta type variables; mutable)
572 * *
573 ************************************************************************
574 -}
575
576 mkMetaTyVarName :: Unique -> FastString -> Name
577 -- Makes a /System/ Name, which is eagerly eliminated by
578 -- the unifier; see TcUnify.nicer_to_update_tv1, and
579 -- TcCanonical.canEqTyVarTyVar (nicer_to_update_tv2)
580 mkMetaTyVarName uniq str = mkSysTvName uniq str
581
582 newSigTyVar :: Name -> Kind -> TcM TcTyVar
583 newSigTyVar name kind
584 = do { details <- newMetaDetails SigTv
585 ; return (mkTcTyVar name kind details) }
586
587 newFmvTyVar :: TcType -> TcM TcTyVar
588 -- Very like newMetaTyVar, except sets mtv_tclvl to one less
589 -- so that the fmv is untouchable.
590 newFmvTyVar fam_ty
591 = do { uniq <- newUnique
592 ; ref <- newMutVar Flexi
593 ; cur_lvl <- getTcLevel
594 ; let details = MetaTv { mtv_info = FlatMetaTv
595 , mtv_ref = ref
596 , mtv_tclvl = fmvTcLevel cur_lvl }
597 name = mkMetaTyVarName uniq (fsLit "s")
598 ; return (mkTcTyVar name (typeKind fam_ty) details) }
599
600 newMetaDetails :: MetaInfo -> TcM TcTyVarDetails
601 newMetaDetails info
602 = do { ref <- newMutVar Flexi
603 ; tclvl <- getTcLevel
604 ; return (MetaTv { mtv_info = info
605 , mtv_ref = ref
606 , mtv_tclvl = tclvl }) }
607
608 cloneMetaTyVar :: TcTyVar -> TcM TcTyVar
609 cloneMetaTyVar tv
610 = ASSERT( isTcTyVar tv )
611 do { uniq <- newUnique
612 ; ref <- newMutVar Flexi
613 ; let name' = setNameUnique (tyVarName tv) uniq
614 details' = case tcTyVarDetails tv of
615 details@(MetaTv {}) -> details { mtv_ref = ref }
616 _ -> pprPanic "cloneMetaTyVar" (ppr tv)
617 ; return (mkTcTyVar name' (tyVarKind tv) details') }
618
619 -- Works for both type and kind variables
620 readMetaTyVar :: TyVar -> TcM MetaDetails
621 readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
622 readMutVar (metaTvRef tyvar)
623
624 isFilledMetaTyVar :: TyVar -> TcM Bool
625 -- True of a filled-in (Indirect) meta type variable
626 isFilledMetaTyVar tv
627 | MetaTv { mtv_ref = ref } <- tcTyVarDetails tv
628 = do { details <- readMutVar ref
629 ; return (isIndirect details) }
630 | otherwise = return False
631
632 isUnfilledMetaTyVar :: TyVar -> TcM Bool
633 -- True of a un-filled-in (Flexi) meta type variable
634 isUnfilledMetaTyVar tv
635 | MetaTv { mtv_ref = ref } <- tcTyVarDetails tv
636 = do { details <- readMutVar ref
637 ; return (isFlexi details) }
638 | otherwise = return False
639
640 --------------------
641 -- Works with both type and kind variables
642 writeMetaTyVar :: TcTyVar -> TcType -> TcM ()
643 -- Write into a currently-empty MetaTyVar
644
645 writeMetaTyVar tyvar ty
646 | not debugIsOn
647 = writeMetaTyVarRef tyvar (metaTvRef tyvar) ty
648
649 -- Everything from here on only happens if DEBUG is on
650 | not (isTcTyVar tyvar)
651 = WARN( True, text "Writing to non-tc tyvar" <+> ppr tyvar )
652 return ()
653
654 | MetaTv { mtv_ref = ref } <- tcTyVarDetails tyvar
655 = writeMetaTyVarRef tyvar ref ty
656
657 | otherwise
658 = WARN( True, text "Writing to non-meta tyvar" <+> ppr tyvar )
659 return ()
660
661 --------------------
662 writeMetaTyVarRef :: TcTyVar -> TcRef MetaDetails -> TcType -> TcM ()
663 -- Here the tyvar is for error checking only;
664 -- the ref cell must be for the same tyvar
665 writeMetaTyVarRef tyvar ref ty
666 | not debugIsOn
667 = do { traceTc "writeMetaTyVar" (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)
668 <+> text ":=" <+> ppr ty)
669 ; writeTcRef ref (Indirect ty) }
670
671 -- Everything from here on only happens if DEBUG is on
672 | otherwise
673 = do { meta_details <- readMutVar ref;
674 -- Zonk kinds to allow the error check to work
675 ; zonked_tv_kind <- zonkTcType tv_kind
676 ; zonked_ty_kind <- zonkTcType ty_kind
677
678 -- Check for double updates
679 ; ASSERT2( isFlexi meta_details,
680 hang (text "Double update of meta tyvar")
681 2 (ppr tyvar $$ ppr meta_details) )
682
683 traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty)
684 ; writeMutVar ref (Indirect ty)
685 ; when ( not (isPredTy tv_kind)
686 -- Don't check kinds for updates to coercion variables
687 && not (zonked_ty_kind `tcEqKind` zonked_tv_kind))
688 $ WARN( True, hang (text "Ill-kinded update to meta tyvar")
689 2 ( ppr tyvar <+> text "::" <+> (ppr tv_kind $$ ppr zonked_tv_kind)
690 <+> text ":="
691 <+> ppr ty <+> text "::" <+> (ppr ty_kind $$ ppr zonked_ty_kind) ) )
692 (return ()) }
693 where
694 tv_kind = tyVarKind tyvar
695 ty_kind = typeKind ty
696
697 {-
698 % Generating fresh variables for pattern match check
699 -}
700
701 -- UNINSTANTIATED VERSION OF tcInstSkolTyCoVars
702 genInstSkolTyVarsX :: SrcSpan -> TCvSubst -> [TyVar]
703 -> TcRnIf gbl lcl (TCvSubst, [TcTyVar])
704 -- Precondition: tyvars should be scoping-ordered
705 -- see Note [Kind substitution when instantiating]
706 -- Get the location from the monad; this is a complete freshening operation
707 genInstSkolTyVarsX loc subst tvs = instSkolTyCoVarsX (mkTcSkolTyVar loc False) subst tvs
708
709 {-
710 ************************************************************************
711 * *
712 MetaTvs: TauTvs
713 * *
714 ************************************************************************
715
716 Note [Never need to instantiate coercion variables]
717 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
718 With coercion variables sloshing around in types, it might seem that we
719 sometimes need to instantiate coercion variables. This would be problematic,
720 because coercion variables inhabit unboxed equality (~#), and the constraint
721 solver thinks in terms only of boxed equality (~). The solution is that
722 we never need to instantiate coercion variables in the first place.
723
724 The tyvars that we need to instantiate come from the types of functions,
725 data constructors, and patterns. These will never be quantified over
726 coercion variables, except for the special case of the promoted Eq#. But,
727 that can't ever appear in user code, so we're safe!
728 -}
729
730 newAnonMetaTyVar :: MetaInfo -> Kind -> TcM TcTyVar
731 -- Make a new meta tyvar out of thin air
732 newAnonMetaTyVar meta_info kind
733 = do { uniq <- newUnique
734 ; let name = mkMetaTyVarName uniq s
735 s = case meta_info of
736 TauTv -> fsLit "t"
737 FlatMetaTv -> fsLit "fmv"
738 SigTv -> fsLit "a"
739 ; details <- newMetaDetails meta_info
740 ; return (mkTcTyVar name kind details) }
741
742 newFlexiTyVar :: Kind -> TcM TcTyVar
743 newFlexiTyVar kind = newAnonMetaTyVar TauTv kind
744
745 newFlexiTyVarTy :: Kind -> TcM TcType
746 newFlexiTyVarTy kind = do
747 tc_tyvar <- newFlexiTyVar kind
748 return (mkTyVarTy tc_tyvar)
749
750 newFlexiTyVarTys :: Int -> Kind -> TcM [TcType]
751 newFlexiTyVarTys n kind = mapM newFlexiTyVarTy (nOfThem n kind)
752
753 -- | Create a tyvar that can be a lifted or unlifted type.
754 newOpenFlexiTyVarTy :: TcM TcType
755 newOpenFlexiTyVarTy
756 = do { rr <- newFlexiTyVarTy runtimeRepTy
757 ; newFlexiTyVarTy (tYPE rr) }
758
759 newMetaSigTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
760 newMetaSigTyVars = mapAccumLM newMetaSigTyVarX emptyTCvSubst
761
762 newMetaTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
763 -- Instantiate with META type variables
764 -- Note that this works for a sequence of kind, type, and coercion variables
765 -- variables. Eg [ (k:*), (a:k->k) ]
766 -- Gives [ (k7:*), (a8:k7->k7) ]
767 newMetaTyVars = mapAccumLM newMetaTyVarX emptyTCvSubst
768 -- emptyTCvSubst has an empty in-scope set, but that's fine here
769 -- Since the tyvars are freshly made, they cannot possibly be
770 -- captured by any existing for-alls.
771
772 newMetaTyVarX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
773 -- Make a new unification variable tyvar whose Name and Kind come from
774 -- an existing TyVar. We substitute kind variables in the kind.
775 newMetaTyVarX subst tyvar = new_meta_tv_x TauTv subst tyvar
776
777 newMetaSigTyVarX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
778 -- Just like newMetaTyVarX, but make a SigTv
779 newMetaSigTyVarX subst tyvar = new_meta_tv_x SigTv subst tyvar
780
781 new_meta_tv_x :: MetaInfo -> TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
782 new_meta_tv_x info subst tyvar
783 = do { uniq <- newUnique
784 ; details <- newMetaDetails info
785 ; let name = mkSystemName uniq (getOccName tyvar)
786 -- See Note [Name of an instantiated type variable]
787 kind = substTyUnchecked subst (tyVarKind tyvar)
788 new_tv = mkTcTyVar name kind details
789 subst1 = extendTvSubstWithClone subst tyvar new_tv
790 ; return (subst1, new_tv) }
791
792 {- Note [Name of an instantiated type variable]
793 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
794 At the moment we give a unification variable a System Name, which
795 influences the way it is tidied; see TypeRep.tidyTyVarBndr.
796
797 ************************************************************************
798 * *
799 Quantification
800 * *
801 ************************************************************************
802
803 Note [quantifyTyVars]
804 ~~~~~~~~~~~~~~~~~~~~~
805 quantifyTyVars is given the free vars of a type that we
806 are about to wrap in a forall.
807
808 It takes these free type/kind variables (partitioned into dependent and
809 non-dependent variables) and
810 1. Zonks them and remove globals and covars
811 2. Extends kvs1 with free kind vars in the kinds of tvs (removing globals)
812 3. Calls zonkQuantifiedTyVar on each
813
814 Step (2) is often unimportant, because the kind variable is often
815 also free in the type. Eg
816 Typeable k (a::k)
817 has free vars {k,a}. But the type (see Trac #7916)
818 (f::k->*) (a::k)
819 has free vars {f,a}, but we must add 'k' as well! Hence step (3).
820
821 This function bothers to distinguish between dependent and non-dependent
822 variables only to keep correct defaulting behavior with -XNoPolyKinds.
823 With -XPolyKinds, it treats both classes of variables identically.
824
825 Note that this function can accept covars, but will never return them.
826 This is because we never want to infer a quantified covar!
827 -}
828
829 quantifyTyVars :: TcTyCoVarSet -- global tvs
830 -> Pair TcTyCoVarSet -- dependent tvs We only distinguish
831 -- nondependent tvs between these for
832 -- -XNoPolyKinds
833 -> TcM [TcTyVar]
834 -- See Note [quantifyTyVars]
835 -- Can be given a mixture of TcTyVars and TyVars, in the case of
836 -- associated type declarations. Also accepts covars, but *never* returns any.
837
838 quantifyTyVars gbl_tvs (Pair dep_tkvs nondep_tkvs)
839 = do { dep_tkvs <- zonkTyCoVarsAndFV dep_tkvs
840 ; nondep_tkvs <- (`minusVarSet` dep_tkvs) <$>
841 zonkTyCoVarsAndFV nondep_tkvs
842 ; gbl_tvs <- zonkTyCoVarsAndFV gbl_tvs
843
844 ; let all_cvs = filterVarSet isCoVar $
845 dep_tkvs `unionVarSet` nondep_tkvs `minusVarSet` gbl_tvs
846 dep_kvs = varSetElemsWellScoped $
847 dep_tkvs `minusVarSet` gbl_tvs
848 `minusVarSet` (closeOverKinds all_cvs)
849 -- remove any tvs that a covar depends on
850
851 nondep_tvs = varSetElemsWellScoped $
852 nondep_tkvs `minusVarSet` gbl_tvs
853 -- no worry about dependent cvs here, as these vars
854 -- are non-dependent
855
856 -- NB kinds of tvs are zonked by zonkTyCoVarsAndFV
857
858 -- In the non-PolyKinds case, default the kind variables
859 -- to *, and zonk the tyvars as usual. Notice that this
860 -- may make quantifyTyVars return a shorter list
861 -- than it was passed, but that's ok
862 ; poly_kinds <- xoptM LangExt.PolyKinds
863 ; dep_vars2 <- if poly_kinds
864 then return dep_kvs
865 else do { let (meta_kvs, skolem_kvs) = partition is_meta dep_kvs
866 is_meta kv = isTcTyVar kv && isMetaTyVar kv
867
868 ; mapM_ defaultKindVar meta_kvs
869 ; return skolem_kvs } -- should be empty
870
871 ; let quant_vars = dep_vars2 ++ nondep_tvs
872
873 ; traceTc "quantifyTyVars"
874 (vcat [ text "globals:" <+> ppr gbl_tvs
875 , text "nondep:" <+> ppr nondep_tvs
876 , text "dep:" <+> ppr dep_kvs
877 , text "dep2:" <+> ppr dep_vars2
878 , text "quant_vars:" <+> ppr quant_vars ])
879
880 ; mapMaybeM zonk_quant quant_vars }
881 -- Because of the order, any kind variables
882 -- mentioned in the kinds of the type variables refer to
883 -- the now-quantified versions
884 where
885 zonk_quant tkv
886 | isTcTyVar tkv = zonkQuantifiedTyVar tkv
887 | otherwise = return $ Just tkv
888 -- For associated types, we have the class variables
889 -- in scope, and they are TyVars not TcTyVars
890
891 zonkQuantifiedTyVar :: TcTyVar -> TcM (Maybe TcTyVar)
892 -- The quantified type variables often include meta type variables
893 -- we want to freeze them into ordinary type variables, and
894 -- default their kind (e.g. from TYPE v to TYPE Lifted)
895 -- The meta tyvar is updated to point to the new skolem TyVar. Now any
896 -- bound occurrences of the original type variable will get zonked to
897 -- the immutable version.
898 --
899 -- We leave skolem TyVars alone; they are immutable.
900 --
901 -- This function is called on both kind and type variables,
902 -- but kind variables *only* if PolyKinds is on.
903 --
904 -- This returns a tyvar if it should be quantified over; otherwise,
905 -- it returns Nothing. Nothing is
906 -- returned only if zonkQuantifiedTyVar is passed a RuntimeRep meta-tyvar,
907 -- in order to default to PtrRepLifted.
908 zonkQuantifiedTyVar tv = left_only `liftM` zonkQuantifiedTyVarOrType tv
909 where left_only :: Either a b -> Maybe a
910 left_only (Left x) = Just x
911 left_only (Right _) = Nothing
912
913 -- | Like zonkQuantifiedTyVar, but if zonking reveals that the tyvar
914 -- should become a type (when defaulting a RuntimeRep var to PtrRepLifted), it
915 -- returns the type instead.
916 zonkQuantifiedTyVarOrType :: TcTyVar -> TcM (Either TcTyVar TcType)
917 zonkQuantifiedTyVarOrType tv
918 = case tcTyVarDetails tv of
919 SkolemTv {} -> do { kind <- zonkTcType (tyVarKind tv)
920 ; return $ Left $ setTyVarKind tv kind }
921 -- It might be a skolem type variable,
922 -- for example from a user type signature
923
924 MetaTv { mtv_ref = ref } ->
925 do when debugIsOn $ do
926 -- [Sept 04] Check for non-empty.
927 -- See note [Silly Type Synonym]
928 cts <- readMutVar ref
929 case cts of
930 Flexi -> return ()
931 Indirect ty -> WARN( True, ppr tv $$ ppr ty )
932 return ()
933 if isRuntimeRepVar tv
934 then do { writeMetaTyVar tv ptrRepLiftedTy
935 ; return (Right ptrRepLiftedTy) }
936 else Left `liftM` skolemiseUnboundMetaTyVar tv vanillaSkolemTv
937 _other -> pprPanic "zonkQuantifiedTyVar" (ppr tv) -- FlatSkol, RuntimeUnk
938
939 -- | Take an (unconstrained) meta tyvar and default it. Works only for
940 -- kind vars (of type *) and RuntimeRep vars (of type RuntimeRep).
941 defaultKindVar :: TcTyVar -> TcM Kind
942 defaultKindVar kv
943 | ASSERT( isMetaTyVar kv )
944 isRuntimeRepVar kv
945 = writeMetaTyVar kv ptrRepLiftedTy >> return ptrRepLiftedTy
946 | otherwise
947 = writeMetaTyVar kv liftedTypeKind >> return liftedTypeKind
948
949 skolemiseUnboundMetaTyVar :: TcTyVar -> TcTyVarDetails -> TcM TyVar
950 -- We have a Meta tyvar with a ref-cell inside it
951 -- Skolemise it, so that
952 -- we are totally out of Meta-tyvar-land
953 -- We create a skolem TyVar, not a regular TyVar
954 -- See Note [Zonking to Skolem]
955 skolemiseUnboundMetaTyVar tv details
956 = ASSERT2( isMetaTyVar tv, ppr tv )
957 do { span <- getSrcSpanM -- Get the location from "here"
958 -- ie where we are generalising
959 ; kind <- zonkTcType (tyVarKind tv)
960 ; let uniq = getUnique tv
961 -- NB: Use same Unique as original tyvar. This is
962 -- important for TcHsType.splitTelescopeTvs to work properly
963
964 tv_name = getOccName tv
965 final_name = mkInternalName uniq tv_name span
966 final_tv = mkTcTyVar final_name kind details
967
968 ; traceTc "Skolemising" (ppr tv <+> text ":=" <+> ppr final_tv)
969 ; writeMetaTyVar tv (mkTyVarTy final_tv)
970 ; return final_tv }
971
972 {-
973 Note [What is a meta variable?]
974 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
975 A "meta type-variable", also know as a "unification variable" is a placeholder
976 introduced by the typechecker for an as-yet-unknown monotype.
977
978 For example, when we see a call `reverse (f xs)`, we know that we calling
979 reverse :: forall a. [a] -> [a]
980 So we know that the argument `f xs` must be a "list of something". But what is
981 the "something"? We don't know until we explore the `f xs` a bit more. So we set
982 out what we do know at the call of `reverse` by instantiate its type with a fresh
983 meta tyvar, `alpha` say. So now the type of the argument `f xs`, and of the
984 result, is `[alpha]`. The unification variable `alpha` stands for the
985 as-yet-unknown type of the elements of the list.
986
987 As type inference progresses we may learn more about `alpha`. For example, suppose
988 `f` has the type
989 f :: forall b. b -> [Maybe b]
990 Then we instantiate `f`'s type with another fresh unification variable, say
991 `beta`; and equate `f`'s result type with reverse's argument type, thus
992 `[alpha] ~ [Maybe beta]`.
993
994 Now we can solve this equality to learn that `alpha ~ Maybe beta`, so we've
995 refined our knowledge about `alpha`. And so on.
996
997 If you found this Note useful, you may also want to have a look at
998 Section 5 of "Practical type inference for higher rank types" (Peyton Jones,
999 Vytiniotis, Weirich and Shields. J. Functional Programming. 2011).
1000
1001 Note [What is zonking?]
1002 ~~~~~~~~~~~~~~~~~~~~~~~
1003 GHC relies heavily on mutability in the typechecker for efficient operation.
1004 For this reason, throughout much of the type checking process meta type
1005 variables (the MetaTv constructor of TcTyVarDetails) are represented by mutable
1006 variables (known as TcRefs).
1007
1008 Zonking is the process of ripping out these mutable variables and replacing them
1009 with a real TcType. This involves traversing the entire type expression, but the
1010 interesting part of replacing the mutable variables occurs in zonkTyVarOcc.
1011
1012 There are two ways to zonk a Type:
1013
1014 * zonkTcTypeToType, which is intended to be used at the end of type-checking
1015 for the final zonk. It has to deal with unfilled metavars, either by filling
1016 it with a value like Any or failing (determined by the UnboundTyVarZonker
1017 used).
1018
1019 * zonkTcType, which will happily ignore unfilled metavars. This is the
1020 appropriate function to use while in the middle of type-checking.
1021
1022 Note [Zonking to Skolem]
1023 ~~~~~~~~~~~~~~~~~~~~~~~~
1024 We used to zonk quantified type variables to regular TyVars. However, this
1025 leads to problems. Consider this program from the regression test suite:
1026
1027 eval :: Int -> String -> String -> String
1028 eval 0 root actual = evalRHS 0 root actual
1029
1030 evalRHS :: Int -> a
1031 evalRHS 0 root actual = eval 0 root actual
1032
1033 It leads to the deferral of an equality (wrapped in an implication constraint)
1034
1035 forall a. () => ((String -> String -> String) ~ a)
1036
1037 which is propagated up to the toplevel (see TcSimplify.tcSimplifyInferCheck).
1038 In the meantime `a' is zonked and quantified to form `evalRHS's signature.
1039 This has the *side effect* of also zonking the `a' in the deferred equality
1040 (which at this point is being handed around wrapped in an implication
1041 constraint).
1042
1043 Finally, the equality (with the zonked `a') will be handed back to the
1044 simplifier by TcRnDriver.tcRnSrcDecls calling TcSimplify.tcSimplifyTop.
1045 If we zonk `a' with a regular type variable, we will have this regular type
1046 variable now floating around in the simplifier, which in many places assumes to
1047 only see proper TcTyVars.
1048
1049 We can avoid this problem by zonking with a skolem. The skolem is rigid
1050 (which we require for a quantified variable), but is still a TcTyVar that the
1051 simplifier knows how to deal with.
1052
1053 Note [Silly Type Synonyms]
1054 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1055 Consider this:
1056 type C u a = u -- Note 'a' unused
1057
1058 foo :: (forall a. C u a -> C u a) -> u
1059 foo x = ...
1060
1061 bar :: Num u => u
1062 bar = foo (\t -> t + t)
1063
1064 * From the (\t -> t+t) we get type {Num d} => d -> d
1065 where d is fresh.
1066
1067 * Now unify with type of foo's arg, and we get:
1068 {Num (C d a)} => C d a -> C d a
1069 where a is fresh.
1070
1071 * Now abstract over the 'a', but float out the Num (C d a) constraint
1072 because it does not 'really' mention a. (see exactTyVarsOfType)
1073 The arg to foo becomes
1074 \/\a -> \t -> t+t
1075
1076 * So we get a dict binding for Num (C d a), which is zonked to give
1077 a = ()
1078 [Note Sept 04: now that we are zonking quantified type variables
1079 on construction, the 'a' will be frozen as a regular tyvar on
1080 quantification, so the floated dict will still have type (C d a).
1081 Which renders this whole note moot; happily!]
1082
1083 * Then the \/\a abstraction has a zonked 'a' in it.
1084
1085 All very silly. I think its harmless to ignore the problem. We'll end up with
1086 a \/\a in the final result but all the occurrences of a will be zonked to ()
1087
1088 ************************************************************************
1089 * *
1090 Zonking types
1091 * *
1092 ************************************************************************
1093
1094 -}
1095
1096 -- | @tcGetGlobalTyCoVars@ returns a fully-zonked set of *scoped* tyvars free in
1097 -- the environment. To improve subsequent calls to the same function it writes
1098 -- the zonked set back into the environment. Note that this returns all
1099 -- variables free in anything (term-level or type-level) in scope. We thus
1100 -- don't have to worry about clashes with things that are not in scope, because
1101 -- if they are reachable, then they'll be returned here.
1102 tcGetGlobalTyCoVars :: TcM TcTyVarSet
1103 tcGetGlobalTyCoVars
1104 = do { (TcLclEnv {tcl_tyvars = gtv_var}) <- getLclEnv
1105 ; gbl_tvs <- readMutVar gtv_var
1106 ; gbl_tvs' <- zonkTyCoVarsAndFV gbl_tvs
1107 ; writeMutVar gtv_var gbl_tvs'
1108 ; return gbl_tvs' }
1109
1110 zonkTcTypeAndFV :: TcType -> TcM TyCoVarSet
1111 -- Zonk a type and take its free variables
1112 -- With kind polymorphism it can be essential to zonk *first*
1113 -- so that we find the right set of free variables. Eg
1114 -- forall k1. forall (a:k2). a
1115 -- where k2:=k1 is in the substitution. We don't want
1116 -- k2 to look free in this type!
1117 -- NB: This might be called from within the knot, so don't use
1118 -- smart constructors. See Note [Zonking within the knot] in TcHsType
1119 zonkTcTypeAndFV ty
1120 = tyCoVarsOfType <$> mapType (zonkTcTypeMapper { tcm_smart = False }) () ty
1121
1122 zonkTyCoVar :: TyCoVar -> TcM TcType
1123 -- Works on TyVars and TcTyVars
1124 zonkTyCoVar tv | isTcTyVar tv = zonkTcTyVar tv
1125 | isTyVar tv = mkTyVarTy <$> zonkTyCoVarKind tv
1126 | otherwise = ASSERT2( isCoVar tv, ppr tv )
1127 mkCoercionTy . mkCoVarCo <$> zonkTyCoVarKind tv
1128 -- Hackily, when typechecking type and class decls
1129 -- we have TyVars in scopeadded (only) in
1130 -- TcHsType.tcTyClTyVars, but it seems
1131 -- painful to make them into TcTyVars there
1132
1133 zonkTyCoVarsAndFV :: TyCoVarSet -> TcM TyCoVarSet
1134 zonkTyCoVarsAndFV tycovars = tyCoVarsOfTypes <$> mapM zonkTyCoVar (varSetElems tycovars)
1135
1136 zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
1137 zonkTcTyVars tyvars = mapM zonkTcTyVar tyvars
1138
1139 ----------------- Types
1140 zonkTyCoVarKind :: TyCoVar -> TcM TyCoVar
1141 zonkTyCoVarKind tv = do { kind' <- zonkTcType (tyVarKind tv)
1142 ; return (setTyVarKind tv kind') }
1143
1144 zonkTcTypes :: [TcType] -> TcM [TcType]
1145 zonkTcTypes tys = mapM zonkTcType tys
1146
1147 {-
1148 ************************************************************************
1149 * *
1150 Zonking constraints
1151 * *
1152 ************************************************************************
1153 -}
1154
1155 zonkImplication :: Implication -> TcM Implication
1156 zonkImplication implic@(Implic { ic_skols = skols
1157 , ic_given = given
1158 , ic_wanted = wanted
1159 , ic_info = info })
1160 = do { skols' <- mapM zonkTcTyCoVarBndr skols -- Need to zonk their kinds!
1161 -- as Trac #7230 showed
1162 ; given' <- mapM zonkEvVar given
1163 ; info' <- zonkSkolemInfo info
1164 ; wanted' <- zonkWCRec wanted
1165 ; return (implic { ic_skols = skols'
1166 , ic_given = given'
1167 , ic_wanted = wanted'
1168 , ic_info = info' }) }
1169
1170 zonkEvVar :: EvVar -> TcM EvVar
1171 zonkEvVar var = do { ty' <- zonkTcType (varType var)
1172 ; return (setVarType var ty') }
1173
1174
1175 zonkWC :: WantedConstraints -> TcM WantedConstraints
1176 zonkWC wc = zonkWCRec wc
1177
1178 zonkWCRec :: WantedConstraints -> TcM WantedConstraints
1179 zonkWCRec (WC { wc_simple = simple, wc_impl = implic, wc_insol = insol })
1180 = do { simple' <- zonkSimples simple
1181 ; implic' <- mapBagM zonkImplication implic
1182 ; insol' <- zonkSimples insol
1183 ; return (WC { wc_simple = simple', wc_impl = implic', wc_insol = insol' }) }
1184
1185 zonkSimples :: Cts -> TcM Cts
1186 zonkSimples cts = do { cts' <- mapBagM zonkCt' cts
1187 ; traceTc "zonkSimples done:" (ppr cts')
1188 ; return cts' }
1189
1190 zonkCt' :: Ct -> TcM Ct
1191 zonkCt' ct = zonkCt ct
1192
1193 zonkCt :: Ct -> TcM Ct
1194 zonkCt ct@(CHoleCan { cc_ev = ev })
1195 = do { ev' <- zonkCtEvidence ev
1196 ; return $ ct { cc_ev = ev' } }
1197 zonkCt ct
1198 = do { fl' <- zonkCtEvidence (cc_ev ct)
1199 ; return (mkNonCanonical fl') }
1200
1201 zonkCtEvidence :: CtEvidence -> TcM CtEvidence
1202 zonkCtEvidence ctev@(CtGiven { ctev_pred = pred })
1203 = do { pred' <- zonkTcType pred
1204 ; return (ctev { ctev_pred = pred'}) }
1205 zonkCtEvidence ctev@(CtWanted { ctev_pred = pred, ctev_dest = dest })
1206 = do { pred' <- zonkTcType pred
1207 ; let dest' = case dest of
1208 EvVarDest ev -> EvVarDest $ setVarType ev pred'
1209 -- necessary in simplifyInfer
1210 HoleDest h -> HoleDest h
1211 ; return (ctev { ctev_pred = pred', ctev_dest = dest' }) }
1212 zonkCtEvidence ctev@(CtDerived { ctev_pred = pred })
1213 = do { pred' <- zonkTcType pred
1214 ; return (ctev { ctev_pred = pred' }) }
1215
1216 zonkSkolemInfo :: SkolemInfo -> TcM SkolemInfo
1217 zonkSkolemInfo (SigSkol cx ty) = do { ty <- readExpType ty
1218 ; ty' <- zonkTcType ty
1219 ; return (SigSkol cx (mkCheckExpType ty')) }
1220 zonkSkolemInfo (InferSkol ntys) = do { ntys' <- mapM do_one ntys
1221 ; return (InferSkol ntys') }
1222 where
1223 do_one (n, ty) = do { ty' <- zonkTcType ty; return (n, ty') }
1224 zonkSkolemInfo skol_info = return skol_info
1225
1226 {-
1227 %************************************************************************
1228 %* *
1229 \subsection{Zonking -- the main work-horses: zonkTcType, zonkTcTyVar}
1230 * *
1231 * For internal use only! *
1232 * *
1233 ************************************************************************
1234
1235 -}
1236
1237 -- zonkId is used *during* typechecking just to zonk the Id's type
1238 zonkId :: TcId -> TcM TcId
1239 zonkId id
1240 = do { ty' <- zonkTcType (idType id)
1241 ; return (Id.setIdType id ty') }
1242
1243 -- | A suitable TyCoMapper for zonking a type inside the knot, and
1244 -- before all metavars are filled in.
1245 zonkTcTypeMapper :: TyCoMapper () TcM
1246 zonkTcTypeMapper = TyCoMapper
1247 { tcm_smart = True
1248 , tcm_tyvar = const zonkTcTyVar
1249 , tcm_covar = const (\cv -> mkCoVarCo <$> zonkTyCoVarKind cv)
1250 , tcm_hole = hole
1251 , tcm_tybinder = \_env tv _vis -> ((), ) <$> zonkTcTyCoVarBndr tv }
1252 where
1253 hole :: () -> CoercionHole -> Role -> Type -> Type
1254 -> TcM Coercion
1255 hole _ h r t1 t2
1256 = do { contents <- unpackCoercionHole_maybe h
1257 ; case contents of
1258 Just co -> do { co <- zonkCo co
1259 ; checkCoercionHole co h r t1 t2 }
1260 Nothing -> do { t1 <- zonkTcType t1
1261 ; t2 <- zonkTcType t2
1262 ; return $ mkHoleCo h r t1 t2 } }
1263
1264
1265 -- For unbound, mutable tyvars, zonkType uses the function given to it
1266 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
1267 -- type variable and zonks the kind too
1268 zonkTcType :: TcType -> TcM TcType
1269 zonkTcType = mapType zonkTcTypeMapper ()
1270
1271 -- | "Zonk" a coercion -- really, just zonk any types in the coercion
1272 zonkCo :: Coercion -> TcM Coercion
1273 zonkCo = mapCoercion zonkTcTypeMapper ()
1274
1275 zonkTcTyCoVarBndr :: TcTyCoVar -> TcM TcTyCoVar
1276 -- A tyvar binder is never a unification variable (MetaTv),
1277 -- rather it is always a skolems. BUT it may have a kind
1278 -- that has not yet been zonked, and may include kind
1279 -- unification variables.
1280 zonkTcTyCoVarBndr tyvar
1281 -- can't use isCoVar, because it looks at a TyCon. Argh.
1282 = ASSERT2( isImmutableTyVar tyvar || (not $ isTyVar tyvar), ppr tyvar ) do
1283 updateTyVarKindM zonkTcType tyvar
1284
1285 -- | Zonk a TyBinder
1286 zonkTcTyBinder :: TcTyBinder -> TcM TcTyBinder
1287 zonkTcTyBinder (Anon ty) = Anon <$> zonkTcType ty
1288 zonkTcTyBinder (Named tv vis) = Named <$> zonkTcTyCoVarBndr tv <*> pure vis
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 $ repSplitAppTys ty)
1325 zonkTidyTcType
1326 -- NB: Use *rep*splitAppTys, else we get #11313
1327
1328 -- | Make an 'ErrorThing' storing a type, with some extra args known about
1329 mkTypeErrorThingArgs :: TcType -> Int -> ErrorThing
1330 mkTypeErrorThingArgs ty num_args
1331 = ErrorThing ty (Just $ (length $ snd $ repSplitAppTys ty) + num_args)
1332 zonkTidyTcType
1333
1334 zonkTidyOrigin :: TidyEnv -> CtOrigin -> TcM (TidyEnv, CtOrigin)
1335 zonkTidyOrigin env (GivenOrigin skol_info)
1336 = do { skol_info1 <- zonkSkolemInfo skol_info
1337 ; let skol_info2 = tidySkolemInfo env skol_info1
1338 ; return (env, GivenOrigin skol_info2) }
1339 zonkTidyOrigin env orig@(TypeEqOrigin { uo_actual = act
1340 , uo_expected = exp
1341 , uo_thing = m_thing })
1342 = do { (env1, act') <- zonkTidyTcType env act
1343 ; mb_exp <- readExpType_maybe exp -- it really should be filled in.
1344 -- unless we're debugging.
1345 ; (env2, exp') <- case mb_exp of
1346 Just ty -> second mkCheckExpType <$> zonkTidyTcType env1 ty
1347 Nothing -> return (env1, exp)
1348 ; (env3, m_thing') <- zonkTidyErrorThing env2 m_thing
1349 ; return ( env3, orig { uo_actual = act'
1350 , uo_expected = exp'
1351 , uo_thing = m_thing' }) }
1352 zonkTidyOrigin env (KindEqOrigin ty1 m_ty2 orig t_or_k)
1353 = do { (env1, ty1') <- zonkTidyTcType env ty1
1354 ; (env2, m_ty2') <- case m_ty2 of
1355 Just ty2 -> second Just <$> zonkTidyTcType env1 ty2
1356 Nothing -> return (env1, Nothing)
1357 ; (env3, orig') <- zonkTidyOrigin env2 orig
1358 ; return (env3, KindEqOrigin ty1' m_ty2' orig' t_or_k) }
1359 zonkTidyOrigin env (FunDepOrigin1 p1 l1 p2 l2)
1360 = do { (env1, p1') <- zonkTidyTcType env p1
1361 ; (env2, p2') <- zonkTidyTcType env1 p2
1362 ; return (env2, FunDepOrigin1 p1' l1 p2' l2) }
1363 zonkTidyOrigin env (FunDepOrigin2 p1 o1 p2 l2)
1364 = do { (env1, p1') <- zonkTidyTcType env p1
1365 ; (env2, p2') <- zonkTidyTcType env1 p2
1366 ; (env3, o1') <- zonkTidyOrigin env2 o1
1367 ; return (env3, FunDepOrigin2 p1' o1' p2' l2) }
1368 zonkTidyOrigin env orig = return (env, orig)
1369
1370 zonkTidyErrorThing :: TidyEnv -> Maybe ErrorThing
1371 -> TcM (TidyEnv, Maybe ErrorThing)
1372 zonkTidyErrorThing env (Just (ErrorThing thing n_args zonker))
1373 = do { (env', thing') <- zonker env thing
1374 ; return (env', Just $ ErrorThing thing' n_args zonker) }
1375 zonkTidyErrorThing env Nothing
1376 = return (env, Nothing)
1377
1378 ----------------
1379 tidyCt :: TidyEnv -> Ct -> Ct
1380 -- Used only in error reporting
1381 -- Also converts it to non-canonical
1382 tidyCt env ct
1383 = case ct of
1384 CHoleCan { cc_ev = ev }
1385 -> ct { cc_ev = tidy_ev env ev }
1386 _ -> mkNonCanonical (tidy_ev env (ctEvidence ct))
1387 where
1388 tidy_ev :: TidyEnv -> CtEvidence -> CtEvidence
1389 -- NB: we do not tidy the ctev_evar field because we don't
1390 -- show it in error messages
1391 tidy_ev env ctev@(CtGiven { ctev_pred = pred })
1392 = ctev { ctev_pred = tidyType env pred }
1393 tidy_ev env ctev@(CtWanted { ctev_pred = pred })
1394 = ctev { ctev_pred = tidyType env pred }
1395 tidy_ev env ctev@(CtDerived { ctev_pred = pred })
1396 = ctev { ctev_pred = tidyType env pred }
1397
1398 ----------------
1399 tidyEvVar :: TidyEnv -> EvVar -> EvVar
1400 tidyEvVar env var = setVarType var (tidyType env (varType var))
1401
1402 ----------------
1403 tidySkolemInfo :: TidyEnv -> SkolemInfo -> SkolemInfo
1404 tidySkolemInfo env (DerivSkol ty) = DerivSkol (tidyType env ty)
1405 tidySkolemInfo env (SigSkol cx ty) = SigSkol cx (mkCheckExpType $
1406 tidyType env $
1407 checkingExpType "tidySkolemInfo" ty)
1408 tidySkolemInfo env (InferSkol ids) = InferSkol (mapSnd (tidyType env) ids)
1409 tidySkolemInfo env (UnifyForAllSkol ty) = UnifyForAllSkol (tidyType env ty)
1410 tidySkolemInfo _ info = info