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