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