2 % (c) The University of Glasgow 2006
3 % (c) The GRASP/AQUA Project, Glasgow University, 1998
6 Type - public interface
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, repType', typePrimRep, coreView, tcView, kindView,
60 mkForAllTy, mkForAllTys, splitForAllTy_maybe, splitForAllTys,
61 applyTy, applyTys, isForAllTy, dropForAlls,
64 predTypeRep, mkPredTy, mkPredTys, pprSourceTyCon, mkFamilyTyConApp,
70 isUnLiftedType, isUnboxedTupleType, isAlgType, isPrimitiveType,
71 isStrictType, isStrictPred,
74 tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta,
75 typeKind, addFreeTyVars,
77 -- Tidying up for printing
79 tidyOpenType, tidyOpenTypes,
80 tidyTyVarBndr, tidyFreeTyVars,
81 tidyOpenTyVar, tidyOpenTyVars,
82 tidyTopType, tidyPred,
86 coreEqType, tcEqType, tcEqTypes, tcCmpType, tcCmpTypes,
87 tcEqPred, tcCmpPred, tcEqTypeX,
93 TvSubstEnv, emptyTvSubstEnv, -- Representation widely visible
94 TvSubst(..), emptyTvSubst, -- Representation visible to a few friends
95 mkTvSubst, mkOpenTvSubst, zipOpenTvSubst, zipTopTvSubst, mkTopTvSubst, notElemTvSubst,
96 getTvSubstEnv, setTvSubstEnv, getTvInScope, extendTvInScope,
97 extendTvSubst, extendTvSubstList, isInScope, composeTvSubst, zipTyEnv,
100 -- Performing substitution on types
101 substTy, substTys, substTyWith, substTheta,
102 substPred, substTyVar, substTyVars, substTyVarBndr, deShadowTy, lookupTyVar,
105 pprType, pprParendType, pprTypeApp, pprTyThingCategory, pprForAll,
106 pprPred, pprTheta, pprThetaArrow, pprClassPred, pprKind, pprParendKind
109 #include "HsVersions.h"
111 -- We import the representation and primitive functions from TypeRep.
112 -- Many things are reexported, but not the representation!
133 import Data.Maybe ( isJust )
137 %************************************************************************
141 %************************************************************************
143 In Core, we "look through" non-recursive newtypes and PredTypes.
146 {-# INLINE coreView #-}
147 coreView :: Type -> Maybe Type
148 -- Strips off the *top layer only* of a type to give
149 -- its underlying representation type.
150 -- Returns Nothing if there is nothing to look through.
152 -- In the case of newtypes, it returns
153 -- *either* a vanilla TyConApp (recursive newtype, or non-saturated)
154 -- *or* the newtype representation (otherwise), meaning the
155 -- type written in the RHS of the newtype decl,
156 -- which may itself be a newtype
158 -- Example: newtype R = MkR S
160 -- newtype T = MkT (T -> T)
161 -- expandNewTcApp on R gives Just S
163 -- on T gives Nothing (no expansion)
165 -- By being non-recursive and inlined, this case analysis gets efficiently
166 -- joined onto the case analysis that the caller is already doing
167 coreView (NoteTy _ ty) = Just ty
169 | isEqPred p = Nothing
170 | otherwise = Just (predTypeRep p)
171 coreView (TyConApp tc tys) | Just (tenv, rhs, tys') <- coreExpandTyCon_maybe tc tys
172 = Just (mkAppTys (substTy (mkTopTvSubst tenv) rhs) tys')
173 -- Its important to use mkAppTys, rather than (foldl AppTy),
174 -- because the function part might well return a
175 -- partially-applied type constructor; indeed, usually will!
176 coreView ty = Nothing
180 -----------------------------------------------
181 {-# INLINE tcView #-}
182 tcView :: Type -> Maybe Type
183 -- Same, but for the type checker, which just looks through synonyms
184 tcView (NoteTy _ ty) = Just ty
185 tcView (TyConApp tc tys) | Just (tenv, rhs, tys') <- tcExpandTyCon_maybe tc tys
186 = Just (mkAppTys (substTy (mkTopTvSubst tenv) rhs) tys')
189 -----------------------------------------------
190 {-# INLINE kindView #-}
191 kindView :: Kind -> Maybe Kind
192 -- C.f. coreView, tcView
193 -- For the moment, we don't even handle synonyms in kinds
194 kindView (NoteTy _ k) = Just k
195 kindView other = Nothing
199 %************************************************************************
201 \subsection{Constructor-specific functions}
203 %************************************************************************
206 ---------------------------------------------------------------------
210 mkTyVarTy :: TyVar -> Type
213 mkTyVarTys :: [TyVar] -> [Type]
214 mkTyVarTys = map mkTyVarTy -- a common use of mkTyVarTy
216 getTyVar :: String -> Type -> TyVar
217 getTyVar msg ty = case getTyVar_maybe ty of
219 Nothing -> panic ("getTyVar: " ++ msg)
221 isTyVarTy :: Type -> Bool
222 isTyVarTy ty = isJust (getTyVar_maybe ty)
224 getTyVar_maybe :: Type -> Maybe TyVar
225 getTyVar_maybe ty | Just ty' <- coreView ty = getTyVar_maybe ty'
226 getTyVar_maybe (TyVarTy tv) = Just tv
227 getTyVar_maybe other = Nothing
232 ---------------------------------------------------------------------
235 We need to be pretty careful with AppTy to make sure we obey the
236 invariant that a TyConApp is always visibly so. mkAppTy maintains the
240 mkAppTy orig_ty1 orig_ty2
243 mk_app (NoteTy _ ty1) = mk_app ty1
244 mk_app (TyConApp tc tys) = mkTyConApp tc (tys ++ [orig_ty2])
245 mk_app ty1 = AppTy orig_ty1 orig_ty2
246 -- Note that the TyConApp could be an
247 -- under-saturated type synonym. GHC allows that; e.g.
248 -- type Foo k = k a -> k a
250 -- foo :: Foo Id -> Foo Id
252 -- Here Id is partially applied in the type sig for Foo,
253 -- but once the type synonyms are expanded all is well
255 mkAppTys :: Type -> [Type] -> Type
256 mkAppTys orig_ty1 [] = orig_ty1
257 -- This check for an empty list of type arguments
258 -- avoids the needless loss of a type synonym constructor.
259 -- For example: mkAppTys Rational []
260 -- returns to (Ratio Integer), which has needlessly lost
261 -- the Rational part.
262 mkAppTys orig_ty1 orig_tys2
265 mk_app (NoteTy _ ty1) = mk_app ty1
266 mk_app (TyConApp tc tys) = mkTyConApp tc (tys ++ orig_tys2)
267 -- mkTyConApp: see notes with mkAppTy
268 mk_app ty1 = foldl AppTy orig_ty1 orig_tys2
271 splitAppTy_maybe :: Type -> Maybe (Type, Type)
272 splitAppTy_maybe ty | Just ty' <- coreView ty
273 = splitAppTy_maybe ty'
274 splitAppTy_maybe ty = repSplitAppTy_maybe ty
277 repSplitAppTy_maybe :: Type -> Maybe (Type,Type)
278 -- Does the AppTy split, but assumes that any view stuff is already done
279 repSplitAppTy_maybe (FunTy ty1 ty2) = Just (TyConApp funTyCon [ty1], ty2)
280 repSplitAppTy_maybe (AppTy ty1 ty2) = Just (ty1, ty2)
281 repSplitAppTy_maybe (TyConApp tc tys) = case snocView tys of
282 Just (tys', ty') -> Just (TyConApp tc tys', ty')
284 repSplitAppTy_maybe other = Nothing
286 splitAppTy :: Type -> (Type, Type)
287 splitAppTy ty = case splitAppTy_maybe ty of
289 Nothing -> panic "splitAppTy"
292 splitAppTys :: Type -> (Type, [Type])
293 splitAppTys ty = split ty ty []
295 split orig_ty ty args | Just ty' <- coreView ty = split orig_ty ty' args
296 split orig_ty (AppTy ty arg) args = split ty ty (arg:args)
297 split orig_ty (TyConApp tc tc_args) args = (TyConApp tc [], tc_args ++ args)
298 split orig_ty (FunTy ty1 ty2) args = ASSERT( null args )
299 (TyConApp funTyCon [], [ty1,ty2])
300 split orig_ty ty args = (orig_ty, args)
305 ---------------------------------------------------------------------
310 mkFunTy :: Type -> Type -> Type
311 mkFunTy (PredTy (EqPred ty1 ty2)) res = mkForAllTy (mkWildCoVar (PredTy (EqPred ty1 ty2))) res
312 mkFunTy arg res = FunTy arg res
314 mkFunTys :: [Type] -> Type -> Type
315 mkFunTys tys ty = foldr mkFunTy ty tys
317 isFunTy :: Type -> Bool
318 isFunTy ty = isJust (splitFunTy_maybe ty)
320 splitFunTy :: Type -> (Type, Type)
321 splitFunTy ty | Just ty' <- coreView ty = splitFunTy ty'
322 splitFunTy (FunTy arg res) = (arg, res)
323 splitFunTy other = pprPanic "splitFunTy" (ppr other)
325 splitFunTy_maybe :: Type -> Maybe (Type, Type)
326 splitFunTy_maybe ty | Just ty' <- coreView ty = splitFunTy_maybe ty'
327 splitFunTy_maybe (FunTy arg res) = Just (arg, res)
328 splitFunTy_maybe other = Nothing
330 splitFunTys :: Type -> ([Type], Type)
331 splitFunTys ty = split [] ty ty
333 split args orig_ty ty | Just ty' <- coreView ty = split args orig_ty ty'
334 split args orig_ty (FunTy arg res) = split (arg:args) res res
335 split args orig_ty ty = (reverse args, orig_ty)
337 splitFunTysN :: Int -> Type -> ([Type], Type)
338 -- Split off exactly n arg tys
339 splitFunTysN 0 ty = ([], ty)
340 splitFunTysN n ty = case splitFunTy ty of { (arg, res) ->
341 case splitFunTysN (n-1) res of { (args, res) ->
344 zipFunTys :: Outputable a => [a] -> Type -> ([(a,Type)], Type)
345 zipFunTys orig_xs orig_ty = split [] orig_xs orig_ty orig_ty
347 split acc [] nty ty = (reverse acc, nty)
349 | Just ty' <- coreView ty = split acc xs nty ty'
350 split acc (x:xs) nty (FunTy arg res) = split ((x,arg):acc) xs res res
351 split acc (x:xs) nty ty = pprPanic "zipFunTys" (ppr orig_xs <+> ppr orig_ty)
353 funResultTy :: Type -> Type
354 funResultTy ty | Just ty' <- coreView ty = funResultTy ty'
355 funResultTy (FunTy arg res) = res
356 funResultTy ty = pprPanic "funResultTy" (ppr ty)
358 funArgTy :: Type -> Type
359 funArgTy ty | Just ty' <- coreView ty = funArgTy ty'
360 funArgTy (FunTy arg res) = arg
361 funArgTy ty = pprPanic "funArgTy" (ppr ty)
365 ---------------------------------------------------------------------
368 @mkTyConApp@ is a key function, because it builds a TyConApp, FunTy or PredTy,
372 mkTyConApp :: TyCon -> [Type] -> Type
374 | isFunTyCon tycon, [ty1,ty2] <- tys
380 mkTyConTy :: TyCon -> Type
381 mkTyConTy tycon = mkTyConApp tycon []
383 -- splitTyConApp "looks through" synonyms, because they don't
384 -- mean a distinct type, but all other type-constructor applications
385 -- including functions are returned as Just ..
387 tyConAppTyCon :: Type -> TyCon
388 tyConAppTyCon ty = fst (splitTyConApp ty)
390 tyConAppArgs :: Type -> [Type]
391 tyConAppArgs ty = snd (splitTyConApp ty)
393 splitTyConApp :: Type -> (TyCon, [Type])
394 splitTyConApp ty = case splitTyConApp_maybe ty of
396 Nothing -> pprPanic "splitTyConApp" (ppr ty)
398 splitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
399 splitTyConApp_maybe ty | Just ty' <- coreView ty = splitTyConApp_maybe ty'
400 splitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
401 splitTyConApp_maybe (FunTy arg res) = Just (funTyCon, [arg,res])
402 splitTyConApp_maybe other = Nothing
404 -- Sometimes we do NOT want to look throught a newtype. When case matching
405 -- on a newtype we want a convenient way to access the arguments of a newty
406 -- constructor so as to properly form a coercion.
407 splitNewTyConApp :: Type -> (TyCon, [Type])
408 splitNewTyConApp ty = case splitNewTyConApp_maybe ty of
410 Nothing -> pprPanic "splitNewTyConApp" (ppr ty)
411 splitNewTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
412 splitNewTyConApp_maybe ty | Just ty' <- tcView ty = splitNewTyConApp_maybe ty'
413 splitNewTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
414 splitNewTyConApp_maybe (FunTy arg res) = Just (funTyCon, [arg,res])
415 splitNewTyConApp_maybe other = Nothing
417 newTyConInstRhs :: TyCon -> [Type] -> Type
418 -- Unwrap one 'layer' of newtype
419 -- Use the eta'd version if possible
420 newTyConInstRhs tycon tys
421 = ASSERT2( equalLength tvs tys1, ppr tycon $$ ppr tys $$ ppr tvs )
422 mkAppTys (substTyWith tvs tys1 ty) tys2
424 (tvs, ty) = newTyConEtadRhs tycon
425 (tys1, tys2) = splitAtList tvs tys
429 ---------------------------------------------------------------------
433 Notes on type synonyms
434 ~~~~~~~~~~~~~~~~~~~~~~
435 The various "split" functions (splitFunTy, splitRhoTy, splitForAllTy) try
436 to return type synonyms whereever possible. Thus
441 splitFunTys (a -> Foo a) = ([a], Foo a)
444 The reason is that we then get better (shorter) type signatures in
445 interfaces. Notably this plays a role in tcTySigs in TcBinds.lhs.
450 repType looks through
454 (d) usage annotations
455 (e) all newtypes, including recursive ones, but not newtype families
456 It's useful in the back end.
459 repType :: Type -> Type
460 -- Only applied to types of kind *; hence tycons are saturated
461 repType ty | Just ty' <- coreView ty = repType ty'
462 repType (ForAllTy _ ty) = repType ty
463 repType (TyConApp tc tys)
465 , (tvs, rep_ty) <- newTyConRep tc
466 = -- Recursive newtypes are opaque to coreView
467 -- but we must expand them here. Sure to
468 -- be saturated because repType is only applied
469 -- to types of kind *
470 ASSERT( tys `lengthIs` tyConArity tc )
471 repType (substTyWith tvs tys rep_ty)
475 -- repType' aims to be a more thorough version of repType
476 -- For now it simply looks through the TyConApp args too
477 repType' ty -- | pprTrace "repType'" (ppr ty $$ ppr (go1 ty)) False = undefined
481 go (TyConApp tc tys) = mkTyConApp tc (map repType' tys)
485 -- ToDo: this could be moved to the code generator, using splitTyConApp instead
486 -- of inspecting the type directly.
487 typePrimRep :: Type -> PrimRep
488 typePrimRep ty = case repType ty of
489 TyConApp tc _ -> tyConPrimRep tc
491 AppTy _ _ -> PtrRep -- See note below
493 other -> pprPanic "typePrimRep" (ppr ty)
494 -- Types of the form 'f a' must be of kind *, not *#, so
495 -- we are guaranteed that they are represented by pointers.
496 -- The reason is that f must have kind *->*, not *->*#, because
497 -- (we claim) there is no way to constrain f's kind any other
502 ---------------------------------------------------------------------
507 mkForAllTy :: TyVar -> Type -> Type
509 = mkForAllTys [tyvar] ty
511 mkForAllTys :: [TyVar] -> Type -> Type
512 mkForAllTys tyvars ty = foldr ForAllTy ty tyvars
514 isForAllTy :: Type -> Bool
515 isForAllTy (NoteTy _ ty) = isForAllTy ty
516 isForAllTy (ForAllTy _ _) = True
517 isForAllTy other_ty = False
519 splitForAllTy_maybe :: Type -> Maybe (TyVar, Type)
520 splitForAllTy_maybe ty = splitFAT_m ty
522 splitFAT_m ty | Just ty' <- coreView ty = splitFAT_m ty'
523 splitFAT_m (ForAllTy tyvar ty) = Just(tyvar, ty)
524 splitFAT_m _ = Nothing
526 splitForAllTys :: Type -> ([TyVar], Type)
527 splitForAllTys ty = split ty ty []
529 split orig_ty ty tvs | Just ty' <- coreView ty = split orig_ty ty' tvs
530 split orig_ty (ForAllTy tv ty) tvs = split ty ty (tv:tvs)
531 split orig_ty t tvs = (reverse tvs, orig_ty)
533 dropForAlls :: Type -> Type
534 dropForAlls ty = snd (splitForAllTys ty)
537 -- (mkPiType now in CoreUtils)
541 Instantiate a for-all type with one or more type arguments.
542 Used when we have a polymorphic function applied to type args:
544 Then we use (applyTys type-of-f [t1,t2]) to compute the type of
548 applyTy :: Type -> Type -> Type
549 applyTy ty arg | Just ty' <- coreView ty = applyTy ty' arg
550 applyTy (ForAllTy tv ty) arg = substTyWith [tv] [arg] ty
551 applyTy other arg = panic "applyTy"
553 applyTys :: Type -> [Type] -> Type
554 -- This function is interesting because
555 -- a) the function may have more for-alls than there are args
556 -- b) less obviously, it may have fewer for-alls
557 -- For case (b) think of
558 -- applyTys (forall a.a) [forall b.b, Int]
559 -- This really can happen, via dressing up polymorphic types with newtype
560 -- clothing. Here's an example:
561 -- newtype R = R (forall a. a->a)
562 -- foo = case undefined :: R of
565 applyTys orig_fun_ty [] = orig_fun_ty
566 applyTys orig_fun_ty arg_tys
567 | n_tvs == n_args -- The vastly common case
568 = substTyWith tvs arg_tys rho_ty
569 | n_tvs > n_args -- Too many for-alls
570 = substTyWith (take n_args tvs) arg_tys
571 (mkForAllTys (drop n_args tvs) rho_ty)
572 | otherwise -- Too many type args
573 = ASSERT2( n_tvs > 0, ppr orig_fun_ty ) -- Zero case gives infnite loop!
574 applyTys (substTyWith tvs (take n_tvs arg_tys) rho_ty)
577 (tvs, rho_ty) = splitForAllTys orig_fun_ty
579 n_args = length arg_tys
583 %************************************************************************
585 \subsection{Source types}
587 %************************************************************************
589 A "source type" is a type that is a separate type as far as the type checker is
590 concerned, but which has low-level representation as far as the back end is concerned.
592 Source types are always lifted.
594 The key function is predTypeRep which gives the representation of a source type:
597 mkPredTy :: PredType -> Type
598 mkPredTy pred = PredTy pred
600 mkPredTys :: ThetaType -> [Type]
601 mkPredTys preds = map PredTy preds
603 predTypeRep :: PredType -> Type
604 -- Convert a PredType to its "representation type";
605 -- the post-type-checking type used by all the Core passes of GHC.
606 -- Unwraps only the outermost level; for example, the result might
607 -- be a newtype application
608 predTypeRep (IParam _ ty) = ty
609 predTypeRep (ClassP clas tys) = mkTyConApp (classTyCon clas) tys
610 -- Result might be a newtype application, but the consumer will
611 -- look through that too if necessary
612 predTypeRep (EqPred ty1 ty2) = pprPanic "predTypeRep" (ppr (EqPred ty1 ty2))
614 mkFamilyTyConApp :: TyCon -> [Type] -> Type
615 -- Given a family instance TyCon and its arg types, return the
616 -- corresponding family type. E.g.
618 -- data instance T (Maybe b) = MkT b -- Instance tycon :RTL
620 -- mkFamilyTyConApp :RTL Int = T (Maybe Int)
621 mkFamilyTyConApp tc tys
622 | Just (fam_tc, fam_tys) <- tyConFamInst_maybe tc
623 , let fam_subst = zipTopTvSubst (tyConTyVars tc) tys
624 = mkTyConApp fam_tc (substTys fam_subst fam_tys)
628 -- Pretty prints a tycon, using the family instance in case of a
629 -- representation tycon. For example
630 -- e.g. data T [a] = ...
631 -- In that case we want to print `T [a]', where T is the family TyCon
633 | Just (fam_tc, tys) <- tyConFamInst_maybe tycon
634 = ppr $ fam_tc `TyConApp` tys -- can't be FunTyCon
640 %************************************************************************
642 \subsection{Kinds and free variables}
644 %************************************************************************
646 ---------------------------------------------------------------------
647 Finding the kind of a type
648 ~~~~~~~~~~~~~~~~~~~~~~~~~~
650 typeKind :: Type -> Kind
651 typeKind (TyConApp tycon tys) = ASSERT( not (isCoercionTyCon tycon) )
652 -- We should be looking for the coercion kind,
654 foldr (\_ k -> kindFunResult k) (tyConKind tycon) tys
655 typeKind (NoteTy _ ty) = typeKind ty
656 typeKind (PredTy pred) = predKind pred
657 typeKind (AppTy fun arg) = kindFunResult (typeKind fun)
658 typeKind (ForAllTy tv ty) = typeKind ty
659 typeKind (TyVarTy tyvar) = tyVarKind tyvar
660 typeKind (FunTy arg res)
661 -- Hack alert. The kind of (Int -> Int#) is liftedTypeKind (*),
662 -- not unliftedTypKind (#)
663 -- The only things that can be after a function arrow are
664 -- (a) types (of kind openTypeKind or its sub-kinds)
665 -- (b) kinds (of super-kind TY) (e.g. * -> (* -> *))
666 | isTySuperKind k = k
667 | otherwise = ASSERT( isSubOpenTypeKind k) liftedTypeKind
671 predKind :: PredType -> Kind
672 predKind (EqPred {}) = coSuperKind -- A coercion kind!
673 predKind (ClassP {}) = liftedTypeKind -- Class and implicitPredicates are
674 predKind (IParam {}) = liftedTypeKind -- always represented by lifted types
678 ---------------------------------------------------------------------
679 Free variables of a type
680 ~~~~~~~~~~~~~~~~~~~~~~~~
682 tyVarsOfType :: Type -> TyVarSet
683 -- NB: for type synonyms tyVarsOfType does *not* expand the synonym
684 tyVarsOfType (TyVarTy tv) = unitVarSet tv
685 tyVarsOfType (TyConApp tycon tys) = tyVarsOfTypes tys
686 tyVarsOfType (NoteTy (FTVNote tvs) ty2) = tvs
687 tyVarsOfType (PredTy sty) = tyVarsOfPred sty
688 tyVarsOfType (FunTy arg res) = tyVarsOfType arg `unionVarSet` tyVarsOfType res
689 tyVarsOfType (AppTy fun arg) = tyVarsOfType fun `unionVarSet` tyVarsOfType arg
690 tyVarsOfType (ForAllTy tyvar ty) = delVarSet (tyVarsOfType ty) tyvar
692 tyVarsOfTypes :: [Type] -> TyVarSet
693 tyVarsOfTypes tys = foldr (unionVarSet.tyVarsOfType) emptyVarSet tys
695 tyVarsOfPred :: PredType -> TyVarSet
696 tyVarsOfPred (IParam _ ty) = tyVarsOfType ty
697 tyVarsOfPred (ClassP _ tys) = tyVarsOfTypes tys
698 tyVarsOfPred (EqPred ty1 ty2) = tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2
700 tyVarsOfTheta :: ThetaType -> TyVarSet
701 tyVarsOfTheta = foldr (unionVarSet . tyVarsOfPred) emptyVarSet
703 -- Add a Note with the free tyvars to the top of the type
704 addFreeTyVars :: Type -> Type
705 addFreeTyVars ty@(NoteTy (FTVNote _) _) = ty
706 addFreeTyVars ty = NoteTy (FTVNote (tyVarsOfType ty)) ty
710 %************************************************************************
712 \subsection{TidyType}
714 %************************************************************************
716 tidyTy tidies up a type for printing in an error message, or in
719 It doesn't change the uniques at all, just the print names.
722 tidyTyVarBndr :: TidyEnv -> TyVar -> (TidyEnv, TyVar)
723 tidyTyVarBndr env@(tidy_env, subst) tyvar
724 = case tidyOccName tidy_env (getOccName name) of
725 (tidy', occ') -> ((tidy', subst'), tyvar'')
727 subst' = extendVarEnv subst tyvar tyvar''
728 tyvar' = setTyVarName tyvar name'
729 name' = tidyNameOcc name occ'
730 -- Don't forget to tidy the kind for coercions!
731 tyvar'' | isCoVar tyvar = setTyVarKind tyvar' kind'
733 kind' = tidyType env (tyVarKind tyvar)
735 name = tyVarName tyvar
737 tidyFreeTyVars :: TidyEnv -> TyVarSet -> TidyEnv
738 -- Add the free tyvars to the env in tidy form,
739 -- so that we can tidy the type they are free in
740 tidyFreeTyVars env tyvars = fst (tidyOpenTyVars env (varSetElems tyvars))
742 tidyOpenTyVars :: TidyEnv -> [TyVar] -> (TidyEnv, [TyVar])
743 tidyOpenTyVars env tyvars = mapAccumL tidyOpenTyVar env tyvars
745 tidyOpenTyVar :: TidyEnv -> TyVar -> (TidyEnv, TyVar)
746 -- Treat a new tyvar as a binder, and give it a fresh tidy name
747 tidyOpenTyVar env@(tidy_env, subst) tyvar
748 = case lookupVarEnv subst tyvar of
749 Just tyvar' -> (env, tyvar') -- Already substituted
750 Nothing -> tidyTyVarBndr env tyvar -- Treat it as a binder
752 tidyType :: TidyEnv -> Type -> Type
753 tidyType env@(tidy_env, subst) ty
756 go (TyVarTy tv) = case lookupVarEnv subst tv of
757 Nothing -> TyVarTy tv
758 Just tv' -> TyVarTy tv'
759 go (TyConApp tycon tys) = let args = map go tys
760 in args `seqList` TyConApp tycon args
761 go (NoteTy note ty) = (NoteTy $! (go_note note)) $! (go ty)
762 go (PredTy sty) = PredTy (tidyPred env sty)
763 go (AppTy fun arg) = (AppTy $! (go fun)) $! (go arg)
764 go (FunTy fun arg) = (FunTy $! (go fun)) $! (go arg)
765 go (ForAllTy tv ty) = ForAllTy tvp $! (tidyType envp ty)
767 (envp, tvp) = tidyTyVarBndr env tv
769 go_note note@(FTVNote ftvs) = note -- No need to tidy the free tyvars
771 tidyTypes env tys = map (tidyType env) tys
773 tidyPred :: TidyEnv -> PredType -> PredType
774 tidyPred env (IParam n ty) = IParam n (tidyType env ty)
775 tidyPred env (ClassP clas tys) = ClassP clas (tidyTypes env tys)
776 tidyPred env (EqPred ty1 ty2) = EqPred (tidyType env ty1) (tidyType env ty2)
780 @tidyOpenType@ grabs the free type variables, tidies them
781 and then uses @tidyType@ to work over the type itself
784 tidyOpenType :: TidyEnv -> Type -> (TidyEnv, Type)
786 = (env', tidyType env' ty)
788 env' = tidyFreeTyVars env (tyVarsOfType ty)
790 tidyOpenTypes :: TidyEnv -> [Type] -> (TidyEnv, [Type])
791 tidyOpenTypes env tys = mapAccumL tidyOpenType env tys
793 tidyTopType :: Type -> Type
794 tidyTopType ty = tidyType emptyTidyEnv ty
799 tidyKind :: TidyEnv -> Kind -> (TidyEnv, Kind)
800 tidyKind env k = tidyOpenType env k
805 %************************************************************************
807 \subsection{Liftedness}
809 %************************************************************************
812 isUnLiftedType :: Type -> Bool
813 -- isUnLiftedType returns True for forall'd unlifted types:
814 -- x :: forall a. Int#
815 -- I found bindings like these were getting floated to the top level.
816 -- They are pretty bogus types, mind you. It would be better never to
819 isUnLiftedType ty | Just ty' <- coreView ty = isUnLiftedType ty'
820 isUnLiftedType (ForAllTy tv ty) = isUnLiftedType ty
821 isUnLiftedType (TyConApp tc _) = isUnLiftedTyCon tc
822 isUnLiftedType other = False
824 isUnboxedTupleType :: Type -> Bool
825 isUnboxedTupleType ty = case splitTyConApp_maybe ty of
826 Just (tc, ty_args) -> isUnboxedTupleTyCon tc
829 -- Should only be applied to *types*; hence the assert
830 isAlgType :: Type -> Bool
831 isAlgType ty = case splitTyConApp_maybe ty of
832 Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
837 @isStrictType@ computes whether an argument (or let RHS) should
838 be computed strictly or lazily, based only on its type.
839 Works just like isUnLiftedType, except that it has a special case
840 for dictionaries. Since it takes account of ClassP, you might think
841 this function should be in TcType, but isStrictType is used by DataCon,
842 which is below TcType in the hierarchy, so it's convenient to put it here.
845 isStrictType (PredTy pred) = isStrictPred pred
846 isStrictType ty | Just ty' <- coreView ty = isStrictType ty'
847 isStrictType (ForAllTy tv ty) = isStrictType ty
848 isStrictType (TyConApp tc _) = isUnLiftedTyCon tc
849 isStrictType other = False
851 isStrictPred (ClassP clas _) = opt_DictsStrict && not (isNewTyCon (classTyCon clas))
852 isStrictPred other = False
853 -- We may be strict in dictionary types, but only if it
854 -- has more than one component.
855 -- [Being strict in a single-component dictionary risks
856 -- poking the dictionary component, which is wrong.]
860 isPrimitiveType :: Type -> Bool
861 -- Returns types that are opaque to Haskell.
862 -- Most of these are unlifted, but now that we interact with .NET, we
863 -- may have primtive (foreign-imported) types that are lifted
864 isPrimitiveType ty = case splitTyConApp_maybe ty of
865 Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
871 %************************************************************************
873 \subsection{Sequencing on types
875 %************************************************************************
878 seqType :: Type -> ()
879 seqType (TyVarTy tv) = tv `seq` ()
880 seqType (AppTy t1 t2) = seqType t1 `seq` seqType t2
881 seqType (FunTy t1 t2) = seqType t1 `seq` seqType t2
882 seqType (NoteTy note t2) = seqNote note `seq` seqType t2
883 seqType (PredTy p) = seqPred p
884 seqType (TyConApp tc tys) = tc `seq` seqTypes tys
885 seqType (ForAllTy tv ty) = tv `seq` seqType ty
887 seqTypes :: [Type] -> ()
889 seqTypes (ty:tys) = seqType ty `seq` seqTypes tys
891 seqNote :: TyNote -> ()
892 seqNote (FTVNote set) = sizeUniqSet set `seq` ()
894 seqPred :: PredType -> ()
895 seqPred (ClassP c tys) = c `seq` seqTypes tys
896 seqPred (IParam n ty) = n `seq` seqType ty
897 seqPred (EqPred ty1 ty2) = seqType ty1 `seq` seqType ty2
901 %************************************************************************
903 Equality for Core types
904 (We don't use instances so that we know where it happens)
906 %************************************************************************
908 Note that eqType works right even for partial applications of newtypes.
909 See Note [Newtype eta] in TyCon.lhs
912 coreEqType :: Type -> Type -> Bool
916 rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfType t1 `unionVarSet` tyVarsOfType t2))
918 eq env (TyVarTy tv1) (TyVarTy tv2) = rnOccL env tv1 == rnOccR env tv2
919 eq env (ForAllTy tv1 t1) (ForAllTy tv2 t2) = eq (rnBndr2 env tv1 tv2) t1 t2
920 eq env (AppTy s1 t1) (AppTy s2 t2) = eq env s1 s2 && eq env t1 t2
921 eq env (FunTy s1 t1) (FunTy s2 t2) = eq env s1 s2 && eq env t1 t2
922 eq env (TyConApp tc1 tys1) (TyConApp tc2 tys2)
923 | tc1 == tc2, all2 (eq env) tys1 tys2 = True
924 -- The lengths should be equal because
925 -- the two types have the same kind
926 -- NB: if the type constructors differ that does not
927 -- necessarily mean that the types aren't equal
928 -- (synonyms, newtypes)
929 -- Even if the type constructors are the same, but the arguments
930 -- differ, the two types could be the same (e.g. if the arg is just
931 -- ignored in the RHS). In both these cases we fall through to an
932 -- attempt to expand one side or the other.
934 -- Now deal with newtypes, synonyms, pred-tys
935 eq env t1 t2 | Just t1' <- coreView t1 = eq env t1' t2
936 | Just t2' <- coreView t2 = eq env t1 t2'
938 -- Fall through case; not equal!
943 %************************************************************************
945 Comparision for source types
946 (We don't use instances so that we know where it happens)
948 %************************************************************************
952 do *not* look through newtypes, PredTypes
955 tcEqType :: Type -> Type -> Bool
956 tcEqType t1 t2 = isEqual $ cmpType t1 t2
958 tcEqTypes :: [Type] -> [Type] -> Bool
959 tcEqTypes tys1 tys2 = isEqual $ cmpTypes tys1 tys2
961 tcCmpType :: Type -> Type -> Ordering
962 tcCmpType t1 t2 = cmpType t1 t2
964 tcCmpTypes :: [Type] -> [Type] -> Ordering
965 tcCmpTypes tys1 tys2 = cmpTypes tys1 tys2
967 tcEqPred :: PredType -> PredType -> Bool
968 tcEqPred p1 p2 = isEqual $ cmpPred p1 p2
970 tcCmpPred :: PredType -> PredType -> Ordering
971 tcCmpPred p1 p2 = cmpPred p1 p2
973 tcEqTypeX :: RnEnv2 -> Type -> Type -> Bool
974 tcEqTypeX env t1 t2 = isEqual $ cmpTypeX env t1 t2
977 Now here comes the real worker
980 cmpType :: Type -> Type -> Ordering
981 cmpType t1 t2 = cmpTypeX rn_env t1 t2
983 rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfType t1 `unionVarSet` tyVarsOfType t2))
985 cmpTypes :: [Type] -> [Type] -> Ordering
986 cmpTypes ts1 ts2 = cmpTypesX rn_env ts1 ts2
988 rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfTypes ts1 `unionVarSet` tyVarsOfTypes ts2))
990 cmpPred :: PredType -> PredType -> Ordering
991 cmpPred p1 p2 = cmpPredX rn_env p1 p2
993 rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfPred p1 `unionVarSet` tyVarsOfPred p2))
995 cmpTypeX :: RnEnv2 -> Type -> Type -> Ordering -- Main workhorse
996 cmpTypeX env t1 t2 | Just t1' <- tcView t1 = cmpTypeX env t1' t2
997 | Just t2' <- tcView t2 = cmpTypeX env t1 t2'
999 cmpTypeX env (TyVarTy tv1) (TyVarTy tv2) = rnOccL env tv1 `compare` rnOccR env tv2
1000 cmpTypeX env (ForAllTy tv1 t1) (ForAllTy tv2 t2) = cmpTypeX (rnBndr2 env tv1 tv2) t1 t2
1001 cmpTypeX env (AppTy s1 t1) (AppTy s2 t2) = cmpTypeX env s1 s2 `thenCmp` cmpTypeX env t1 t2
1002 cmpTypeX env (FunTy s1 t1) (FunTy s2 t2) = cmpTypeX env s1 s2 `thenCmp` cmpTypeX env t1 t2
1003 cmpTypeX env (PredTy p1) (PredTy p2) = cmpPredX env p1 p2
1004 cmpTypeX env (TyConApp tc1 tys1) (TyConApp tc2 tys2) = (tc1 `compare` tc2) `thenCmp` cmpTypesX env tys1 tys2
1005 cmpTypeX env t1 (NoteTy _ t2) = cmpTypeX env t1 t2
1007 -- Deal with the rest: TyVarTy < AppTy < FunTy < TyConApp < ForAllTy < PredTy
1008 cmpTypeX env (AppTy _ _) (TyVarTy _) = GT
1010 cmpTypeX env (FunTy _ _) (TyVarTy _) = GT
1011 cmpTypeX env (FunTy _ _) (AppTy _ _) = GT
1013 cmpTypeX env (TyConApp _ _) (TyVarTy _) = GT
1014 cmpTypeX env (TyConApp _ _) (AppTy _ _) = GT
1015 cmpTypeX env (TyConApp _ _) (FunTy _ _) = GT
1017 cmpTypeX env (ForAllTy _ _) (TyVarTy _) = GT
1018 cmpTypeX env (ForAllTy _ _) (AppTy _ _) = GT
1019 cmpTypeX env (ForAllTy _ _) (FunTy _ _) = GT
1020 cmpTypeX env (ForAllTy _ _) (TyConApp _ _) = GT
1022 cmpTypeX env (PredTy _) t2 = GT
1024 cmpTypeX env _ _ = LT
1027 cmpTypesX :: RnEnv2 -> [Type] -> [Type] -> Ordering
1028 cmpTypesX env [] [] = EQ
1029 cmpTypesX env (t1:tys1) (t2:tys2) = cmpTypeX env t1 t2 `thenCmp` cmpTypesX env tys1 tys2
1030 cmpTypesX env [] tys = LT
1031 cmpTypesX env ty [] = GT
1034 cmpPredX :: RnEnv2 -> PredType -> PredType -> Ordering
1035 cmpPredX env (IParam n1 ty1) (IParam n2 ty2) = (n1 `compare` n2) `thenCmp` cmpTypeX env ty1 ty2
1036 -- Compare names only for implicit parameters
1037 -- This comparison is used exclusively (I believe)
1038 -- for the Avails finite map built in TcSimplify
1039 -- If the types differ we keep them distinct so that we see
1040 -- a distinct pair to run improvement on
1041 cmpPredX env (ClassP c1 tys1) (ClassP c2 tys2) = (c1 `compare` c2) `thenCmp` (cmpTypesX env tys1 tys2)
1042 cmpPredX env (EqPred ty1 ty2) (EqPred ty1' ty2') = (cmpTypeX env ty1 ty1') `thenCmp` (cmpTypeX env ty2 ty2')
1044 -- Constructor order: IParam < ClassP < EqPred
1045 cmpPredX env (IParam {}) _ = LT
1046 cmpPredX env (ClassP {}) (IParam {}) = GT
1047 cmpPredX env (ClassP {}) (EqPred {}) = LT
1048 cmpPredX env (EqPred {}) _ = GT
1051 PredTypes are used as a FM key in TcSimplify,
1052 so we take the easy path and make them an instance of Ord
1055 instance Eq PredType where { (==) = tcEqPred }
1056 instance Ord PredType where { compare = tcCmpPred }
1060 %************************************************************************
1064 %************************************************************************
1068 = TvSubst InScopeSet -- The in-scope type variables
1069 TvSubstEnv -- The substitution itself
1070 -- See Note [Apply Once]
1071 -- and Note [Extending the TvSubstEnv]
1073 {- ----------------------------------------------------------
1077 We use TvSubsts to instantiate things, and we might instantiate
1081 So the substition might go [a->b, b->a]. A similar situation arises in Core
1082 when we find a beta redex like
1083 (/\ a /\ b -> e) b a
1084 Then we also end up with a substition that permutes type variables. Other
1085 variations happen to; for example [a -> (a, b)].
1087 ***************************************************
1088 *** So a TvSubst must be applied precisely once ***
1089 ***************************************************
1091 A TvSubst is not idempotent, but, unlike the non-idempotent substitution
1092 we use during unifications, it must not be repeatedly applied.
1094 Note [Extending the TvSubst]
1095 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1096 The following invariant should hold of a TvSubst
1098 The in-scope set is needed *only* to
1099 guide the generation of fresh uniques
1101 In particular, the *kind* of the type variables in
1102 the in-scope set is not relevant
1104 This invariant allows a short-cut when the TvSubstEnv is empty:
1105 if the TvSubstEnv is empty --- i.e. (isEmptyTvSubt subst) holds ---
1106 then (substTy subst ty) does nothing.
1108 For example, consider:
1109 (/\a. /\b:(a~Int). ...b..) Int
1110 We substitute Int for 'a'. The Unique of 'b' does not change, but
1111 nevertheless we add 'b' to the TvSubstEnv, because b's type does change
1113 This invariant has several crucial consequences:
1115 * In substTyVarBndr, we need extend the TvSubstEnv
1116 - if the unique has changed
1117 - or if the kind has changed
1119 * In substTyVar, we do not need to consult the in-scope set;
1120 the TvSubstEnv is enough
1122 * In substTy, substTheta, we can short-circuit when the TvSubstEnv is empty
1125 -------------------------------------------------------------- -}
1128 type TvSubstEnv = TyVarEnv Type
1129 -- A TvSubstEnv is used both inside a TvSubst (with the apply-once
1130 -- invariant discussed in Note [Apply Once]), and also independently
1131 -- in the middle of matching, and unification (see Types.Unify)
1132 -- So you have to look at the context to know if it's idempotent or
1133 -- apply-once or whatever
1134 emptyTvSubstEnv :: TvSubstEnv
1135 emptyTvSubstEnv = emptyVarEnv
1137 composeTvSubst :: InScopeSet -> TvSubstEnv -> TvSubstEnv -> TvSubstEnv
1138 -- (compose env1 env2)(x) is env1(env2(x)); i.e. apply env2 then env1
1139 -- It assumes that both are idempotent
1140 -- Typically, env1 is the refinement to a base substitution env2
1141 composeTvSubst in_scope env1 env2
1142 = env1 `plusVarEnv` mapVarEnv (substTy subst1) env2
1143 -- First apply env1 to the range of env2
1144 -- Then combine the two, making sure that env1 loses if
1145 -- both bind the same variable; that's why env1 is the
1146 -- *left* argument to plusVarEnv, because the right arg wins
1148 subst1 = TvSubst in_scope env1
1150 emptyTvSubst = TvSubst emptyInScopeSet emptyVarEnv
1152 isEmptyTvSubst :: TvSubst -> Bool
1153 -- See Note [Extending the TvSubstEnv]
1154 isEmptyTvSubst (TvSubst _ env) = isEmptyVarEnv env
1156 mkTvSubst :: InScopeSet -> TvSubstEnv -> TvSubst
1159 getTvSubstEnv :: TvSubst -> TvSubstEnv
1160 getTvSubstEnv (TvSubst _ env) = env
1162 getTvInScope :: TvSubst -> InScopeSet
1163 getTvInScope (TvSubst in_scope _) = in_scope
1165 isInScope :: Var -> TvSubst -> Bool
1166 isInScope v (TvSubst in_scope _) = v `elemInScopeSet` in_scope
1168 notElemTvSubst :: TyVar -> TvSubst -> Bool
1169 notElemTvSubst tv (TvSubst _ env) = not (tv `elemVarEnv` env)
1171 setTvSubstEnv :: TvSubst -> TvSubstEnv -> TvSubst
1172 setTvSubstEnv (TvSubst in_scope _) env = TvSubst in_scope env
1174 extendTvInScope :: TvSubst -> [Var] -> TvSubst
1175 extendTvInScope (TvSubst in_scope env) vars = TvSubst (extendInScopeSetList in_scope vars) env
1177 extendTvSubst :: TvSubst -> TyVar -> Type -> TvSubst
1178 extendTvSubst (TvSubst in_scope env) tv ty = TvSubst in_scope (extendVarEnv env tv ty)
1180 extendTvSubstList :: TvSubst -> [TyVar] -> [Type] -> TvSubst
1181 extendTvSubstList (TvSubst in_scope env) tvs tys
1182 = TvSubst in_scope (extendVarEnvList env (tvs `zip` tys))
1184 -- mkOpenTvSubst and zipOpenTvSubst generate the in-scope set from
1185 -- the types given; but it's just a thunk so with a bit of luck
1186 -- it'll never be evaluated
1188 mkOpenTvSubst :: TvSubstEnv -> TvSubst
1189 mkOpenTvSubst env = TvSubst (mkInScopeSet (tyVarsOfTypes (varEnvElts env))) env
1191 zipOpenTvSubst :: [TyVar] -> [Type] -> TvSubst
1192 zipOpenTvSubst tyvars tys
1194 | length tyvars /= length tys
1195 = pprTrace "zipOpenTvSubst" (ppr tyvars $$ ppr tys) emptyTvSubst
1198 = TvSubst (mkInScopeSet (tyVarsOfTypes tys)) (zipTyEnv tyvars tys)
1200 -- mkTopTvSubst is called when doing top-level substitutions.
1201 -- Here we expect that the free vars of the range of the
1202 -- substitution will be empty.
1203 mkTopTvSubst :: [(TyVar, Type)] -> TvSubst
1204 mkTopTvSubst prs = TvSubst emptyInScopeSet (mkVarEnv prs)
1206 zipTopTvSubst :: [TyVar] -> [Type] -> TvSubst
1207 zipTopTvSubst tyvars tys
1209 | length tyvars /= length tys
1210 = pprTrace "zipTopTvSubst" (ppr tyvars $$ ppr tys) emptyTvSubst
1213 = TvSubst emptyInScopeSet (zipTyEnv tyvars tys)
1215 zipTyEnv :: [TyVar] -> [Type] -> TvSubstEnv
1218 | length tyvars /= length tys
1219 = pprTrace "mkTopTvSubst" (ppr tyvars $$ ppr tys) emptyVarEnv
1222 = zip_ty_env tyvars tys emptyVarEnv
1224 -- Later substitutions in the list over-ride earlier ones,
1225 -- but there should be no loops
1226 zip_ty_env [] [] env = env
1227 zip_ty_env (tv:tvs) (ty:tys) env = zip_ty_env tvs tys (extendVarEnv env tv ty)
1228 -- There used to be a special case for when
1230 -- (a not-uncommon case) in which case the substitution was dropped.
1231 -- But the type-tidier changes the print-name of a type variable without
1232 -- changing the unique, and that led to a bug. Why? Pre-tidying, we had
1233 -- a type {Foo t}, where Foo is a one-method class. So Foo is really a newtype.
1234 -- And it happened that t was the type variable of the class. Post-tiding,
1235 -- it got turned into {Foo t2}. The ext-core printer expanded this using
1236 -- sourceTypeRep, but that said "Oh, t == t2" because they have the same unique,
1237 -- and so generated a rep type mentioning t not t2.
1239 -- Simplest fix is to nuke the "optimisation"
1240 zip_ty_env tvs tys env = pprTrace "Var/Type length mismatch: " (ppr tvs $$ ppr tys) env
1241 -- zip_ty_env _ _ env = env
1243 instance Outputable TvSubst where
1244 ppr (TvSubst ins env)
1245 = brackets $ sep[ ptext SLIT("TvSubst"),
1246 nest 2 (ptext SLIT("In scope:") <+> ppr ins),
1247 nest 2 (ptext SLIT("Env:") <+> ppr env) ]
1250 %************************************************************************
1252 Performing type substitutions
1254 %************************************************************************
1257 substTyWith :: [TyVar] -> [Type] -> Type -> Type
1258 substTyWith tvs tys = ASSERT( length tvs == length tys )
1259 substTy (zipOpenTvSubst tvs tys)
1261 substTy :: TvSubst -> Type -> Type
1262 substTy subst ty | isEmptyTvSubst subst = ty
1263 | otherwise = subst_ty subst ty
1265 substTys :: TvSubst -> [Type] -> [Type]
1266 substTys subst tys | isEmptyTvSubst subst = tys
1267 | otherwise = map (subst_ty subst) tys
1269 substTheta :: TvSubst -> ThetaType -> ThetaType
1270 substTheta subst theta
1271 | isEmptyTvSubst subst = theta
1272 | otherwise = map (substPred subst) theta
1274 substPred :: TvSubst -> PredType -> PredType
1275 substPred subst (IParam n ty) = IParam n (subst_ty subst ty)
1276 substPred subst (ClassP clas tys) = ClassP clas (map (subst_ty subst) tys)
1277 substPred subst (EqPred ty1 ty2) = EqPred (subst_ty subst ty1) (subst_ty subst ty2)
1279 deShadowTy :: TyVarSet -> Type -> Type -- Remove any nested binders mentioning tvs
1281 = subst_ty (mkTvSubst in_scope emptyTvSubstEnv) ty
1283 in_scope = mkInScopeSet tvs
1285 subst_ty :: TvSubst -> Type -> Type
1286 -- subst_ty is the main workhorse for type substitution
1288 -- Note that the in_scope set is poked only if we hit a forall
1289 -- so it may often never be fully computed
1293 go (TyVarTy tv) = substTyVar subst tv
1294 go (TyConApp tc tys) = let args = map go tys
1295 in args `seqList` TyConApp tc args
1297 go (PredTy p) = PredTy $! (substPred subst p)
1299 go (NoteTy (FTVNote _) ty2) = go ty2 -- Discard the free tyvar note
1301 go (FunTy arg res) = (FunTy $! (go arg)) $! (go res)
1302 go (AppTy fun arg) = mkAppTy (go fun) $! (go arg)
1303 -- The mkAppTy smart constructor is important
1304 -- we might be replacing (a Int), represented with App
1305 -- by [Int], represented with TyConApp
1306 go (ForAllTy tv ty) = case substTyVarBndr subst tv of
1307 (subst', tv') -> ForAllTy tv' $! (subst_ty subst' ty)
1309 substTyVar :: TvSubst -> TyVar -> Type
1310 substTyVar subst@(TvSubst in_scope env) tv
1311 = case lookupTyVar subst tv of {
1312 Nothing -> TyVarTy tv;
1313 Just ty -> ty -- See Note [Apply Once]
1316 substTyVars :: TvSubst -> [TyVar] -> [Type]
1317 substTyVars subst tvs = map (substTyVar subst) tvs
1319 lookupTyVar :: TvSubst -> TyVar -> Maybe Type
1320 -- See Note [Extending the TvSubst]
1321 lookupTyVar (TvSubst in_scope env) tv = lookupVarEnv env tv
1323 substTyVarBndr :: TvSubst -> TyVar -> (TvSubst, TyVar)
1324 substTyVarBndr subst@(TvSubst in_scope env) old_var
1325 = (TvSubst (in_scope `extendInScopeSet` new_var) new_env, new_var)
1327 is_co_var = isCoVar old_var
1329 new_env | no_change = delVarEnv env old_var
1330 | otherwise = extendVarEnv env old_var (TyVarTy new_var)
1332 no_change = new_var == old_var && not is_co_var
1333 -- no_change means that the new_var is identical in
1334 -- all respects to the old_var (same unique, same kind)
1335 -- See Note [Extending the TvSubst]
1337 -- In that case we don't need to extend the substitution
1338 -- to map old to new. But instead we must zap any
1339 -- current substitution for the variable. For example:
1340 -- (\x.e) with id_subst = [x |-> e']
1341 -- Here we must simply zap the substitution for x
1343 new_var = uniqAway in_scope subst_old_var
1344 -- The uniqAway part makes sure the new variable is not already in scope
1346 subst_old_var -- subst_old_var is old_var with the substitution applied to its kind
1347 -- It's only worth doing the substitution for coercions,
1348 -- becuase only they can have free type variables
1349 | is_co_var = setTyVarKind old_var (substTy subst (tyVarKind old_var))
1350 | otherwise = old_var
1353 ----------------------------------------------------
1358 There's a little subtyping at the kind level:
1367 where * [LiftedTypeKind] means boxed type
1368 # [UnliftedTypeKind] means unboxed type
1369 (#) [UbxTupleKind] means unboxed tuple
1370 ?? [ArgTypeKind] is the lub of *,#
1371 ? [OpenTypeKind] means any type at all
1375 error :: forall a:?. String -> a
1376 (->) :: ?? -> ? -> *
1377 (\(x::t) -> ...) Here t::?? (i.e. not unboxed tuple)
1380 type KindVar = TyVar -- invariant: KindVar will always be a
1381 -- TcTyVar with details MetaTv TauTv ...
1382 -- kind var constructors and functions are in TcType
1384 type SimpleKind = Kind
1389 During kind inference, a kind variable unifies only with
1391 sk ::= * | sk1 -> sk2
1393 data T a = MkT a (T Int#)
1394 fails. We give T the kind (k -> *), and the kind variable k won't unify
1395 with # (the kind of Int#).
1399 When creating a fresh internal type variable, we give it a kind to express
1400 constraints on it. E.g. in (\x->e) we make up a fresh type variable for x,
1403 During unification we only bind an internal type variable to a type
1404 whose kind is lower in the sub-kind hierarchy than the kind of the tyvar.
1406 When unifying two internal type variables, we collect their kind constraints by
1407 finding the GLB of the two. Since the partial order is a tree, they only
1408 have a glb if one is a sub-kind of the other. In that case, we bind the
1409 less-informative one to the more informative one. Neat, eh?
1416 %************************************************************************
1418 Functions over Kinds
1420 %************************************************************************
1423 kindFunResult :: Kind -> Kind
1424 kindFunResult k = funResultTy k
1426 splitKindFunTys :: Kind -> ([Kind],Kind)
1427 splitKindFunTys k = splitFunTys k
1429 splitKindFunTysN :: Int -> Kind -> ([Kind],Kind)
1430 splitKindFunTysN k = splitFunTysN k
1432 isUbxTupleKind, isOpenTypeKind, isArgTypeKind, isUnliftedTypeKind :: Kind -> Bool
1434 isOpenTypeKindCon tc = tyConUnique tc == openTypeKindTyConKey
1436 isOpenTypeKind (TyConApp tc _) = isOpenTypeKindCon tc
1437 isOpenTypeKind other = False
1439 isUbxTupleKindCon tc = tyConUnique tc == ubxTupleKindTyConKey
1441 isUbxTupleKind (TyConApp tc _) = isUbxTupleKindCon tc
1442 isUbxTupleKind other = False
1444 isArgTypeKindCon tc = tyConUnique tc == argTypeKindTyConKey
1446 isArgTypeKind (TyConApp tc _) = isArgTypeKindCon tc
1447 isArgTypeKind other = False
1449 isUnliftedTypeKindCon tc = tyConUnique tc == unliftedTypeKindTyConKey
1451 isUnliftedTypeKind (TyConApp tc _) = isUnliftedTypeKindCon tc
1452 isUnliftedTypeKind other = False
1454 isSubOpenTypeKind :: Kind -> Bool
1455 -- True of any sub-kind of OpenTypeKind (i.e. anything except arrow)
1456 isSubOpenTypeKind (FunTy k1 k2) = ASSERT2 ( isKind k1, text "isSubOpenTypeKind" <+> ppr k1 <+> text "::" <+> ppr (typeKind k1) )
1457 ASSERT2 ( isKind k2, text "isSubOpenTypeKind" <+> ppr k2 <+> text "::" <+> ppr (typeKind k2) )
1459 isSubOpenTypeKind (TyConApp kc []) = ASSERT( isKind (TyConApp kc []) ) True
1460 isSubOpenTypeKind other = ASSERT( isKind other ) False
1461 -- This is a conservative answer
1462 -- It matters in the call to isSubKind in
1463 -- checkExpectedKind.
1465 isSubArgTypeKindCon kc
1466 | isUnliftedTypeKindCon kc = True
1467 | isLiftedTypeKindCon kc = True
1468 | isArgTypeKindCon kc = True
1471 isSubArgTypeKind :: Kind -> Bool
1472 -- True of any sub-kind of ArgTypeKind
1473 isSubArgTypeKind (TyConApp kc []) = isSubArgTypeKindCon kc
1474 isSubArgTypeKind other = False
1476 isSuperKind :: Type -> Bool
1477 isSuperKind (TyConApp (skc) []) = isSuperKindTyCon skc
1478 isSuperKind other = False
1480 isKind :: Kind -> Bool
1481 isKind k = isSuperKind (typeKind k)
1483 isSubKind :: Kind -> Kind -> Bool
1484 -- (k1 `isSubKind` k2) checks that k1 <: k2
1485 isSubKind (TyConApp kc1 []) (TyConApp kc2 []) = kc1 `isSubKindCon` kc2
1486 isSubKind (FunTy a1 r1) (FunTy a2 r2) = (a2 `isSubKind` a1) && (r1 `isSubKind` r2)
1487 isSubKind (PredTy (EqPred ty1 ty2)) (PredTy (EqPred ty1' ty2'))
1488 = ty1 `tcEqType` ty1' && ty2 `tcEqType` ty2'
1489 isSubKind k1 k2 = False
1491 eqKind :: Kind -> Kind -> Bool
1494 isSubKindCon :: TyCon -> TyCon -> Bool
1495 -- (kc1 `isSubKindCon` kc2) checks that kc1 <: kc2
1496 isSubKindCon kc1 kc2
1497 | isLiftedTypeKindCon kc1 && isLiftedTypeKindCon kc2 = True
1498 | isUnliftedTypeKindCon kc1 && isUnliftedTypeKindCon kc2 = True
1499 | isUbxTupleKindCon kc1 && isUbxTupleKindCon kc2 = True
1500 | isOpenTypeKindCon kc2 = True
1501 -- we already know kc1 is not a fun, its a TyCon
1502 | isArgTypeKindCon kc2 && isSubArgTypeKindCon kc1 = True
1505 defaultKind :: Kind -> Kind
1506 -- Used when generalising: default kind '?' and '??' to '*'
1508 -- When we generalise, we make generic type variables whose kind is
1509 -- simple (* or *->* etc). So generic type variables (other than
1510 -- built-in constants like 'error') always have simple kinds. This is important;
1513 -- We want f to get type
1514 -- f :: forall (a::*). a -> Bool
1516 -- f :: forall (a::??). a -> Bool
1517 -- because that would allow a call like (f 3#) as well as (f True),
1518 --and the calling conventions differ. This defaulting is done in TcMType.zonkTcTyVarBndr.
1520 | isSubOpenTypeKind k = liftedTypeKind
1521 | isSubArgTypeKind k = liftedTypeKind
1524 isEqPred :: PredType -> Bool
1525 isEqPred (EqPred _ _) = True
1526 isEqPred other = False