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