ae5e031f319b848f87af14af67b5c6f9847dc4a4
[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, zonkTcTyVarToTyVar,
71 zonkTyCoVarsAndFV, zonkTcTypeAndFV,
72 zonkTyCoVarsAndFVList,
73 zonkTcTypeAndSplitDepVars, zonkTcTypesAndSplitDepVars,
74 zonkQuantifiedTyVar, zonkQuantifiedTyVarOrType,
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 -> TcType -- ^ Type to instantiate
437 -> TcM ([TcTyVar], TcThetaType, TcType) -- ^ Result
438 -- (type vars, preds (incl equalities), rho)
439 tcInstType inst_tyvars ty
440 = case tcSplitForAllTys ty 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 ; return (tyvars', theta, tau) }
450
451 tcSkolDFunType :: Type -> TcM ([TcTyVar], TcThetaType, TcType)
452 -- Instantiate a type signature with skolem constants.
453 -- We could give them fresh names, but no need to do so
454 tcSkolDFunType ty = tcInstType tcInstSuperSkolTyVars ty
455
456 tcSuperSkolTyVars :: [TyVar] -> (TCvSubst, [TcTyVar])
457 -- Make skolem constants, but do *not* give them new names, as above
458 -- Moreover, make them "super skolems"; see comments with superSkolemTv
459 -- see Note [Kind substitution when instantiating]
460 -- Precondition: tyvars should be ordered by scoping
461 tcSuperSkolTyVars = mapAccumL tcSuperSkolTyVar emptyTCvSubst
462
463 tcSuperSkolTyVar :: TCvSubst -> TyVar -> (TCvSubst, TcTyVar)
464 tcSuperSkolTyVar subst tv
465 = (extendTvSubstWithClone subst tv new_tv, new_tv)
466 where
467 kind = substTyUnchecked subst (tyVarKind tv)
468 new_tv = mkTcTyVar (tyVarName tv) kind superSkolemTv
469
470 -- Wrappers
471 -- we need to be able to do this from outside the TcM monad:
472 tcInstSkolTyVarsLoc :: SrcSpan -> [TyVar] -> TcRnIf gbl lcl (TCvSubst, [TcTyVar])
473 tcInstSkolTyVarsLoc loc = instSkolTyCoVars (mkTcSkolTyVar loc False)
474
475 -- | Given a list of @['TyVar']@, skolemize the type variables,
476 -- returning a substitution mapping the original tyvars to the
477 -- skolems, and the list of newly bound skolems. See also
478 -- tcInstSkolTyVars' for a precondition. The resulting
479 -- skolems are non-overlappable; see Note [Overlap and deriving]
480 -- for an example where this matters.
481 tcInstSkolTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
482 tcInstSkolTyVars = tcInstSkolTyVars' False emptyTCvSubst
483
484 tcInstSuperSkolTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
485 tcInstSuperSkolTyVars = tcInstSuperSkolTyVarsX emptyTCvSubst
486
487 tcInstSuperSkolTyVarsX :: TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
488 tcInstSuperSkolTyVarsX subst = tcInstSkolTyVars' True subst
489
490 tcInstSkolTyVars' :: Bool -> TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
491 -- Precondition: tyvars should be ordered (kind vars first)
492 -- see Note [Kind substitution when instantiating]
493 -- Get the location from the monad; this is a complete freshening operation
494 tcInstSkolTyVars' overlappable subst tvs
495 = do { loc <- getSrcSpanM
496 ; instSkolTyCoVarsX (mkTcSkolTyVar loc overlappable) subst tvs }
497
498 mkTcSkolTyVar :: SrcSpan -> Bool -> Unique -> Name -> Kind -> TcTyVar
499 mkTcSkolTyVar loc overlappable uniq old_name kind
500 = mkTcTyVar (mkInternalName uniq (getOccName old_name) loc)
501 kind
502 (SkolemTv overlappable)
503
504 tcInstSigTyVarsLoc :: SrcSpan -> [TyVar]
505 -> TcRnIf gbl lcl (TCvSubst, [TcTyVar])
506 -- We specify the location
507 tcInstSigTyVarsLoc loc = instSkolTyCoVars (mkTcSkolTyVar loc False)
508
509 tcInstSigTyVars :: [TyVar] -> TcRnIf gbl lcl (TCvSubst, [TcTyVar])
510 -- Get the location from the TyVar itself, not the monad
511 tcInstSigTyVars
512 = instSkolTyCoVars mk_tv
513 where
514 mk_tv uniq old_name kind
515 = mkTcTyVar (setNameUnique old_name uniq) kind (SkolemTv False)
516
517 tcInstSkolType :: TcType -> TcM ([TcTyVar], TcThetaType, TcType)
518 -- Instantiate a type with fresh skolem constants
519 -- Binding location comes from the monad
520 tcInstSkolType ty = tcInstType tcInstSkolTyVars ty
521
522 ------------------
523 freshenTyVarBndrs :: [TyVar] -> TcRnIf gbl lcl (TCvSubst, [TyVar])
524 -- ^ Give fresh uniques to a bunch of TyVars, but they stay
525 -- as TyVars, rather than becoming TcTyVars
526 -- Used in FamInst.newFamInst, and Inst.newClsInst
527 freshenTyVarBndrs = instSkolTyCoVars mk_tv
528 where
529 mk_tv uniq old_name kind = mkTyVar (setNameUnique old_name uniq) kind
530
531 freshenCoVarBndrsX :: TCvSubst -> [CoVar] -> TcRnIf gbl lcl (TCvSubst, [CoVar])
532 -- ^ Give fresh uniques to a bunch of CoVars
533 -- Used in FamInst.newFamInst
534 freshenCoVarBndrsX subst = instSkolTyCoVarsX mk_cv subst
535 where
536 mk_cv uniq old_name kind = mkCoVar (setNameUnique old_name uniq) kind
537
538 ------------------
539 instSkolTyCoVars :: (Unique -> Name -> Kind -> TyCoVar)
540 -> [TyVar] -> TcRnIf gbl lcl (TCvSubst, [TyCoVar])
541 instSkolTyCoVars mk_tcv = instSkolTyCoVarsX mk_tcv emptyTCvSubst
542
543 instSkolTyCoVarsX :: (Unique -> Name -> Kind -> TyCoVar)
544 -> TCvSubst -> [TyCoVar] -> TcRnIf gbl lcl (TCvSubst, [TyCoVar])
545 instSkolTyCoVarsX mk_tcv = mapAccumLM (instSkolTyCoVarX mk_tcv)
546
547 instSkolTyCoVarX :: (Unique -> Name -> Kind -> TyCoVar)
548 -> TCvSubst -> TyCoVar -> TcRnIf gbl lcl (TCvSubst, TyCoVar)
549 instSkolTyCoVarX mk_tcv subst tycovar
550 = do { uniq <- newUnique -- using a new unique is critical. See
551 -- Note [Skolems in zonkSyntaxExpr] in TcHsSyn
552 ; let new_tcv = mk_tcv uniq old_name kind
553 subst1 | isTyVar new_tcv
554 = extendTvSubstWithClone subst tycovar new_tcv
555 | otherwise
556 = extendCvSubstWithClone subst tycovar new_tcv
557 ; return (subst1, new_tcv) }
558 where
559 old_name = tyVarName tycovar
560 kind = substTyUnchecked subst (tyVarKind tycovar)
561
562 newFskTyVar :: TcType -> TcM TcTyVar
563 newFskTyVar fam_ty
564 = do { uniq <- newUnique
565 ; let name = mkSysTvName uniq (fsLit "fsk")
566 ; return (mkTcTyVar name (typeKind fam_ty) (FlatSkol fam_ty)) }
567 {-
568 Note [Kind substitution when instantiating]
569 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
570 When we instantiate a bunch of kind and type variables, first we
571 expect them to be topologically sorted.
572 Then we have to instantiate the kind variables, build a substitution
573 from old variables to the new variables, then instantiate the type
574 variables substituting the original kind.
575
576 Exemple: If we want to instantiate
577 [(k1 :: *), (k2 :: *), (a :: k1 -> k2), (b :: k1)]
578 we want
579 [(?k1 :: *), (?k2 :: *), (?a :: ?k1 -> ?k2), (?b :: ?k1)]
580 instead of the buggous
581 [(?k1 :: *), (?k2 :: *), (?a :: k1 -> k2), (?b :: k1)]
582
583
584 ************************************************************************
585 * *
586 MetaTvs (meta type variables; mutable)
587 * *
588 ************************************************************************
589 -}
590
591 mkMetaTyVarName :: Unique -> FastString -> Name
592 -- Makes a /System/ Name, which is eagerly eliminated by
593 -- the unifier; see TcUnify.nicer_to_update_tv1, and
594 -- TcCanonical.canEqTyVarTyVar (nicer_to_update_tv2)
595 mkMetaTyVarName uniq str = mkSysTvName uniq str
596
597 newSigTyVar :: Name -> Kind -> TcM TcTyVar
598 newSigTyVar name kind
599 = do { details <- newMetaDetails SigTv
600 ; return (mkTcTyVar name kind details) }
601
602 newFmvTyVar :: TcType -> TcM TcTyVar
603 -- Very like newMetaTyVar, except sets mtv_tclvl to one less
604 -- so that the fmv is untouchable.
605 newFmvTyVar fam_ty
606 = do { uniq <- newUnique
607 ; ref <- newMutVar Flexi
608 ; cur_lvl <- getTcLevel
609 ; let details = MetaTv { mtv_info = FlatMetaTv
610 , mtv_ref = ref
611 , mtv_tclvl = fmvTcLevel cur_lvl }
612 name = mkMetaTyVarName uniq (fsLit "s")
613 ; return (mkTcTyVar name (typeKind fam_ty) details) }
614
615 newMetaDetails :: MetaInfo -> TcM TcTyVarDetails
616 newMetaDetails info
617 = do { ref <- newMutVar Flexi
618 ; tclvl <- getTcLevel
619 ; return (MetaTv { mtv_info = info
620 , mtv_ref = ref
621 , mtv_tclvl = tclvl }) }
622
623 cloneMetaTyVar :: TcTyVar -> TcM TcTyVar
624 cloneMetaTyVar tv
625 = ASSERT( isTcTyVar tv )
626 do { uniq <- newUnique
627 ; ref <- newMutVar Flexi
628 ; let name' = setNameUnique (tyVarName tv) uniq
629 details' = case tcTyVarDetails tv of
630 details@(MetaTv {}) -> details { mtv_ref = ref }
631 _ -> pprPanic "cloneMetaTyVar" (ppr tv)
632 ; return (mkTcTyVar name' (tyVarKind tv) details') }
633
634 -- Works for both type and kind variables
635 readMetaTyVar :: TyVar -> TcM MetaDetails
636 readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
637 readMutVar (metaTvRef tyvar)
638
639 isFilledMetaTyVar :: TyVar -> TcM Bool
640 -- True of a filled-in (Indirect) meta type variable
641 isFilledMetaTyVar tv
642 | MetaTv { mtv_ref = ref } <- tcTyVarDetails tv
643 = do { details <- readMutVar ref
644 ; return (isIndirect details) }
645 | otherwise = return False
646
647 isUnfilledMetaTyVar :: TyVar -> TcM Bool
648 -- True of a un-filled-in (Flexi) meta type variable
649 isUnfilledMetaTyVar tv
650 | MetaTv { mtv_ref = ref } <- tcTyVarDetails tv
651 = do { details <- readMutVar ref
652 ; return (isFlexi details) }
653 | otherwise = return False
654
655 --------------------
656 -- Works with both type and kind variables
657 writeMetaTyVar :: TcTyVar -> TcType -> TcM ()
658 -- Write into a currently-empty MetaTyVar
659
660 writeMetaTyVar tyvar ty
661 | not debugIsOn
662 = writeMetaTyVarRef tyvar (metaTvRef tyvar) ty
663
664 -- Everything from here on only happens if DEBUG is on
665 | not (isTcTyVar tyvar)
666 = WARN( True, text "Writing to non-tc tyvar" <+> ppr tyvar )
667 return ()
668
669 | MetaTv { mtv_ref = ref } <- tcTyVarDetails tyvar
670 = writeMetaTyVarRef tyvar ref ty
671
672 | otherwise
673 = WARN( True, text "Writing to non-meta tyvar" <+> ppr tyvar )
674 return ()
675
676 --------------------
677 writeMetaTyVarRef :: TcTyVar -> TcRef MetaDetails -> TcType -> TcM ()
678 -- Here the tyvar is for error checking only;
679 -- the ref cell must be for the same tyvar
680 writeMetaTyVarRef tyvar ref ty
681 | not debugIsOn
682 = do { traceTc "writeMetaTyVar" (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)
683 <+> text ":=" <+> ppr ty)
684 ; writeTcRef ref (Indirect ty) }
685
686 -- Everything from here on only happens if DEBUG is on
687 | otherwise
688 = do { meta_details <- readMutVar ref;
689 -- Zonk kinds to allow the error check to work
690 ; zonked_tv_kind <- zonkTcType tv_kind
691 ; zonked_ty_kind <- zonkTcType ty_kind
692
693 -- Check for double updates
694 ; ASSERT2( isFlexi meta_details,
695 hang (text "Double update of meta tyvar")
696 2 (ppr tyvar $$ ppr meta_details) )
697
698 traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty)
699 ; writeMutVar ref (Indirect ty)
700 ; when ( not (isPredTy tv_kind)
701 -- Don't check kinds for updates to coercion variables
702 && not (zonked_ty_kind `tcEqKind` zonked_tv_kind))
703 $ WARN( True, hang (text "Ill-kinded update to meta tyvar")
704 2 ( ppr tyvar <+> text "::" <+> (ppr tv_kind $$ ppr zonked_tv_kind)
705 <+> text ":="
706 <+> ppr ty <+> text "::" <+> (ppr ty_kind $$ ppr zonked_ty_kind) ) )
707 (return ()) }
708 where
709 tv_kind = tyVarKind tyvar
710 ty_kind = typeKind ty
711
712 {-
713 % Generating fresh variables for pattern match check
714 -}
715
716 -- UNINSTANTIATED VERSION OF tcInstSkolTyCoVars
717 genInstSkolTyVarsX :: SrcSpan -> TCvSubst -> [TyVar]
718 -> TcRnIf gbl lcl (TCvSubst, [TcTyVar])
719 -- Precondition: tyvars should be scoping-ordered
720 -- see Note [Kind substitution when instantiating]
721 -- Get the location from the monad; this is a complete freshening operation
722 genInstSkolTyVarsX loc subst tvs = instSkolTyCoVarsX (mkTcSkolTyVar loc False) subst tvs
723
724 {-
725 ************************************************************************
726 * *
727 MetaTvs: TauTvs
728 * *
729 ************************************************************************
730
731 Note [Never need to instantiate coercion variables]
732 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
733 With coercion variables sloshing around in types, it might seem that we
734 sometimes need to instantiate coercion variables. This would be problematic,
735 because coercion variables inhabit unboxed equality (~#), and the constraint
736 solver thinks in terms only of boxed equality (~). The solution is that
737 we never need to instantiate coercion variables in the first place.
738
739 The tyvars that we need to instantiate come from the types of functions,
740 data constructors, and patterns. These will never be quantified over
741 coercion variables, except for the special case of the promoted Eq#. But,
742 that can't ever appear in user code, so we're safe!
743 -}
744
745 newAnonMetaTyVar :: MetaInfo -> Kind -> TcM TcTyVar
746 -- Make a new meta tyvar out of thin air
747 newAnonMetaTyVar meta_info kind
748 = do { uniq <- newUnique
749 ; let name = mkMetaTyVarName uniq s
750 s = case meta_info of
751 TauTv -> fsLit "t"
752 FlatMetaTv -> fsLit "fmv"
753 SigTv -> fsLit "a"
754 ; details <- newMetaDetails meta_info
755 ; return (mkTcTyVar name kind details) }
756
757 newFlexiTyVar :: Kind -> TcM TcTyVar
758 newFlexiTyVar kind = newAnonMetaTyVar TauTv kind
759
760 newFlexiTyVarTy :: Kind -> TcM TcType
761 newFlexiTyVarTy kind = do
762 tc_tyvar <- newFlexiTyVar kind
763 return (mkTyVarTy tc_tyvar)
764
765 newFlexiTyVarTys :: Int -> Kind -> TcM [TcType]
766 newFlexiTyVarTys n kind = mapM newFlexiTyVarTy (nOfThem n kind)
767
768 -- | Create a tyvar that can be a lifted or unlifted type.
769 newOpenFlexiTyVarTy :: TcM TcType
770 newOpenFlexiTyVarTy
771 = do { rr <- newFlexiTyVarTy runtimeRepTy
772 ; newFlexiTyVarTy (tYPE rr) }
773
774 newMetaSigTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
775 newMetaSigTyVars = mapAccumLM newMetaSigTyVarX emptyTCvSubst
776
777 newMetaTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
778 -- Instantiate with META type variables
779 -- Note that this works for a sequence of kind, type, and coercion variables
780 -- variables. Eg [ (k:*), (a:k->k) ]
781 -- Gives [ (k7:*), (a8:k7->k7) ]
782 newMetaTyVars = mapAccumLM newMetaTyVarX emptyTCvSubst
783 -- emptyTCvSubst has an empty in-scope set, but that's fine here
784 -- Since the tyvars are freshly made, they cannot possibly be
785 -- captured by any existing for-alls.
786
787 newMetaTyVarX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
788 -- Make a new unification variable tyvar whose Name and Kind come from
789 -- an existing TyVar. We substitute kind variables in the kind.
790 newMetaTyVarX subst tyvar = new_meta_tv_x TauTv subst tyvar
791
792 newMetaSigTyVarX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
793 -- Just like newMetaTyVarX, but make a SigTv
794 newMetaSigTyVarX subst tyvar = new_meta_tv_x SigTv subst tyvar
795
796 new_meta_tv_x :: MetaInfo -> TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
797 new_meta_tv_x info subst tyvar
798 = do { uniq <- newUnique
799 ; details <- newMetaDetails info
800 ; let name = mkSystemName uniq (getOccName tyvar)
801 -- See Note [Name of an instantiated type variable]
802 kind = substTyUnchecked subst (tyVarKind tyvar)
803 new_tv = mkTcTyVar name kind details
804 subst1 = extendTvSubstWithClone subst tyvar new_tv
805 ; return (subst1, new_tv) }
806
807 {- Note [Name of an instantiated type variable]
808 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
809 At the moment we give a unification variable a System Name, which
810 influences the way it is tidied; see TypeRep.tidyTyVarBndr.
811
812 ************************************************************************
813 * *
814 Quantification
815 * *
816 ************************************************************************
817
818 Note [quantifyTyVars]
819 ~~~~~~~~~~~~~~~~~~~~~
820 quantifyTyVars is given the free vars of a type that we
821 are about to wrap in a forall.
822
823 It takes these free type/kind variables (partitioned into dependent and
824 non-dependent variables) and
825 1. Zonks them and remove globals and covars
826 2. Extends kvs1 with free kind vars in the kinds of tvs (removing globals)
827 3. Calls zonkQuantifiedTyVar on each
828
829 Step (2) is often unimportant, because the kind variable is often
830 also free in the type. Eg
831 Typeable k (a::k)
832 has free vars {k,a}. But the type (see Trac #7916)
833 (f::k->*) (a::k)
834 has free vars {f,a}, but we must add 'k' as well! Hence step (3).
835
836 * This function distinguishes between dependent and non-dependent
837 variables only to keep correct defaulting behavior with -XNoPolyKinds.
838 With -XPolyKinds, it treats both classes of variables identically.
839
840 * quantifyTyVars never quantifies over
841 - a coercion variable
842 - a runtime-rep variable
843
844 Note [quantifyTyVars determinism]
845 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
846 The results of quantifyTyVars are wrapped in a forall and can end up in the
847 interface file. One such example is inferred type signatures. They also affect
848 the results of optimizations, for example worker-wrapper. This means that to
849 get deterministic builds quantifyTyVars needs to be deterministic.
850
851 To achieve this TcDepVars is backed by deterministic sets which allows them
852 to be later converted to a list in a deterministic order.
853
854 For more information about deterministic sets see
855 Note [Deterministic UniqFM] in UniqDFM.
856 -}
857
858 quantifyTyVars, quantifyZonkedTyVars
859 :: TcTyCoVarSet -- global tvs
860 -> TcDepVars -- See Note [Dependent type variables] in TcType
861 -> TcM [TcTyVar]
862 -- See Note [quantifyTyVars]
863 -- Can be given a mixture of TcTyVars and TyVars, in the case of
864 -- associated type declarations. Also accepts covars, but *never* returns any.
865
866 -- The zonked variant assumes everything is already zonked.
867
868 quantifyTyVars gbl_tvs (DV { dv_kvs = dep_tkvs, dv_tvs = nondep_tkvs })
869 = do { dep_tkvs <- zonkTyCoVarsAndFVDSet dep_tkvs
870 ; nondep_tkvs <- zonkTyCoVarsAndFVDSet nondep_tkvs
871 ; gbl_tvs <- zonkTyCoVarsAndFV gbl_tvs
872 ; quantifyZonkedTyVars gbl_tvs (DV { dv_kvs = dep_tkvs, dv_tvs = nondep_tkvs }) }
873
874 quantifyZonkedTyVars gbl_tvs dvs@(DV{ dv_kvs = dep_tkvs, dv_tvs = nondep_tkvs })
875 = do { traceTc "quantifyZonkedTyVars" (vcat [ppr dvs, ppr gbl_tvs])
876 ; let all_cvs = filterVarSet isCoVar $ dVarSetToVarSet dep_tkvs
877 dep_kvs = dVarSetElemsWellScoped $
878 dep_tkvs `dVarSetMinusVarSet` gbl_tvs
879 `dVarSetMinusVarSet` closeOverKinds all_cvs
880 -- dVarSetElemsWellScoped: put the kind variables into
881 -- well-scoped order.
882 -- E.g. [k, (a::k)] not the other way roud
883 -- closeOverKinds all_cvs: do not quantify over coercion
884 -- variables, or any any tvs that a covar depends on
885
886 nondep_tvs = dVarSetElems $
887 (nondep_tkvs `minusDVarSet` dep_tkvs)
888 `dVarSetMinusVarSet` gbl_tvs
889 -- See Note [Dependent type variables] in TcType
890 -- The `minus` dep_tkvs removes any kind-level vars
891 -- e.g. T k (a::k) Since k appear in a kind it'll
892 -- be in dv_kvs, and is dependent. So remove it from
893 -- dv_tvs which will also contain k
894 -- No worry about dependent covars here;
895 -- they are all in dep_tkvs
896 -- No worry about scoping, because these are all
897 -- type variables
898 -- NB kinds of tvs are zonked by zonkTyCoVarsAndFV
899
900 -- In the non-PolyKinds case, default the kind variables
901 -- to *, and zonk the tyvars as usual. Notice that this
902 -- may make quantifyTyVars return a shorter list
903 -- than it was passed, but that's ok
904 ; poly_kinds <- xoptM LangExt.PolyKinds
905 ; dep_kvs' <- mapMaybeM (zonk_quant (not poly_kinds)) dep_kvs
906 ; nondep_tvs' <- mapMaybeM (zonk_quant False) nondep_tvs
907 -- Because of the order, any kind variables
908 -- mentioned in the kinds of the nondep_tvs'
909 -- now refer to the dep_kvs'
910
911 ; traceTc "quantifyTyVars"
912 (vcat [ text "globals:" <+> ppr gbl_tvs
913 , text "nondep:" <+> ppr nondep_tvs
914 , text "dep:" <+> ppr dep_kvs
915 , text "dep_kvs'" <+> ppr dep_kvs'
916 , text "nondep_tvs'" <+> ppr nondep_tvs' ])
917
918 ; return (dep_kvs' ++ nondep_tvs') }
919 where
920 zonk_quant default_kind tkv
921 | isTcTyVar tkv = zonkQuantifiedTyVar default_kind tkv
922 | otherwise = return $ Just tkv
923 -- For associated types, we have the class variables
924 -- in scope, and they are TyVars not TcTyVars
925
926 zonkQuantifiedTyVar :: Bool -- True <=> this is a kind var and -XNoPolyKinds
927 -- False <=> not a kind var or -XPolyKinds
928 -> TcTyVar
929 -> TcM (Maybe TcTyVar)
930 -- The quantified type variables often include meta type variables
931 -- we want to freeze them into ordinary type variables, and
932 -- default their kind (e.g. from TYPE v to TYPE Lifted)
933 -- The meta tyvar is updated to point to the new skolem TyVar. Now any
934 -- bound occurrences of the original type variable will get zonked to
935 -- the immutable version.
936 --
937 -- We leave skolem TyVars alone; they are immutable.
938 --
939 -- This function is called on both kind and type variables,
940 -- but kind variables *only* if PolyKinds is on.
941 --
942 -- This returns a tyvar if it should be quantified over;
943 -- otherwise, it returns Nothing. The latter case happens for
944 -- * Kind variables, with -XNoPolyKinds: don't quantify over these
945 -- * RuntimeRep variables: we never quantify over these
946
947 zonkQuantifiedTyVar default_kind tv
948 = do { mb_tv' <- zonkQuantifiedTyVarOrType default_kind tv
949 ; return (case mb_tv' of
950 Left x -> Just x -- Quantify over this
951 Right _ -> Nothing) -- Do not quantify over this
952 }
953
954 -- | Like zonkQuantifiedTyVar, but if zonking reveals that the tyvar
955 -- should become a type (when defaulting a RuntimeRep var to PtrRepLifted), it
956 -- returns the type instead.
957 zonkQuantifiedTyVarOrType :: Bool -- True <=> this is a kind var and -XNoPolyKinds
958 -- False <=> not a kind var or -XPolyKindsBool
959 -> TcTyVar
960 -> TcM (Either TcTyVar TcType)
961 zonkQuantifiedTyVarOrType default_kind tv
962 = case tcTyVarDetails tv of
963 SkolemTv {} -> do { kind <- zonkTcType (tyVarKind tv)
964 ; return $ Left $ setTyVarKind tv kind }
965 -- It might be a skolem type variable,
966 -- for example from a user type signature
967
968 MetaTv { mtv_ref = ref }
969 -> do { when debugIsOn (check_empty ref)
970 ; zonk_meta_tv tv }
971
972 _other -> pprPanic "zonkQuantifiedTyVar" (ppr tv) -- FlatSkol, RuntimeUnk
973
974 where
975 zonk_meta_tv :: TcTyVar -> TcM (Either TcTyVar TcType)
976 zonk_meta_tv tv
977 | isRuntimeRepVar tv -- Never quantify over a RuntimeRep var
978 = do { writeMetaTyVar tv ptrRepLiftedTy
979 ; return (Right ptrRepLiftedTy) }
980
981 | default_kind -- -XNoPolyKinds and this is a kind var
982 = do { kind <- default_kind_var tv
983 ; return (Right kind) }
984
985 | otherwise
986 = do { tv' <- skolemiseUnboundMetaTyVar tv vanillaSkolemTv
987 ; return (Left tv') }
988
989 default_kind_var :: TyVar -> TcM Type
990 -- defaultKindVar is used exclusively with -XNoPolyKinds
991 -- See Note [Defaulting with -XNoPolyKinds]
992 -- It takes an (unconstrained) meta tyvar and defaults it.
993 -- Works only on vars of type *; for other kinds, it issues an error.
994 default_kind_var kv
995 | isStarKind (tyVarKind kv)
996 = do { writeMetaTyVar kv liftedTypeKind
997 ; return liftedTypeKind }
998 | otherwise
999 = do { addErr (vcat [ text "Cannot default kind variable" <+> quotes (ppr kv')
1000 , text "of kind:" <+> ppr (tyVarKind kv')
1001 , text "Perhaps enable PolyKinds or add a kind signature" ])
1002 ; return (mkTyVarTy kv) }
1003 where
1004 (_, kv') = tidyOpenTyCoVar emptyTidyEnv kv
1005
1006 check_empty ref -- [Sept 04] Check for non-empty.
1007 = when debugIsOn $ -- See note [Silly Type Synonym]
1008 do { cts <- readMutVar ref
1009 ; case cts of
1010 Flexi -> return ()
1011 Indirect ty -> WARN( True, ppr tv $$ ppr ty )
1012 return () }
1013
1014 skolemiseUnboundMetaTyVar :: TcTyVar -> TcTyVarDetails -> TcM TyVar
1015 -- We have a Meta tyvar with a ref-cell inside it
1016 -- Skolemise it, so that
1017 -- we are totally out of Meta-tyvar-land
1018 -- We create a skolem TyVar, not a regular TyVar
1019 -- See Note [Zonking to Skolem]
1020 skolemiseUnboundMetaTyVar tv details
1021 = ASSERT2( isMetaTyVar tv, ppr tv )
1022 do { span <- getSrcSpanM -- Get the location from "here"
1023 -- ie where we are generalising
1024 ; kind <- zonkTcType (tyVarKind tv)
1025 ; let uniq = getUnique tv
1026 -- NB: Use same Unique as original tyvar. This is
1027 -- important for TcHsType.splitTelescopeTvs to work properly
1028
1029 tv_name = getOccName tv
1030 final_name = mkInternalName uniq tv_name span
1031 final_tv = mkTcTyVar final_name kind details
1032
1033 ; traceTc "Skolemising" (ppr tv <+> text ":=" <+> ppr final_tv)
1034 ; writeMetaTyVar tv (mkTyVarTy final_tv)
1035 ; return final_tv }
1036
1037 {- Note [Defaulting with -XNoPolyKinds]
1038 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1039 Consider
1040
1041 data Compose f g a = Mk (f (g a))
1042
1043 We infer
1044
1045 Compose :: forall k1 k2. (k2 -> *) -> (k1 -> k2) -> k1 -> *
1046 Mk :: forall k1 k2 (f :: k2 -> *) (g :: k1 -> k2) (a :: k1).
1047 f (g a) -> Compose k1 k2 f g a
1048
1049 Now, in another module, we have -XNoPolyKinds -XDataKinds in effect.
1050 What does 'Mk mean? Pre GHC-8.0 with -XNoPolyKinds,
1051 we just defaulted all kind variables to *. But that's no good here,
1052 because the kind variables in 'Mk aren't of kind *, so defaulting to *
1053 is ill-kinded.
1054
1055 After some debate on #11334, we decided to issue an error in this case.
1056 The code is in defaultKindVar.
1057
1058 Note [What is a meta variable?]
1059 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1060 A "meta type-variable", also know as a "unification variable" is a placeholder
1061 introduced by the typechecker for an as-yet-unknown monotype.
1062
1063 For example, when we see a call `reverse (f xs)`, we know that we calling
1064 reverse :: forall a. [a] -> [a]
1065 So we know that the argument `f xs` must be a "list of something". But what is
1066 the "something"? We don't know until we explore the `f xs` a bit more. So we set
1067 out what we do know at the call of `reverse` by instantiate its type with a fresh
1068 meta tyvar, `alpha` say. So now the type of the argument `f xs`, and of the
1069 result, is `[alpha]`. The unification variable `alpha` stands for the
1070 as-yet-unknown type of the elements of the list.
1071
1072 As type inference progresses we may learn more about `alpha`. For example, suppose
1073 `f` has the type
1074 f :: forall b. b -> [Maybe b]
1075 Then we instantiate `f`'s type with another fresh unification variable, say
1076 `beta`; and equate `f`'s result type with reverse's argument type, thus
1077 `[alpha] ~ [Maybe beta]`.
1078
1079 Now we can solve this equality to learn that `alpha ~ Maybe beta`, so we've
1080 refined our knowledge about `alpha`. And so on.
1081
1082 If you found this Note useful, you may also want to have a look at
1083 Section 5 of "Practical type inference for higher rank types" (Peyton Jones,
1084 Vytiniotis, Weirich and Shields. J. Functional Programming. 2011).
1085
1086 Note [What is zonking?]
1087 ~~~~~~~~~~~~~~~~~~~~~~~
1088 GHC relies heavily on mutability in the typechecker for efficient operation.
1089 For this reason, throughout much of the type checking process meta type
1090 variables (the MetaTv constructor of TcTyVarDetails) are represented by mutable
1091 variables (known as TcRefs).
1092
1093 Zonking is the process of ripping out these mutable variables and replacing them
1094 with a real TcType. This involves traversing the entire type expression, but the
1095 interesting part of replacing the mutable variables occurs in zonkTyVarOcc.
1096
1097 There are two ways to zonk a Type:
1098
1099 * zonkTcTypeToType, which is intended to be used at the end of type-checking
1100 for the final zonk. It has to deal with unfilled metavars, either by filling
1101 it with a value like Any or failing (determined by the UnboundTyVarZonker
1102 used).
1103
1104 * zonkTcType, which will happily ignore unfilled metavars. This is the
1105 appropriate function to use while in the middle of type-checking.
1106
1107 Note [Zonking to Skolem]
1108 ~~~~~~~~~~~~~~~~~~~~~~~~
1109 We used to zonk quantified type variables to regular TyVars. However, this
1110 leads to problems. Consider this program from the regression test suite:
1111
1112 eval :: Int -> String -> String -> String
1113 eval 0 root actual = evalRHS 0 root actual
1114
1115 evalRHS :: Int -> a
1116 evalRHS 0 root actual = eval 0 root actual
1117
1118 It leads to the deferral of an equality (wrapped in an implication constraint)
1119
1120 forall a. () => ((String -> String -> String) ~ a)
1121
1122 which is propagated up to the toplevel (see TcSimplify.tcSimplifyInferCheck).
1123 In the meantime `a' is zonked and quantified to form `evalRHS's signature.
1124 This has the *side effect* of also zonking the `a' in the deferred equality
1125 (which at this point is being handed around wrapped in an implication
1126 constraint).
1127
1128 Finally, the equality (with the zonked `a') will be handed back to the
1129 simplifier by TcRnDriver.tcRnSrcDecls calling TcSimplify.tcSimplifyTop.
1130 If we zonk `a' with a regular type variable, we will have this regular type
1131 variable now floating around in the simplifier, which in many places assumes to
1132 only see proper TcTyVars.
1133
1134 We can avoid this problem by zonking with a skolem. The skolem is rigid
1135 (which we require for a quantified variable), but is still a TcTyVar that the
1136 simplifier knows how to deal with.
1137
1138 Note [Silly Type Synonyms]
1139 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1140 Consider this:
1141 type C u a = u -- Note 'a' unused
1142
1143 foo :: (forall a. C u a -> C u a) -> u
1144 foo x = ...
1145
1146 bar :: Num u => u
1147 bar = foo (\t -> t + t)
1148
1149 * From the (\t -> t+t) we get type {Num d} => d -> d
1150 where d is fresh.
1151
1152 * Now unify with type of foo's arg, and we get:
1153 {Num (C d a)} => C d a -> C d a
1154 where a is fresh.
1155
1156 * Now abstract over the 'a', but float out the Num (C d a) constraint
1157 because it does not 'really' mention a. (see exactTyVarsOfType)
1158 The arg to foo becomes
1159 \/\a -> \t -> t+t
1160
1161 * So we get a dict binding for Num (C d a), which is zonked to give
1162 a = ()
1163 [Note Sept 04: now that we are zonking quantified type variables
1164 on construction, the 'a' will be frozen as a regular tyvar on
1165 quantification, so the floated dict will still have type (C d a).
1166 Which renders this whole note moot; happily!]
1167
1168 * Then the \/\a abstraction has a zonked 'a' in it.
1169
1170 All very silly. I think its harmless to ignore the problem. We'll end up with
1171 a \/\a in the final result but all the occurrences of a will be zonked to ()
1172
1173 ************************************************************************
1174 * *
1175 Zonking types
1176 * *
1177 ************************************************************************
1178
1179 -}
1180
1181 -- | @tcGetGlobalTyCoVars@ returns a fully-zonked set of *scoped* tyvars free in
1182 -- the environment. To improve subsequent calls to the same function it writes
1183 -- the zonked set back into the environment. Note that this returns all
1184 -- variables free in anything (term-level or type-level) in scope. We thus
1185 -- don't have to worry about clashes with things that are not in scope, because
1186 -- if they are reachable, then they'll be returned here.
1187 tcGetGlobalTyCoVars :: TcM TcTyVarSet
1188 tcGetGlobalTyCoVars
1189 = do { (TcLclEnv {tcl_tyvars = gtv_var}) <- getLclEnv
1190 ; gbl_tvs <- readMutVar gtv_var
1191 ; gbl_tvs' <- zonkTyCoVarsAndFV gbl_tvs
1192 ; writeMutVar gtv_var gbl_tvs'
1193 ; return gbl_tvs' }
1194
1195 -- | Zonk a type without using the smart constructors; the result type
1196 -- is available for inspection within the type-checking knot.
1197 zonkTcTypeInKnot :: TcType -> TcM TcType
1198 zonkTcTypeInKnot = mapType (zonkTcTypeMapper { tcm_smart = False }) ()
1199
1200 zonkTcTypeAndFV :: TcType -> TcM DTyCoVarSet
1201 -- Zonk a type and take its free variables
1202 -- With kind polymorphism it can be essential to zonk *first*
1203 -- so that we find the right set of free variables. Eg
1204 -- forall k1. forall (a:k2). a
1205 -- where k2:=k1 is in the substitution. We don't want
1206 -- k2 to look free in this type!
1207 -- NB: This might be called from within the knot, so don't use
1208 -- smart constructors. See Note [Zonking within the knot] in TcHsType
1209 zonkTcTypeAndFV ty
1210 = tyCoVarsOfTypeDSet <$> zonkTcTypeInKnot ty
1211
1212 -- | Zonk a type and call 'splitDepVarsOfType' on it.
1213 -- Works within the knot.
1214 zonkTcTypeAndSplitDepVars :: TcType -> TcM TcDepVars
1215 zonkTcTypeAndSplitDepVars ty
1216 = splitDepVarsOfType <$> zonkTcTypeInKnot ty
1217
1218 zonkTcTypesAndSplitDepVars :: [TcType] -> TcM TcDepVars
1219 zonkTcTypesAndSplitDepVars tys
1220 = splitDepVarsOfTypes <$> mapM zonkTcTypeInKnot tys
1221
1222 zonkTyCoVar :: TyCoVar -> TcM TcType
1223 -- Works on TyVars and TcTyVars
1224 zonkTyCoVar tv | isTcTyVar tv = zonkTcTyVar tv
1225 | isTyVar tv = mkTyVarTy <$> zonkTyCoVarKind tv
1226 | otherwise = ASSERT2( isCoVar tv, ppr tv )
1227 mkCoercionTy . mkCoVarCo <$> zonkTyCoVarKind tv
1228 -- Hackily, when typechecking type and class decls
1229 -- we have TyVars in scopeadded (only) in
1230 -- TcHsType.tcTyClTyVars, but it seems
1231 -- painful to make them into TcTyVars there
1232
1233 zonkTyCoVarsAndFV :: TyCoVarSet -> TcM TyCoVarSet
1234 zonkTyCoVarsAndFV tycovars =
1235 tyCoVarsOfTypes <$> mapM zonkTyCoVar (nonDetEltsUFM tycovars)
1236 -- It's OK to use nonDetEltsUFM here because we immediately forget about
1237 -- the ordering by turning it into a nondeterministic set and the order
1238 -- of zonking doesn't matter for determinism.
1239
1240 -- Takes a list of TyCoVars, zonks them and returns a
1241 -- deterministically ordered list of their free variables.
1242 zonkTyCoVarsAndFVList :: [TyCoVar] -> TcM [TyCoVar]
1243 zonkTyCoVarsAndFVList tycovars =
1244 tyCoVarsOfTypesList <$> mapM zonkTyCoVar tycovars
1245
1246 -- Takes a deterministic set of TyCoVars, zonks them and returns a
1247 -- deterministic set of their free variables.
1248 -- See Note [quantifyTyVars determinism].
1249 zonkTyCoVarsAndFVDSet :: DTyCoVarSet -> TcM DTyCoVarSet
1250 zonkTyCoVarsAndFVDSet tycovars =
1251 tyCoVarsOfTypesDSet <$> mapM zonkTyCoVar (dVarSetElems tycovars)
1252
1253 zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
1254 zonkTcTyVars tyvars = mapM zonkTcTyVar tyvars
1255
1256 ----------------- Types
1257 zonkTyCoVarKind :: TyCoVar -> TcM TyCoVar
1258 zonkTyCoVarKind tv = do { kind' <- zonkTcType (tyVarKind tv)
1259 ; return (setTyVarKind tv kind') }
1260
1261 zonkTcTypes :: [TcType] -> TcM [TcType]
1262 zonkTcTypes tys = mapM zonkTcType tys
1263
1264 {-
1265 ************************************************************************
1266 * *
1267 Zonking constraints
1268 * *
1269 ************************************************************************
1270 -}
1271
1272 zonkImplication :: Implication -> TcM Implication
1273 zonkImplication implic@(Implic { ic_skols = skols
1274 , ic_given = given
1275 , ic_wanted = wanted
1276 , ic_info = info })
1277 = do { skols' <- mapM zonkTcTyCoVarBndr skols -- Need to zonk their kinds!
1278 -- as Trac #7230 showed
1279 ; given' <- mapM zonkEvVar given
1280 ; info' <- zonkSkolemInfo info
1281 ; wanted' <- zonkWCRec wanted
1282 ; return (implic { ic_skols = skols'
1283 , ic_given = given'
1284 , ic_wanted = wanted'
1285 , ic_info = info' }) }
1286
1287 zonkEvVar :: EvVar -> TcM EvVar
1288 zonkEvVar var = do { ty' <- zonkTcType (varType var)
1289 ; return (setVarType var ty') }
1290
1291
1292 zonkWC :: WantedConstraints -> TcM WantedConstraints
1293 zonkWC wc = zonkWCRec wc
1294
1295 zonkWCRec :: WantedConstraints -> TcM WantedConstraints
1296 zonkWCRec (WC { wc_simple = simple, wc_impl = implic, wc_insol = insol })
1297 = do { simple' <- zonkSimples simple
1298 ; implic' <- mapBagM zonkImplication implic
1299 ; insol' <- zonkSimples insol
1300 ; return (WC { wc_simple = simple', wc_impl = implic', wc_insol = insol' }) }
1301
1302 zonkSimples :: Cts -> TcM Cts
1303 zonkSimples cts = do { cts' <- mapBagM zonkCt' cts
1304 ; traceTc "zonkSimples done:" (ppr cts')
1305 ; return cts' }
1306
1307 zonkCt' :: Ct -> TcM Ct
1308 zonkCt' ct = zonkCt ct
1309
1310 zonkCt :: Ct -> TcM Ct
1311 zonkCt ct@(CHoleCan { cc_ev = ev })
1312 = do { ev' <- zonkCtEvidence ev
1313 ; return $ ct { cc_ev = ev' } }
1314 zonkCt ct
1315 = do { fl' <- zonkCtEvidence (cc_ev ct)
1316 ; return (mkNonCanonical fl') }
1317
1318 zonkCtEvidence :: CtEvidence -> TcM CtEvidence
1319 zonkCtEvidence ctev@(CtGiven { ctev_pred = pred })
1320 = do { pred' <- zonkTcType pred
1321 ; return (ctev { ctev_pred = pred'}) }
1322 zonkCtEvidence ctev@(CtWanted { ctev_pred = pred, ctev_dest = dest })
1323 = do { pred' <- zonkTcType pred
1324 ; let dest' = case dest of
1325 EvVarDest ev -> EvVarDest $ setVarType ev pred'
1326 -- necessary in simplifyInfer
1327 HoleDest h -> HoleDest h
1328 ; return (ctev { ctev_pred = pred', ctev_dest = dest' }) }
1329 zonkCtEvidence ctev@(CtDerived { ctev_pred = pred })
1330 = do { pred' <- zonkTcType pred
1331 ; return (ctev { ctev_pred = pred' }) }
1332
1333 zonkSkolemInfo :: SkolemInfo -> TcM SkolemInfo
1334 zonkSkolemInfo (SigSkol cx ty) = do { ty' <- zonkTcType ty
1335 ; return (SigSkol cx ty') }
1336 zonkSkolemInfo (InferSkol ntys) = do { ntys' <- mapM do_one ntys
1337 ; return (InferSkol ntys') }
1338 where
1339 do_one (n, ty) = do { ty' <- zonkTcType ty; return (n, ty') }
1340 zonkSkolemInfo skol_info = return skol_info
1341
1342 {-
1343 %************************************************************************
1344 %* *
1345 \subsection{Zonking -- the main work-horses: zonkTcType, zonkTcTyVar}
1346 * *
1347 * For internal use only! *
1348 * *
1349 ************************************************************************
1350
1351 -}
1352
1353 -- zonkId is used *during* typechecking just to zonk the Id's type
1354 zonkId :: TcId -> TcM TcId
1355 zonkId id
1356 = do { ty' <- zonkTcType (idType id)
1357 ; return (Id.setIdType id ty') }
1358
1359 -- | A suitable TyCoMapper for zonking a type inside the knot, and
1360 -- before all metavars are filled in.
1361 zonkTcTypeMapper :: TyCoMapper () TcM
1362 zonkTcTypeMapper = TyCoMapper
1363 { tcm_smart = True
1364 , tcm_tyvar = const zonkTcTyVar
1365 , tcm_covar = const (\cv -> mkCoVarCo <$> zonkTyCoVarKind cv)
1366 , tcm_hole = hole
1367 , tcm_tybinder = \_env tv _vis -> ((), ) <$> zonkTcTyCoVarBndr tv }
1368 where
1369 hole :: () -> CoercionHole -> Role -> Type -> Type
1370 -> TcM Coercion
1371 hole _ h r t1 t2
1372 = do { contents <- unpackCoercionHole_maybe h
1373 ; case contents of
1374 Just co -> do { co <- zonkCo co
1375 ; checkCoercionHole co h r t1 t2 }
1376 Nothing -> do { t1 <- zonkTcType t1
1377 ; t2 <- zonkTcType t2
1378 ; return $ mkHoleCo h r t1 t2 } }
1379
1380
1381 -- For unbound, mutable tyvars, zonkType uses the function given to it
1382 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
1383 -- type variable and zonks the kind too
1384 zonkTcType :: TcType -> TcM TcType
1385 zonkTcType = mapType zonkTcTypeMapper ()
1386
1387 -- | "Zonk" a coercion -- really, just zonk any types in the coercion
1388 zonkCo :: Coercion -> TcM Coercion
1389 zonkCo = mapCoercion zonkTcTypeMapper ()
1390
1391 zonkTcTyCoVarBndr :: TcTyCoVar -> TcM TcTyCoVar
1392 -- A tyvar binder is never a unification variable (MetaTv),
1393 -- rather it is always a skolems. BUT it may have a kind
1394 -- that has not yet been zonked, and may include kind
1395 -- unification variables.
1396 zonkTcTyCoVarBndr tyvar
1397 -- can't use isCoVar, because it looks at a TyCon. Argh.
1398 = ASSERT2( isImmutableTyVar tyvar || (not $ isTyVar tyvar), pprTvBndr tyvar )
1399 updateTyVarKindM zonkTcType tyvar
1400
1401 -- | Zonk a TyBinder
1402 zonkTcTyBinder :: TcTyBinder -> TcM TcTyBinder
1403 zonkTcTyBinder (Anon ty) = Anon <$> zonkTcType ty
1404 zonkTcTyBinder (Named tv vis) = Named <$> zonkTcTyCoVarBndr tv <*> pure vis
1405
1406 zonkTcTyVar :: TcTyVar -> TcM TcType
1407 -- Simply look through all Flexis
1408 zonkTcTyVar tv
1409 | isTcTyVar tv
1410 = case tcTyVarDetails tv of
1411 SkolemTv {} -> zonk_kind_and_return
1412 RuntimeUnk {} -> zonk_kind_and_return
1413 FlatSkol ty -> zonkTcType ty
1414 MetaTv { mtv_ref = ref }
1415 -> do { cts <- readMutVar ref
1416 ; case cts of
1417 Flexi -> zonk_kind_and_return
1418 Indirect ty -> zonkTcType ty }
1419
1420 | otherwise -- coercion variable
1421 = zonk_kind_and_return
1422 where
1423 zonk_kind_and_return = do { z_tv <- zonkTyCoVarKind tv
1424 ; return (mkTyVarTy z_tv) }
1425
1426 -- Variant that assumes that any result of zonking is still a TyVar.
1427 -- Should be used only on skolems and SigTvs
1428 zonkTcTyVarToTyVar :: TcTyVar -> TcM TcTyVar
1429 zonkTcTyVarToTyVar tv
1430 = do { ty <- zonkTcTyVar tv
1431 ; return (tcGetTyVar "zonkTcTyVarToVar" ty) }
1432
1433 {-
1434 %************************************************************************
1435 %* *
1436 Tidying
1437 * *
1438 ************************************************************************
1439 -}
1440
1441 zonkTidyTcType :: TidyEnv -> TcType -> TcM (TidyEnv, TcType)
1442 zonkTidyTcType env ty = do { ty' <- zonkTcType ty
1443 ; return (tidyOpenType env ty') }
1444
1445 -- | Make an 'ErrorThing' storing a type.
1446 mkTypeErrorThing :: TcType -> ErrorThing
1447 mkTypeErrorThing ty = ErrorThing ty (Just $ length $ snd $ repSplitAppTys ty)
1448 zonkTidyTcType
1449 -- NB: Use *rep*splitAppTys, else we get #11313
1450
1451 -- | Make an 'ErrorThing' storing a type, with some extra args known about
1452 mkTypeErrorThingArgs :: TcType -> Int -> ErrorThing
1453 mkTypeErrorThingArgs ty num_args
1454 = ErrorThing ty (Just $ (length $ snd $ repSplitAppTys ty) + num_args)
1455 zonkTidyTcType
1456
1457 zonkTidyOrigin :: TidyEnv -> CtOrigin -> TcM (TidyEnv, CtOrigin)
1458 zonkTidyOrigin env (GivenOrigin skol_info)
1459 = do { skol_info1 <- zonkSkolemInfo skol_info
1460 ; let skol_info2 = tidySkolemInfo env skol_info1
1461 ; return (env, GivenOrigin skol_info2) }
1462 zonkTidyOrigin env orig@(TypeEqOrigin { uo_actual = act
1463 , uo_expected = exp
1464 , uo_thing = m_thing })
1465 = do { (env1, act') <- zonkTidyTcType env act
1466 ; mb_exp <- readExpType_maybe exp -- it really should be filled in.
1467 -- unless we're debugging.
1468 ; (env2, exp') <- case mb_exp of
1469 Just ty -> second mkCheckExpType <$> zonkTidyTcType env1 ty
1470 Nothing -> return (env1, exp)
1471 ; (env3, m_thing') <- zonkTidyErrorThing env2 m_thing
1472 ; return ( env3, orig { uo_actual = act'
1473 , uo_expected = exp'
1474 , uo_thing = m_thing' }) }
1475 zonkTidyOrigin env (KindEqOrigin ty1 m_ty2 orig t_or_k)
1476 = do { (env1, ty1') <- zonkTidyTcType env ty1
1477 ; (env2, m_ty2') <- case m_ty2 of
1478 Just ty2 -> second Just <$> zonkTidyTcType env1 ty2
1479 Nothing -> return (env1, Nothing)
1480 ; (env3, orig') <- zonkTidyOrigin env2 orig
1481 ; return (env3, KindEqOrigin ty1' m_ty2' orig' t_or_k) }
1482 zonkTidyOrigin env (FunDepOrigin1 p1 l1 p2 l2)
1483 = do { (env1, p1') <- zonkTidyTcType env p1
1484 ; (env2, p2') <- zonkTidyTcType env1 p2
1485 ; return (env2, FunDepOrigin1 p1' l1 p2' l2) }
1486 zonkTidyOrigin env (FunDepOrigin2 p1 o1 p2 l2)
1487 = do { (env1, p1') <- zonkTidyTcType env p1
1488 ; (env2, p2') <- zonkTidyTcType env1 p2
1489 ; (env3, o1') <- zonkTidyOrigin env2 o1
1490 ; return (env3, FunDepOrigin2 p1' o1' p2' l2) }
1491 zonkTidyOrigin env orig = return (env, orig)
1492
1493 zonkTidyErrorThing :: TidyEnv -> Maybe ErrorThing
1494 -> TcM (TidyEnv, Maybe ErrorThing)
1495 zonkTidyErrorThing env (Just (ErrorThing thing n_args zonker))
1496 = do { (env', thing') <- zonker env thing
1497 ; return (env', Just $ ErrorThing thing' n_args zonker) }
1498 zonkTidyErrorThing env Nothing
1499 = return (env, Nothing)
1500
1501 ----------------
1502 tidyCt :: TidyEnv -> Ct -> Ct
1503 -- Used only in error reporting
1504 -- Also converts it to non-canonical
1505 tidyCt env ct
1506 = case ct of
1507 CHoleCan { cc_ev = ev }
1508 -> ct { cc_ev = tidy_ev env ev }
1509 _ -> mkNonCanonical (tidy_ev env (ctEvidence ct))
1510 where
1511 tidy_ev :: TidyEnv -> CtEvidence -> CtEvidence
1512 -- NB: we do not tidy the ctev_evar field because we don't
1513 -- show it in error messages
1514 tidy_ev env ctev@(CtGiven { ctev_pred = pred })
1515 = ctev { ctev_pred = tidyType env pred }
1516 tidy_ev env ctev@(CtWanted { ctev_pred = pred })
1517 = ctev { ctev_pred = tidyType env pred }
1518 tidy_ev env ctev@(CtDerived { ctev_pred = pred })
1519 = ctev { ctev_pred = tidyType env pred }
1520
1521 ----------------
1522 tidyEvVar :: TidyEnv -> EvVar -> EvVar
1523 tidyEvVar env var = setVarType var (tidyType env (varType var))
1524
1525 ----------------
1526 tidySkolemInfo :: TidyEnv -> SkolemInfo -> SkolemInfo
1527 tidySkolemInfo env (DerivSkol ty) = DerivSkol (tidyType env ty)
1528 tidySkolemInfo env (SigSkol cx ty) = SigSkol cx (tidyType env ty)
1529 tidySkolemInfo env (InferSkol ids) = InferSkol (mapSnd (tidyType env) ids)
1530 tidySkolemInfo env (UnifyForAllSkol ty) = UnifyForAllSkol (tidyType env ty)
1531 tidySkolemInfo _ info = info