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