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