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