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