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