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