2 % (c) The University of Glasgow 2006
3 % (c) The GRASP/AQUA Project, Glasgow University, 1998
6 Type - public interface
9 {-# OPTIONS -fno-warn-incomplete-patterns #-}
10 -- The above warning supression flag is a temporary kludge.
11 -- While working on this module you are encouraged to remove it and fix
12 -- any warnings in the module. See
13 -- http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings
17 -- re-exports from TypeRep
18 TyThing(..), Type, PredType(..), ThetaType,
22 Kind, SimpleKind, KindVar,
23 kindFunResult, splitKindFunTys, splitKindFunTysN,
25 liftedTypeKindTyCon, openTypeKindTyCon, unliftedTypeKindTyCon,
26 argTypeKindTyCon, ubxTupleKindTyCon,
28 liftedTypeKind, unliftedTypeKind, openTypeKind,
29 argTypeKind, ubxTupleKind,
31 tySuperKind, coSuperKind,
33 isLiftedTypeKind, isUnliftedTypeKind, isOpenTypeKind,
34 isUbxTupleKind, isArgTypeKind, isKind, isTySuperKind,
35 isCoSuperKind, isSuperKind, isCoercionKind, isEqPred,
36 mkArrowKind, mkArrowKinds,
38 isSubArgTypeKind, isSubOpenTypeKind, isSubKind, defaultKind, eqKind,
41 -- Re-exports from TyCon
44 mkTyVarTy, mkTyVarTys, getTyVar, getTyVar_maybe, isTyVarTy,
46 mkAppTy, mkAppTys, splitAppTy, splitAppTys,
47 splitAppTy_maybe, repSplitAppTy_maybe,
49 mkFunTy, mkFunTys, splitFunTy, splitFunTy_maybe,
50 splitFunTys, splitFunTysN,
51 funResultTy, funArgTy, zipFunTys, isFunTy,
53 mkTyConApp, mkTyConTy,
54 tyConAppTyCon, tyConAppArgs,
55 splitTyConApp_maybe, splitTyConApp,
56 splitNewTyConApp_maybe, splitNewTyConApp,
58 repType, typePrimRep, coreView, tcView, kindView, rttiView,
60 mkForAllTy, mkForAllTys, splitForAllTy_maybe, splitForAllTys,
61 applyTy, applyTys, isForAllTy, dropForAlls,
64 predTypeRep, mkPredTy, mkPredTys, pprSourceTyCon, mkFamilyTyConApp,
70 isUnLiftedType, isUnboxedTupleType, isAlgType, isClosedAlgType,
71 isPrimitiveType, isStrictType, isStrictPred,
74 tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta,
75 typeKind, addFreeTyVars,
80 -- Tidying up for printing
82 tidyOpenType, tidyOpenTypes,
83 tidyTyVarBndr, tidyFreeTyVars,
84 tidyOpenTyVar, tidyOpenTyVars,
85 tidyTopType, tidyPred,
89 coreEqType, tcEqType, tcEqTypes, tcCmpType, tcCmpTypes,
90 tcEqPred, tcCmpPred, tcEqTypeX, tcPartOfType, tcPartOfPred,
96 TvSubstEnv, emptyTvSubstEnv, -- Representation widely visible
97 TvSubst(..), emptyTvSubst, -- Representation visible to a few friends
98 mkTvSubst, mkOpenTvSubst, zipOpenTvSubst, zipTopTvSubst, mkTopTvSubst, notElemTvSubst,
99 getTvSubstEnv, setTvSubstEnv, getTvInScope, extendTvInScope,
100 extendTvSubst, extendTvSubstList, isInScope, composeTvSubst, zipTyEnv,
103 -- Performing substitution on types
104 substTy, substTys, substTyWith, substTheta,
105 substPred, substTyVar, substTyVars, substTyVarBndr, deShadowTy, lookupTyVar,
108 pprType, pprParendType, pprTypeApp, pprTyThingCategory, pprTyThing, pprForAll,
109 pprPred, pprTheta, pprThetaArrow, pprClassPred, pprKind, pprParendKind
112 #include "HsVersions.h"
114 -- We import the representation and primitive functions from TypeRep.
115 -- Many things are reexported, but not the representation!
136 import Data.Maybe ( isJust )
140 %************************************************************************
144 %************************************************************************
146 In Core, we "look through" non-recursive newtypes and PredTypes.
149 {-# INLINE coreView #-}
150 coreView :: Type -> Maybe Type
151 -- Strips off the *top layer only* of a type to give
152 -- its underlying representation type.
153 -- Returns Nothing if there is nothing to look through.
155 -- In the case of newtypes, it returns
156 -- *either* a vanilla TyConApp (recursive newtype, or non-saturated)
157 -- *or* the newtype representation (otherwise), meaning the
158 -- type written in the RHS of the newtype decl,
159 -- which may itself be a newtype
161 -- Example: newtype R = MkR S
163 -- newtype T = MkT (T -> T)
164 -- expandNewTcApp on R gives Just S
166 -- on T gives Nothing (no expansion)
168 -- By being non-recursive and inlined, this case analysis gets efficiently
169 -- joined onto the case analysis that the caller is already doing
170 coreView (NoteTy _ ty) = Just ty
172 | isEqPred p = Nothing
173 | otherwise = Just (predTypeRep p)
174 coreView (TyConApp tc tys) | Just (tenv, rhs, tys') <- coreExpandTyCon_maybe tc tys
175 = Just (mkAppTys (substTy (mkTopTvSubst tenv) rhs) tys')
176 -- Its important to use mkAppTys, rather than (foldl AppTy),
177 -- because the function part might well return a
178 -- partially-applied type constructor; indeed, usually will!
183 -----------------------------------------------
184 {-# INLINE tcView #-}
185 tcView :: Type -> Maybe Type
186 -- Same, but for the type checker, which just looks through synonyms
187 tcView (NoteTy _ ty) = Just ty
188 tcView (TyConApp tc tys) | Just (tenv, rhs, tys') <- tcExpandTyCon_maybe tc tys
189 = Just (mkAppTys (substTy (mkTopTvSubst tenv) rhs) tys')
192 -----------------------------------------------
193 rttiView :: Type -> Type
194 -- Same, but for the RTTI system, which cannot deal with predicates nor polymorphism
195 rttiView (ForAllTy _ ty) = rttiView ty
196 rttiView (NoteTy _ ty) = rttiView ty
197 rttiView (FunTy PredTy{} ty) = rttiView ty
198 rttiView (FunTy NoteTy{} ty) = rttiView ty
199 rttiView ty@TyConApp{} | Just ty' <- coreView ty
201 rttiView (TyConApp tc tys) = mkTyConApp tc (map rttiView 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
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 _ = 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 :: Type -> Type -> Type
256 mkAppTy orig_ty1 orig_ty2
259 mk_app (NoteTy _ ty1) = mk_app ty1
260 mk_app (TyConApp tc tys) = mkTyConApp tc (tys ++ [orig_ty2])
261 mk_app _ = AppTy orig_ty1 orig_ty2
262 -- Note that the TyConApp could be an
263 -- under-saturated type synonym. GHC allows that; e.g.
264 -- type Foo k = k a -> k a
266 -- foo :: Foo Id -> Foo Id
268 -- Here Id is partially applied in the type sig for Foo,
269 -- but once the type synonyms are expanded all is well
271 mkAppTys :: Type -> [Type] -> Type
272 mkAppTys orig_ty1 [] = orig_ty1
273 -- This check for an empty list of type arguments
274 -- avoids the needless loss of a type synonym constructor.
275 -- For example: mkAppTys Rational []
276 -- returns to (Ratio Integer), which has needlessly lost
277 -- the Rational part.
278 mkAppTys orig_ty1 orig_tys2
281 mk_app (NoteTy _ ty1) = mk_app ty1
282 mk_app (TyConApp tc tys) = mkTyConApp tc (tys ++ orig_tys2)
283 -- mkTyConApp: see notes with mkAppTy
284 mk_app _ = foldl AppTy orig_ty1 orig_tys2
287 splitAppTy_maybe :: Type -> Maybe (Type, Type)
288 splitAppTy_maybe ty | Just ty' <- coreView ty
289 = splitAppTy_maybe ty'
290 splitAppTy_maybe ty = repSplitAppTy_maybe ty
293 repSplitAppTy_maybe :: Type -> Maybe (Type,Type)
294 -- Does the AppTy split, but assumes that any view stuff is already done
295 repSplitAppTy_maybe (FunTy ty1 ty2) = Just (TyConApp funTyCon [ty1], ty2)
296 repSplitAppTy_maybe (AppTy ty1 ty2) = Just (ty1, ty2)
297 repSplitAppTy_maybe (TyConApp tc tys)
298 | not (isOpenSynTyCon tc) || length tys > tyConArity tc
299 = case snocView tys of -- never create unsaturated type family apps
300 Just (tys', ty') -> Just (TyConApp tc tys', ty')
302 repSplitAppTy_maybe _other = Nothing
304 splitAppTy :: Type -> (Type, Type)
305 splitAppTy ty = case splitAppTy_maybe ty of
307 Nothing -> panic "splitAppTy"
310 splitAppTys :: Type -> (Type, [Type])
311 splitAppTys ty = split ty ty []
313 split orig_ty ty args | Just ty' <- coreView ty = split orig_ty ty' args
314 split _ (AppTy ty arg) args = split ty ty (arg:args)
315 split _ (TyConApp tc tc_args) args
316 = let -- keep type families saturated
317 n | isOpenSynTyCon tc = tyConArity tc
319 (tc_args1, tc_args2) = splitAt n tc_args
321 (TyConApp tc tc_args1, tc_args2 ++ args)
322 split _ (FunTy ty1 ty2) args = ASSERT( null args )
323 (TyConApp funTyCon [], [ty1,ty2])
324 split orig_ty _ args = (orig_ty, args)
329 ---------------------------------------------------------------------
334 mkFunTy :: Type -> Type -> Type
335 mkFunTy (PredTy (EqPred ty1 ty2)) res = mkForAllTy (mkWildCoVar (PredTy (EqPred ty1 ty2))) res
336 mkFunTy arg res = FunTy arg res
338 mkFunTys :: [Type] -> Type -> Type
339 mkFunTys tys ty = foldr mkFunTy ty tys
341 isFunTy :: Type -> Bool
342 isFunTy ty = isJust (splitFunTy_maybe ty)
344 splitFunTy :: Type -> (Type, Type)
345 splitFunTy ty | Just ty' <- coreView ty = splitFunTy ty'
346 splitFunTy (FunTy arg res) = (arg, res)
347 splitFunTy other = pprPanic "splitFunTy" (ppr other)
349 splitFunTy_maybe :: Type -> Maybe (Type, Type)
350 splitFunTy_maybe ty | Just ty' <- coreView ty = splitFunTy_maybe ty'
351 splitFunTy_maybe (FunTy arg res) = Just (arg, res)
352 splitFunTy_maybe _ = Nothing
354 splitFunTys :: Type -> ([Type], Type)
355 splitFunTys ty = split [] ty ty
357 split args orig_ty ty | Just ty' <- coreView ty = split args orig_ty ty'
358 split args _ (FunTy arg res) = split (arg:args) res res
359 split args orig_ty _ = (reverse args, orig_ty)
361 splitFunTysN :: Int -> Type -> ([Type], Type)
362 -- Split off exactly n arg tys
363 splitFunTysN 0 ty = ([], ty)
364 splitFunTysN n ty = case splitFunTy ty of { (arg, res) ->
365 case splitFunTysN (n-1) res of { (args, res) ->
368 zipFunTys :: Outputable a => [a] -> Type -> ([(a,Type)], Type)
369 zipFunTys orig_xs orig_ty = split [] orig_xs orig_ty orig_ty
371 split acc [] nty _ = (reverse acc, nty)
373 | Just ty' <- coreView ty = split acc xs nty ty'
374 split acc (x:xs) _ (FunTy arg res) = split ((x,arg):acc) xs res res
375 split _ _ _ _ = pprPanic "zipFunTys" (ppr orig_xs <+> ppr orig_ty)
377 funResultTy :: Type -> Type
378 funResultTy ty | Just ty' <- coreView ty = funResultTy ty'
379 funResultTy (FunTy _arg res) = res
380 funResultTy ty = pprPanic "funResultTy" (ppr ty)
382 funArgTy :: Type -> Type
383 funArgTy ty | Just ty' <- coreView ty = funArgTy ty'
384 funArgTy (FunTy arg _res) = arg
385 funArgTy ty = pprPanic "funArgTy" (ppr ty)
389 ---------------------------------------------------------------------
392 @mkTyConApp@ is a key function, because it builds a TyConApp, FunTy or PredTy,
396 mkTyConApp :: TyCon -> [Type] -> Type
398 | isFunTyCon tycon, [ty1,ty2] <- tys
404 mkTyConTy :: TyCon -> Type
405 mkTyConTy tycon = mkTyConApp tycon []
407 -- splitTyConApp "looks through" synonyms, because they don't
408 -- mean a distinct type, but all other type-constructor applications
409 -- including functions are returned as Just ..
411 tyConAppTyCon :: Type -> TyCon
412 tyConAppTyCon ty = fst (splitTyConApp ty)
414 tyConAppArgs :: Type -> [Type]
415 tyConAppArgs ty = snd (splitTyConApp ty)
417 splitTyConApp :: Type -> (TyCon, [Type])
418 splitTyConApp ty = case splitTyConApp_maybe ty of
420 Nothing -> pprPanic "splitTyConApp" (ppr ty)
422 splitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
423 splitTyConApp_maybe ty | Just ty' <- coreView ty = splitTyConApp_maybe ty'
424 splitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
425 splitTyConApp_maybe (FunTy arg res) = Just (funTyCon, [arg,res])
426 splitTyConApp_maybe _ = Nothing
428 -- Sometimes we do NOT want to look throught a newtype. When case matching
429 -- on a newtype we want a convenient way to access the arguments of a newty
430 -- constructor so as to properly form a coercion.
431 splitNewTyConApp :: Type -> (TyCon, [Type])
432 splitNewTyConApp ty = case splitNewTyConApp_maybe ty of
434 Nothing -> pprPanic "splitNewTyConApp" (ppr ty)
435 splitNewTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
436 splitNewTyConApp_maybe ty | Just ty' <- tcView ty = splitNewTyConApp_maybe ty'
437 splitNewTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
438 splitNewTyConApp_maybe (FunTy arg res) = Just (funTyCon, [arg,res])
439 splitNewTyConApp_maybe _ = Nothing
441 newTyConInstRhs :: TyCon -> [Type] -> Type
442 -- Unwrap one 'layer' of newtype
443 -- Use the eta'd version if possible
444 newTyConInstRhs tycon tys
445 = ASSERT2( equalLength tvs tys1, ppr tycon $$ ppr tys $$ ppr tvs )
446 mkAppTys (substTyWith tvs tys1 ty) tys2
448 (tvs, ty) = newTyConEtadRhs tycon
449 (tys1, tys2) = splitAtList tvs tys
453 ---------------------------------------------------------------------
457 Notes on type synonyms
458 ~~~~~~~~~~~~~~~~~~~~~~
459 The various "split" functions (splitFunTy, splitRhoTy, splitForAllTy) try
460 to return type synonyms whereever possible. Thus
465 splitFunTys (a -> Foo a) = ([a], Foo a)
468 The reason is that we then get better (shorter) type signatures in
469 interfaces. Notably this plays a role in tcTySigs in TcBinds.lhs.
472 Note [Expanding newtypes]
473 ~~~~~~~~~~~~~~~~~~~~~~~~~
474 When expanding a type to expose a data-type constructor, we need to be
475 careful about newtypes, lest we fall into an infinite loop. Here are
478 newtype Id x = MkId x
479 newtype Fix f = MkFix (f (Fix f))
480 newtype T = MkT (T -> T)
483 --------------------------
485 Fix Maybe Maybe (Fix Maybe)
489 Notice that we can expand T, even though it's recursive.
490 And we can expand Id (Id Int), even though the Id shows up
491 twice at the outer level.
493 So, when expanding, we keep track of when we've seen a recursive
494 newtype at outermost level; and bale out if we see it again.
499 repType looks through
503 (d) usage annotations
504 (e) all newtypes, including recursive ones, but not newtype families
505 It's useful in the back end.
508 repType :: Type -> Type
509 -- Only applied to types of kind *; hence tycons are saturated
513 go :: [TyCon] -> Type -> Type
514 go rec_nts ty | Just ty' <- coreView ty -- Expand synonyms
517 go rec_nts (ForAllTy _ ty) -- Look through foralls
520 go rec_nts ty@(TyConApp tc tys) -- Expand newtypes
521 | Just _co_con <- newTyConCo_maybe tc -- See Note [Expanding newtypes]
522 = if tc `elem` rec_nts -- in Type.lhs
524 else go rec_nts' nt_rhs
526 nt_rhs = newTyConInstRhs tc tys
527 rec_nts' | isRecursiveTyCon tc = tc:rec_nts
528 | otherwise = rec_nts
533 -- ToDo: this could be moved to the code generator, using splitTyConApp instead
534 -- of inspecting the type directly.
535 typePrimRep :: Type -> PrimRep
536 typePrimRep ty = case repType ty of
537 TyConApp tc _ -> tyConPrimRep tc
539 AppTy _ _ -> PtrRep -- See note below
541 _ -> pprPanic "typePrimRep" (ppr ty)
542 -- Types of the form 'f a' must be of kind *, not *#, so
543 -- we are guaranteed that they are represented by pointers.
544 -- The reason is that f must have kind *->*, not *->*#, because
545 -- (we claim) there is no way to constrain f's kind any other
550 ---------------------------------------------------------------------
555 mkForAllTy :: TyVar -> Type -> Type
557 = mkForAllTys [tyvar] ty
559 mkForAllTys :: [TyVar] -> Type -> Type
560 mkForAllTys tyvars ty = foldr ForAllTy ty tyvars
562 isForAllTy :: Type -> Bool
563 isForAllTy (NoteTy _ ty) = isForAllTy ty
564 isForAllTy (ForAllTy _ _) = True
567 splitForAllTy_maybe :: Type -> Maybe (TyVar, Type)
568 splitForAllTy_maybe ty = splitFAT_m ty
570 splitFAT_m ty | Just ty' <- coreView ty = splitFAT_m ty'
571 splitFAT_m (ForAllTy tyvar ty) = Just(tyvar, ty)
572 splitFAT_m _ = Nothing
574 splitForAllTys :: Type -> ([TyVar], Type)
575 splitForAllTys ty = split ty ty []
577 split orig_ty ty tvs | Just ty' <- coreView ty = split orig_ty ty' tvs
578 split _ (ForAllTy tv ty) tvs = split ty ty (tv:tvs)
579 split orig_ty _ tvs = (reverse tvs, orig_ty)
581 dropForAlls :: Type -> Type
582 dropForAlls ty = snd (splitForAllTys ty)
585 -- (mkPiType now in CoreUtils)
589 Instantiate a for-all type with one or more type arguments.
590 Used when we have a polymorphic function applied to type args:
592 Then we use (applyTys type-of-f [t1,t2]) to compute the type of
596 applyTy :: Type -> Type -> Type
597 applyTy ty arg | Just ty' <- coreView ty = applyTy ty' arg
598 applyTy (ForAllTy tv ty) arg = substTyWith [tv] [arg] ty
599 applyTy _ _ = panic "applyTy"
601 applyTys :: Type -> [Type] -> Type
602 -- This function is interesting because
603 -- a) the function may have more for-alls than there are args
604 -- b) less obviously, it may have fewer for-alls
605 -- For case (b) think of
606 -- applyTys (forall a.a) [forall b.b, Int]
607 -- This really can happen, via dressing up polymorphic types with newtype
608 -- clothing. Here's an example:
609 -- newtype R = R (forall a. a->a)
610 -- foo = case undefined :: R of
613 applyTys orig_fun_ty [] = orig_fun_ty
614 applyTys orig_fun_ty arg_tys
615 | n_tvs == n_args -- The vastly common case
616 = substTyWith tvs arg_tys rho_ty
617 | n_tvs > n_args -- Too many for-alls
618 = substTyWith (take n_args tvs) arg_tys
619 (mkForAllTys (drop n_args tvs) rho_ty)
620 | otherwise -- Too many type args
621 = ASSERT2( n_tvs > 0, ppr orig_fun_ty ) -- Zero case gives infnite loop!
622 applyTys (substTyWith tvs (take n_tvs arg_tys) rho_ty)
625 (tvs, rho_ty) = splitForAllTys orig_fun_ty
627 n_args = length arg_tys
631 %************************************************************************
633 \subsection{Source types}
635 %************************************************************************
637 A "source type" is a type that is a separate type as far as the type checker is
638 concerned, but which has low-level representation as far as the back end is concerned.
640 Source types are always lifted.
642 The key function is predTypeRep which gives the representation of a source type:
645 mkPredTy :: PredType -> Type
646 mkPredTy pred = PredTy pred
648 mkPredTys :: ThetaType -> [Type]
649 mkPredTys preds = map PredTy preds
651 predTypeRep :: PredType -> Type
652 -- Convert a PredType to its "representation type";
653 -- the post-type-checking type used by all the Core passes of GHC.
654 -- Unwraps only the outermost level; for example, the result might
655 -- be a newtype application
656 predTypeRep (IParam _ ty) = ty
657 predTypeRep (ClassP clas tys) = mkTyConApp (classTyCon clas) tys
658 -- Result might be a newtype application, but the consumer will
659 -- look through that too if necessary
660 predTypeRep (EqPred ty1 ty2) = pprPanic "predTypeRep" (ppr (EqPred ty1 ty2))
662 mkFamilyTyConApp :: TyCon -> [Type] -> Type
663 -- Given a family instance TyCon and its arg types, return the
664 -- corresponding family type. E.g.
666 -- data instance T (Maybe b) = MkT b -- Instance tycon :RTL
668 -- mkFamilyTyConApp :RTL Int = T (Maybe Int)
669 mkFamilyTyConApp tc tys
670 | Just (fam_tc, fam_tys) <- tyConFamInst_maybe tc
671 , let fam_subst = zipTopTvSubst (tyConTyVars tc) tys
672 = mkTyConApp fam_tc (substTys fam_subst fam_tys)
676 -- Pretty prints a tycon, using the family instance in case of a
677 -- representation tycon. For example
678 -- e.g. data T [a] = ...
679 -- In that case we want to print `T [a]', where T is the family TyCon
680 pprSourceTyCon :: TyCon -> SDoc
682 | Just (fam_tc, tys) <- tyConFamInst_maybe tycon
683 = ppr $ fam_tc `TyConApp` tys -- can't be FunTyCon
689 %************************************************************************
691 \subsection{Kinds and free variables}
693 %************************************************************************
695 ---------------------------------------------------------------------
696 Finding the kind of a type
697 ~~~~~~~~~~~~~~~~~~~~~~~~~~
699 typeKind :: Type -> Kind
700 typeKind (TyConApp tycon tys) = ASSERT( not (isCoercionTyCon tycon) )
701 -- We should be looking for the coercion kind,
703 foldr (\_ k -> kindFunResult k) (tyConKind tycon) tys
704 typeKind (NoteTy _ ty) = typeKind ty
705 typeKind (PredTy pred) = predKind pred
706 typeKind (AppTy fun _) = kindFunResult (typeKind fun)
707 typeKind (ForAllTy _ ty) = typeKind ty
708 typeKind (TyVarTy tyvar) = tyVarKind tyvar
709 typeKind (FunTy _arg res)
710 -- Hack alert. The kind of (Int -> Int#) is liftedTypeKind (*),
711 -- not unliftedTypKind (#)
712 -- The only things that can be after a function arrow are
713 -- (a) types (of kind openTypeKind or its sub-kinds)
714 -- (b) kinds (of super-kind TY) (e.g. * -> (* -> *))
715 | isTySuperKind k = k
716 | otherwise = ASSERT( isSubOpenTypeKind k) liftedTypeKind
720 predKind :: PredType -> Kind
721 predKind (EqPred {}) = coSuperKind -- A coercion kind!
722 predKind (ClassP {}) = liftedTypeKind -- Class and implicitPredicates are
723 predKind (IParam {}) = liftedTypeKind -- always represented by lifted types
727 ---------------------------------------------------------------------
728 Free variables of a type
729 ~~~~~~~~~~~~~~~~~~~~~~~~
731 tyVarsOfType :: Type -> TyVarSet
732 -- NB: for type synonyms tyVarsOfType does *not* expand the synonym
733 tyVarsOfType (TyVarTy tv) = unitVarSet tv
734 tyVarsOfType (TyConApp _ tys) = tyVarsOfTypes tys
735 tyVarsOfType (NoteTy (FTVNote tvs) _) = tvs
736 tyVarsOfType (PredTy sty) = tyVarsOfPred sty
737 tyVarsOfType (FunTy arg res) = tyVarsOfType arg `unionVarSet` tyVarsOfType res
738 tyVarsOfType (AppTy fun arg) = tyVarsOfType fun `unionVarSet` tyVarsOfType arg
739 tyVarsOfType (ForAllTy tyvar ty) = delVarSet (tyVarsOfType ty) tyvar
741 tyVarsOfTypes :: [Type] -> TyVarSet
742 tyVarsOfTypes tys = foldr (unionVarSet.tyVarsOfType) emptyVarSet tys
744 tyVarsOfPred :: PredType -> TyVarSet
745 tyVarsOfPred (IParam _ ty) = tyVarsOfType ty
746 tyVarsOfPred (ClassP _ tys) = tyVarsOfTypes tys
747 tyVarsOfPred (EqPred ty1 ty2) = tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2
749 tyVarsOfTheta :: ThetaType -> TyVarSet
750 tyVarsOfTheta = foldr (unionVarSet . tyVarsOfPred) emptyVarSet
752 -- Add a Note with the free tyvars to the top of the type
753 addFreeTyVars :: Type -> Type
754 addFreeTyVars ty@(NoteTy (FTVNote _) _) = ty
755 addFreeTyVars ty = NoteTy (FTVNote (tyVarsOfType ty)) ty
759 %************************************************************************
761 \subsection{Type families}
763 %************************************************************************
765 Type family instances occuring in a type after expanding synonyms.
768 tyFamInsts :: Type -> [(TyCon, [Type])]
770 | Just exp_ty <- tcView ty = tyFamInsts exp_ty
771 tyFamInsts (TyVarTy _) = []
772 tyFamInsts (TyConApp tc tys)
773 | isOpenSynTyCon tc = [(tc, tys)]
774 | otherwise = concat (map tyFamInsts tys)
775 tyFamInsts (FunTy ty1 ty2) = tyFamInsts ty1 ++ tyFamInsts ty2
776 tyFamInsts (AppTy ty1 ty2) = tyFamInsts ty1 ++ tyFamInsts ty2
777 tyFamInsts (ForAllTy _ ty) = tyFamInsts ty
781 %************************************************************************
783 \subsection{TidyType}
785 %************************************************************************
787 tidyTy tidies up a type for printing in an error message, or in
790 It doesn't change the uniques at all, just the print names.
793 tidyTyVarBndr :: TidyEnv -> TyVar -> (TidyEnv, TyVar)
794 tidyTyVarBndr env@(tidy_env, subst) tyvar
795 = case tidyOccName tidy_env (getOccName name) of
796 (tidy', occ') -> ((tidy', subst'), tyvar'')
798 subst' = extendVarEnv subst tyvar tyvar''
799 tyvar' = setTyVarName tyvar name'
800 name' = tidyNameOcc name occ'
801 -- Don't forget to tidy the kind for coercions!
802 tyvar'' | isCoVar tyvar = setTyVarKind tyvar' kind'
804 kind' = tidyType env (tyVarKind tyvar)
806 name = tyVarName tyvar
808 tidyFreeTyVars :: TidyEnv -> TyVarSet -> TidyEnv
809 -- Add the free tyvars to the env in tidy form,
810 -- so that we can tidy the type they are free in
811 tidyFreeTyVars env tyvars = fst (tidyOpenTyVars env (varSetElems tyvars))
813 tidyOpenTyVars :: TidyEnv -> [TyVar] -> (TidyEnv, [TyVar])
814 tidyOpenTyVars env tyvars = mapAccumL tidyOpenTyVar env tyvars
816 tidyOpenTyVar :: TidyEnv -> TyVar -> (TidyEnv, TyVar)
817 -- Treat a new tyvar as a binder, and give it a fresh tidy name
818 tidyOpenTyVar env@(_, subst) tyvar
819 = case lookupVarEnv subst tyvar of
820 Just tyvar' -> (env, tyvar') -- Already substituted
821 Nothing -> tidyTyVarBndr env tyvar -- Treat it as a binder
823 tidyType :: TidyEnv -> Type -> Type
824 tidyType env@(_, subst) ty
827 go (TyVarTy tv) = case lookupVarEnv subst tv of
828 Nothing -> TyVarTy tv
829 Just tv' -> TyVarTy tv'
830 go (TyConApp tycon tys) = let args = map go tys
831 in args `seqList` TyConApp tycon args
832 go (NoteTy note ty) = (NoteTy $! (go_note note)) $! (go ty)
833 go (PredTy sty) = PredTy (tidyPred env sty)
834 go (AppTy fun arg) = (AppTy $! (go fun)) $! (go arg)
835 go (FunTy fun arg) = (FunTy $! (go fun)) $! (go arg)
836 go (ForAllTy tv ty) = ForAllTy tvp $! (tidyType envp ty)
838 (envp, tvp) = tidyTyVarBndr env tv
840 go_note note@(FTVNote _ftvs) = note -- No need to tidy the free tyvars
842 tidyTypes :: TidyEnv -> [Type] -> [Type]
843 tidyTypes env tys = map (tidyType env) tys
845 tidyPred :: TidyEnv -> PredType -> PredType
846 tidyPred env (IParam n ty) = IParam n (tidyType env ty)
847 tidyPred env (ClassP clas tys) = ClassP clas (tidyTypes env tys)
848 tidyPred env (EqPred ty1 ty2) = EqPred (tidyType env ty1) (tidyType env ty2)
852 @tidyOpenType@ grabs the free type variables, tidies them
853 and then uses @tidyType@ to work over the type itself
856 tidyOpenType :: TidyEnv -> Type -> (TidyEnv, Type)
858 = (env', tidyType env' ty)
860 env' = tidyFreeTyVars env (tyVarsOfType ty)
862 tidyOpenTypes :: TidyEnv -> [Type] -> (TidyEnv, [Type])
863 tidyOpenTypes env tys = mapAccumL tidyOpenType env tys
865 tidyTopType :: Type -> Type
866 tidyTopType ty = tidyType emptyTidyEnv ty
871 tidyKind :: TidyEnv -> Kind -> (TidyEnv, Kind)
872 tidyKind env k = tidyOpenType env k
877 %************************************************************************
879 \subsection{Liftedness}
881 %************************************************************************
884 isUnLiftedType :: Type -> Bool
885 -- isUnLiftedType returns True for forall'd unlifted types:
886 -- x :: forall a. Int#
887 -- I found bindings like these were getting floated to the top level.
888 -- They are pretty bogus types, mind you. It would be better never to
891 isUnLiftedType ty | Just ty' <- coreView ty = isUnLiftedType ty'
892 isUnLiftedType (ForAllTy _ ty) = isUnLiftedType ty
893 isUnLiftedType (TyConApp tc _) = isUnLiftedTyCon tc
894 isUnLiftedType _ = False
896 isUnboxedTupleType :: Type -> Bool
897 isUnboxedTupleType ty = case splitTyConApp_maybe ty of
898 Just (tc, _ty_args) -> isUnboxedTupleTyCon tc
901 -- Should only be applied to *types*; hence the assert
902 isAlgType :: Type -> Bool
904 = case splitTyConApp_maybe ty of
905 Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
909 -- Should only be applied to *types*; hence the assert
910 isClosedAlgType :: Type -> Bool
912 = case splitTyConApp_maybe ty of
913 Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
914 isAlgTyCon tc && not (isOpenTyCon tc)
918 @isStrictType@ computes whether an argument (or let RHS) should
919 be computed strictly or lazily, based only on its type.
920 Works just like isUnLiftedType, except that it has a special case
921 for dictionaries. Since it takes account of ClassP, you might think
922 this function should be in TcType, but isStrictType is used by DataCon,
923 which is below TcType in the hierarchy, so it's convenient to put it here.
926 isStrictType :: Type -> Bool
927 isStrictType (PredTy pred) = isStrictPred pred
928 isStrictType ty | Just ty' <- coreView ty = isStrictType ty'
929 isStrictType (ForAllTy _ ty) = isStrictType ty
930 isStrictType (TyConApp tc _) = isUnLiftedTyCon tc
931 isStrictType _ = False
933 isStrictPred :: PredType -> Bool
934 isStrictPred (ClassP clas _) = opt_DictsStrict && not (isNewTyCon (classTyCon clas))
935 isStrictPred _ = False
936 -- We may be strict in dictionary types, but only if it
937 -- has more than one component.
938 -- [Being strict in a single-component dictionary risks
939 -- poking the dictionary component, which is wrong.]
943 isPrimitiveType :: Type -> Bool
944 -- Returns types that are opaque to Haskell.
945 -- Most of these are unlifted, but now that we interact with .NET, we
946 -- may have primtive (foreign-imported) types that are lifted
947 isPrimitiveType ty = case splitTyConApp_maybe ty of
948 Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
954 %************************************************************************
956 \subsection{Sequencing on types
958 %************************************************************************
961 seqType :: Type -> ()
962 seqType (TyVarTy tv) = tv `seq` ()
963 seqType (AppTy t1 t2) = seqType t1 `seq` seqType t2
964 seqType (FunTy t1 t2) = seqType t1 `seq` seqType t2
965 seqType (NoteTy note t2) = seqNote note `seq` seqType t2
966 seqType (PredTy p) = seqPred p
967 seqType (TyConApp tc tys) = tc `seq` seqTypes tys
968 seqType (ForAllTy tv ty) = tv `seq` seqType ty
970 seqTypes :: [Type] -> ()
972 seqTypes (ty:tys) = seqType ty `seq` seqTypes tys
974 seqNote :: TyNote -> ()
975 seqNote (FTVNote set) = sizeUniqSet set `seq` ()
977 seqPred :: PredType -> ()
978 seqPred (ClassP c tys) = c `seq` seqTypes tys
979 seqPred (IParam n ty) = n `seq` seqType ty
980 seqPred (EqPred ty1 ty2) = seqType ty1 `seq` seqType ty2
984 %************************************************************************
986 Equality for Core types
987 (We don't use instances so that we know where it happens)
989 %************************************************************************
991 Note that eqType works right even for partial applications of newtypes.
992 See Note [Newtype eta] in TyCon.lhs
995 coreEqType :: Type -> Type -> Bool
999 rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfType t1 `unionVarSet` tyVarsOfType t2))
1001 eq env (TyVarTy tv1) (TyVarTy tv2) = rnOccL env tv1 == rnOccR env tv2
1002 eq env (ForAllTy tv1 t1) (ForAllTy tv2 t2) = eq (rnBndr2 env tv1 tv2) t1 t2
1003 eq env (AppTy s1 t1) (AppTy s2 t2) = eq env s1 s2 && eq env t1 t2
1004 eq env (FunTy s1 t1) (FunTy s2 t2) = eq env s1 s2 && eq env t1 t2
1005 eq env (TyConApp tc1 tys1) (TyConApp tc2 tys2)
1006 | tc1 == tc2, all2 (eq env) tys1 tys2 = True
1007 -- The lengths should be equal because
1008 -- the two types have the same kind
1009 -- NB: if the type constructors differ that does not
1010 -- necessarily mean that the types aren't equal
1011 -- (synonyms, newtypes)
1012 -- Even if the type constructors are the same, but the arguments
1013 -- differ, the two types could be the same (e.g. if the arg is just
1014 -- ignored in the RHS). In both these cases we fall through to an
1015 -- attempt to expand one side or the other.
1017 -- Now deal with newtypes, synonyms, pred-tys
1018 eq env t1 t2 | Just t1' <- coreView t1 = eq env t1' t2
1019 | Just t2' <- coreView t2 = eq env t1 t2'
1021 -- Fall through case; not equal!
1026 %************************************************************************
1028 Comparision for source types
1029 (We don't use instances so that we know where it happens)
1031 %************************************************************************
1035 do *not* look through newtypes, PredTypes
1038 tcEqType :: Type -> Type -> Bool
1039 tcEqType t1 t2 = isEqual $ cmpType t1 t2
1041 tcEqTypes :: [Type] -> [Type] -> Bool
1042 tcEqTypes tys1 tys2 = isEqual $ cmpTypes tys1 tys2
1044 tcCmpType :: Type -> Type -> Ordering
1045 tcCmpType t1 t2 = cmpType t1 t2
1047 tcCmpTypes :: [Type] -> [Type] -> Ordering
1048 tcCmpTypes tys1 tys2 = cmpTypes tys1 tys2
1050 tcEqPred :: PredType -> PredType -> Bool
1051 tcEqPred p1 p2 = isEqual $ cmpPred p1 p2
1053 tcCmpPred :: PredType -> PredType -> Ordering
1054 tcCmpPred p1 p2 = cmpPred p1 p2
1056 tcEqTypeX :: RnEnv2 -> Type -> Type -> Bool
1057 tcEqTypeX env t1 t2 = isEqual $ cmpTypeX env t1 t2
1060 Checks whether the second argument is a subterm of the first. (We don't care
1061 about binders, as we are only interested in syntactic subterms.)
1064 tcPartOfType :: Type -> Type -> Bool
1066 | tcEqType t1 t2 = True
1068 | Just t2' <- tcView t2 = tcPartOfType t1 t2'
1069 tcPartOfType _ (TyVarTy _) = False
1070 tcPartOfType t1 (ForAllTy _ t2) = tcPartOfType t1 t2
1071 tcPartOfType t1 (AppTy s2 t2) = tcPartOfType t1 s2 || tcPartOfType t1 t2
1072 tcPartOfType t1 (FunTy s2 t2) = tcPartOfType t1 s2 || tcPartOfType t1 t2
1073 tcPartOfType t1 (PredTy p2) = tcPartOfPred t1 p2
1074 tcPartOfType t1 (TyConApp _ ts) = any (tcPartOfType t1) ts
1075 tcPartOfType t1 (NoteTy _ t2) = tcPartOfType t1 t2
1077 tcPartOfPred :: Type -> PredType -> Bool
1078 tcPartOfPred t1 (IParam _ t2) = tcPartOfType t1 t2
1079 tcPartOfPred t1 (ClassP _ ts) = any (tcPartOfType t1) ts
1080 tcPartOfPred t1 (EqPred s2 t2) = tcPartOfType t1 s2 || tcPartOfType t1 t2
1083 Now here comes the real worker
1086 cmpType :: Type -> Type -> Ordering
1087 cmpType t1 t2 = cmpTypeX rn_env t1 t2
1089 rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfType t1 `unionVarSet` tyVarsOfType t2))
1091 cmpTypes :: [Type] -> [Type] -> Ordering
1092 cmpTypes ts1 ts2 = cmpTypesX rn_env ts1 ts2
1094 rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfTypes ts1 `unionVarSet` tyVarsOfTypes ts2))
1096 cmpPred :: PredType -> PredType -> Ordering
1097 cmpPred p1 p2 = cmpPredX rn_env p1 p2
1099 rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfPred p1 `unionVarSet` tyVarsOfPred p2))
1101 cmpTypeX :: RnEnv2 -> Type -> Type -> Ordering -- Main workhorse
1102 cmpTypeX env t1 t2 | Just t1' <- tcView t1 = cmpTypeX env t1' t2
1103 | Just t2' <- tcView t2 = cmpTypeX env t1 t2'
1105 cmpTypeX env (TyVarTy tv1) (TyVarTy tv2) = rnOccL env tv1 `compare` rnOccR env tv2
1106 cmpTypeX env (ForAllTy tv1 t1) (ForAllTy tv2 t2) = cmpTypeX (rnBndr2 env tv1 tv2) t1 t2
1107 cmpTypeX env (AppTy s1 t1) (AppTy s2 t2) = cmpTypeX env s1 s2 `thenCmp` cmpTypeX env t1 t2
1108 cmpTypeX env (FunTy s1 t1) (FunTy s2 t2) = cmpTypeX env s1 s2 `thenCmp` cmpTypeX env t1 t2
1109 cmpTypeX env (PredTy p1) (PredTy p2) = cmpPredX env p1 p2
1110 cmpTypeX env (TyConApp tc1 tys1) (TyConApp tc2 tys2) = (tc1 `compare` tc2) `thenCmp` cmpTypesX env tys1 tys2
1111 cmpTypeX env t1 (NoteTy _ t2) = cmpTypeX env t1 t2
1113 -- Deal with the rest: TyVarTy < AppTy < FunTy < TyConApp < ForAllTy < PredTy
1114 cmpTypeX _ (AppTy _ _) (TyVarTy _) = GT
1116 cmpTypeX _ (FunTy _ _) (TyVarTy _) = GT
1117 cmpTypeX _ (FunTy _ _) (AppTy _ _) = GT
1119 cmpTypeX _ (TyConApp _ _) (TyVarTy _) = GT
1120 cmpTypeX _ (TyConApp _ _) (AppTy _ _) = GT
1121 cmpTypeX _ (TyConApp _ _) (FunTy _ _) = GT
1123 cmpTypeX _ (ForAllTy _ _) (TyVarTy _) = GT
1124 cmpTypeX _ (ForAllTy _ _) (AppTy _ _) = GT
1125 cmpTypeX _ (ForAllTy _ _) (FunTy _ _) = GT
1126 cmpTypeX _ (ForAllTy _ _) (TyConApp _ _) = GT
1128 cmpTypeX _ (PredTy _) _ = GT
1133 cmpTypesX :: RnEnv2 -> [Type] -> [Type] -> Ordering
1134 cmpTypesX _ [] [] = EQ
1135 cmpTypesX env (t1:tys1) (t2:tys2) = cmpTypeX env t1 t2 `thenCmp` cmpTypesX env tys1 tys2
1136 cmpTypesX _ [] _ = LT
1137 cmpTypesX _ _ [] = GT
1140 cmpPredX :: RnEnv2 -> PredType -> PredType -> Ordering
1141 cmpPredX env (IParam n1 ty1) (IParam n2 ty2) = (n1 `compare` n2) `thenCmp` cmpTypeX env ty1 ty2
1142 -- Compare names only for implicit parameters
1143 -- This comparison is used exclusively (I believe)
1144 -- for the Avails finite map built in TcSimplify
1145 -- If the types differ we keep them distinct so that we see
1146 -- a distinct pair to run improvement on
1147 cmpPredX env (ClassP c1 tys1) (ClassP c2 tys2) = (c1 `compare` c2) `thenCmp` (cmpTypesX env tys1 tys2)
1148 cmpPredX env (EqPred ty1 ty2) (EqPred ty1' ty2') = (cmpTypeX env ty1 ty1') `thenCmp` (cmpTypeX env ty2 ty2')
1150 -- Constructor order: IParam < ClassP < EqPred
1151 cmpPredX _ (IParam {}) _ = LT
1152 cmpPredX _ (ClassP {}) (IParam {}) = GT
1153 cmpPredX _ (ClassP {}) (EqPred {}) = LT
1154 cmpPredX _ (EqPred {}) _ = GT
1157 PredTypes are used as a FM key in TcSimplify,
1158 so we take the easy path and make them an instance of Ord
1161 instance Eq PredType where { (==) = tcEqPred }
1162 instance Ord PredType where { compare = tcCmpPred }
1166 %************************************************************************
1170 %************************************************************************
1174 = TvSubst InScopeSet -- The in-scope type variables
1175 TvSubstEnv -- The substitution itself
1176 -- See Note [Apply Once]
1177 -- and Note [Extending the TvSubstEnv]
1179 {- ----------------------------------------------------------
1183 We use TvSubsts to instantiate things, and we might instantiate
1187 So the substition might go [a->b, b->a]. A similar situation arises in Core
1188 when we find a beta redex like
1189 (/\ a /\ b -> e) b a
1190 Then we also end up with a substition that permutes type variables. Other
1191 variations happen to; for example [a -> (a, b)].
1193 ***************************************************
1194 *** So a TvSubst must be applied precisely once ***
1195 ***************************************************
1197 A TvSubst is not idempotent, but, unlike the non-idempotent substitution
1198 we use during unifications, it must not be repeatedly applied.
1200 Note [Extending the TvSubst]
1201 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1202 The following invariant should hold of a TvSubst
1204 The in-scope set is needed *only* to
1205 guide the generation of fresh uniques
1207 In particular, the *kind* of the type variables in
1208 the in-scope set is not relevant
1210 This invariant allows a short-cut when the TvSubstEnv is empty:
1211 if the TvSubstEnv is empty --- i.e. (isEmptyTvSubt subst) holds ---
1212 then (substTy subst ty) does nothing.
1214 For example, consider:
1215 (/\a. /\b:(a~Int). ...b..) Int
1216 We substitute Int for 'a'. The Unique of 'b' does not change, but
1217 nevertheless we add 'b' to the TvSubstEnv, because b's type does change
1219 This invariant has several crucial consequences:
1221 * In substTyVarBndr, we need extend the TvSubstEnv
1222 - if the unique has changed
1223 - or if the kind has changed
1225 * In substTyVar, we do not need to consult the in-scope set;
1226 the TvSubstEnv is enough
1228 * In substTy, substTheta, we can short-circuit when the TvSubstEnv is empty
1231 -------------------------------------------------------------- -}
1234 type TvSubstEnv = TyVarEnv Type
1235 -- A TvSubstEnv is used both inside a TvSubst (with the apply-once
1236 -- invariant discussed in Note [Apply Once]), and also independently
1237 -- in the middle of matching, and unification (see Types.Unify)
1238 -- So you have to look at the context to know if it's idempotent or
1239 -- apply-once or whatever
1240 emptyTvSubstEnv :: TvSubstEnv
1241 emptyTvSubstEnv = emptyVarEnv
1243 composeTvSubst :: InScopeSet -> TvSubstEnv -> TvSubstEnv -> TvSubstEnv
1244 -- (compose env1 env2)(x) is env1(env2(x)); i.e. apply env2 then env1
1245 -- It assumes that both are idempotent
1246 -- Typically, env1 is the refinement to a base substitution env2
1247 composeTvSubst in_scope env1 env2
1248 = env1 `plusVarEnv` mapVarEnv (substTy subst1) env2
1249 -- First apply env1 to the range of env2
1250 -- Then combine the two, making sure that env1 loses if
1251 -- both bind the same variable; that's why env1 is the
1252 -- *left* argument to plusVarEnv, because the right arg wins
1254 subst1 = TvSubst in_scope env1
1256 emptyTvSubst :: TvSubst
1257 emptyTvSubst = TvSubst emptyInScopeSet emptyVarEnv
1259 isEmptyTvSubst :: TvSubst -> Bool
1260 -- See Note [Extending the TvSubstEnv]
1261 isEmptyTvSubst (TvSubst _ env) = isEmptyVarEnv env
1263 mkTvSubst :: InScopeSet -> TvSubstEnv -> TvSubst
1266 getTvSubstEnv :: TvSubst -> TvSubstEnv
1267 getTvSubstEnv (TvSubst _ env) = env
1269 getTvInScope :: TvSubst -> InScopeSet
1270 getTvInScope (TvSubst in_scope _) = in_scope
1272 isInScope :: Var -> TvSubst -> Bool
1273 isInScope v (TvSubst in_scope _) = v `elemInScopeSet` in_scope
1275 notElemTvSubst :: TyVar -> TvSubst -> Bool
1276 notElemTvSubst tv (TvSubst _ env) = not (tv `elemVarEnv` env)
1278 setTvSubstEnv :: TvSubst -> TvSubstEnv -> TvSubst
1279 setTvSubstEnv (TvSubst in_scope _) env = TvSubst in_scope env
1281 extendTvInScope :: TvSubst -> [Var] -> TvSubst
1282 extendTvInScope (TvSubst in_scope env) vars = TvSubst (extendInScopeSetList in_scope vars) env
1284 extendTvSubst :: TvSubst -> TyVar -> Type -> TvSubst
1285 extendTvSubst (TvSubst in_scope env) tv ty = TvSubst in_scope (extendVarEnv env tv ty)
1287 extendTvSubstList :: TvSubst -> [TyVar] -> [Type] -> TvSubst
1288 extendTvSubstList (TvSubst in_scope env) tvs tys
1289 = TvSubst in_scope (extendVarEnvList env (tvs `zip` tys))
1291 -- mkOpenTvSubst and zipOpenTvSubst generate the in-scope set from
1292 -- the types given; but it's just a thunk so with a bit of luck
1293 -- it'll never be evaluated
1295 mkOpenTvSubst :: TvSubstEnv -> TvSubst
1296 mkOpenTvSubst env = TvSubst (mkInScopeSet (tyVarsOfTypes (varEnvElts env))) env
1298 zipOpenTvSubst :: [TyVar] -> [Type] -> TvSubst
1299 zipOpenTvSubst tyvars tys
1301 | length tyvars /= length tys
1302 = pprTrace "zipOpenTvSubst" (ppr tyvars $$ ppr tys) emptyTvSubst
1305 = TvSubst (mkInScopeSet (tyVarsOfTypes tys)) (zipTyEnv tyvars tys)
1307 -- mkTopTvSubst is called when doing top-level substitutions.
1308 -- Here we expect that the free vars of the range of the
1309 -- substitution will be empty.
1310 mkTopTvSubst :: [(TyVar, Type)] -> TvSubst
1311 mkTopTvSubst prs = TvSubst emptyInScopeSet (mkVarEnv prs)
1313 zipTopTvSubst :: [TyVar] -> [Type] -> TvSubst
1314 zipTopTvSubst tyvars tys
1316 | length tyvars /= length tys
1317 = pprTrace "zipTopTvSubst" (ppr tyvars $$ ppr tys) emptyTvSubst
1320 = TvSubst emptyInScopeSet (zipTyEnv tyvars tys)
1322 zipTyEnv :: [TyVar] -> [Type] -> TvSubstEnv
1325 | length tyvars /= length tys
1326 = pprTrace "mkTopTvSubst" (ppr tyvars $$ ppr tys) emptyVarEnv
1329 = zip_ty_env tyvars tys emptyVarEnv
1331 -- Later substitutions in the list over-ride earlier ones,
1332 -- but there should be no loops
1333 zip_ty_env :: [TyVar] -> [Type] -> TvSubstEnv -> TvSubstEnv
1334 zip_ty_env [] [] env = env
1335 zip_ty_env (tv:tvs) (ty:tys) env = zip_ty_env tvs tys (extendVarEnv env tv ty)
1336 -- There used to be a special case for when
1338 -- (a not-uncommon case) in which case the substitution was dropped.
1339 -- But the type-tidier changes the print-name of a type variable without
1340 -- changing the unique, and that led to a bug. Why? Pre-tidying, we had
1341 -- a type {Foo t}, where Foo is a one-method class. So Foo is really a newtype.
1342 -- And it happened that t was the type variable of the class. Post-tiding,
1343 -- it got turned into {Foo t2}. The ext-core printer expanded this using
1344 -- sourceTypeRep, but that said "Oh, t == t2" because they have the same unique,
1345 -- and so generated a rep type mentioning t not t2.
1347 -- Simplest fix is to nuke the "optimisation"
1348 zip_ty_env tvs tys env = pprTrace "Var/Type length mismatch: " (ppr tvs $$ ppr tys) env
1349 -- zip_ty_env _ _ env = env
1351 instance Outputable TvSubst where
1352 ppr (TvSubst ins env)
1353 = brackets $ sep[ ptext SLIT("TvSubst"),
1354 nest 2 (ptext SLIT("In scope:") <+> ppr ins),
1355 nest 2 (ptext SLIT("Env:") <+> ppr env) ]
1358 %************************************************************************
1360 Performing type substitutions
1362 %************************************************************************
1365 substTyWith :: [TyVar] -> [Type] -> Type -> Type
1366 substTyWith tvs tys = ASSERT( length tvs == length tys )
1367 substTy (zipOpenTvSubst tvs tys)
1369 substTy :: TvSubst -> Type -> Type
1370 substTy subst ty | isEmptyTvSubst subst = ty
1371 | otherwise = subst_ty subst ty
1373 substTys :: TvSubst -> [Type] -> [Type]
1374 substTys subst tys | isEmptyTvSubst subst = tys
1375 | otherwise = map (subst_ty subst) tys
1377 substTheta :: TvSubst -> ThetaType -> ThetaType
1378 substTheta subst theta
1379 | isEmptyTvSubst subst = theta
1380 | otherwise = map (substPred subst) theta
1382 substPred :: TvSubst -> PredType -> PredType
1383 substPred subst (IParam n ty) = IParam n (subst_ty subst ty)
1384 substPred subst (ClassP clas tys) = ClassP clas (map (subst_ty subst) tys)
1385 substPred subst (EqPred ty1 ty2) = EqPred (subst_ty subst ty1) (subst_ty subst ty2)
1387 deShadowTy :: TyVarSet -> Type -> Type -- Remove any nested binders mentioning tvs
1389 = subst_ty (mkTvSubst in_scope emptyTvSubstEnv) ty
1391 in_scope = mkInScopeSet tvs
1393 subst_ty :: TvSubst -> Type -> Type
1394 -- subst_ty is the main workhorse for type substitution
1396 -- Note that the in_scope set is poked only if we hit a forall
1397 -- so it may often never be fully computed
1401 go (TyVarTy tv) = substTyVar subst tv
1402 go (TyConApp tc tys) = let args = map go tys
1403 in args `seqList` TyConApp tc args
1405 go (PredTy p) = PredTy $! (substPred subst p)
1407 go (NoteTy (FTVNote _) ty2) = go ty2 -- Discard the free tyvar note
1409 go (FunTy arg res) = (FunTy $! (go arg)) $! (go res)
1410 go (AppTy fun arg) = mkAppTy (go fun) $! (go arg)
1411 -- The mkAppTy smart constructor is important
1412 -- we might be replacing (a Int), represented with App
1413 -- by [Int], represented with TyConApp
1414 go (ForAllTy tv ty) = case substTyVarBndr subst tv of
1415 (subst', tv') -> ForAllTy tv' $! (subst_ty subst' ty)
1417 substTyVar :: TvSubst -> TyVar -> Type
1418 substTyVar subst@(TvSubst _ _) tv
1419 = case lookupTyVar subst tv of {
1420 Nothing -> TyVarTy tv;
1421 Just ty -> ty -- See Note [Apply Once]
1424 substTyVars :: TvSubst -> [TyVar] -> [Type]
1425 substTyVars subst tvs = map (substTyVar subst) tvs
1427 lookupTyVar :: TvSubst -> TyVar -> Maybe Type
1428 -- See Note [Extending the TvSubst]
1429 lookupTyVar (TvSubst _ env) tv = lookupVarEnv env tv
1431 substTyVarBndr :: TvSubst -> TyVar -> (TvSubst, TyVar)
1432 substTyVarBndr subst@(TvSubst in_scope env) old_var
1433 = (TvSubst (in_scope `extendInScopeSet` new_var) new_env, new_var)
1435 is_co_var = isCoVar old_var
1437 new_env | no_change = delVarEnv env old_var
1438 | otherwise = extendVarEnv env old_var (TyVarTy new_var)
1440 no_change = new_var == old_var && not is_co_var
1441 -- no_change means that the new_var is identical in
1442 -- all respects to the old_var (same unique, same kind)
1443 -- See Note [Extending the TvSubst]
1445 -- In that case we don't need to extend the substitution
1446 -- to map old to new. But instead we must zap any
1447 -- current substitution for the variable. For example:
1448 -- (\x.e) with id_subst = [x |-> e']
1449 -- Here we must simply zap the substitution for x
1451 new_var = uniqAway in_scope subst_old_var
1452 -- The uniqAway part makes sure the new variable is not already in scope
1454 subst_old_var -- subst_old_var is old_var with the substitution applied to its kind
1455 -- It's only worth doing the substitution for coercions,
1456 -- becuase only they can have free type variables
1457 | is_co_var = setTyVarKind old_var (substTy subst (tyVarKind old_var))
1458 | otherwise = old_var
1461 ----------------------------------------------------
1466 There's a little subtyping at the kind level:
1475 where * [LiftedTypeKind] means boxed type
1476 # [UnliftedTypeKind] means unboxed type
1477 (#) [UbxTupleKind] means unboxed tuple
1478 ?? [ArgTypeKind] is the lub of *,#
1479 ? [OpenTypeKind] means any type at all
1483 error :: forall a:?. String -> a
1484 (->) :: ?? -> ? -> *
1485 (\(x::t) -> ...) Here t::?? (i.e. not unboxed tuple)
1488 type KindVar = TyVar -- invariant: KindVar will always be a
1489 -- TcTyVar with details MetaTv TauTv ...
1490 -- kind var constructors and functions are in TcType
1492 type SimpleKind = Kind
1497 During kind inference, a kind variable unifies only with
1499 sk ::= * | sk1 -> sk2
1501 data T a = MkT a (T Int#)
1502 fails. We give T the kind (k -> *), and the kind variable k won't unify
1503 with # (the kind of Int#).
1507 When creating a fresh internal type variable, we give it a kind to express
1508 constraints on it. E.g. in (\x->e) we make up a fresh type variable for x,
1511 During unification we only bind an internal type variable to a type
1512 whose kind is lower in the sub-kind hierarchy than the kind of the tyvar.
1514 When unifying two internal type variables, we collect their kind constraints by
1515 finding the GLB of the two. Since the partial order is a tree, they only
1516 have a glb if one is a sub-kind of the other. In that case, we bind the
1517 less-informative one to the more informative one. Neat, eh?
1524 %************************************************************************
1526 Functions over Kinds
1528 %************************************************************************
1531 kindFunResult :: Kind -> Kind
1532 kindFunResult k = funResultTy k
1534 splitKindFunTys :: Kind -> ([Kind],Kind)
1535 splitKindFunTys k = splitFunTys k
1537 splitKindFunTysN :: Int -> Kind -> ([Kind],Kind)
1538 splitKindFunTysN k = splitFunTysN k
1540 isUbxTupleKind, isOpenTypeKind, isArgTypeKind, isUnliftedTypeKind :: Kind -> Bool
1541 isOpenTypeKindCon, isUbxTupleKindCon, isArgTypeKindCon,
1542 isUnliftedTypeKindCon, isSubArgTypeKindCon :: TyCon -> Bool
1544 isOpenTypeKindCon tc = tyConUnique tc == openTypeKindTyConKey
1546 isOpenTypeKind (TyConApp tc _) = isOpenTypeKindCon tc
1547 isOpenTypeKind _ = False
1549 isUbxTupleKindCon tc = tyConUnique tc == ubxTupleKindTyConKey
1551 isUbxTupleKind (TyConApp tc _) = isUbxTupleKindCon tc
1552 isUbxTupleKind _ = False
1554 isArgTypeKindCon tc = tyConUnique tc == argTypeKindTyConKey
1556 isArgTypeKind (TyConApp tc _) = isArgTypeKindCon tc
1557 isArgTypeKind _ = False
1559 isUnliftedTypeKindCon tc = tyConUnique tc == unliftedTypeKindTyConKey
1561 isUnliftedTypeKind (TyConApp tc _) = isUnliftedTypeKindCon tc
1562 isUnliftedTypeKind _ = False
1564 isSubOpenTypeKind :: Kind -> Bool
1565 -- True of any sub-kind of OpenTypeKind (i.e. anything except arrow)
1566 isSubOpenTypeKind (FunTy k1 k2) = ASSERT2 ( isKind k1, text "isSubOpenTypeKind" <+> ppr k1 <+> text "::" <+> ppr (typeKind k1) )
1567 ASSERT2 ( isKind k2, text "isSubOpenTypeKind" <+> ppr k2 <+> text "::" <+> ppr (typeKind k2) )
1569 isSubOpenTypeKind (TyConApp kc []) = ASSERT( isKind (TyConApp kc []) ) True
1570 isSubOpenTypeKind other = ASSERT( isKind other ) False
1571 -- This is a conservative answer
1572 -- It matters in the call to isSubKind in
1573 -- checkExpectedKind.
1575 isSubArgTypeKindCon kc
1576 | isUnliftedTypeKindCon kc = True
1577 | isLiftedTypeKindCon kc = True
1578 | isArgTypeKindCon kc = True
1581 isSubArgTypeKind :: Kind -> Bool
1582 -- True of any sub-kind of ArgTypeKind
1583 isSubArgTypeKind (TyConApp kc []) = isSubArgTypeKindCon kc
1584 isSubArgTypeKind _ = False
1586 isSuperKind :: Type -> Bool
1587 isSuperKind (TyConApp (skc) []) = isSuperKindTyCon skc
1588 isSuperKind _ = False
1590 isKind :: Kind -> Bool
1591 isKind k = isSuperKind (typeKind k)
1593 isSubKind :: Kind -> Kind -> Bool
1594 -- (k1 `isSubKind` k2) checks that k1 <: k2
1595 isSubKind (TyConApp kc1 []) (TyConApp kc2 []) = kc1 `isSubKindCon` kc2
1596 isSubKind (FunTy a1 r1) (FunTy a2 r2) = (a2 `isSubKind` a1) && (r1 `isSubKind` r2)
1597 isSubKind (PredTy (EqPred ty1 ty2)) (PredTy (EqPred ty1' ty2'))
1598 = ty1 `tcEqType` ty1' && ty2 `tcEqType` ty2'
1599 isSubKind _ _ = False
1601 eqKind :: Kind -> Kind -> Bool
1604 isSubKindCon :: TyCon -> TyCon -> Bool
1605 -- (kc1 `isSubKindCon` kc2) checks that kc1 <: kc2
1606 isSubKindCon kc1 kc2
1607 | isLiftedTypeKindCon kc1 && isLiftedTypeKindCon kc2 = True
1608 | isUnliftedTypeKindCon kc1 && isUnliftedTypeKindCon kc2 = True
1609 | isUbxTupleKindCon kc1 && isUbxTupleKindCon kc2 = True
1610 | isOpenTypeKindCon kc2 = True
1611 -- we already know kc1 is not a fun, its a TyCon
1612 | isArgTypeKindCon kc2 && isSubArgTypeKindCon kc1 = True
1615 defaultKind :: Kind -> Kind
1616 -- Used when generalising: default kind '?' and '??' to '*'
1618 -- When we generalise, we make generic type variables whose kind is
1619 -- simple (* or *->* etc). So generic type variables (other than
1620 -- built-in constants like 'error') always have simple kinds. This is important;
1623 -- We want f to get type
1624 -- f :: forall (a::*). a -> Bool
1626 -- f :: forall (a::??). a -> Bool
1627 -- because that would allow a call like (f 3#) as well as (f True),
1628 --and the calling conventions differ. This defaulting is done in TcMType.zonkTcTyVarBndr.
1630 | isSubOpenTypeKind k = liftedTypeKind
1631 | isSubArgTypeKind k = liftedTypeKind
1634 isEqPred :: PredType -> Bool
1635 isEqPred (EqPred _ _) = True