2 % (c) The GRASP/AQUA Project, Glasgow University, 1998
4 \section[Type]{Type - public interface}
9 -- re-exports from TypeRep
10 TyThing(..), Type, PredType(..), ThetaType,
14 Kind, SimpleKind, KindVar,
15 kindFunResult, splitKindFunTys,
17 liftedTypeKindTyCon, openTypeKindTyCon, unliftedTypeKindTyCon,
18 argTypeKindTyCon, ubxTupleKindTyCon,
20 liftedTypeKind, unliftedTypeKind, openTypeKind,
21 argTypeKind, ubxTupleKind,
23 tySuperKind, coSuperKind,
25 isLiftedTypeKind, isUnliftedTypeKind, isOpenTypeKind,
26 isUbxTupleKind, isArgTypeKind, isKind, isTySuperKind,
27 isCoSuperKind, isSuperKind, isCoercionKind,
28 mkArrowKind, mkArrowKinds,
30 isSubArgTypeKind, isSubOpenTypeKind, isSubKind, defaultKind, eqKind,
33 -- Re-exports from TyCon
36 mkTyVarTy, mkTyVarTys, getTyVar, getTyVar_maybe, isTyVarTy,
38 mkAppTy, mkAppTys, splitAppTy, splitAppTys,
39 splitAppTy_maybe, repSplitAppTy_maybe,
41 mkFunTy, mkFunTys, splitFunTy, splitFunTy_maybe,
42 splitFunTys, splitFunTysN,
43 funResultTy, funArgTy, zipFunTys, isFunTy,
45 mkTyConApp, mkTyConTy,
46 tyConAppTyCon, tyConAppArgs,
47 splitTyConApp_maybe, splitTyConApp,
48 splitNewTyConApp_maybe, splitNewTyConApp,
50 repType, typePrimRep, coreView, tcView, stgView, kindView,
52 mkForAllTy, mkForAllTys, splitForAllTy_maybe, splitForAllTys,
53 applyTy, applyTys, isForAllTy, dropForAlls,
56 predTypeRep, mkPredTy, mkPredTys,
59 splitRecNewType_maybe,
62 isUnLiftedType, isUnboxedTupleType, isAlgType, isPrimitiveType,
63 isStrictType, isStrictPred,
66 tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta,
67 typeKind, addFreeTyVars,
69 -- Tidying up for printing
71 tidyOpenType, tidyOpenTypes,
72 tidyTyVarBndr, tidyFreeTyVars,
73 tidyOpenTyVar, tidyOpenTyVars,
74 tidyTopType, tidyPred,
78 coreEqType, tcEqType, tcEqTypes, tcCmpType, tcCmpTypes,
79 tcEqPred, tcCmpPred, tcEqTypeX,
85 TvSubstEnv, emptyTvSubstEnv, -- Representation widely visible
86 TvSubst(..), emptyTvSubst, -- Representation visible to a few friends
87 mkTvSubst, mkOpenTvSubst, zipOpenTvSubst, zipTopTvSubst, mkTopTvSubst, notElemTvSubst,
88 getTvSubstEnv, setTvSubstEnv, getTvInScope, extendTvInScope,
89 extendTvSubst, extendTvSubstList, isInScope, composeTvSubst, zipTyEnv,
91 -- Performing substitution on types
92 substTy, substTys, substTyWith, substTheta,
93 substPred, substTyVar, substTyVarBndr, deShadowTy, lookupTyVar,
96 pprType, pprParendType, pprTyThingCategory,
97 pprPred, pprTheta, pprThetaArrow, pprClassPred, pprKind, pprParendKind
100 #include "HsVersions.h"
102 -- We import the representation and primitive functions from TypeRep.
103 -- Many things are reexported, but not the representation!
108 import Var ( Var, TyVar, tyVarKind, tyVarName,
109 setTyVarName, setTyVarKind, mkTyVar, isTyVar )
110 import Name ( Name(..) )
111 import Unique ( Unique )
115 import OccName ( tidyOccName )
116 import Name ( NamedThing(..), mkInternalName, tidyNameOcc )
117 import Class ( Class, classTyCon )
118 import PrelNames( openTypeKindTyConKey, unliftedTypeKindTyConKey,
119 ubxTupleKindTyConKey, argTypeKindTyConKey,
120 eqCoercionKindTyConKey )
121 import TyCon ( TyCon, isRecursiveTyCon, isPrimTyCon,
122 isUnboxedTupleTyCon, isUnLiftedTyCon,
123 isFunTyCon, isNewTyCon, newTyConRep, newTyConRhs,
124 isAlgTyCon, tyConArity, isSuperKindTyCon,
125 tcExpandTyCon_maybe, coreExpandTyCon_maybe,
126 stgExpandTyCon_maybe,
127 tyConKind, PrimRep(..), tyConPrimRep, tyConUnique,
128 isCoercionTyCon_maybe, isCoercionTyCon
132 import StaticFlags ( opt_DictsStrict )
133 import SrcLoc ( noSrcLoc )
134 import Util ( mapAccumL, seqList, lengthIs, snocView, thenCmp, isEqual, all2 )
136 import UniqSet ( sizeUniqSet ) -- Should come via VarSet
137 import Maybe ( isJust )
141 %************************************************************************
145 %************************************************************************
147 In Core, we "look through" non-recursive newtypes and PredTypes.
150 {-# INLINE coreView #-}
151 coreView :: Type -> Maybe Type
152 -- Strips off the *top layer only* of a type to give
153 -- its underlying representation type.
154 -- Returns Nothing if there is nothing to look through.
156 -- In the case of newtypes, it returns
157 -- *either* a vanilla TyConApp (recursive newtype, or non-saturated)
158 -- *or* the newtype representation (otherwise), meaning the
159 -- type written in the RHS of the newtype decl,
160 -- which may itself be a newtype
162 -- Example: newtype R = MkR S
164 -- newtype T = MkT (T -> T)
165 -- expandNewTcApp on R gives Just S
167 -- on T gives Nothing (no expansion)
169 -- By being non-recursive and inlined, this case analysis gets efficiently
170 -- joined onto the case analysis that the caller is already doing
171 coreView (NoteTy _ ty) = Just ty
172 coreView (PredTy p) = Just (predTypeRep p)
173 coreView (TyConApp tc tys) | Just (tenv, rhs, tys') <- coreExpandTyCon_maybe tc tys
174 = Just (mkAppTys (substTy (mkTopTvSubst tenv) rhs) tys')
175 -- Its important to use mkAppTys, rather than (foldl AppTy),
176 -- because the function part might well return a
177 -- partially-applied type constructor; indeed, usually will!
178 coreView ty = Nothing
180 {-# INLINE stgView #-}
181 stgView :: Type -> Maybe Type
182 -- When generating STG from Core it is important that we look through newtypes
183 -- but for the rest of Core we are just using coercions. This does just what
184 -- coreView USED to do.
185 stgView (NoteTy _ ty) = Just ty
186 stgView (PredTy p) = Just (predTypeRep p)
187 stgView (TyConApp tc tys) | Just (tenv, rhs, tys') <- stgExpandTyCon_maybe tc tys
188 = Just (mkAppTys (substTy (mkTopTvSubst tenv) rhs) tys')
189 -- Its important to use mkAppTys, rather than (foldl AppTy),
190 -- because the function part might well return a
191 -- partially-applied type constructor; indeed, usually will!
195 -----------------------------------------------
196 {-# INLINE tcView #-}
197 tcView :: Type -> Maybe Type
198 -- Same, but for the type checker, which just looks through synonyms
199 tcView (NoteTy _ ty) = Just ty
200 tcView (TyConApp tc tys) | Just (tenv, rhs, tys') <- tcExpandTyCon_maybe tc tys
201 = Just (mkAppTys (substTy (mkTopTvSubst tenv) rhs) tys')
204 -----------------------------------------------
205 {-# INLINE kindView #-}
206 kindView :: Kind -> Maybe Kind
207 -- C.f. coreView, tcView
208 -- For the moment, we don't even handle synonyms in kinds
209 kindView (NoteTy _ k) = Just k
210 kindView other = Nothing
214 %************************************************************************
216 \subsection{Constructor-specific functions}
218 %************************************************************************
221 ---------------------------------------------------------------------
225 mkTyVarTy :: TyVar -> Type
228 mkTyVarTys :: [TyVar] -> [Type]
229 mkTyVarTys = map mkTyVarTy -- a common use of mkTyVarTy
231 getTyVar :: String -> Type -> TyVar
232 getTyVar msg ty = case getTyVar_maybe ty of
234 Nothing -> panic ("getTyVar: " ++ msg)
236 isTyVarTy :: Type -> Bool
237 isTyVarTy ty = isJust (getTyVar_maybe ty)
239 getTyVar_maybe :: Type -> Maybe TyVar
240 getTyVar_maybe ty | Just ty' <- coreView ty = getTyVar_maybe ty'
241 getTyVar_maybe (TyVarTy tv) = Just tv
242 getTyVar_maybe other = Nothing
247 ---------------------------------------------------------------------
250 We need to be pretty careful with AppTy to make sure we obey the
251 invariant that a TyConApp is always visibly so. mkAppTy maintains the
255 mkAppTy orig_ty1 orig_ty2
258 mk_app (NoteTy _ ty1) = mk_app ty1
259 mk_app (TyConApp tc tys) = mkTyConApp tc (tys ++ [orig_ty2])
260 mk_app ty1 = AppTy orig_ty1 orig_ty2
261 -- Note that the TyConApp could be an
262 -- under-saturated type synonym. GHC allows that; e.g.
263 -- type Foo k = k a -> k a
265 -- foo :: Foo Id -> Foo Id
267 -- Here Id is partially applied in the type sig for Foo,
268 -- but once the type synonyms are expanded all is well
270 mkAppTys :: Type -> [Type] -> Type
271 mkAppTys orig_ty1 [] = orig_ty1
272 -- This check for an empty list of type arguments
273 -- avoids the needless loss of a type synonym constructor.
274 -- For example: mkAppTys Rational []
275 -- returns to (Ratio Integer), which has needlessly lost
276 -- the Rational part.
277 mkAppTys orig_ty1 orig_tys2
280 mk_app (NoteTy _ ty1) = mk_app ty1
281 mk_app (TyConApp tc tys) = mkTyConApp tc (tys ++ orig_tys2)
282 -- mkTyConApp: see notes with mkAppTy
283 mk_app ty1 = foldl AppTy orig_ty1 orig_tys2
286 splitAppTy_maybe :: Type -> Maybe (Type, Type)
287 splitAppTy_maybe ty | Just ty' <- coreView ty
288 = splitAppTy_maybe ty'
289 splitAppTy_maybe ty = repSplitAppTy_maybe ty
292 repSplitAppTy_maybe :: Type -> Maybe (Type,Type)
293 -- Does the AppTy split, but assumes that any view stuff is already done
294 repSplitAppTy_maybe (FunTy ty1 ty2) = Just (TyConApp funTyCon [ty1], ty2)
295 repSplitAppTy_maybe (AppTy ty1 ty2) = Just (ty1, ty2)
296 repSplitAppTy_maybe (TyConApp tc tys) = case snocView tys of
297 Just (tys', ty') -> Just (TyConApp tc tys', ty')
299 repSplitAppTy_maybe other = Nothing
301 splitAppTy :: Type -> (Type, Type)
302 splitAppTy ty = case splitAppTy_maybe ty of
304 Nothing -> panic "splitAppTy"
307 splitAppTys :: Type -> (Type, [Type])
308 splitAppTys ty = split ty ty []
310 split orig_ty ty args | Just ty' <- coreView ty = split orig_ty ty' args
311 split orig_ty (AppTy ty arg) args = split ty ty (arg:args)
312 split orig_ty (TyConApp tc tc_args) args = (TyConApp tc [], tc_args ++ args)
313 split orig_ty (FunTy ty1 ty2) args = ASSERT( null args )
314 (TyConApp funTyCon [], [ty1,ty2])
315 split orig_ty ty args = (orig_ty, args)
320 ---------------------------------------------------------------------
325 mkFunTy :: Type -> Type -> Type
326 mkFunTy arg res = FunTy arg res
328 mkFunTys :: [Type] -> Type -> Type
329 mkFunTys tys ty = foldr FunTy ty tys
331 isFunTy :: Type -> Bool
332 isFunTy ty = isJust (splitFunTy_maybe ty)
334 splitFunTy :: Type -> (Type, Type)
335 splitFunTy ty | Just ty' <- coreView ty = splitFunTy ty'
336 splitFunTy (FunTy arg res) = (arg, res)
337 splitFunTy other = pprPanic "splitFunTy" (ppr other)
339 splitFunTy_maybe :: Type -> Maybe (Type, Type)
340 splitFunTy_maybe ty | Just ty' <- coreView ty = splitFunTy_maybe ty'
341 splitFunTy_maybe (FunTy arg res) = Just (arg, res)
342 splitFunTy_maybe other = Nothing
344 splitFunTys :: Type -> ([Type], Type)
345 splitFunTys ty = split [] ty ty
347 split args orig_ty ty | Just ty' <- coreView ty = split args orig_ty ty'
348 split args orig_ty (FunTy arg res) = split (arg:args) res res
349 split args orig_ty ty = (reverse args, orig_ty)
351 splitFunTysN :: Int -> Type -> ([Type], Type)
352 -- Split off exactly n arg tys
353 splitFunTysN 0 ty = ([], ty)
354 splitFunTysN n ty = case splitFunTy ty of { (arg, res) ->
355 case splitFunTysN (n-1) res of { (args, res) ->
358 zipFunTys :: Outputable a => [a] -> Type -> ([(a,Type)], Type)
359 zipFunTys orig_xs orig_ty = split [] orig_xs orig_ty orig_ty
361 split acc [] nty ty = (reverse acc, nty)
363 | Just ty' <- coreView ty = split acc xs nty ty'
364 split acc (x:xs) nty (FunTy arg res) = split ((x,arg):acc) xs res res
365 split acc (x:xs) nty ty = pprPanic "zipFunTys" (ppr orig_xs <+> ppr orig_ty)
367 funResultTy :: Type -> Type
368 funResultTy ty | Just ty' <- coreView ty = funResultTy ty'
369 funResultTy (FunTy arg res) = res
370 funResultTy ty = pprPanic "funResultTy" (ppr ty)
372 funArgTy :: Type -> Type
373 funArgTy ty | Just ty' <- coreView ty = funArgTy ty'
374 funArgTy (FunTy arg res) = arg
375 funArgTy ty = pprPanic "funArgTy" (ppr ty)
379 ---------------------------------------------------------------------
382 @mkTyConApp@ is a key function, because it builds a TyConApp, FunTy or PredTy,
386 mkTyConApp :: TyCon -> [Type] -> Type
388 | isFunTyCon tycon, [ty1,ty2] <- tys
394 mkTyConTy :: TyCon -> Type
395 mkTyConTy tycon = mkTyConApp tycon []
397 -- splitTyConApp "looks through" synonyms, because they don't
398 -- mean a distinct type, but all other type-constructor applications
399 -- including functions are returned as Just ..
401 tyConAppTyCon :: Type -> TyCon
402 tyConAppTyCon ty = fst (splitTyConApp ty)
404 tyConAppArgs :: Type -> [Type]
405 tyConAppArgs ty = snd (splitTyConApp ty)
407 splitTyConApp :: Type -> (TyCon, [Type])
408 splitTyConApp ty = case splitTyConApp_maybe ty of
410 Nothing -> pprPanic "splitTyConApp" (ppr ty)
412 splitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
413 splitTyConApp_maybe ty | Just ty' <- coreView ty = splitTyConApp_maybe ty'
414 splitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
415 splitTyConApp_maybe (FunTy arg res) = Just (funTyCon, [arg,res])
416 splitTyConApp_maybe other = Nothing
418 -- Sometimes we do NOT want to look throught a newtype. When case matching
419 -- on a newtype we want a convenient way to access the arguments of a newty
420 -- constructor so as to properly form a coercion.
421 splitNewTyConApp :: Type -> (TyCon, [Type])
422 splitNewTyConApp ty = case splitNewTyConApp_maybe ty of
424 Nothing -> pprPanic "splitNewTyConApp" (ppr ty)
425 splitNewTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
426 splitNewTyConApp_maybe ty | Just ty' <- tcView ty = splitNewTyConApp_maybe ty'
427 splitNewTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
428 splitNewTyConApp_maybe (FunTy arg res) = Just (funTyCon, [arg,res])
429 splitNewTyConApp_maybe other = Nothing
434 ---------------------------------------------------------------------
438 Notes on type synonyms
439 ~~~~~~~~~~~~~~~~~~~~~~
440 The various "split" functions (splitFunTy, splitRhoTy, splitForAllTy) try
441 to return type synonyms whereever possible. Thus
446 splitFunTys (a -> Foo a) = ([a], Foo a)
449 The reason is that we then get better (shorter) type signatures in
450 interfaces. Notably this plays a role in tcTySigs in TcBinds.lhs.
455 repType looks through
459 (d) usage annotations
460 (e) all newtypes, including recursive ones
461 It's useful in the back end.
464 repType :: Type -> Type
465 -- Only applied to types of kind *; hence tycons are saturated
466 repType ty | Just ty' <- coreView ty = repType ty'
467 repType (ForAllTy _ ty) = repType ty
468 repType (TyConApp tc tys)
469 | isNewTyCon tc = -- Recursive newtypes are opaque to coreView
470 -- but we must expand them here. Sure to
471 -- be saturated because repType is only applied
472 -- to types of kind *
473 ASSERT( {- isRecursiveTyCon tc && -} tys `lengthIs` tyConArity tc )
474 repType (new_type_rep tc tys)
477 -- new_type_rep doesn't ask any questions:
478 -- it just expands newtype, whether recursive or not
479 new_type_rep new_tycon tys = ASSERT( tys `lengthIs` tyConArity new_tycon )
480 case newTyConRep new_tycon of
481 (tvs, rep_ty) -> substTyWith tvs tys rep_ty
483 -- ToDo: this could be moved to the code generator, using splitTyConApp instead
484 -- of inspecting the type directly.
485 typePrimRep :: Type -> PrimRep
486 typePrimRep ty = case repType ty of
487 TyConApp tc _ -> tyConPrimRep tc
489 AppTy _ _ -> PtrRep -- See note below
491 other -> pprPanic "typePrimRep" (ppr ty)
492 -- Types of the form 'f a' must be of kind *, not *#, so
493 -- we are guaranteed that they are represented by pointers.
494 -- The reason is that f must have kind *->*, not *->*#, because
495 -- (we claim) there is no way to constrain f's kind any other
501 ---------------------------------------------------------------------
506 mkForAllTy :: TyVar -> Type -> Type
508 = mkForAllTys [tyvar] ty
510 mkForAllTys :: [TyVar] -> Type -> Type
511 mkForAllTys tyvars ty = foldr ForAllTy ty tyvars
513 isForAllTy :: Type -> Bool
514 isForAllTy (NoteTy _ ty) = isForAllTy ty
515 isForAllTy (ForAllTy _ _) = True
516 isForAllTy other_ty = False
518 splitForAllTy_maybe :: Type -> Maybe (TyVar, Type)
519 splitForAllTy_maybe ty = splitFAT_m ty
521 splitFAT_m ty | Just ty' <- coreView ty = splitFAT_m ty'
522 splitFAT_m (ForAllTy tyvar ty) = Just(tyvar, ty)
523 splitFAT_m _ = Nothing
525 splitForAllTys :: Type -> ([TyVar], Type)
526 splitForAllTys ty = split ty ty []
528 split orig_ty ty tvs | Just ty' <- coreView ty = split orig_ty ty' tvs
529 split orig_ty (ForAllTy tv ty) tvs = split ty ty (tv:tvs)
530 split orig_ty t tvs = (reverse tvs, orig_ty)
532 dropForAlls :: Type -> Type
533 dropForAlls ty = snd (splitForAllTys ty)
536 -- (mkPiType now in CoreUtils)
540 Instantiate a for-all type with one or more type arguments.
541 Used when we have a polymorphic function applied to type args:
543 Then we use (applyTys type-of-f [t1,t2]) to compute the type of
547 applyTy :: Type -> Type -> Type
548 applyTy ty arg | Just ty' <- coreView ty = applyTy ty' arg
549 applyTy (ForAllTy tv ty) arg = substTyWith [tv] [arg] ty
550 applyTy other arg = panic "applyTy"
552 applyTys :: Type -> [Type] -> Type
553 -- This function is interesting because
554 -- a) the function may have more for-alls than there are args
555 -- b) less obviously, it may have fewer for-alls
556 -- For case (b) think of
557 -- applyTys (forall a.a) [forall b.b, Int]
558 -- This really can happen, via dressing up polymorphic types with newtype
559 -- clothing. Here's an example:
560 -- newtype R = R (forall a. a->a)
561 -- foo = case undefined :: R of
564 applyTys orig_fun_ty [] = orig_fun_ty
565 applyTys orig_fun_ty arg_tys
566 | n_tvs == n_args -- The vastly common case
567 = substTyWith tvs arg_tys rho_ty
568 | n_tvs > n_args -- Too many for-alls
569 = substTyWith (take n_args tvs) arg_tys
570 (mkForAllTys (drop n_args tvs) rho_ty)
571 | otherwise -- Too many type args
572 = ASSERT2( n_tvs > 0, ppr orig_fun_ty ) -- Zero case gives infnite loop!
573 applyTys (substTyWith tvs (take n_tvs arg_tys) rho_ty)
576 (tvs, rho_ty) = splitForAllTys orig_fun_ty
578 n_args = length arg_tys
582 %************************************************************************
584 \subsection{Source types}
586 %************************************************************************
588 A "source type" is a type that is a separate type as far as the type checker is
589 concerned, but which has low-level representation as far as the back end is concerned.
591 Source types are always lifted.
593 The key function is predTypeRep which gives the representation of a source type:
596 mkPredTy :: PredType -> Type
597 mkPredTy pred = PredTy pred
599 mkPredTys :: ThetaType -> [Type]
600 mkPredTys preds = map PredTy preds
602 predTypeRep :: PredType -> Type
603 -- Convert a PredType to its "representation type";
604 -- the post-type-checking type used by all the Core passes of GHC.
605 -- Unwraps only the outermost level; for example, the result might
606 -- be a newtype application
607 predTypeRep (IParam _ ty) = ty
608 predTypeRep (ClassP clas tys) = mkTyConApp (classTyCon clas) tys
609 -- Result might be a newtype application, but the consumer will
610 -- look through that too if necessary
614 %************************************************************************
618 %************************************************************************
621 splitRecNewType_maybe :: Type -> Maybe Type
622 -- Sometimes we want to look through a recursive newtype, and that's what happens here
623 -- It only strips *one layer* off, so the caller will usually call itself recursively
624 -- Only applied to types of kind *, hence the newtype is always saturated
625 splitRecNewType_maybe ty | Just ty' <- coreView ty = splitRecNewType_maybe ty'
626 splitRecNewType_maybe (TyConApp tc tys)
628 = ASSERT( tys `lengthIs` tyConArity tc ) -- splitRecNewType_maybe only be applied
629 -- to *types* (of kind *)
630 ASSERT( isRecursiveTyCon tc ) -- Guaranteed by coreView
631 case newTyConRhs tc of
632 (tvs, rep_ty) -> ASSERT( length tvs == length tys )
633 Just (substTyWith tvs tys rep_ty)
635 splitRecNewType_maybe other = Nothing
642 %************************************************************************
644 \subsection{Kinds and free variables}
646 %************************************************************************
648 ---------------------------------------------------------------------
649 Finding the kind of a type
650 ~~~~~~~~~~~~~~~~~~~~~~~~~~
652 typeKind :: Type -> Kind
653 typeKind (TyConApp tycon tys) = ASSERT( not (isCoercionTyCon tycon) )
654 -- We should be looking for the coercion kind,
656 foldr (\_ k -> kindFunResult k) (tyConKind tycon) tys
657 typeKind (NoteTy _ ty) = typeKind ty
658 typeKind (PredTy pred) = predKind pred
659 typeKind (AppTy fun arg) = kindFunResult (typeKind fun)
660 typeKind (ForAllTy tv ty) = typeKind ty
661 typeKind (TyVarTy tyvar) = tyVarKind tyvar
662 typeKind (FunTy arg res)
663 -- Hack alert. The kind of (Int -> Int#) is liftedTypeKind (*),
664 -- not unliftedTypKind (#)
665 -- The only things that can be after a function arrow are
666 -- (a) types (of kind openTypeKind or its sub-kinds)
667 -- (b) kinds (of super-kind TY) (e.g. * -> (* -> *))
668 | isTySuperKind k = k
669 | otherwise = ASSERT( isSubOpenTypeKind k) liftedTypeKind
673 predKind :: PredType -> Kind
674 predKind (EqPred {}) = coSuperKind -- A coercion kind!
675 predKind (ClassP {}) = liftedTypeKind -- Class and implicitPredicates are
676 predKind (IParam {}) = liftedTypeKind -- always represented by lifted types
680 ---------------------------------------------------------------------
681 Free variables of a type
682 ~~~~~~~~~~~~~~~~~~~~~~~~
684 tyVarsOfType :: Type -> TyVarSet
685 -- NB: for type synonyms tyVarsOfType does *not* expand the synonym
686 tyVarsOfType (TyVarTy tv) = unitVarSet tv
687 tyVarsOfType (TyConApp tycon tys) = tyVarsOfTypes tys
688 tyVarsOfType (NoteTy (FTVNote tvs) ty2) = tvs
689 tyVarsOfType (PredTy sty) = tyVarsOfPred sty
690 tyVarsOfType (FunTy arg res) = tyVarsOfType arg `unionVarSet` tyVarsOfType res
691 tyVarsOfType (AppTy fun arg) = tyVarsOfType fun `unionVarSet` tyVarsOfType arg
692 tyVarsOfType (ForAllTy tyvar ty) = delVarSet (tyVarsOfType ty) tyvar
694 tyVarsOfTypes :: [Type] -> TyVarSet
695 tyVarsOfTypes tys = foldr (unionVarSet.tyVarsOfType) emptyVarSet tys
697 tyVarsOfPred :: PredType -> TyVarSet
698 tyVarsOfPred (IParam _ ty) = tyVarsOfType ty
699 tyVarsOfPred (ClassP _ tys) = tyVarsOfTypes tys
701 tyVarsOfTheta :: ThetaType -> TyVarSet
702 tyVarsOfTheta = foldr (unionVarSet . tyVarsOfPred) emptyVarSet
704 -- Add a Note with the free tyvars to the top of the type
705 addFreeTyVars :: Type -> Type
706 addFreeTyVars ty@(NoteTy (FTVNote _) _) = ty
707 addFreeTyVars ty = NoteTy (FTVNote (tyVarsOfType ty)) ty
711 %************************************************************************
713 \subsection{TidyType}
715 %************************************************************************
717 tidyTy tidies up a type for printing in an error message, or in
720 It doesn't change the uniques at all, just the print names.
723 tidyTyVarBndr :: TidyEnv -> TyVar -> (TidyEnv, TyVar)
724 tidyTyVarBndr (tidy_env, subst) tyvar
725 = case tidyOccName tidy_env (getOccName name) of
726 (tidy', occ') -> ((tidy', subst'), tyvar')
728 subst' = extendVarEnv subst tyvar tyvar'
729 tyvar' = setTyVarName tyvar name'
730 name' = tidyNameOcc name occ'
732 name = tyVarName tyvar
734 tidyFreeTyVars :: TidyEnv -> TyVarSet -> TidyEnv
735 -- Add the free tyvars to the env in tidy form,
736 -- so that we can tidy the type they are free in
737 tidyFreeTyVars env tyvars = fst (tidyOpenTyVars env (varSetElems tyvars))
739 tidyOpenTyVars :: TidyEnv -> [TyVar] -> (TidyEnv, [TyVar])
740 tidyOpenTyVars env tyvars = mapAccumL tidyOpenTyVar env tyvars
742 tidyOpenTyVar :: TidyEnv -> TyVar -> (TidyEnv, TyVar)
743 -- Treat a new tyvar as a binder, and give it a fresh tidy name
744 tidyOpenTyVar env@(tidy_env, subst) tyvar
745 = case lookupVarEnv subst tyvar of
746 Just tyvar' -> (env, tyvar') -- Already substituted
747 Nothing -> tidyTyVarBndr env tyvar -- Treat it as a binder
749 tidyType :: TidyEnv -> Type -> Type
750 tidyType env@(tidy_env, subst) ty
753 go (TyVarTy tv) = case lookupVarEnv subst tv of
754 Nothing -> TyVarTy tv
755 Just tv' -> TyVarTy tv'
756 go (TyConApp tycon tys) = let args = map go tys
757 in args `seqList` TyConApp tycon args
758 go (NoteTy note ty) = (NoteTy $! (go_note note)) $! (go ty)
759 go (PredTy sty) = PredTy (tidyPred env sty)
760 go (AppTy fun arg) = (AppTy $! (go fun)) $! (go arg)
761 go (FunTy fun arg) = (FunTy $! (go fun)) $! (go arg)
762 go (ForAllTy tv ty) = ForAllTy tvp $! (tidyType envp ty)
764 (envp, tvp) = tidyTyVarBndr env tv
766 go_note note@(FTVNote ftvs) = note -- No need to tidy the free tyvars
768 tidyTypes env tys = map (tidyType env) tys
770 tidyPred :: TidyEnv -> PredType -> PredType
771 tidyPred env (IParam n ty) = IParam n (tidyType env ty)
772 tidyPred env (ClassP clas tys) = ClassP clas (tidyTypes env tys)
776 @tidyOpenType@ grabs the free type variables, tidies them
777 and then uses @tidyType@ to work over the type itself
780 tidyOpenType :: TidyEnv -> Type -> (TidyEnv, Type)
782 = (env', tidyType env' ty)
784 env' = tidyFreeTyVars env (tyVarsOfType ty)
786 tidyOpenTypes :: TidyEnv -> [Type] -> (TidyEnv, [Type])
787 tidyOpenTypes env tys = mapAccumL tidyOpenType env tys
789 tidyTopType :: Type -> Type
790 tidyTopType ty = tidyType emptyTidyEnv ty
795 tidyKind :: TidyEnv -> Kind -> (TidyEnv, Kind)
796 tidyKind env k = tidyOpenType env k
801 %************************************************************************
803 \subsection{Liftedness}
805 %************************************************************************
808 isUnLiftedType :: Type -> Bool
809 -- isUnLiftedType returns True for forall'd unlifted types:
810 -- x :: forall a. Int#
811 -- I found bindings like these were getting floated to the top level.
812 -- They are pretty bogus types, mind you. It would be better never to
815 isUnLiftedType ty | Just ty' <- coreView ty = isUnLiftedType ty'
816 isUnLiftedType (ForAllTy tv ty) = isUnLiftedType ty
817 isUnLiftedType (TyConApp tc _) = isUnLiftedTyCon tc
818 isUnLiftedType other = False
820 isUnboxedTupleType :: Type -> Bool
821 isUnboxedTupleType ty = case splitTyConApp_maybe ty of
822 Just (tc, ty_args) -> isUnboxedTupleTyCon tc
825 -- Should only be applied to *types*; hence the assert
826 isAlgType :: Type -> Bool
827 isAlgType ty = case splitTyConApp_maybe ty of
828 Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
833 @isStrictType@ computes whether an argument (or let RHS) should
834 be computed strictly or lazily, based only on its type.
835 Works just like isUnLiftedType, except that it has a special case
836 for dictionaries. Since it takes account of ClassP, you might think
837 this function should be in TcType, but isStrictType is used by DataCon,
838 which is below TcType in the hierarchy, so it's convenient to put it here.
841 isStrictType (PredTy pred) = isStrictPred pred
842 isStrictType ty | Just ty' <- coreView ty = isStrictType ty'
843 isStrictType (ForAllTy tv ty) = isStrictType ty
844 isStrictType (TyConApp tc _) = isUnLiftedTyCon tc
845 isStrictType other = False
847 isStrictPred (ClassP clas _) = opt_DictsStrict && not (isNewTyCon (classTyCon clas))
848 isStrictPred other = False
849 -- We may be strict in dictionary types, but only if it
850 -- has more than one component.
851 -- [Being strict in a single-component dictionary risks
852 -- poking the dictionary component, which is wrong.]
856 isPrimitiveType :: Type -> Bool
857 -- Returns types that are opaque to Haskell.
858 -- Most of these are unlifted, but now that we interact with .NET, we
859 -- may have primtive (foreign-imported) types that are lifted
860 isPrimitiveType ty = case splitTyConApp_maybe ty of
861 Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
867 %************************************************************************
869 \subsection{Sequencing on types
871 %************************************************************************
874 seqType :: Type -> ()
875 seqType (TyVarTy tv) = tv `seq` ()
876 seqType (AppTy t1 t2) = seqType t1 `seq` seqType t2
877 seqType (FunTy t1 t2) = seqType t1 `seq` seqType t2
878 seqType (NoteTy note t2) = seqNote note `seq` seqType t2
879 seqType (PredTy p) = seqPred p
880 seqType (TyConApp tc tys) = tc `seq` seqTypes tys
881 seqType (ForAllTy tv ty) = tv `seq` seqType ty
883 seqTypes :: [Type] -> ()
885 seqTypes (ty:tys) = seqType ty `seq` seqTypes tys
887 seqNote :: TyNote -> ()
888 seqNote (FTVNote set) = sizeUniqSet set `seq` ()
890 seqPred :: PredType -> ()
891 seqPred (ClassP c tys) = c `seq` seqTypes tys
892 seqPred (IParam n ty) = n `seq` seqType ty
896 %************************************************************************
898 Equality for Core types
899 (We don't use instances so that we know where it happens)
901 %************************************************************************
903 Note that eqType works right even for partial applications of newtypes.
904 See Note [Newtype eta] in TyCon.lhs
907 coreEqType :: Type -> Type -> Bool
911 rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfType t1 `unionVarSet` tyVarsOfType t2))
913 eq env (TyVarTy tv1) (TyVarTy tv2) = rnOccL env tv1 == rnOccR env tv2
914 eq env (ForAllTy tv1 t1) (ForAllTy tv2 t2) = eq (rnBndr2 env tv1 tv2) t1 t2
915 eq env (AppTy s1 t1) (AppTy s2 t2) = eq env s1 s2 && eq env t1 t2
916 eq env (FunTy s1 t1) (FunTy s2 t2) = eq env s1 s2 && eq env t1 t2
917 eq env (TyConApp tc1 tys1) (TyConApp tc2 tys2)
918 | tc1 == tc2, all2 (eq env) tys1 tys2 = True
919 -- The lengths should be equal because
920 -- the two types have the same kind
921 -- NB: if the type constructors differ that does not
922 -- necessarily mean that the types aren't equal
923 -- (synonyms, newtypes)
924 -- Even if the type constructors are the same, but the arguments
925 -- differ, the two types could be the same (e.g. if the arg is just
926 -- ignored in the RHS). In both these cases we fall through to an
927 -- attempt to expand one side or the other.
929 -- Now deal with newtypes, synonyms, pred-tys
930 eq env t1 t2 | Just t1' <- coreView t1 = eq env t1' t2
931 | Just t2' <- coreView t2 = eq env t1 t2'
933 -- Fall through case; not equal!
938 %************************************************************************
940 Comparision for source types
941 (We don't use instances so that we know where it happens)
943 %************************************************************************
947 do *not* look through newtypes, PredTypes
950 tcEqType :: Type -> Type -> Bool
951 tcEqType t1 t2 = isEqual $ cmpType t1 t2
953 tcEqTypes :: [Type] -> [Type] -> Bool
954 tcEqTypes tys1 tys2 = isEqual $ cmpTypes tys1 tys2
956 tcCmpType :: Type -> Type -> Ordering
957 tcCmpType t1 t2 = cmpType t1 t2
959 tcCmpTypes :: [Type] -> [Type] -> Ordering
960 tcCmpTypes tys1 tys2 = cmpTypes tys1 tys2
962 tcEqPred :: PredType -> PredType -> Bool
963 tcEqPred p1 p2 = isEqual $ cmpPred p1 p2
965 tcCmpPred :: PredType -> PredType -> Ordering
966 tcCmpPred p1 p2 = cmpPred p1 p2
968 tcEqTypeX :: RnEnv2 -> Type -> Type -> Bool
969 tcEqTypeX env t1 t2 = isEqual $ cmpTypeX env t1 t2
972 Now here comes the real worker
975 cmpType :: Type -> Type -> Ordering
976 cmpType t1 t2 = cmpTypeX rn_env t1 t2
978 rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfType t1 `unionVarSet` tyVarsOfType t2))
980 cmpTypes :: [Type] -> [Type] -> Ordering
981 cmpTypes ts1 ts2 = cmpTypesX rn_env ts1 ts2
983 rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfTypes ts1 `unionVarSet` tyVarsOfTypes ts2))
985 cmpPred :: PredType -> PredType -> Ordering
986 cmpPred p1 p2 = cmpPredX rn_env p1 p2
988 rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfPred p1 `unionVarSet` tyVarsOfPred p2))
990 cmpTypeX :: RnEnv2 -> Type -> Type -> Ordering -- Main workhorse
991 cmpTypeX env t1 t2 | Just t1' <- tcView t1 = cmpTypeX env t1' t2
992 | Just t2' <- tcView t2 = cmpTypeX env t1 t2'
994 cmpTypeX env (TyVarTy tv1) (TyVarTy tv2) = rnOccL env tv1 `compare` rnOccR env tv2
995 cmpTypeX env (ForAllTy tv1 t1) (ForAllTy tv2 t2) = cmpTypeX (rnBndr2 env tv1 tv2) t1 t2
996 cmpTypeX env (AppTy s1 t1) (AppTy s2 t2) = cmpTypeX env s1 s2 `thenCmp` cmpTypeX env t1 t2
997 cmpTypeX env (FunTy s1 t1) (FunTy s2 t2) = cmpTypeX env s1 s2 `thenCmp` cmpTypeX env t1 t2
998 cmpTypeX env (PredTy p1) (PredTy p2) = cmpPredX env p1 p2
999 cmpTypeX env (TyConApp tc1 tys1) (TyConApp tc2 tys2) = (tc1 `compare` tc2) `thenCmp` cmpTypesX env tys1 tys2
1000 cmpTypeX env t1 (NoteTy _ t2) = cmpTypeX env t1 t2
1002 -- Deal with the rest: TyVarTy < AppTy < FunTy < TyConApp < ForAllTy < PredTy
1003 cmpTypeX env (AppTy _ _) (TyVarTy _) = GT
1005 cmpTypeX env (FunTy _ _) (TyVarTy _) = GT
1006 cmpTypeX env (FunTy _ _) (AppTy _ _) = GT
1008 cmpTypeX env (TyConApp _ _) (TyVarTy _) = GT
1009 cmpTypeX env (TyConApp _ _) (AppTy _ _) = GT
1010 cmpTypeX env (TyConApp _ _) (FunTy _ _) = GT
1012 cmpTypeX env (ForAllTy _ _) (TyVarTy _) = GT
1013 cmpTypeX env (ForAllTy _ _) (AppTy _ _) = GT
1014 cmpTypeX env (ForAllTy _ _) (FunTy _ _) = GT
1015 cmpTypeX env (ForAllTy _ _) (TyConApp _ _) = GT
1017 cmpTypeX env (PredTy _) t2 = GT
1019 cmpTypeX env _ _ = LT
1022 cmpTypesX :: RnEnv2 -> [Type] -> [Type] -> Ordering
1023 cmpTypesX env [] [] = EQ
1024 cmpTypesX env (t1:tys1) (t2:tys2) = cmpTypeX env t1 t2 `thenCmp` cmpTypesX env tys1 tys2
1025 cmpTypesX env [] tys = LT
1026 cmpTypesX env ty [] = GT
1029 cmpPredX :: RnEnv2 -> PredType -> PredType -> Ordering
1030 cmpPredX env (IParam n1 ty1) (IParam n2 ty2) = (n1 `compare` n2) `thenCmp` cmpTypeX env ty1 ty2
1031 -- Compare types as well as names for implicit parameters
1032 -- This comparison is used exclusively (I think) for the
1033 -- finite map built in TcSimplify
1034 cmpPredX env (ClassP c1 tys1) (ClassP c2 tys2) = (c1 `compare` c2) `thenCmp` cmpTypesX env tys1 tys2
1035 cmpPredX env (IParam _ _) (ClassP _ _) = LT
1036 cmpPredX env (ClassP _ _) (IParam _ _) = GT
1039 PredTypes are used as a FM key in TcSimplify,
1040 so we take the easy path and make them an instance of Ord
1043 instance Eq PredType where { (==) = tcEqPred }
1044 instance Ord PredType where { compare = tcCmpPred }
1048 %************************************************************************
1052 %************************************************************************
1056 = TvSubst InScopeSet -- The in-scope type variables
1057 TvSubstEnv -- The substitution itself
1058 -- See Note [Apply Once]
1060 {- ----------------------------------------------------------
1063 We use TvSubsts to instantiate things, and we might instantiate
1067 So the substition might go [a->b, b->a]. A similar situation arises in Core
1068 when we find a beta redex like
1069 (/\ a /\ b -> e) b a
1070 Then we also end up with a substition that permutes type variables. Other
1071 variations happen to; for example [a -> (a, b)].
1073 ***************************************************
1074 *** So a TvSubst must be applied precisely once ***
1075 ***************************************************
1077 A TvSubst is not idempotent, but, unlike the non-idempotent substitution
1078 we use during unifications, it must not be repeatedly applied.
1079 -------------------------------------------------------------- -}
1082 type TvSubstEnv = TyVarEnv Type
1083 -- A TvSubstEnv is used both inside a TvSubst (with the apply-once
1084 -- invariant discussed in Note [Apply Once]), and also independently
1085 -- in the middle of matching, and unification (see Types.Unify)
1086 -- So you have to look at the context to know if it's idempotent or
1087 -- apply-once or whatever
1088 emptyTvSubstEnv :: TvSubstEnv
1089 emptyTvSubstEnv = emptyVarEnv
1091 composeTvSubst :: InScopeSet -> TvSubstEnv -> TvSubstEnv -> TvSubstEnv
1092 -- (compose env1 env2)(x) is env1(env2(x)); i.e. apply env2 then env1
1093 -- It assumes that both are idempotent
1094 -- Typically, env1 is the refinement to a base substitution env2
1095 composeTvSubst in_scope env1 env2
1096 = env1 `plusVarEnv` mapVarEnv (substTy subst1) env2
1097 -- First apply env1 to the range of env2
1098 -- Then combine the two, making sure that env1 loses if
1099 -- both bind the same variable; that's why env1 is the
1100 -- *left* argument to plusVarEnv, because the right arg wins
1102 subst1 = TvSubst in_scope env1
1104 emptyTvSubst = TvSubst emptyInScopeSet emptyVarEnv
1106 isEmptyTvSubst :: TvSubst -> Bool
1107 isEmptyTvSubst (TvSubst _ env) = isEmptyVarEnv env
1109 mkTvSubst :: InScopeSet -> TvSubstEnv -> TvSubst
1112 getTvSubstEnv :: TvSubst -> TvSubstEnv
1113 getTvSubstEnv (TvSubst _ env) = env
1115 getTvInScope :: TvSubst -> InScopeSet
1116 getTvInScope (TvSubst in_scope _) = in_scope
1118 isInScope :: Var -> TvSubst -> Bool
1119 isInScope v (TvSubst in_scope _) = v `elemInScopeSet` in_scope
1121 notElemTvSubst :: TyVar -> TvSubst -> Bool
1122 notElemTvSubst tv (TvSubst _ env) = not (tv `elemVarEnv` env)
1124 setTvSubstEnv :: TvSubst -> TvSubstEnv -> TvSubst
1125 setTvSubstEnv (TvSubst in_scope _) env = TvSubst in_scope env
1127 extendTvInScope :: TvSubst -> [Var] -> TvSubst
1128 extendTvInScope (TvSubst in_scope env) vars = TvSubst (extendInScopeSetList in_scope vars) env
1130 extendTvSubst :: TvSubst -> TyVar -> Type -> TvSubst
1131 extendTvSubst (TvSubst in_scope env) tv ty = TvSubst in_scope (extendVarEnv env tv ty)
1133 extendTvSubstList :: TvSubst -> [TyVar] -> [Type] -> TvSubst
1134 extendTvSubstList (TvSubst in_scope env) tvs tys
1135 = TvSubst in_scope (extendVarEnvList env (tvs `zip` tys))
1137 -- mkOpenTvSubst and zipOpenTvSubst generate the in-scope set from
1138 -- the types given; but it's just a thunk so with a bit of luck
1139 -- it'll never be evaluated
1141 mkOpenTvSubst :: TvSubstEnv -> TvSubst
1142 mkOpenTvSubst env = TvSubst (mkInScopeSet (tyVarsOfTypes (varEnvElts env))) env
1144 zipOpenTvSubst :: [TyVar] -> [Type] -> TvSubst
1145 zipOpenTvSubst tyvars tys
1147 | length tyvars /= length tys
1148 = pprTrace "zipOpenTvSubst" (ppr tyvars $$ ppr tys) emptyTvSubst
1151 = TvSubst (mkInScopeSet (tyVarsOfTypes tys)) (zipTyEnv tyvars tys)
1153 -- mkTopTvSubst is called when doing top-level substitutions.
1154 -- Here we expect that the free vars of the range of the
1155 -- substitution will be empty.
1156 mkTopTvSubst :: [(TyVar, Type)] -> TvSubst
1157 mkTopTvSubst prs = TvSubst emptyInScopeSet (mkVarEnv prs)
1159 zipTopTvSubst :: [TyVar] -> [Type] -> TvSubst
1160 zipTopTvSubst tyvars tys
1162 | length tyvars /= length tys
1163 = pprTrace "zipOpenTvSubst" (ppr tyvars $$ ppr tys) emptyTvSubst
1166 = TvSubst emptyInScopeSet (zipTyEnv tyvars tys)
1168 zipTyEnv :: [TyVar] -> [Type] -> TvSubstEnv
1171 | length tyvars /= length tys
1172 = pprTrace "mkTopTvSubst" (ppr tyvars $$ ppr tys) emptyVarEnv
1175 = zip_ty_env tyvars tys emptyVarEnv
1177 -- Later substitutions in the list over-ride earlier ones,
1178 -- but there should be no loops
1179 zip_ty_env [] [] env = env
1180 zip_ty_env (tv:tvs) (ty:tys) env = zip_ty_env tvs tys (extendVarEnv env tv ty)
1181 -- There used to be a special case for when
1183 -- (a not-uncommon case) in which case the substitution was dropped.
1184 -- But the type-tidier changes the print-name of a type variable without
1185 -- changing the unique, and that led to a bug. Why? Pre-tidying, we had
1186 -- a type {Foo t}, where Foo is a one-method class. So Foo is really a newtype.
1187 -- And it happened that t was the type variable of the class. Post-tiding,
1188 -- it got turned into {Foo t2}. The ext-core printer expanded this using
1189 -- sourceTypeRep, but that said "Oh, t == t2" because they have the same unique,
1190 -- and so generated a rep type mentioning t not t2.
1192 -- Simplest fix is to nuke the "optimisation"
1193 zip_ty_env tvs tys env = pprTrace "Var/Type length mismatch: " (ppr tvs $$ ppr tys) env
1194 -- zip_ty_env _ _ env = env
1196 instance Outputable TvSubst where
1197 ppr (TvSubst ins env)
1198 = brackets $ sep[ ptext SLIT("TvSubst"),
1199 nest 2 (ptext SLIT("In scope:") <+> ppr ins),
1200 nest 2 (ptext SLIT("Env:") <+> ppr env) ]
1203 %************************************************************************
1205 Performing type substitutions
1207 %************************************************************************
1210 substTyWith :: [TyVar] -> [Type] -> Type -> Type
1211 substTyWith tvs tys = ASSERT( length tvs == length tys )
1212 substTy (zipOpenTvSubst tvs tys)
1214 substTy :: TvSubst -> Type -> Type
1215 substTy subst ty | isEmptyTvSubst subst = ty
1216 | otherwise = subst_ty subst ty
1218 substTys :: TvSubst -> [Type] -> [Type]
1219 substTys subst tys | isEmptyTvSubst subst = tys
1220 | otherwise = map (subst_ty subst) tys
1222 substTheta :: TvSubst -> ThetaType -> ThetaType
1223 substTheta subst theta
1224 | isEmptyTvSubst subst = theta
1225 | otherwise = map (substPred subst) theta
1227 substPred :: TvSubst -> PredType -> PredType
1228 substPred subst (IParam n ty) = IParam n (subst_ty subst ty)
1229 substPred subst (ClassP clas tys) = ClassP clas (map (subst_ty subst) tys)
1230 substPred subst (EqPred ty1 ty2) = EqPred (subst_ty subst ty1) (subst_ty subst ty2)
1232 deShadowTy :: TyVarSet -> Type -> Type -- Remove any nested binders mentioning tvs
1234 = subst_ty (mkTvSubst in_scope emptyTvSubstEnv) ty
1236 in_scope = mkInScopeSet tvs
1238 subst_ty :: TvSubst -> Type -> Type
1239 -- subst_ty is the main workhorse for type substitution
1241 -- Note that the in_scope set is poked only if we hit a forall
1242 -- so it may often never be fully computed
1246 go (TyVarTy tv) = substTyVar subst tv
1247 go (TyConApp tc tys) = let args = map go tys
1248 in args `seqList` TyConApp tc args
1250 go (PredTy p) = PredTy $! (substPred subst p)
1252 go (NoteTy (FTVNote _) ty2) = go ty2 -- Discard the free tyvar note
1254 go (FunTy arg res) = (FunTy $! (go arg)) $! (go res)
1255 go (AppTy fun arg) = mkAppTy (go fun) $! (go arg)
1256 -- The mkAppTy smart constructor is important
1257 -- we might be replacing (a Int), represented with App
1258 -- by [Int], represented with TyConApp
1259 go (ForAllTy tv ty) = case substTyVarBndr subst tv of
1260 (subst', tv') -> ForAllTy tv' $! (subst_ty subst' ty)
1262 substTyVar :: TvSubst -> TyVar -> Type
1263 substTyVar subst@(TvSubst in_scope env) tv
1264 = case lookupTyVar subst tv of {
1265 Nothing -> TyVarTy tv;
1266 Just ty -> ty -- See Note [Apply Once]
1269 lookupTyVar :: TvSubst -> TyVar -> Maybe Type
1270 lookupTyVar (TvSubst in_scope env) tv = lookupVarEnv env tv
1272 substTyVarBndr :: TvSubst -> TyVar -> (TvSubst, TyVar)
1273 substTyVarBndr subst@(TvSubst in_scope env) old_var
1274 = (TvSubst (in_scope `extendInScopeSet` new_var) new_env, new_var)
1277 new_env | no_change = delVarEnv env old_var
1278 | otherwise = extendVarEnv env old_var (TyVarTy new_var)
1280 no_change = new_var == old_var && not is_co_var
1281 -- no_change means that the new_var is identical in
1282 -- all respects to the old_var (same unique, same kind)
1284 -- In that case we don't need to extend the substitution
1285 -- to map old to new. But instead we must zap any
1286 -- current substitution for the variable. For example:
1287 -- (\x.e) with id_subst = [x |-> e']
1288 -- Here we must simply zap the substitution for x
1290 new_var = uniqAway in_scope subst_old_var
1291 -- The uniqAway part makes sure the new variable is not already in scope
1293 subst_old_var -- subst_old_var is old_var with the substitution applied to its kind
1294 -- It's only worth doing the substitution for coercions,
1295 -- becuase only they can have free type variables
1296 | is_co_var = setTyVarKind old_var (substTy subst kind)
1297 | otherwise = old_var
1298 kind = tyVarKind old_var
1299 is_co_var = isCoercionKind kind
1302 ----------------------------------------------------
1307 There's a little subtyping at the kind level:
1316 where * [LiftedTypeKind] means boxed type
1317 # [UnliftedTypeKind] means unboxed type
1318 (#) [UbxTupleKind] means unboxed tuple
1319 ?? [ArgTypeKind] is the lub of *,#
1320 ? [OpenTypeKind] means any type at all
1324 error :: forall a:?. String -> a
1325 (->) :: ?? -> ? -> *
1326 (\(x::t) -> ...) Here t::?? (i.e. not unboxed tuple)
1329 type KindVar = TyVar -- invariant: KindVar will always be a
1330 -- TcTyVar with details MetaTv TauTv ...
1331 -- kind var constructors and functions are in TcType
1333 type SimpleKind = Kind
1338 During kind inference, a kind variable unifies only with
1340 sk ::= * | sk1 -> sk2
1342 data T a = MkT a (T Int#)
1343 fails. We give T the kind (k -> *), and the kind variable k won't unify
1344 with # (the kind of Int#).
1348 When creating a fresh internal type variable, we give it a kind to express
1349 constraints on it. E.g. in (\x->e) we make up a fresh type variable for x,
1352 During unification we only bind an internal type variable to a type
1353 whose kind is lower in the sub-kind hierarchy than the kind of the tyvar.
1355 When unifying two internal type variables, we collect their kind constraints by
1356 finding the GLB of the two. Since the partial order is a tree, they only
1357 have a glb if one is a sub-kind of the other. In that case, we bind the
1358 less-informative one to the more informative one. Neat, eh?
1365 %************************************************************************
1367 Functions over Kinds
1369 %************************************************************************
1372 kindFunResult :: Kind -> Kind
1373 kindFunResult k = funResultTy k
1375 splitKindFunTys :: Kind -> ([Kind],Kind)
1376 splitKindFunTys k = splitFunTys k
1378 isUbxTupleKind, isOpenTypeKind, isArgTypeKind, isUnliftedTypeKind :: Kind -> Bool
1380 isOpenTypeKindCon tc = tyConUnique tc == openTypeKindTyConKey
1382 isOpenTypeKind (TyConApp tc _) = isOpenTypeKindCon tc
1383 isOpenTypeKind other = False
1385 isUbxTupleKindCon tc = tyConUnique tc == ubxTupleKindTyConKey
1387 isUbxTupleKind (TyConApp tc _) = isUbxTupleKindCon tc
1388 isUbxTupleKind other = False
1390 isArgTypeKindCon tc = tyConUnique tc == argTypeKindTyConKey
1392 isArgTypeKind (TyConApp tc _) = isArgTypeKindCon tc
1393 isArgTypeKind other = False
1395 isUnliftedTypeKindCon tc = tyConUnique tc == unliftedTypeKindTyConKey
1397 isUnliftedTypeKind (TyConApp tc _) = isUnliftedTypeKindCon tc
1398 isUnliftedTypeKind other = False
1400 isSubOpenTypeKind :: Kind -> Bool
1401 -- True of any sub-kind of OpenTypeKind (i.e. anything except arrow)
1402 isSubOpenTypeKind (FunTy k1 k2) = ASSERT2 ( isKind k1, text "isSubOpenTypeKind" <+> ppr k1 <+> text "::" <+> ppr (typeKind k1) )
1403 ASSERT2 ( isKind k2, text "isSubOpenTypeKind" <+> ppr k2 <+> text "::" <+> ppr (typeKind k2) )
1405 isSubOpenTypeKind (TyConApp kc []) = ASSERT( isKind (TyConApp kc []) ) True
1406 isSubOpenTypeKind other = ASSERT( isKind other ) False
1407 -- This is a conservative answer
1408 -- It matters in the call to isSubKind in
1409 -- checkExpectedKind.
1411 isSubArgTypeKindCon kc
1412 | isUnliftedTypeKindCon kc = True
1413 | isLiftedTypeKindCon kc = True
1414 | isArgTypeKindCon kc = True
1417 isSubArgTypeKind :: Kind -> Bool
1418 -- True of any sub-kind of ArgTypeKind
1419 isSubArgTypeKind (TyConApp kc []) = isSubArgTypeKindCon kc
1420 isSubArgTypeKind other = False
1422 isSuperKind :: Type -> Bool
1423 isSuperKind (TyConApp (skc) []) = isSuperKindTyCon skc
1424 isSuperKind other = False
1426 isKind :: Kind -> Bool
1427 isKind k = isSuperKind (typeKind k)
1431 isSubKind :: Kind -> Kind -> Bool
1432 -- (k1 `isSubKind` k2) checks that k1 <: k2
1433 isSubKind (TyConApp kc1 []) (TyConApp kc2 []) = kc1 `isSubKindCon` kc1
1434 isSubKind (FunTy a1 r1) (FunTy a2 r2) = (a2 `isSubKind` a1) && (r1 `isSubKind` r2)
1435 isSubKind k1 k2 = False
1437 eqKind :: Kind -> Kind -> Bool
1440 isSubKindCon :: TyCon -> TyCon -> Bool
1441 -- (kc1 `isSubKindCon` kc2) checks that kc1 <: kc2
1442 isSubKindCon kc1 kc2
1443 | isLiftedTypeKindCon kc1 && isLiftedTypeKindCon kc2 = True
1444 | isUnliftedTypeKindCon kc1 && isUnliftedTypeKindCon kc2 = True
1445 | isUbxTupleKindCon kc1 && isUbxTupleKindCon kc2 = True
1446 | isOpenTypeKindCon kc2 = True
1447 -- we already know kc1 is not a fun, its a TyCon
1448 | isArgTypeKindCon kc2 && isSubArgTypeKindCon kc1 = True
1451 defaultKind :: Kind -> Kind
1452 -- Used when generalising: default kind '?' and '??' to '*'
1454 -- When we generalise, we make generic type variables whose kind is
1455 -- simple (* or *->* etc). So generic type variables (other than
1456 -- built-in constants like 'error') always have simple kinds. This is important;
1459 -- We want f to get type
1460 -- f :: forall (a::*). a -> Bool
1462 -- f :: forall (a::??). a -> Bool
1463 -- because that would allow a call like (f 3#) as well as (f True),
1464 --and the calling conventions differ. This defaulting is done in TcMType.zonkTcTyVarBndr.
1466 | isSubOpenTypeKind k = liftedTypeKind
1467 | isSubArgTypeKind k = liftedTypeKind
1470 isCoercionKind :: Kind -> Bool
1471 -- All coercions are of form (ty1 :=: ty2)
1472 -- This function is here rather than in Coercion,
1473 -- because it's used by substTy
1474 isCoercionKind k | Just k' <- kindView k = isCoercionKind k'
1475 isCoercionKind (PredTy (EqPred {})) = True
1476 isCoercionKind other = False