module Type (
TyThing(..), Type, KindOrType, PredType, ThetaType,
Var, TyVar, isTyVar,
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_maybe, tyConAppArgs_maybe, tyConAppTyCon, tyConAppArgs,
splitTyConApp_maybe, splitTyConApp, tyConAppArgN, nextRole,
mkForAllTy, mkForAllTys, splitForAllTy_maybe, splitForAllTys,
mkPiKinds, mkPiType, mkPiTypes,
applyTy, applyTys, applyTysD, applyTysX, dropForAlls,
mkNumLitTy, isNumLitTy,
mkStrLitTy, isStrLitTy,
coAxNthLHS,
newTyConInstRhs,
mkFamilyTyConApp,
isDictLikeTy,
mkEqPred, mkCoerciblePred, mkPrimEqPred, mkReprPrimEqPred,
mkClassPred,
isClassPred, isEqPred,
isIPPred, isIPPred_maybe, isIPTyCon, isIPClass,
PredTree(..), EqRel(..), eqRelRole, classifyPredType,
getClassPredTys, getClassPredTys_maybe,
getEqPredTys, getEqPredTys_maybe, getEqPredRole,
predTypeEqRel,
funTyCon,
isTypeVar, isKindVar, allDistinctTyVars, isForAllTy,
isTyVarTy, isFunTy, isDictTy, isPredTy, isVoidTy,
isUnLiftedType, isUnboxedTupleType, isAlgType, isClosedAlgType,
isPrimitiveType, isStrictType,
Kind, SimpleKind, MetaKindVar,
typeKind,
anyKind, liftedTypeKind, unliftedTypeKind, openTypeKind,
constraintKind, superKind,
liftedTypeKindTyCon, openTypeKindTyCon, unliftedTypeKindTyCon,
constraintKindTyCon, anyKindTyCon,
tyVarsOfType, tyVarsOfTypes, closeOverKinds,
expandTypeSynonyms,
typeSize, varSetElemsKvsFirst,
eqType, eqTypeX, eqTypes, cmpType, cmpTypes,
eqPred, eqPredX, cmpPred, eqKind, eqTyVarBndrs,
seqType, seqTypes,
coreView, tcView,
UnaryType, RepType(..), flattenRepType, repType,
tyConsOfType,
typePrimRep, typeRepArity,
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,
substTyVar, substTyVars, substTyVarBndr,
cloneTyVarBndr, deShadowTy, lookupTyVar,
substKiWith, substKisWith,
pprType, pprParendType, pprTypeApp, pprTyThingCategory, pprTyThing,
pprTvBndr, pprTvBndrs, pprForAll, pprUserForAll, pprSigmaType,
pprTheta, pprThetaArrowTy, pprClassPred,
pprKind, pprParendKind, pprSourceTyCon,
TyPrec(..), maybeParen, pprSigmaTypeExtraCts,
tidyType, tidyTypes,
tidyOpenType, tidyOpenTypes,
tidyOpenKind,
tidyTyVarBndr, tidyTyVarBndrs, tidyFreeTyVars,
tidyOpenTyVar, tidyOpenTyVars,
tidyTyVarOcc,
tidyTopType,
tidyKind,
) where
#include "HsVersions.h"
import Kind
import TypeRep
import Var
import VarEnv
import VarSet
import NameEnv
import Class
import TyCon
import TysPrim
import TysWiredIn ( eqTyCon, coercibleTyCon, typeNatKind, typeSymbolKind )
import PrelNames ( eqTyConKey, coercibleTyConKey,
ipClassNameKey, openTypeKindTyConKey,
constraintKindTyConKey, liftedTypeKindTyConKey )
import CoAxiom
import Unique ( Unique, hasKey )
import BasicTypes ( Arity, RepArity )
import Util
import ListSetOps ( getNth )
import Outputable
import FastString
import Maybes ( orElse )
import Data.Maybe ( isJust )
import Control.Monad ( guard )
infixr 3 `mkFunTy`
coreView :: Type -> Maybe Type
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 (LitTy l) = LitTy l
go (TyVarTy tv) = TyVarTy tv
go (AppTy t1 t2) = mkAppTy (go t1) (go t2)
go (FunTy t1 t2) = FunTy (go t1) (go t2)
go (ForAllTy tv t) = ForAllTy tv (go t)
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
allDistinctTyVars :: [KindOrType] -> Bool
allDistinctTyVars tkvs = go emptyVarSet tkvs
where
go _ [] = True
go so_far (ty : tys)
= case getTyVar_maybe ty of
Nothing -> False
Just tv | tv `elemVarSet` so_far -> False
| otherwise -> go (so_far `extendVarSet` tv) tys
mkAppTy :: Type -> Type -> Type
mkAppTy (TyConApp tc tys) ty2 = mkTyConApp tc (tys ++ [ty2])
mkAppTy ty1 ty2 = AppTy ty1 ty2
mkAppTys :: Type -> [Type] -> Type
mkAppTys ty1 [] = ty1
mkAppTys (TyConApp tc tys1) tys2 = mkTyConApp tc (tys1 ++ tys2)
mkAppTys ty1 tys2 = foldl AppTy ty1 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)
| isConstraintKind (typeKind ty1) = Nothing
| otherwise = Just (TyConApp funTyCon [ty1], ty2)
repSplitAppTy_maybe (AppTy ty1 ty2) = Just (ty1, ty2)
repSplitAppTy_maybe (TyConApp tc tys)
| isDecomposableTyCon tc || tys `lengthExceeds` tyConArity tc
, Just (tys', ty') <- snocView tys
= Just (TyConApp tc tys', ty')
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)
mkNumLitTy :: Integer -> Type
mkNumLitTy n = LitTy (NumTyLit n)
isNumLitTy :: Type -> Maybe Integer
isNumLitTy ty | Just ty1 <- tcView ty = isNumLitTy ty1
isNumLitTy (LitTy (NumTyLit n)) = Just n
isNumLitTy _ = Nothing
mkStrLitTy :: FastString -> Type
mkStrLitTy s = LitTy (StrTyLit s)
isStrLitTy :: Type -> Maybe FastString
isStrLitTy ty | Just ty1 <- tcView ty = isStrLitTy ty1
isStrLitTy (LitTy (StrTyLit s)) = Just s
isStrLitTy _ = Nothing
mkFunTy :: Type -> Type -> Type
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)
mkTyConApp :: TyCon -> [Type] -> Type
mkTyConApp tycon tys
| isFunTyCon tycon, [ty1,ty2] <- tys
= FunTy ty1 ty2
| otherwise
= TyConApp tycon tys
tyConAppTyCon_maybe :: Type -> Maybe TyCon
tyConAppTyCon_maybe ty | Just ty' <- coreView ty = tyConAppTyCon_maybe ty'
tyConAppTyCon_maybe (TyConApp tc _) = Just tc
tyConAppTyCon_maybe (FunTy {}) = Just funTyCon
tyConAppTyCon_maybe _ = Nothing
tyConAppTyCon :: Type -> TyCon
tyConAppTyCon ty = tyConAppTyCon_maybe ty `orElse` pprPanic "tyConAppTyCon" (ppr ty)
tyConAppArgs_maybe :: Type -> Maybe [Type]
tyConAppArgs_maybe ty | Just ty' <- coreView ty = tyConAppArgs_maybe ty'
tyConAppArgs_maybe (TyConApp _ tys) = Just tys
tyConAppArgs_maybe (FunTy arg res) = Just [arg,res]
tyConAppArgs_maybe _ = Nothing
tyConAppArgs :: Type -> [Type]
tyConAppArgs ty = tyConAppArgs_maybe ty `orElse` pprPanic "tyConAppArgs" (ppr ty)
tyConAppArgN :: Int -> Type -> Type
tyConAppArgN n ty
= case tyConAppArgs_maybe ty of
Just tys -> ASSERT2( n < length tys, ppr n <+> ppr tys ) tys !! n
Nothing -> pprPanic "tyConAppArgN" (ppr n <+> ppr 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
nextRole :: Type -> Role
nextRole ty
| Just (tc, tys) <- splitTyConApp_maybe ty
, let num_tys = length tys
, num_tys < tyConArity tc
= tyConRoles tc `getNth` num_tys
| otherwise
= Nominal
newTyConInstRhs :: TyCon -> [Type] -> Type
newTyConInstRhs tycon tys
= ASSERT2( tvs `leLength` tys, ppr tycon $$ ppr tys $$ ppr tvs )
applyTysX tvs rhs tys
where
(tvs, rhs) = newTyConEtadRhs tycon
type UnaryType = Type
data RepType = UbxTupleRep [UnaryType]
| UnaryRep UnaryType
flattenRepType :: RepType -> [UnaryType]
flattenRepType (UbxTupleRep tys) = tys
flattenRepType (UnaryRep ty) = [ty]
repType :: Type -> RepType
repType ty
= go initRecTc ty
where
go :: RecTcChecker -> Type -> RepType
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)
| isNewTyCon tc
, tys `lengthAtLeast` tyConArity tc
, Just rec_nts' <- checkRecTc rec_nts tc
= go rec_nts' (newTyConInstRhs tc tys)
| isUnboxedTupleTyCon tc
= if null tys
then UnaryRep voidPrimTy
else UbxTupleRep (concatMap (flattenRepType . go rec_nts) tys)
go _ ty = UnaryRep ty
tyConsOfType :: Type -> NameEnv TyCon
tyConsOfType ty
= go ty
where
go :: Type -> NameEnv TyCon
go ty | Just ty' <- tcView ty = go ty'
go (TyVarTy {}) = emptyNameEnv
go (LitTy {}) = emptyNameEnv
go (TyConApp tc tys) = go_tc tc tys
go (AppTy a b) = go a `plusNameEnv` go b
go (FunTy a b) = go a `plusNameEnv` go b
go (ForAllTy _ ty) = go ty
go_tc tc tys = extendNameEnv (go_s tys) (tyConName tc) tc
go_s tys = foldr (plusNameEnv . go) emptyNameEnv tys
typePrimRep :: UnaryType -> PrimRep
typePrimRep ty
= case repType ty of
UbxTupleRep _ -> pprPanic "typePrimRep: UbxTupleRep" (ppr ty)
UnaryRep rep -> case rep of
TyConApp tc _ -> tyConPrimRep tc
FunTy _ _ -> PtrRep
AppTy _ _ -> PtrRep
TyVarTy _ -> PtrRep
_ -> pprPanic "typePrimRep: UnaryRep" (ppr ty)
typeRepArity :: Arity -> Type -> RepArity
typeRepArity 0 _ = 0
typeRepArity n ty = case repType ty of
UnaryRep (FunTy ty1 ty2) -> length (flattenRepType (repType ty1)) + typeRepArity (n 1) ty2
_ -> pprPanic "typeRepArity: arity greater than type can handle" (ppr (n, ty))
isVoidTy :: Type -> Bool
isVoidTy ty = case repType ty of
UnaryRep (TyConApp tc _) -> isVoidRep (tyConPrimRep tc)
_ -> False
mkForAllTy :: TyVar -> Type -> Type
mkForAllTy tyvar ty
= ForAllTy tyvar ty
mkForAllTys :: [TyVar] -> Type -> Type
mkForAllTys tyvars ty = foldr ForAllTy ty tyvars
mkPiKinds :: [TyVar] -> Kind -> Kind
mkPiKinds [] res = res
mkPiKinds (tv:tvs) res
| isKindVar tv = ForAllTy tv (mkPiKinds tvs res)
| otherwise = FunTy (tyVarKind tv) (mkPiKinds tvs res)
mkPiType :: Var -> Type -> Type
mkPiTypes :: [Var] -> Type -> Type
mkPiType v ty
| isId v = mkFunTy (varType v) ty
| otherwise = mkForAllTy v ty
mkPiTypes vs ty = foldr mkPiType ty vs
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)
applyTy :: Type -> KindOrType -> 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 -> [KindOrType] -> 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 $$ ppr arg_tys )
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
applyTysX :: [TyVar] -> Type -> [Type] -> Type
applyTysX tvs body_ty arg_tys
= ASSERT2( length arg_tys >= n_tvs, ppr tvs $$ ppr body_ty $$ ppr arg_tys )
mkAppTys (substTyWith tvs (take n_tvs arg_tys) body_ty)
(drop n_tvs arg_tys)
where
n_tvs = length tvs
isPredTy :: Type -> Bool
isPredTy ty = go ty []
where
go :: Type -> [KindOrType] -> Bool
go (AppTy ty1 ty2) args = go ty1 (ty2 : args)
go (TyConApp tc tys) args = go_k (tyConKind tc) (tys ++ args)
go (TyVarTy tv) args = go_k (tyVarKind tv) args
go _ _ = False
go_k :: Kind -> [KindOrType] -> Bool
go_k k [] = isConstraintKind k
go_k (FunTy _ k1) (_ :args) = go_k k1 args
go_k (ForAllTy kv k1) (k2:args) = go_k (substKiWith [kv] [k2] k1) args
go_k _ _ = False
isClassPred, isEqPred, isIPPred :: PredType -> Bool
isClassPred ty = case tyConAppTyCon_maybe ty of
Just tyCon | isClassTyCon tyCon -> True
_ -> False
isEqPred ty = case tyConAppTyCon_maybe ty of
Just tyCon -> tyCon `hasKey` eqTyConKey
_ -> False
isIPPred ty = case tyConAppTyCon_maybe ty of
Just tc -> isIPTyCon tc
_ -> False
isIPTyCon :: TyCon -> Bool
isIPTyCon tc = tc `hasKey` ipClassNameKey
isIPClass :: Class -> Bool
isIPClass cls = cls `hasKey` ipClassNameKey
isIPPred_maybe :: Type -> Maybe (FastString, Type)
isIPPred_maybe ty =
do (tc,[t1,t2]) <- splitTyConApp_maybe ty
guard (isIPTyCon tc)
x <- isStrLitTy t1
return (x,t2)
mkEqPred :: Type -> Type -> PredType
mkEqPred ty1 ty2
= WARN( not (k `eqKind` typeKind ty2), ppr ty1 $$ ppr ty2 $$ ppr k $$ ppr (typeKind ty2) )
TyConApp eqTyCon [k, ty1, ty2]
where
k = typeKind ty1
mkCoerciblePred :: Type -> Type -> PredType
mkCoerciblePred ty1 ty2
= WARN( not (k `eqKind` typeKind ty2), ppr ty1 $$ ppr ty2 $$ ppr k $$ ppr (typeKind ty2) )
TyConApp coercibleTyCon [k, ty1, ty2]
where
k = typeKind ty1
mkPrimEqPred :: Type -> Type -> Type
mkPrimEqPred ty1 ty2
= WARN( not (k `eqKind` typeKind ty2), ppr ty1 $$ ppr ty2 )
TyConApp eqPrimTyCon [k, ty1, ty2]
where
k = typeKind ty1
mkReprPrimEqPred :: Type -> Type -> Type
mkReprPrimEqPred ty1 ty2
= WARN( not (k `eqKind` typeKind ty2), ppr ty1 $$ ppr ty2 )
TyConApp eqReprPrimTyCon [k, ty1, ty2]
where
k = typeKind ty1
mkClassPred :: Class -> [Type] -> PredType
mkClassPred clas tys = TyConApp (classTyCon clas) tys
isDictTy :: Type -> Bool
isDictTy = isClassPred
isDictLikeTy :: Type -> Bool
isDictLikeTy ty | Just ty' <- coreView ty = isDictLikeTy ty'
isDictLikeTy ty = case splitTyConApp_maybe ty of
Just (tc, tys) | isClassTyCon tc -> True
| isTupleTyCon tc -> all isDictLikeTy tys
_other -> False
data EqRel = NomEq | ReprEq
deriving (Eq, Ord)
instance Outputable EqRel where
ppr NomEq = text "nominal equality"
ppr ReprEq = text "representational equality"
eqRelRole :: EqRel -> Role
eqRelRole NomEq = Nominal
eqRelRole ReprEq = Representational
data PredTree = ClassPred Class [Type]
| EqPred EqRel Type Type
| TuplePred [PredType]
| IrredPred PredType
classifyPredType :: PredType -> PredTree
classifyPredType ev_ty = case splitTyConApp_maybe ev_ty of
Just (tc, tys) | tc `hasKey` coercibleTyConKey
, let [_, ty1, ty2] = tys
-> EqPred ReprEq ty1 ty2
Just (tc, tys) | tc `hasKey` eqTyConKey
, let [_, ty1, ty2] = tys
-> EqPred NomEq ty1 ty2
Just (tc, tys) | Just clas <- tyConClass_maybe tc
-> ClassPred clas tys
Just (tc, tys) | isTupleTyCon tc
-> TuplePred tys
_ -> IrredPred ev_ty
getClassPredTys :: PredType -> (Class, [Type])
getClassPredTys ty = case getClassPredTys_maybe ty of
Just (clas, tys) -> (clas, tys)
Nothing -> pprPanic "getClassPredTys" (ppr ty)
getClassPredTys_maybe :: PredType -> Maybe (Class, [Type])
getClassPredTys_maybe ty = case splitTyConApp_maybe ty of
Just (tc, tys) | Just clas <- tyConClass_maybe tc -> Just (clas, tys)
_ -> Nothing
getEqPredTys :: PredType -> (Type, Type)
getEqPredTys ty
= case splitTyConApp_maybe ty of
Just (tc, (_ : ty1 : ty2 : tys)) ->
ASSERT( null tys && (tc `hasKey` eqTyConKey
|| tc `hasKey` coercibleTyConKey) )
(ty1, ty2)
_ -> pprPanic "getEqPredTys" (ppr ty)
getEqPredTys_maybe :: PredType -> Maybe (Role, Type, Type)
getEqPredTys_maybe ty
= case splitTyConApp_maybe ty of
Just (tc, [_, ty1, ty2])
| tc `hasKey` eqTyConKey -> Just (Nominal, ty1, ty2)
| tc `hasKey` coercibleTyConKey -> Just (Representational, ty1, ty2)
_ -> Nothing
getEqPredRole :: PredType -> Role
getEqPredRole ty
= case splitTyConApp_maybe ty of
Just (tc, [_, _, _])
| tc `hasKey` eqTyConKey -> Nominal
| tc `hasKey` coercibleTyConKey -> Representational
_ -> pprPanic "getEqPredRole" (ppr ty)
predTypeEqRel :: PredType -> EqRel
predTypeEqRel ty
| Just (tc, _) <- splitTyConApp_maybe ty
, tc `hasKey` coercibleTyConKey
= ReprEq
| otherwise
= NomEq
typeSize :: Type -> Int
typeSize (LitTy {}) = 1
typeSize (TyVarTy {}) = 1
typeSize (AppTy t1 t2) = typeSize t1 + typeSize t2
typeSize (FunTy t1 t2) = typeSize t1 + typeSize t2
typeSize (ForAllTy _ t) = 1 + typeSize t
typeSize (TyConApp _ ts) = 1 + sum (map typeSize ts)
mkFamilyTyConApp :: TyCon -> [Type] -> Type
mkFamilyTyConApp tc tys
| Just (fam_tc, fam_tys) <- tyConFamInst_maybe tc
, let tvs = tyConTyVars tc
fam_subst = ASSERT2( length tvs == length tys, ppr tc <+> ppr tys )
zipTopTvSubst tvs tys
= mkTyConApp fam_tc (substTys fam_subst fam_tys)
| otherwise
= mkTyConApp tc tys
coAxNthLHS :: CoAxiom br -> Int -> Type
coAxNthLHS ax ind =
mkTyConApp (coAxiomTyCon ax) (coAxBranchLHS (coAxiomNthBranch ax ind))
pprSourceTyCon :: TyCon -> SDoc
pprSourceTyCon tycon
| Just (fam_tc, tys) <- tyConFamInst_maybe tycon
= ppr $ fam_tc `TyConApp` tys
| otherwise
= ppr tycon
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 tyConAppTyCon_maybe ty of
Just tc -> 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) | isAlgTyCon tc && not (isFamilyTyCon tc)
-> ASSERT2( ty_args `lengthIs` tyConArity tc, ppr ty ) True
_other -> False
isStrictType :: Type -> Bool
isStrictType = isUnLiftedType
isPrimitiveType :: Type -> Bool
isPrimitiveType ty = case splitTyConApp_maybe ty of
Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
isPrimTyCon tc
_ -> False
seqType :: Type -> ()
seqType (LitTy n) = n `seq` ()
seqType (TyVarTy tv) = tv `seq` ()
seqType (AppTy t1 t2) = seqType t1 `seq` seqType t2
seqType (FunTy t1 t2) = seqType t1 `seq` seqType t2
seqType (TyConApp tc tys) = tc `seq` seqTypes tys
seqType (ForAllTy tv ty) = seqType (tyVarKind tv) `seq` seqType ty
seqTypes :: [Type] -> ()
seqTypes [] = ()
seqTypes (ty:tys) = seqType ty `seq` seqTypes tys
eqKind :: Kind -> Kind -> Bool
eqKind = eqType
eqType :: Type -> Type -> Bool
eqType t1 t2 = isEqual $ cmpType t1 t2
instance Eq Type where
(==) = eqType
eqTypeX :: RnEnv2 -> Type -> Type -> Bool
eqTypeX env t1 t2 = isEqual $ cmpTypeX env t1 t2
eqTypes :: [Type] -> [Type] -> Bool
eqTypes tys1 tys2 = isEqual $ cmpTypes tys1 tys2
eqPred :: PredType -> PredType -> Bool
eqPred = eqType
eqPredX :: RnEnv2 -> PredType -> PredType -> Bool
eqPredX env p1 p2 = isEqual $ cmpTypeX env p1 p2
eqTyVarBndrs :: RnEnv2 -> [TyVar] -> [TyVar] -> Maybe RnEnv2
eqTyVarBndrs env [] []
= Just env
eqTyVarBndrs env (tv1:tvs1) (tv2:tvs2)
| eqTypeX env (tyVarKind tv1) (tyVarKind tv2)
= eqTyVarBndrs (rnBndr2 env tv1 tv2) tvs1 tvs2
eqTyVarBndrs _ _ _= Nothing
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 = cmpTypeX rn_env p1 p2
where
rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfType p1 `unionVarSet` tyVarsOfType p2))
cmpTypeX :: RnEnv2 -> Type -> Type -> Ordering
cmpTypeX env t1 t2 | Just t1' <- coreView t1 = cmpTypeX env t1' t2
| Just t2' <- coreView 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 env (tyVarKind tv1) (tyVarKind tv2)
`thenCmp` 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 (TyConApp tc1 tys1) (TyConApp tc2 tys2) = (tc1 `cmpTc` tc2) `thenCmp` cmpTypesX env tys1 tys2
cmpTypeX _ (LitTy l1) (LitTy l2) = compare l1 l2
cmpTypeX _ (AppTy _ _) (TyVarTy _) = GT
cmpTypeX _ (FunTy _ _) (TyVarTy _) = GT
cmpTypeX _ (FunTy _ _) (AppTy _ _) = GT
cmpTypeX _ (LitTy _) (TyVarTy _) = GT
cmpTypeX _ (LitTy _) (AppTy _ _) = GT
cmpTypeX _ (LitTy _) (FunTy _ _) = GT
cmpTypeX _ (TyConApp _ _) (TyVarTy _) = GT
cmpTypeX _ (TyConApp _ _) (AppTy _ _) = GT
cmpTypeX _ (TyConApp _ _) (FunTy _ _) = GT
cmpTypeX _ (TyConApp _ _) (LitTy _) = GT
cmpTypeX _ (ForAllTy _ _) (TyVarTy _) = GT
cmpTypeX _ (ForAllTy _ _) (AppTy _ _) = GT
cmpTypeX _ (ForAllTy _ _) (FunTy _ _) = GT
cmpTypeX _ (ForAllTy _ _) (LitTy _) = GT
cmpTypeX _ (ForAllTy _ _) (TyConApp _ _) = 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
cmpTc :: TyCon -> TyCon -> Ordering
cmpTc tc1 tc2
| u1 == openTypeKindTyConKey, isSubOpenTypeKindKey u2 = EQ
| u2 == openTypeKindTyConKey, isSubOpenTypeKindKey u1 = EQ
| otherwise = nu1 `compare` nu2
where
u1 = tyConUnique tc1
nu1 = if u1==constraintKindTyConKey then liftedTypeKindTyConKey else u1
u2 = tyConUnique tc2
nu2 = if u2==constraintKindTyConKey then liftedTypeKindTyConKey else u2
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 emptyTvSubstEnv
isEmptyTvSubst :: TvSubst -> Bool
isEmptyTvSubst (TvSubst _ tenv) = isEmptyVarEnv tenv
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 :: CoVar -> TvSubst -> Bool
notElemTvSubst v (TvSubst _ tenv) = not (v `elemVarEnv` tenv)
setTvSubstEnv :: TvSubst -> TvSubstEnv -> TvSubst
setTvSubstEnv (TvSubst in_scope _) tenv = TvSubst in_scope tenv
zapTvSubstEnv :: TvSubst -> TvSubst
zapTvSubstEnv (TvSubst in_scope _) = TvSubst in_scope emptyVarEnv
extendTvInScope :: TvSubst -> Var -> TvSubst
extendTvInScope (TvSubst in_scope tenv) var = TvSubst (extendInScopeSet in_scope var) tenv
extendTvInScopeList :: TvSubst -> [Var] -> TvSubst
extendTvInScopeList (TvSubst in_scope tenv) vars = TvSubst (extendInScopeSetList in_scope vars) tenv
extendTvSubst :: TvSubst -> TyVar -> Type -> TvSubst
extendTvSubst (TvSubst in_scope tenv) tv ty = TvSubst in_scope (extendVarEnv tenv tv ty)
extendTvSubstList :: TvSubst -> [TyVar] -> [Type] -> TvSubst
extendTvSubstList (TvSubst in_scope tenv) tvs tys
= TvSubst in_scope (extendVarEnvList tenv (tvs `zip` tys))
unionTvSubst :: TvSubst -> TvSubst -> TvSubst
unionTvSubst (TvSubst in_scope1 tenv1) (TvSubst in_scope2 tenv2)
= ASSERT( not (tenv1 `intersectsVarEnv` tenv2) )
TvSubst (in_scope1 `unionInScope` in_scope2)
(tenv1 `plusVarEnv` tenv2)
mkOpenTvSubst :: TvSubstEnv -> TvSubst
mkOpenTvSubst tenv = TvSubst (mkInScopeSet (tyVarsOfTypes (varEnvElts tenv))) tenv
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 "zipTyEnv" (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 tenv)
= brackets $ sep[ ptext (sLit "TvSubst"),
nest 2 (ptext (sLit "In scope:") <+> ppr ins),
nest 2 (ptext (sLit "Type env:") <+> ppr tenv) ]
substTyWith :: [TyVar] -> [Type] -> Type -> Type
substTyWith tvs tys = ASSERT( length tvs == length tys )
substTy (zipOpenTvSubst tvs tys)
substKiWith :: [KindVar] -> [Kind] -> Kind -> Kind
substKiWith = substTyWith
substTysWith :: [TyVar] -> [Type] -> [Type] -> [Type]
substTysWith tvs tys = ASSERT( length tvs == length tys )
substTys (zipOpenTvSubst tvs tys)
substKisWith :: [KindVar] -> [Kind] -> [Kind] -> [Kind]
substKisWith = substTysWith
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 (substTy subst) theta
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 (LitTy n) = n `seq` LitTy n
go (TyVarTy tv) = substTyVar subst tv
go (TyConApp tc tys) = let args = map go tys
in args `seqList` TyConApp tc args
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 (TvSubst _ tenv) tv
| Just ty <- lookupVarEnv tenv tv = ty
| otherwise = ASSERT( isTyVar tv ) TyVarTy tv
substTyVars :: TvSubst -> [TyVar] -> [Type]
substTyVars subst tvs = map (substTyVar subst) tvs
lookupTyVar :: TvSubst -> TyVar -> Maybe Type
lookupTyVar (TvSubst _ tenv) tv = lookupVarEnv tenv tv
substTyVarBndr :: TvSubst -> TyVar -> (TvSubst, TyVar)
substTyVarBndr subst@(TvSubst in_scope tenv) old_var
= ASSERT2( _no_capture, ppr old_var $$ ppr subst )
(TvSubst (in_scope `extendInScopeSet` new_var) new_env, new_var)
where
new_env | no_change = delVarEnv tenv old_var
| otherwise = extendVarEnv tenv old_var (TyVarTy new_var)
_no_capture = not (new_var `elemVarSet` tyVarsOfTypes (varEnvElts tenv))
old_ki = tyVarKind old_var
no_kind_change = isEmptyVarSet (tyVarsOfType old_ki)
no_change = no_kind_change && (new_var == old_var)
new_var | no_kind_change = uniqAway in_scope old_var
| otherwise = uniqAway in_scope $ updateTyVarKind (substTy subst) old_var
cloneTyVarBndr :: TvSubst -> TyVar -> Unique -> (TvSubst, TyVar)
cloneTyVarBndr (TvSubst in_scope tv_env) tv uniq
= (TvSubst (extendInScopeSet in_scope tv')
(extendVarEnv tv_env tv (mkTyVarTy tv')), tv')
where
tv' = setVarUnique tv uniq
type MetaKindVar = TyVar
type SimpleKind = Kind
typeKind :: Type -> Kind
typeKind orig_ty = go orig_ty
where
go ty@(TyConApp tc tys)
| isPromotedTyCon tc
= ASSERT( tyConArity tc == length tys ) superKind
| otherwise
= kindAppResult (ptext (sLit "typeKind 1") <+> ppr ty $$ ppr orig_ty)
(tyConKind tc) tys
go ty@(AppTy fun arg) = kindAppResult (ptext (sLit "typeKind 2") <+> ppr ty $$ ppr orig_ty)
(go fun) [arg]
go (LitTy l) = typeLiteralKind l
go (ForAllTy _ ty) = go ty
go (TyVarTy tyvar) = tyVarKind tyvar
go _ty@(FunTy _arg res)
| isSuperKind k = k
| otherwise = ASSERT2( isSubOpenTypeKind k, ppr _ty $$ ppr k ) liftedTypeKind
where
k = go res
typeLiteralKind :: TyLit -> Kind
typeLiteralKind l =
case l of
NumTyLit _ -> typeNatKind
StrTyLit _ -> typeSymbolKind