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