%
% (c) The University of Glasgow 2006
% (c) The GRASP/AQUA Project, Glasgow University, 1998
%
Type - public interface
\begin{code}
module Type (
TyThing(..), Type, PredType(..), ThetaType,
mkTyVarTy, mkTyVarTys, getTyVar, getTyVar_maybe,
mkAppTy, mkAppTys, splitAppTy, splitAppTys,
splitAppTy_maybe, repSplitAppTy_maybe,
mkFunTy, mkFunTys, splitFunTy, splitFunTy_maybe,
splitFunTys, splitFunTysN,
funResultTy, funArgTy, zipFunTys,
mkTyConApp, mkTyConTy,
tyConAppTyCon, tyConAppArgs,
splitTyConApp_maybe, splitTyConApp,
mkForAllTy, mkForAllTys, splitForAllTy_maybe, splitForAllTys,
applyTy, applyTys, applyTysD, isForAllTy, dropForAlls,
newTyConInstRhs, carefullySplitNewType_maybe,
tyFamInsts, predFamInsts,
mkPredTy, mkPredTys, mkFamilyTyConApp, isEqPred, coVarPred,
funTyCon,
isTyVarTy, isFunTy, isDictTy,
isUnLiftedType, isUnboxedTupleType, isAlgType, isClosedAlgType,
isPrimitiveType, isStrictType, isStrictPred,
Kind, SimpleKind, KindVar,
liftedTypeKind, unliftedTypeKind, openTypeKind,
argTypeKind, ubxTupleKind,
tySuperKind, coSuperKind,
liftedTypeKindTyCon, openTypeKindTyCon, unliftedTypeKindTyCon,
argTypeKindTyCon, ubxTupleKindTyCon,
tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta,
expandTypeSynonyms,
coreEqType, coreEqType2,
tcEqType, tcEqTypes, tcCmpType, tcCmpTypes,
tcEqPred, tcEqPredX, tcCmpPred, tcEqTypeX, tcPartOfType, tcPartOfPred,
seqType, seqTypes,
coreView, tcView, kindView,
repType,
PrimRep(..),
typePrimRep, predTypeRep,
TvSubstEnv,
TvSubst(..),
emptyTvSubstEnv, emptyTvSubst,
mkTvSubst, mkOpenTvSubst, zipOpenTvSubst, zipTopTvSubst, mkTopTvSubst, notElemTvSubst,
getTvSubstEnv, setTvSubstEnv, zapTvSubstEnv, getTvInScope,
extendTvInScope, extendTvInScopeList,
extendTvSubst, extendTvSubstList, isInScope, composeTvSubst, zipTyEnv,
isEmptyTvSubst, unionTvSubst,
substTy, substTys, substTyWith, substTysWith, substTheta,
substPred, substTyVar, substTyVars, substTyVarBndr, deShadowTy, lookupTyVar,
pprType, pprParendType, pprTypeApp, pprTyThingCategory, pprTyThing, pprForAll,
pprPred, pprEqPred, pprTheta, pprThetaArrow, pprClassPred, pprKind, pprParendKind,
pprSourceTyCon
) where
#include "HsVersions.h"
import TypeRep
import Var
import VarEnv
import VarSet
import Class
import TyCon
import StaticFlags
import Util
import Outputable
import FastString
import Data.Maybe ( isJust )
infixr 3 `mkFunTy`
\end{code}
\begin{code}
\end{code}
%************************************************************************
%* *
Type representation
%* *
%************************************************************************
\begin{code}
coreView :: Type -> Maybe Type
coreView (PredTy p)
| isEqPred p = Nothing
| otherwise = Just (predTypeRep p)
coreView (TyConApp tc tys) | Just (tenv, rhs, tys') <- coreExpandTyCon_maybe tc tys
= Just (mkAppTys (substTy (mkTopTvSubst tenv) rhs) tys')
coreView _ = Nothing
tcView :: Type -> Maybe Type
tcView (TyConApp tc tys) | Just (tenv, rhs, tys') <- tcExpandTyCon_maybe tc tys
= Just (mkAppTys (substTy (mkTopTvSubst tenv) rhs) tys')
tcView _ = Nothing
expandTypeSynonyms :: Type -> Type
expandTypeSynonyms ty
= go ty
where
go (TyConApp tc tys)
| Just (tenv, rhs, tys') <- tcExpandTyCon_maybe tc tys
= go (mkAppTys (substTy (mkTopTvSubst tenv) rhs) tys')
| otherwise
= TyConApp tc (map go tys)
go (TyVarTy tv) = TyVarTy tv
go (AppTy t1 t2) = AppTy (go t1) (go t2)
go (FunTy t1 t2) = FunTy (go t1) (go t2)
go (ForAllTy tv t) = ForAllTy tv (go t)
go (PredTy p) = PredTy (go_pred p)
go_pred (ClassP c ts) = ClassP c (map go ts)
go_pred (IParam ip t) = IParam ip (go t)
go_pred (EqPred t1 t2) = EqPred (go t1) (go t2)
kindView :: Kind -> Maybe Kind
kindView _ = Nothing
\end{code}
%************************************************************************
%* *
\subsection{Constructor-specific functions}
%* *
%************************************************************************
---------------------------------------------------------------------
TyVarTy
~~~~~~~
\begin{code}
mkTyVarTy :: TyVar -> Type
mkTyVarTy = TyVarTy
mkTyVarTys :: [TyVar] -> [Type]
mkTyVarTys = map mkTyVarTy
getTyVar :: String -> Type -> TyVar
getTyVar msg ty = case getTyVar_maybe ty of
Just tv -> tv
Nothing -> panic ("getTyVar: " ++ msg)
isTyVarTy :: Type -> Bool
isTyVarTy ty = isJust (getTyVar_maybe ty)
getTyVar_maybe :: Type -> Maybe TyVar
getTyVar_maybe ty | Just ty' <- coreView ty = getTyVar_maybe ty'
getTyVar_maybe (TyVarTy tv) = Just tv
getTyVar_maybe _ = Nothing
\end{code}
---------------------------------------------------------------------
AppTy
~~~~~
We need to be pretty careful with AppTy to make sure we obey the
invariant that a TyConApp is always visibly so. mkAppTy maintains the
invariant: use it.
\begin{code}
mkAppTy :: Type -> Type -> Type
mkAppTy orig_ty1 orig_ty2
= mk_app orig_ty1
where
mk_app (TyConApp tc tys) = mkTyConApp tc (tys ++ [orig_ty2])
mk_app _ = AppTy orig_ty1 orig_ty2
mkAppTys :: Type -> [Type] -> Type
mkAppTys orig_ty1 [] = orig_ty1
mkAppTys orig_ty1 orig_tys2
= mk_app orig_ty1
where
mk_app (TyConApp tc tys) = mkTyConApp tc (tys ++ orig_tys2)
mk_app _ = foldl AppTy orig_ty1 orig_tys2
splitAppTy_maybe :: Type -> Maybe (Type, Type)
splitAppTy_maybe ty | Just ty' <- coreView ty
= splitAppTy_maybe ty'
splitAppTy_maybe ty = repSplitAppTy_maybe ty
repSplitAppTy_maybe :: Type -> Maybe (Type,Type)
repSplitAppTy_maybe (FunTy ty1 ty2) = Just (TyConApp funTyCon [ty1], ty2)
repSplitAppTy_maybe (AppTy ty1 ty2) = Just (ty1, ty2)
repSplitAppTy_maybe (TyConApp tc tys)
| isDecomposableTyCon tc || length tys > tyConArity tc
= case snocView tys of
Just (tys', ty') -> Just (TyConApp tc tys', ty')
Nothing -> Nothing
repSplitAppTy_maybe _other = Nothing
splitAppTy :: Type -> (Type, Type)
splitAppTy ty = case splitAppTy_maybe ty of
Just pr -> pr
Nothing -> panic "splitAppTy"
splitAppTys :: Type -> (Type, [Type])
splitAppTys ty = split ty ty []
where
split orig_ty ty args | Just ty' <- coreView ty = split orig_ty ty' args
split _ (AppTy ty arg) args = split ty ty (arg:args)
split _ (TyConApp tc tc_args) args
= let
n | isDecomposableTyCon tc = 0
| otherwise = tyConArity tc
(tc_args1, tc_args2) = splitAt n tc_args
in
(TyConApp tc tc_args1, tc_args2 ++ args)
split _ (FunTy ty1 ty2) args = ASSERT( null args )
(TyConApp funTyCon [], [ty1,ty2])
split orig_ty _ args = (orig_ty, args)
\end{code}
---------------------------------------------------------------------
FunTy
~~~~~
\begin{code}
mkFunTy :: Type -> Type -> Type
mkFunTy arg@(PredTy (EqPred {})) res = ForAllTy (mkWildCoVar arg) res
mkFunTy arg res = FunTy arg res
mkFunTys :: [Type] -> Type -> Type
mkFunTys tys ty = foldr mkFunTy ty tys
isFunTy :: Type -> Bool
isFunTy ty = isJust (splitFunTy_maybe ty)
splitFunTy :: Type -> (Type, Type)
splitFunTy ty | Just ty' <- coreView ty = splitFunTy ty'
splitFunTy (FunTy arg res) = (arg, res)
splitFunTy other = pprPanic "splitFunTy" (ppr other)
splitFunTy_maybe :: Type -> Maybe (Type, Type)
splitFunTy_maybe ty | Just ty' <- coreView ty = splitFunTy_maybe ty'
splitFunTy_maybe (FunTy arg res) = Just (arg, res)
splitFunTy_maybe _ = Nothing
splitFunTys :: Type -> ([Type], Type)
splitFunTys ty = split [] ty ty
where
split args orig_ty ty | Just ty' <- coreView ty = split args orig_ty ty'
split args _ (FunTy arg res) = split (arg:args) res res
split args orig_ty _ = (reverse args, orig_ty)
splitFunTysN :: Int -> Type -> ([Type], Type)
splitFunTysN 0 ty = ([], ty)
splitFunTysN n ty = ASSERT2( isFunTy ty, int n <+> ppr ty )
case splitFunTy ty of { (arg, res) ->
case splitFunTysN (n1) res of { (args, res) ->
(arg:args, res) }}
zipFunTys :: Outputable a => [a] -> Type -> ([(a, Type)], Type)
zipFunTys orig_xs orig_ty = split [] orig_xs orig_ty orig_ty
where
split acc [] nty _ = (reverse acc, nty)
split acc xs nty ty
| Just ty' <- coreView ty = split acc xs nty ty'
split acc (x:xs) _ (FunTy arg res) = split ((x,arg):acc) xs res res
split _ _ _ _ = pprPanic "zipFunTys" (ppr orig_xs <+> ppr orig_ty)
funResultTy :: Type -> Type
funResultTy ty | Just ty' <- coreView ty = funResultTy ty'
funResultTy (FunTy _arg res) = res
funResultTy ty = pprPanic "funResultTy" (ppr ty)
funArgTy :: Type -> Type
funArgTy ty | Just ty' <- coreView ty = funArgTy ty'
funArgTy (FunTy arg _res) = arg
funArgTy ty = pprPanic "funArgTy" (ppr ty)
\end{code}
---------------------------------------------------------------------
TyConApp
~~~~~~~~
\begin{code}
mkTyConApp :: TyCon -> [Type] -> Type
mkTyConApp tycon tys
| isFunTyCon tycon, [ty1,ty2] <- tys
= FunTy ty1 ty2
| otherwise
= TyConApp tycon tys
mkTyConTy :: TyCon -> Type
mkTyConTy tycon = mkTyConApp tycon []
tyConAppTyCon :: Type -> TyCon
tyConAppTyCon ty = fst (splitTyConApp ty)
tyConAppArgs :: Type -> [Type]
tyConAppArgs ty = snd (splitTyConApp ty)
splitTyConApp :: Type -> (TyCon, [Type])
splitTyConApp ty = case splitTyConApp_maybe ty of
Just stuff -> stuff
Nothing -> pprPanic "splitTyConApp" (ppr ty)
splitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe ty | Just ty' <- coreView ty = splitTyConApp_maybe ty'
splitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
splitTyConApp_maybe (FunTy arg res) = Just (funTyCon, [arg,res])
splitTyConApp_maybe _ = Nothing
newTyConInstRhs :: TyCon -> [Type] -> Type
newTyConInstRhs tycon tys
= ASSERT2( equalLength tvs tys1, ppr tycon $$ ppr tys $$ ppr tvs )
mkAppTys (substTyWith tvs tys1 ty) tys2
where
(tvs, ty) = newTyConEtadRhs tycon
(tys1, tys2) = splitAtList tvs tys
\end{code}
---------------------------------------------------------------------
SynTy
~~~~~
Notes on type synonyms
~~~~~~~~~~~~~~~~~~~~~~
The various "split" functions (splitFunTy, splitRhoTy, splitForAllTy) try
to return type synonyms whereever possible. Thus
type Foo a = a -> a
we want
splitFunTys (a -> Foo a) = ([a], Foo a)
not ([a], a -> a)
The reason is that we then get better (shorter) type signatures in
interfaces. Notably this plays a role in tcTySigs in TcBinds.lhs.
Note [Expanding newtypes]
~~~~~~~~~~~~~~~~~~~~~~~~~
When expanding a type to expose a data-type constructor, we need to be
careful about newtypes, lest we fall into an infinite loop. Here are
the key examples:
newtype Id x = MkId x
newtype Fix f = MkFix (f (Fix f))
newtype T = MkT (T -> T)
Type Expansion
--------------------------
T T -> T
Fix Maybe Maybe (Fix Maybe)
Id (Id Int) Int
Fix Id NO NO NO
Notice that we can expand T, even though it's recursive.
And we can expand Id (Id Int), even though the Id shows up
twice at the outer level.
So, when expanding, we keep track of when we've seen a recursive
newtype at outermost level; and bale out if we see it again.
Representation types
~~~~~~~~~~~~~~~~~~~~
\begin{code}
repType :: Type -> Type
repType ty
= go [] ty
where
go :: [TyCon] -> Type -> Type
go rec_nts ty | Just ty' <- coreView ty
= go rec_nts ty'
go rec_nts (ForAllTy _ ty)
= go rec_nts ty
go rec_nts (TyConApp tc tys)
| Just (rec_nts', ty') <- carefullySplitNewType_maybe rec_nts tc tys
= go rec_nts' ty'
go _ ty = ty
carefullySplitNewType_maybe :: [TyCon] -> TyCon -> [Type] -> Maybe ([TyCon],Type)
carefullySplitNewType_maybe rec_nts tc tys
| isNewTyCon tc
, not (tc `elem` rec_nts) = Just (rec_nts', newTyConInstRhs tc tys)
| otherwise = Nothing
where
rec_nts' | isRecursiveTyCon tc = tc:rec_nts
| otherwise = rec_nts
typePrimRep :: Type -> PrimRep
typePrimRep ty = case repType ty of
TyConApp tc _ -> tyConPrimRep tc
FunTy _ _ -> PtrRep
AppTy _ _ -> PtrRep
TyVarTy _ -> PtrRep
_ -> pprPanic "typePrimRep" (ppr ty)
\end{code}
---------------------------------------------------------------------
ForAllTy
~~~~~~~~
\begin{code}
mkForAllTy :: TyVar -> Type -> Type
mkForAllTy tyvar ty
= ForAllTy tyvar ty
mkForAllTys :: [TyVar] -> Type -> Type
mkForAllTys tyvars ty = foldr ForAllTy ty tyvars
isForAllTy :: Type -> Bool
isForAllTy (ForAllTy _ _) = True
isForAllTy _ = False
splitForAllTy_maybe :: Type -> Maybe (TyVar, Type)
splitForAllTy_maybe ty = splitFAT_m ty
where
splitFAT_m ty | Just ty' <- coreView ty = splitFAT_m ty'
splitFAT_m (ForAllTy tyvar ty) = Just(tyvar, ty)
splitFAT_m _ = Nothing
splitForAllTys :: Type -> ([TyVar], Type)
splitForAllTys ty = split ty ty []
where
split orig_ty ty tvs | Just ty' <- coreView ty = split orig_ty ty' tvs
split _ (ForAllTy tv ty) tvs = split ty ty (tv:tvs)
split orig_ty _ tvs = (reverse tvs, orig_ty)
dropForAlls :: Type -> Type
dropForAlls ty = snd (splitForAllTys ty)
\end{code}
-- (mkPiType now in CoreUtils)
applyTy, applyTys
~~~~~~~~~~~~~~~~~
\begin{code}
applyTy :: Type -> Type -> Type
applyTy ty arg | Just ty' <- coreView ty = applyTy ty' arg
applyTy (ForAllTy tv ty) arg = substTyWith [tv] [arg] ty
applyTy _ _ = panic "applyTy"
applyTys :: Type -> [Type] -> Type
applyTys ty args = applyTysD empty ty args
applyTysD :: SDoc -> Type -> [Type] -> Type
applyTysD _ orig_fun_ty [] = orig_fun_ty
applyTysD doc orig_fun_ty arg_tys
| n_tvs == n_args
= substTyWith tvs arg_tys rho_ty
| n_tvs > n_args
= substTyWith (take n_args tvs) arg_tys
(mkForAllTys (drop n_args tvs) rho_ty)
| otherwise
= ASSERT2( n_tvs > 0, doc $$ ppr orig_fun_ty )
applyTysD doc (substTyWith tvs (take n_tvs arg_tys) rho_ty)
(drop n_tvs arg_tys)
where
(tvs, rho_ty) = splitForAllTys orig_fun_ty
n_tvs = length tvs
n_args = length arg_tys
\end{code}
%************************************************************************
%* *
\subsection{Source types}
%* *
%************************************************************************
Source types are always lifted.
The key function is predTypeRep which gives the representation of a source type:
\begin{code}
mkPredTy :: PredType -> Type
mkPredTy pred = PredTy pred
mkPredTys :: ThetaType -> [Type]
mkPredTys preds = map PredTy preds
isEqPred :: PredType -> Bool
isEqPred (EqPred _ _) = True
isEqPred _ = False
predTypeRep :: PredType -> Type
predTypeRep (IParam _ ty) = ty
predTypeRep (ClassP clas tys) = mkTyConApp (classTyCon clas) tys
predTypeRep (EqPred ty1 ty2) = pprPanic "predTypeRep" (ppr (EqPred ty1 ty2))
mkFamilyTyConApp :: TyCon -> [Type] -> Type
mkFamilyTyConApp tc tys
| Just (fam_tc, fam_tys) <- tyConFamInst_maybe tc
, let fam_subst = zipTopTvSubst (tyConTyVars tc) tys
= mkTyConApp fam_tc (substTys fam_subst fam_tys)
| otherwise
= mkTyConApp tc tys
pprSourceTyCon :: TyCon -> SDoc
pprSourceTyCon tycon
| Just (fam_tc, tys) <- tyConFamInst_maybe tycon
= ppr $ fam_tc `TyConApp` tys
| otherwise
= ppr tycon
isDictTy :: Type -> Bool
isDictTy ty = case splitTyConApp_maybe ty of
Just (tc, _) -> isClassTyCon tc
Nothing -> False
\end{code}
%************************************************************************
%* *
The free variables of a type
%* *
%************************************************************************
\begin{code}
tyVarsOfType :: Type -> TyVarSet
tyVarsOfType (TyVarTy tv) = unitVarSet tv
tyVarsOfType (TyConApp _ tys) = tyVarsOfTypes tys
tyVarsOfType (PredTy sty) = tyVarsOfPred sty
tyVarsOfType (FunTy arg res) = tyVarsOfType arg `unionVarSet` tyVarsOfType res
tyVarsOfType (AppTy fun arg) = tyVarsOfType fun `unionVarSet` tyVarsOfType arg
tyVarsOfType (ForAllTy tv ty)
| isTyVar tv = inner_tvs `delVarSet` tv
| otherwise =
inner_tvs `unionVarSet` tyVarsOfType (tyVarKind tv)
where
inner_tvs = tyVarsOfType ty
tyVarsOfTypes :: [Type] -> TyVarSet
tyVarsOfTypes tys = foldr (unionVarSet.tyVarsOfType) emptyVarSet tys
tyVarsOfPred :: PredType -> TyVarSet
tyVarsOfPred (IParam _ ty) = tyVarsOfType ty
tyVarsOfPred (ClassP _ tys) = tyVarsOfTypes tys
tyVarsOfPred (EqPred ty1 ty2) = tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2
tyVarsOfTheta :: ThetaType -> TyVarSet
tyVarsOfTheta = foldr (unionVarSet . tyVarsOfPred) emptyVarSet
\end{code}
%************************************************************************
%* *
\subsection{Type families}
%* *
%************************************************************************
\begin{code}
tyFamInsts :: Type -> [(TyCon, [Type])]
tyFamInsts ty
| Just exp_ty <- tcView ty = tyFamInsts exp_ty
tyFamInsts (TyVarTy _) = []
tyFamInsts (TyConApp tc tys)
| isSynFamilyTyCon tc = [(tc, tys)]
| otherwise = concat (map tyFamInsts tys)
tyFamInsts (FunTy ty1 ty2) = tyFamInsts ty1 ++ tyFamInsts ty2
tyFamInsts (AppTy ty1 ty2) = tyFamInsts ty1 ++ tyFamInsts ty2
tyFamInsts (ForAllTy _ ty) = tyFamInsts ty
tyFamInsts (PredTy pty) = predFamInsts pty
predFamInsts :: PredType -> [(TyCon, [Type])]
predFamInsts (ClassP _cla tys) = concat (map tyFamInsts tys)
predFamInsts (IParam _ ty) = tyFamInsts ty
predFamInsts (EqPred ty1 ty2) = tyFamInsts ty1 ++ tyFamInsts ty2
\end{code}
%************************************************************************
%* *
\subsection{Liftedness}
%* *
%************************************************************************
\begin{code}
isUnLiftedType :: Type -> Bool
isUnLiftedType ty | Just ty' <- coreView ty = isUnLiftedType ty'
isUnLiftedType (ForAllTy _ ty) = isUnLiftedType ty
isUnLiftedType (TyConApp tc _) = isUnLiftedTyCon tc
isUnLiftedType _ = False
isUnboxedTupleType :: Type -> Bool
isUnboxedTupleType ty = case splitTyConApp_maybe ty of
Just (tc, _ty_args) -> isUnboxedTupleTyCon tc
_ -> False
isAlgType :: Type -> Bool
isAlgType ty
= case splitTyConApp_maybe ty of
Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
isAlgTyCon tc
_other -> False
isClosedAlgType :: Type -> Bool
isClosedAlgType ty
= case splitTyConApp_maybe ty of
Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
isAlgTyCon tc && not (isFamilyTyCon tc)
_other -> False
\end{code}
\begin{code}
isStrictType :: Type -> Bool
isStrictType (PredTy pred) = isStrictPred pred
isStrictType ty | Just ty' <- coreView ty = isStrictType ty'
isStrictType (ForAllTy _ ty) = isStrictType ty
isStrictType (TyConApp tc _) = isUnLiftedTyCon tc
isStrictType _ = False
isStrictPred :: PredType -> Bool
isStrictPred (ClassP clas _) = opt_DictsStrict && not (isNewTyCon (classTyCon clas))
isStrictPred _ = False
\end{code}
\begin{code}
isPrimitiveType :: Type -> Bool
isPrimitiveType ty = case splitTyConApp_maybe ty of
Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
isPrimTyCon tc
_ -> False
\end{code}
%************************************************************************
%* *
\subsection{Sequencing on types}
%* *
%************************************************************************
\begin{code}
seqType :: Type -> ()
seqType (TyVarTy tv) = tv `seq` ()
seqType (AppTy t1 t2) = seqType t1 `seq` seqType t2
seqType (FunTy t1 t2) = seqType t1 `seq` seqType t2
seqType (PredTy p) = seqPred p
seqType (TyConApp tc tys) = tc `seq` seqTypes tys
seqType (ForAllTy tv ty) = tv `seq` seqType ty
seqTypes :: [Type] -> ()
seqTypes [] = ()
seqTypes (ty:tys) = seqType ty `seq` seqTypes tys
seqPred :: PredType -> ()
seqPred (ClassP c tys) = c `seq` seqTypes tys
seqPred (IParam n ty) = n `seq` seqType ty
seqPred (EqPred ty1 ty2) = seqType ty1 `seq` seqType ty2
\end{code}
%************************************************************************
%* *
Equality for Core types
(We don't use instances so that we know where it happens)
%* *
%************************************************************************
Note that eqType works right even for partial applications of newtypes.
See Note [Newtype eta] in TyCon.lhs
\begin{code}
coreEqType :: Type -> Type -> Bool
coreEqType t1 t2 = coreEqType2 rn_env t1 t2
where
rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfType t1 `unionVarSet` tyVarsOfType t2))
coreEqType2 :: RnEnv2 -> Type -> Type -> Bool
coreEqType2 rn_env t1 t2
= eq rn_env t1 t2
where
eq env (TyVarTy tv1) (TyVarTy tv2) = rnOccL env tv1 == rnOccR env tv2
eq env (ForAllTy tv1 t1) (ForAllTy tv2 t2) = eq (rnBndr2 env tv1 tv2) t1 t2
eq env (AppTy s1 t1) (AppTy s2 t2) = eq env s1 s2 && eq env t1 t2
eq env (FunTy s1 t1) (FunTy s2 t2) = eq env s1 s2 && eq env t1 t2
eq env (TyConApp tc1 tys1) (TyConApp tc2 tys2)
| tc1 == tc2, all2 (eq env) tys1 tys2 = True
eq env t1 t2 | Just t1' <- coreView t1 = eq env t1' t2
| Just t2' <- coreView t2 = eq env t1 t2'
eq _ _ _ = False
\end{code}
%************************************************************************
%* *
Comparision for source types
(We don't use instances so that we know where it happens)
%* *
%************************************************************************
\begin{code}
tcEqType :: Type -> Type -> Bool
tcEqType t1 t2 = isEqual $ cmpType t1 t2
tcEqTypes :: [Type] -> [Type] -> Bool
tcEqTypes tys1 tys2 = isEqual $ cmpTypes tys1 tys2
tcCmpType :: Type -> Type -> Ordering
tcCmpType t1 t2 = cmpType t1 t2
tcCmpTypes :: [Type] -> [Type] -> Ordering
tcCmpTypes tys1 tys2 = cmpTypes tys1 tys2
tcEqPred :: PredType -> PredType -> Bool
tcEqPred p1 p2 = isEqual $ cmpPred p1 p2
tcEqPredX :: RnEnv2 -> PredType -> PredType -> Bool
tcEqPredX env p1 p2 = isEqual $ cmpPredX env p1 p2
tcCmpPred :: PredType -> PredType -> Ordering
tcCmpPred p1 p2 = cmpPred p1 p2
tcEqTypeX :: RnEnv2 -> Type -> Type -> Bool
tcEqTypeX env t1 t2 = isEqual $ cmpTypeX env t1 t2
\end{code}
\begin{code}
tcPartOfType :: Type -> Type -> Bool
tcPartOfType t1 t2
| tcEqType t1 t2 = True
tcPartOfType t1 t2
| Just t2' <- tcView t2 = tcPartOfType t1 t2'
tcPartOfType _ (TyVarTy _) = False
tcPartOfType t1 (ForAllTy _ t2) = tcPartOfType t1 t2
tcPartOfType t1 (AppTy s2 t2) = tcPartOfType t1 s2 || tcPartOfType t1 t2
tcPartOfType t1 (FunTy s2 t2) = tcPartOfType t1 s2 || tcPartOfType t1 t2
tcPartOfType t1 (PredTy p2) = tcPartOfPred t1 p2
tcPartOfType t1 (TyConApp _ ts) = any (tcPartOfType t1) ts
tcPartOfPred :: Type -> PredType -> Bool
tcPartOfPred t1 (IParam _ t2) = tcPartOfType t1 t2
tcPartOfPred t1 (ClassP _ ts) = any (tcPartOfType t1) ts
tcPartOfPred t1 (EqPred s2 t2) = tcPartOfType t1 s2 || tcPartOfType t1 t2
\end{code}
Now here comes the real worker
\begin{code}
cmpType :: Type -> Type -> Ordering
cmpType t1 t2 = cmpTypeX rn_env t1 t2
where
rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfType t1 `unionVarSet` tyVarsOfType t2))
cmpTypes :: [Type] -> [Type] -> Ordering
cmpTypes ts1 ts2 = cmpTypesX rn_env ts1 ts2
where
rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfTypes ts1 `unionVarSet` tyVarsOfTypes ts2))
cmpPred :: PredType -> PredType -> Ordering
cmpPred p1 p2 = cmpPredX rn_env p1 p2
where
rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfPred p1 `unionVarSet` tyVarsOfPred p2))
cmpTypeX :: RnEnv2 -> Type -> Type -> Ordering
cmpTypeX env t1 t2 | Just t1' <- tcView t1 = cmpTypeX env t1' t2
| Just t2' <- tcView t2 = cmpTypeX env t1 t2'
cmpTypeX env (TyVarTy tv1) (TyVarTy tv2) = rnOccL env tv1 `compare` rnOccR env tv2
cmpTypeX env (ForAllTy tv1 t1) (ForAllTy tv2 t2) = cmpTypeX (rnBndr2 env tv1 tv2) t1 t2
cmpTypeX env (AppTy s1 t1) (AppTy s2 t2) = cmpTypeX env s1 s2 `thenCmp` cmpTypeX env t1 t2
cmpTypeX env (FunTy s1 t1) (FunTy s2 t2) = cmpTypeX env s1 s2 `thenCmp` cmpTypeX env t1 t2
cmpTypeX env (PredTy p1) (PredTy p2) = cmpPredX env p1 p2
cmpTypeX env (TyConApp tc1 tys1) (TyConApp tc2 tys2) = (tc1 `compare` tc2) `thenCmp` cmpTypesX env tys1 tys2
cmpTypeX _ (AppTy _ _) (TyVarTy _) = GT
cmpTypeX _ (FunTy _ _) (TyVarTy _) = GT
cmpTypeX _ (FunTy _ _) (AppTy _ _) = GT
cmpTypeX _ (TyConApp _ _) (TyVarTy _) = GT
cmpTypeX _ (TyConApp _ _) (AppTy _ _) = GT
cmpTypeX _ (TyConApp _ _) (FunTy _ _) = GT
cmpTypeX _ (ForAllTy _ _) (TyVarTy _) = GT
cmpTypeX _ (ForAllTy _ _) (AppTy _ _) = GT
cmpTypeX _ (ForAllTy _ _) (FunTy _ _) = GT
cmpTypeX _ (ForAllTy _ _) (TyConApp _ _) = GT
cmpTypeX _ (PredTy _) _ = GT
cmpTypeX _ _ _ = LT
cmpTypesX :: RnEnv2 -> [Type] -> [Type] -> Ordering
cmpTypesX _ [] [] = EQ
cmpTypesX env (t1:tys1) (t2:tys2) = cmpTypeX env t1 t2 `thenCmp` cmpTypesX env tys1 tys2
cmpTypesX _ [] _ = LT
cmpTypesX _ _ [] = GT
cmpPredX :: RnEnv2 -> PredType -> PredType -> Ordering
cmpPredX env (IParam n1 ty1) (IParam n2 ty2) = (n1 `compare` n2) `thenCmp` cmpTypeX env ty1 ty2
cmpPredX env (ClassP c1 tys1) (ClassP c2 tys2) = (c1 `compare` c2) `thenCmp` (cmpTypesX env tys1 tys2)
cmpPredX env (EqPred ty1 ty2) (EqPred ty1' ty2') = (cmpTypeX env ty1 ty1') `thenCmp` (cmpTypeX env ty2 ty2')
cmpPredX _ (IParam {}) _ = LT
cmpPredX _ (ClassP {}) (IParam {}) = GT
cmpPredX _ (ClassP {}) (EqPred {}) = LT
cmpPredX _ (EqPred {}) _ = GT
\end{code}
PredTypes are used as a FM key in TcSimplify,
so we take the easy path and make them an instance of Ord
\begin{code}
instance Eq PredType where { (==) = tcEqPred }
instance Ord PredType where { compare = tcCmpPred }
\end{code}
%************************************************************************
%* *
Type substitutions
%* *
%************************************************************************
\begin{code}
data TvSubst
= TvSubst InScopeSet
TvSubstEnv
type TvSubstEnv = TyVarEnv Type
emptyTvSubstEnv :: TvSubstEnv
emptyTvSubstEnv = emptyVarEnv
composeTvSubst :: InScopeSet -> TvSubstEnv -> TvSubstEnv -> TvSubstEnv
composeTvSubst in_scope env1 env2
= env1 `plusVarEnv` mapVarEnv (substTy subst1) env2
where
subst1 = TvSubst in_scope env1
emptyTvSubst :: TvSubst
emptyTvSubst = TvSubst emptyInScopeSet emptyVarEnv
isEmptyTvSubst :: TvSubst -> Bool
isEmptyTvSubst (TvSubst _ env) = isEmptyVarEnv env
mkTvSubst :: InScopeSet -> TvSubstEnv -> TvSubst
mkTvSubst = TvSubst
getTvSubstEnv :: TvSubst -> TvSubstEnv
getTvSubstEnv (TvSubst _ env) = env
getTvInScope :: TvSubst -> InScopeSet
getTvInScope (TvSubst in_scope _) = in_scope
isInScope :: Var -> TvSubst -> Bool
isInScope v (TvSubst in_scope _) = v `elemInScopeSet` in_scope
notElemTvSubst :: TyVar -> TvSubst -> Bool
notElemTvSubst tv (TvSubst _ env) = not (tv `elemVarEnv` env)
setTvSubstEnv :: TvSubst -> TvSubstEnv -> TvSubst
setTvSubstEnv (TvSubst in_scope _) env = TvSubst in_scope env
zapTvSubstEnv :: TvSubst -> TvSubst
zapTvSubstEnv (TvSubst in_scope _) = TvSubst in_scope emptyVarEnv
extendTvInScope :: TvSubst -> Var -> TvSubst
extendTvInScope (TvSubst in_scope env) var = TvSubst (extendInScopeSet in_scope var) env
extendTvInScopeList :: TvSubst -> [Var] -> TvSubst
extendTvInScopeList (TvSubst in_scope env) vars = TvSubst (extendInScopeSetList in_scope vars) env
extendTvSubst :: TvSubst -> TyVar -> Type -> TvSubst
extendTvSubst (TvSubst in_scope env) tv ty = TvSubst in_scope (extendVarEnv env tv ty)
extendTvSubstList :: TvSubst -> [TyVar] -> [Type] -> TvSubst
extendTvSubstList (TvSubst in_scope env) tvs tys
= TvSubst in_scope (extendVarEnvList env (tvs `zip` tys))
unionTvSubst :: TvSubst -> TvSubst -> TvSubst
unionTvSubst (TvSubst in_scope1 env1) (TvSubst in_scope2 env2)
= ASSERT( not (env1 `intersectsVarEnv` env2) )
TvSubst (in_scope1 `unionInScope` in_scope2)
(env1 `plusVarEnv` env2)
mkOpenTvSubst :: TvSubstEnv -> TvSubst
mkOpenTvSubst env = TvSubst (mkInScopeSet (tyVarsOfTypes (varEnvElts env))) env
zipOpenTvSubst :: [TyVar] -> [Type] -> TvSubst
zipOpenTvSubst tyvars tys
| debugIsOn && (length tyvars /= length tys)
= pprTrace "zipOpenTvSubst" (ppr tyvars $$ ppr tys) emptyTvSubst
| otherwise
= TvSubst (mkInScopeSet (tyVarsOfTypes tys)) (zipTyEnv tyvars tys)
mkTopTvSubst :: [(TyVar, Type)] -> TvSubst
mkTopTvSubst prs = TvSubst emptyInScopeSet (mkVarEnv prs)
zipTopTvSubst :: [TyVar] -> [Type] -> TvSubst
zipTopTvSubst tyvars tys
| debugIsOn && (length tyvars /= length tys)
= pprTrace "zipTopTvSubst" (ppr tyvars $$ ppr tys) emptyTvSubst
| otherwise
= TvSubst emptyInScopeSet (zipTyEnv tyvars tys)
zipTyEnv :: [TyVar] -> [Type] -> TvSubstEnv
zipTyEnv tyvars tys
| debugIsOn && (length tyvars /= length tys)
= pprTrace "mkTopTvSubst" (ppr tyvars $$ ppr tys) emptyVarEnv
| otherwise
= zip_ty_env tyvars tys emptyVarEnv
zip_ty_env :: [TyVar] -> [Type] -> TvSubstEnv -> TvSubstEnv
zip_ty_env [] [] env = env
zip_ty_env (tv:tvs) (ty:tys) env = zip_ty_env tvs tys (extendVarEnv env tv ty)
zip_ty_env tvs tys env = pprTrace "Var/Type length mismatch: " (ppr tvs $$ ppr tys) env
instance Outputable TvSubst where
ppr (TvSubst ins env)
= brackets $ sep[ ptext (sLit "TvSubst"),
nest 2 (ptext (sLit "In scope:") <+> ppr ins),
nest 2 (ptext (sLit "Env:") <+> ppr env) ]
\end{code}
%************************************************************************
%* *
Performing type substitutions
%* *
%************************************************************************
\begin{code}
substTyWith :: [TyVar] -> [Type] -> Type -> Type
substTyWith tvs tys = ASSERT( length tvs == length tys )
substTy (zipOpenTvSubst tvs tys)
substTysWith :: [TyVar] -> [Type] -> [Type] -> [Type]
substTysWith tvs tys = ASSERT( length tvs == length tys )
substTys (zipOpenTvSubst tvs tys)
substTy :: TvSubst -> Type -> Type
substTy subst ty | isEmptyTvSubst subst = ty
| otherwise = subst_ty subst ty
substTys :: TvSubst -> [Type] -> [Type]
substTys subst tys | isEmptyTvSubst subst = tys
| otherwise = map (subst_ty subst) tys
substTheta :: TvSubst -> ThetaType -> ThetaType
substTheta subst theta
| isEmptyTvSubst subst = theta
| otherwise = map (substPred subst) theta
substPred :: TvSubst -> PredType -> PredType
substPred subst (IParam n ty) = IParam n (subst_ty subst ty)
substPred subst (ClassP clas tys) = ClassP clas (map (subst_ty subst) tys)
substPred subst (EqPred ty1 ty2) = EqPred (subst_ty subst ty1) (subst_ty subst ty2)
deShadowTy :: TyVarSet -> Type -> Type
deShadowTy tvs ty
= subst_ty (mkTvSubst in_scope emptyTvSubstEnv) ty
where
in_scope = mkInScopeSet tvs
subst_ty :: TvSubst -> Type -> Type
subst_ty subst ty
= go ty
where
go (TyVarTy tv) = substTyVar subst tv
go (TyConApp tc tys) = let args = map go tys
in args `seqList` TyConApp tc args
go (PredTy p) = PredTy $! (substPred subst p)
go (FunTy arg res) = (FunTy $! (go arg)) $! (go res)
go (AppTy fun arg) = mkAppTy (go fun) $! (go arg)
go (ForAllTy tv ty) = case substTyVarBndr subst tv of
(subst', tv') ->
ForAllTy tv' $! (subst_ty subst' ty)
substTyVar :: TvSubst -> TyVar -> Type
substTyVar subst@(TvSubst _ _) tv
= case lookupTyVar subst tv of {
Nothing -> TyVarTy tv;
Just ty -> ty
}
substTyVars :: TvSubst -> [TyVar] -> [Type]
substTyVars subst tvs = map (substTyVar subst) tvs
lookupTyVar :: TvSubst -> TyVar -> Maybe Type
lookupTyVar (TvSubst _ env) tv = lookupVarEnv env tv
substTyVarBndr :: TvSubst -> TyVar -> (TvSubst, TyVar)
substTyVarBndr subst@(TvSubst in_scope env) old_var
= (TvSubst (in_scope `extendInScopeSet` new_var) new_env, new_var)
where
is_co_var = isCoVar old_var
new_env | no_change = delVarEnv env old_var
| otherwise = extendVarEnv env old_var (TyVarTy new_var)
no_change = new_var == old_var && not is_co_var
new_var = uniqAway in_scope subst_old_var
subst_old_var
| is_co_var = setTyVarKind old_var (substTy subst (tyVarKind old_var))
| otherwise = old_var
\end{code}
----------------------------------------------------
-- Kind Stuff
Kinds
~~~~~
\begin{code}
type KindVar = TyVar
type SimpleKind = Kind
\end{code}
Kind inference
~~~~~~~~~~~~~~
During kind inference, a kind variable unifies only with
a "simple kind", sk
sk ::= * | sk1 -> sk2
For example
data T a = MkT a (T Int#)
fails. We give T the kind (k -> *), and the kind variable k won't unify
with # (the kind of Int#).
Type inference
~~~~~~~~~~~~~~
When creating a fresh internal type variable, we give it a kind to express
constraints on it. E.g. in (\x->e) we make up a fresh type variable for x,
with kind ??.
During unification we only bind an internal type variable to a type
whose kind is lower in the sub-kind hierarchy than the kind of the tyvar.
When unifying two internal type variables, we collect their kind constraints by
finding the GLB of the two. Since the partial order is a tree, they only
have a glb if one is a sub-kind of the other. In that case, we bind the
less-informative one to the more informative one. Neat, eh?