module Type (
TyThing(..), Type, VisibilityFlag(..), KindOrType, PredType, ThetaType,
Var, TyVar, isTyVar, TyCoVar, TyBinder,
mkTyVarTy, mkTyVarTys, getTyVar, getTyVar_maybe, repGetTyVar_maybe,
getCastedTyVar_maybe, tyVarKind,
mkAppTy, mkAppTys, splitAppTy, splitAppTys, repSplitAppTys,
splitAppTy_maybe, repSplitAppTy_maybe, tcRepSplitAppTy_maybe,
mkFunTy, mkFunTys, splitFunTy, splitFunTy_maybe,
splitFunTys, splitFunTysN,
funResultTy, funArgTy,
mkTyConApp, mkTyConTy,
tyConAppTyCon_maybe, tyConAppTyConPicky_maybe,
tyConAppArgs_maybe, tyConAppTyCon, tyConAppArgs,
splitTyConApp_maybe, splitTyConApp, tyConAppArgN, nextRole,
splitListTyConApp_maybe,
repSplitTyConApp_maybe,
mkForAllTy, mkForAllTys, mkInvForAllTys, mkSpecForAllTys,
mkVisForAllTys,
mkNamedForAllTy,
splitForAllTy_maybe, splitForAllTys, splitForAllTy,
splitPiTy_maybe, splitPiTys, splitPiTy,
splitNamedPiTys,
mkPiType, mkPiTypes, mkTyBindersPreferAnon,
piResultTy, piResultTys,
applyTysX, dropForAlls,
mkNumLitTy, isNumLitTy,
mkStrLitTy, isStrLitTy,
mkCastTy, mkCoercionTy, splitCastTy_maybe,
userTypeError_maybe, pprUserTypeErrorTy,
coAxNthLHS,
stripCoercionTy, splitCoercionType_maybe,
splitPiTysInvisible, filterOutInvisibleTypes,
filterOutInvisibleTyVars, partitionInvisibles,
synTyConResKind,
TyCoMapper(..), mapType, mapCoercion,
newTyConInstRhs,
mkFamilyTyConApp,
isDictLikeTy,
mkPrimEqPred, mkReprPrimEqPred, mkPrimEqPredRole,
equalityTyCon,
mkHeteroPrimEqPred, mkHeteroReprPrimEqPred,
mkClassPred,
isClassPred, isEqPred, isNomEqPred,
isIPPred, isIPPred_maybe, isIPTyCon, isIPClass,
isCTupleClass,
PredTree(..), EqRel(..), eqRelRole, classifyPredType,
getClassPredTys, getClassPredTys_maybe,
getEqPredTys, getEqPredTys_maybe, getEqPredRole,
predTypeEqRel,
sameVis,
mkNamedBinder, mkNamedBinders,
mkAnonBinder, isNamedBinder, isAnonBinder,
isIdLikeBinder, binderVisibility, binderVar_maybe,
binderVar, binderRelevantType_maybe, caseBinder,
partitionBinders, partitionBindersIntoBinders,
binderType, isVisibleBinder, isInvisibleBinder,
funTyCon,
allDistinctTyVars,
isTyVarTy, isFunTy, isDictTy, isPredTy, isVoidTy, isCoercionTy,
isCoercionTy_maybe, isCoercionType, isForAllTy,
isPiTy,
isUnliftedType, isUnboxedTupleType, isAlgType, isClosedAlgType,
isPrimitiveType, isStrictType,
isRuntimeRepTy, isRuntimeRepVar, isRuntimeRepKindedTy,
dropRuntimeRepArgs,
getRuntimeRep, getRuntimeRepFromKind,
Kind,
typeKind,
liftedTypeKind,
tyCoVarsOfType, tyCoVarsOfTypes, tyCoVarsOfTypeAcc,
tyCoVarsOfTypeDSet,
coVarsOfType,
coVarsOfTypes, closeOverKinds,
splitDepVarsOfType, splitDepVarsOfTypes,
splitVisVarsOfType, splitVisVarsOfTypes,
expandTypeSynonyms,
typeSize,
varSetElemsWellScoped, toposortTyVars, tyCoVarsOfTypeWellScoped,
tyCoVarsOfTypesWellScoped,
eqType, eqTypeX, eqTypes, cmpType, cmpTypes, cmpTypeX, cmpTypesX, cmpTc,
eqVarBndrs,
seqType, seqTypes,
coreView, coreViewOneStarKind,
UnaryType, RepType(..), flattenRepType, repType,
tyConsOfType,
typePrimRep, typeRepArity, kindPrimRep, tyConPrimRep,
TvSubstEnv,
TCvSubst(..),
emptyTvSubstEnv, emptyTCvSubst, mkEmptyTCvSubst,
mkTCvSubst, zipTvSubst, mkTvSubstPrs,
notElemTCvSubst,
getTvSubstEnv, setTvSubstEnv,
zapTCvSubst, getTCvInScope,
extendTCvInScope, extendTCvInScopeList, extendTCvInScopeSet,
extendTCvSubst, extendCvSubst,
extendTvSubst, extendTvSubstList, extendTvSubstAndInScope,
isInScope, composeTCvSubstEnv, composeTCvSubst, zipTyEnv, zipCoEnv,
isEmptyTCvSubst, unionTCvSubst,
substTy, substTys, substTyWith, substTysWith, substTheta,
substTyAddInScope,
substTyUnchecked, substTysUnchecked, substThetaUnchecked,
substTyWithBindersUnchecked, substTyWithUnchecked,
substCoUnchecked, substCoWithUnchecked,
substTyVarBndr, substTyVar, substTyVars,
cloneTyVarBndr, cloneTyVarBndrs, lookupTyVar,
pprType, pprParendType, pprTypeApp, pprTyThingCategory, pprTyThing,
pprTvBndr, pprTvBndrs, pprForAll, pprForAllImplicit, pprUserForAll,
pprSigmaType,
pprTheta, pprThetaArrowTy, pprClassPred,
pprKind, pprParendKind, pprSourceTyCon,
TyPrec(..), maybeParen,
pprTyVar, pprTcAppTy, pprPrefixApp, pprArrowChain,
tidyType, tidyTypes,
tidyOpenType, tidyOpenTypes,
tidyOpenKind,
tidyTyCoVarBndr, tidyTyCoVarBndrs, tidyFreeTyCoVars,
tidyOpenTyCoVar, tidyOpenTyCoVars,
tidyTyVarOcc,
tidyTopType,
tidyKind,
tidyTyBinder, tidyTyBinders
) where
#include "HsVersions.h"
import Kind
import TyCoRep
import Var
import VarEnv
import VarSet
import NameEnv
import Class
import TyCon
import TysPrim
import TysWiredIn ( listTyCon, typeNatKind
, typeSymbolKind, liftedTypeKind )
import PrelNames
import CoAxiom
import Coercion
import BasicTypes ( Arity, RepArity )
import Util
import Outputable
import FastString
import Pair
import ListSetOps
import Digraph
import Maybes ( orElse )
import Data.Maybe ( isJust, mapMaybe )
import Control.Monad ( guard )
import Control.Arrow ( first, second )
#if __GLASGOW_HASKELL__ < 709
import Control.Applicative ( Applicative, (<*>), (<$>), pure )
import Data.Monoid ( Monoid(..) )
import Data.Foldable ( foldMap )
#endif
coreView :: Type -> Maybe Type
coreView (TyConApp tc tys) | Just (tenv, rhs, tys') <- expandSynTyCon_maybe tc tys
= Just (mkAppTys (substTy (mkTvSubstPrs tenv) rhs) tys')
coreView _ = Nothing
coreViewOneStarKind :: Type -> Maybe Type
coreViewOneStarKind = go Nothing
where
go _ t | Just t' <- coreView t = go (Just t') t'
go _ (TyConApp tc []) | isStarKindSynonymTyCon tc = go (Just t') t'
where t' = liftedTypeKind
go res _ = res
expandTypeSynonyms :: Type -> Type
expandTypeSynonyms ty
= go (mkEmptyTCvSubst in_scope) ty
where
in_scope = mkInScopeSet (tyCoVarsOfType ty)
go subst (TyConApp tc tys)
| Just (tenv, rhs, tys') <- expandSynTyCon_maybe tc expanded_tys
= let subst' = mkTvSubst in_scope (mkVarEnv tenv)
in mkAppTys (go subst' rhs) tys'
| otherwise
= TyConApp tc expanded_tys
where
expanded_tys = (map (go subst) tys)
go _ (LitTy l) = LitTy l
go subst (TyVarTy tv) = substTyVar subst tv
go subst (AppTy t1 t2) = mkAppTy (go subst t1) (go subst t2)
go subst (ForAllTy (Anon arg) res)
= mkFunTy (go subst arg) (go subst res)
go subst (ForAllTy (Named tv vis) t)
= let (subst', tv') = substTyVarBndrCallback go subst tv in
ForAllTy (Named tv' vis) (go subst' t)
go subst (CastTy ty co) = mkCastTy (go subst ty) (go_co subst co)
go subst (CoercionTy co) = mkCoercionTy (go_co subst co)
go_co subst (Refl r ty)
= mkReflCo r (go subst ty)
go_co subst (TyConAppCo r tc args)
= mkTyConAppCo r tc (map (go_co subst) args)
go_co subst (AppCo co arg)
= mkAppCo (go_co subst co) (go_co subst arg)
go_co subst (ForAllCo tv kind_co co)
= let (subst', tv', kind_co') = go_cobndr subst tv kind_co in
mkForAllCo tv' kind_co' (go_co subst' co)
go_co subst (CoVarCo cv)
= substCoVar subst cv
go_co subst (AxiomInstCo ax ind args)
= mkAxiomInstCo ax ind (map (go_co subst) args)
go_co subst (UnivCo p r t1 t2)
= mkUnivCo (go_prov subst p) r (go subst t1) (go subst t2)
go_co subst (SymCo co)
= mkSymCo (go_co subst co)
go_co subst (TransCo co1 co2)
= mkTransCo (go_co subst co1) (go_co subst co2)
go_co subst (NthCo n co)
= mkNthCo n (go_co subst co)
go_co subst (LRCo lr co)
= mkLRCo lr (go_co subst co)
go_co subst (InstCo co arg)
= mkInstCo (go_co subst co) (go_co subst arg)
go_co subst (CoherenceCo co1 co2)
= mkCoherenceCo (go_co subst co1) (go_co subst co2)
go_co subst (KindCo co)
= mkKindCo (go_co subst co)
go_co subst (SubCo co)
= mkSubCo (go_co subst co)
go_co subst (AxiomRuleCo ax cs) = AxiomRuleCo ax (map (go_co subst) cs)
go_prov _ UnsafeCoerceProv = UnsafeCoerceProv
go_prov subst (PhantomProv co) = PhantomProv (go_co subst co)
go_prov subst (ProofIrrelProv co) = ProofIrrelProv (go_co subst co)
go_prov _ p@(PluginProv _) = p
go_prov _ (HoleProv h) = pprPanic "expandTypeSynonyms hit a hole" (ppr h)
go_cobndr subst = substForAllCoBndrCallback False (go_co subst) subst
data TyCoMapper env m
= TyCoMapper
{ tcm_smart :: Bool
, tcm_tyvar :: env -> TyVar -> m Type
, tcm_covar :: env -> CoVar -> m Coercion
, tcm_hole :: env -> CoercionHole -> Role
-> Type -> Type -> m Coercion
, tcm_tybinder :: env -> TyVar -> VisibilityFlag -> m (env, TyVar)
}
mapType :: (Applicative m, Monad m) => TyCoMapper env m -> env -> Type -> m Type
mapType mapper@(TyCoMapper { tcm_smart = smart, tcm_tyvar = tyvar
, tcm_tybinder = tybinder })
env ty
= go ty
where
go (TyVarTy tv) = tyvar env tv
go (AppTy t1 t2) = mkappty <$> go t1 <*> go t2
go t@(TyConApp _ []) = return t
go (TyConApp tc tys) = mktyconapp tc <$> mapM go tys
go (ForAllTy (Anon arg) res) = mkfunty <$> go arg <*> go res
go (ForAllTy (Named tv vis) inner)
= do { (env', tv') <- tybinder env tv vis
; inner' <- mapType mapper env' inner
; return $ ForAllTy (Named tv' vis) inner' }
go ty@(LitTy {}) = return ty
go (CastTy ty co) = mkcastty <$> go ty <*> mapCoercion mapper env co
go (CoercionTy co) = CoercionTy <$> mapCoercion mapper env co
(mktyconapp, mkappty, mkcastty, mkfunty)
| smart = (mkTyConApp, mkAppTy, mkCastTy, mkFunTy)
| otherwise = (TyConApp, AppTy, CastTy, ForAllTy . Anon)
mapCoercion :: (Applicative m, Monad m)
=> TyCoMapper env m -> env -> Coercion -> m Coercion
mapCoercion mapper@(TyCoMapper { tcm_smart = smart, tcm_covar = covar
, tcm_hole = cohole, tcm_tybinder = tybinder })
env co
= go co
where
go (Refl r ty) = Refl r <$> mapType mapper env ty
go (TyConAppCo r tc args)
= mktyconappco r tc <$> mapM go args
go (AppCo c1 c2) = mkappco <$> go c1 <*> go c2
go (ForAllCo tv kind_co co)
= do { kind_co' <- go kind_co
; (env', tv') <- tybinder env tv Invisible
; co' <- mapCoercion mapper env' co
; return $ mkforallco tv' kind_co' co' }
go (CoVarCo cv) = covar env cv
go (AxiomInstCo ax i args)
= mkaxiominstco ax i <$> mapM go args
go (UnivCo (HoleProv hole) r t1 t2)
= cohole env hole r t1 t2
go (UnivCo p r t1 t2)
= mkunivco <$> go_prov p <*> pure r
<*> mapType mapper env t1 <*> mapType mapper env t2
go (SymCo co) = mksymco <$> go co
go (TransCo c1 c2) = mktransco <$> go c1 <*> go c2
go (AxiomRuleCo r cos) = AxiomRuleCo r <$> mapM go cos
go (NthCo i co) = mknthco i <$> go co
go (LRCo lr co) = mklrco lr <$> go co
go (InstCo co arg) = mkinstco <$> go co <*> go arg
go (CoherenceCo c1 c2) = mkcoherenceco <$> go c1 <*> go c2
go (KindCo co) = mkkindco <$> go co
go (SubCo co) = mksubco <$> go co
go_prov UnsafeCoerceProv = return UnsafeCoerceProv
go_prov (PhantomProv co) = PhantomProv <$> go co
go_prov (ProofIrrelProv co) = ProofIrrelProv <$> go co
go_prov p@(PluginProv _) = return p
go_prov (HoleProv _) = panic "mapCoercion"
( mktyconappco, mkappco, mkaxiominstco, mkunivco
, mksymco, mktransco, mknthco, mklrco, mkinstco, mkcoherenceco
, mkkindco, mksubco, mkforallco)
| smart
= ( mkTyConAppCo, mkAppCo, mkAxiomInstCo, mkUnivCo
, mkSymCo, mkTransCo, mkNthCo, mkLRCo, mkInstCo, mkCoherenceCo
, mkKindCo, mkSubCo, mkForAllCo )
| otherwise
= ( TyConAppCo, AppCo, AxiomInstCo, UnivCo
, SymCo, TransCo, NthCo, LRCo, InstCo, CoherenceCo
, KindCo, SubCo, ForAllCo )
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'
| otherwise = repGetTyVar_maybe ty
getCastedTyVar_maybe :: Type -> Maybe (TyVar, Coercion)
getCastedTyVar_maybe ty | Just ty' <- coreView ty = getCastedTyVar_maybe ty'
getCastedTyVar_maybe (CastTy (TyVarTy tv) co) = Just (tv, co)
getCastedTyVar_maybe (TyVarTy tv)
= Just (tv, mkReflCo Nominal (tyVarKind tv))
getCastedTyVar_maybe _ = Nothing
repGetTyVar_maybe :: Type -> Maybe TyVar
repGetTyVar_maybe (TyVarTy tv) = Just tv
repGetTyVar_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 (ForAllTy (Anon ty1) ty2)
= Just (TyConApp funTyCon [ty1], ty2)
repSplitAppTy_maybe (AppTy ty1 ty2) = Just (ty1, ty2)
repSplitAppTy_maybe (TyConApp tc tys)
| mightBeUnsaturatedTyCon tc || tys `lengthExceeds` tyConArity tc
, Just (tys', ty') <- snocView tys
= Just (TyConApp tc tys', ty')
repSplitAppTy_maybe _other = Nothing
tcRepSplitAppTy_maybe :: Type -> Maybe (Type,Type)
tcRepSplitAppTy_maybe (ForAllTy (Anon ty1) ty2)
| isConstraintKind (typeKind ty1) = Nothing
| otherwise = Just (TyConApp funTyCon [ty1], ty2)
tcRepSplitAppTy_maybe (AppTy ty1 ty2) = Just (ty1, ty2)
tcRepSplitAppTy_maybe (TyConApp tc tys)
| mightBeUnsaturatedTyCon tc || tys `lengthExceeds` tyConArity tc
, Just (tys', ty') <- snocView tys
= Just (TyConApp tc tys', ty')
tcRepSplitAppTy_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 | mightBeUnsaturatedTyCon tc = 0
| otherwise = tyConArity tc
(tc_args1, tc_args2) = splitAt n tc_args
in
(TyConApp tc tc_args1, tc_args2 ++ args)
split _ (ForAllTy (Anon ty1) ty2) args = ASSERT( null args )
(TyConApp funTyCon [], [ty1,ty2])
split orig_ty _ args = (orig_ty, args)
repSplitAppTys :: Type -> (Type, [Type])
repSplitAppTys ty = split ty []
where
split (AppTy ty arg) args = split ty (arg:args)
split (TyConApp tc tc_args) args
= let n | mightBeUnsaturatedTyCon tc = 0
| otherwise = tyConArity tc
(tc_args1, tc_args2) = splitAt n tc_args
in
(TyConApp tc tc_args1, tc_args2 ++ args)
split (ForAllTy (Anon ty1) ty2) args = ASSERT( null args )
(TyConApp funTyCon [], [ty1, ty2])
split ty args = (ty, args)
mkNumLitTy :: Integer -> Type
mkNumLitTy n = LitTy (NumTyLit n)
isNumLitTy :: Type -> Maybe Integer
isNumLitTy ty | Just ty1 <- coreView 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 <- coreView ty = isStrLitTy ty1
isStrLitTy (LitTy (StrTyLit s)) = Just s
isStrLitTy _ = Nothing
userTypeError_maybe :: Type -> Maybe Type
userTypeError_maybe t
= do { (tc, _kind : msg : _) <- splitTyConApp_maybe t
; guard (tyConName tc == errorMessageTypeErrorFamName)
; return msg }
pprUserTypeErrorTy :: Type -> SDoc
pprUserTypeErrorTy ty =
case splitTyConApp_maybe ty of
Just (tc,[txt])
| tyConName tc == typeErrorTextDataConName
, Just str <- isStrLitTy txt -> ftext str
Just (tc,[_k,t])
| tyConName tc == typeErrorShowTypeDataConName -> ppr t
Just (tc,[t1,t2])
| tyConName tc == typeErrorAppendDataConName ->
pprUserTypeErrorTy t1 <> pprUserTypeErrorTy t2
Just (tc,[t1,t2])
| tyConName tc == typeErrorVAppendDataConName ->
pprUserTypeErrorTy t1 $$ pprUserTypeErrorTy t2
_ -> ppr ty
isFunTy :: Type -> Bool
isFunTy ty = isJust (splitFunTy_maybe ty)
splitFunTy :: Type -> (Type, Type)
splitFunTy ty | Just ty' <- coreView ty = splitFunTy ty'
splitFunTy (ForAllTy (Anon 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 (ForAllTy (Anon 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 _ (ForAllTy (Anon 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) }}
funResultTy :: Type -> Type
funResultTy ty | Just ty' <- coreView ty = funResultTy ty'
funResultTy (ForAllTy (Anon {}) res) = res
funResultTy ty = pprPanic "funResultTy" (ppr ty)
funArgTy :: Type -> Type
funArgTy ty | Just ty' <- coreView ty = funArgTy ty'
funArgTy (ForAllTy (Anon arg) _res) = arg
funArgTy ty = pprPanic "funArgTy" (ppr ty)
piResultTy :: Type -> Type -> Type
piResultTy ty arg
| Just ty' <- coreView ty = piResultTy ty' arg
| ForAllTy bndr res <- ty
= case bndr of
Anon {} -> res
Named tv _ -> substTy (extendTvSubst empty_subst tv arg) res
where
empty_subst = mkEmptyTCvSubst $ mkInScopeSet $
tyCoVarsOfTypes [arg,res]
| otherwise
= pprPanic "piResultTy" (ppr ty $$ ppr arg)
piResultTys :: Type -> [Type] -> Type
piResultTys ty [] = ty
piResultTys ty orig_args@(arg:args)
| Just ty' <- coreView ty
= piResultTys ty' orig_args
| ForAllTy bndr res <- ty
= case bndr of
Anon {} -> piResultTys res args
Named tv _ -> go (extendVarEnv emptyTvSubstEnv tv arg) res args
| otherwise
= pprPanic "piResultTys1" (ppr ty $$ ppr orig_args)
where
go :: TvSubstEnv -> Type -> [Type] -> Type
go tv_env ty [] = substTy (mkTvSubst in_scope tv_env) ty
where
in_scope = mkInScopeSet (tyCoVarsOfTypes (ty:orig_args))
go tv_env ty all_args@(arg:args)
| Just ty' <- coreView ty
= go tv_env ty' all_args
| ForAllTy bndr res <- ty
= case bndr of
Anon _ -> go tv_env res args
Named tv _ -> go (extendVarEnv tv_env tv arg) res args
| TyVarTy tv <- ty
, Just ty' <- lookupVarEnv tv_env tv
= piResultTys ty' all_args
| otherwise
= pprPanic "piResultTys2" (ppr ty $$ ppr orig_args $$ ppr all_args)
mkTyConApp :: TyCon -> [Type] -> Type
mkTyConApp tycon tys
| isFunTyCon tycon, [ty1,ty2] <- tys
= ForAllTy (Anon ty1) ty2
| otherwise
= TyConApp tycon tys
tyConAppTyConPicky_maybe :: Type -> Maybe TyCon
tyConAppTyConPicky_maybe (TyConApp tc _) = Just tc
tyConAppTyConPicky_maybe (ForAllTy (Anon _) _) = Just funTyCon
tyConAppTyConPicky_maybe _ = Nothing
tyConAppTyCon_maybe :: Type -> Maybe TyCon
tyConAppTyCon_maybe ty | Just ty' <- coreView ty = tyConAppTyCon_maybe ty'
tyConAppTyCon_maybe (TyConApp tc _) = Just tc
tyConAppTyCon_maybe (ForAllTy (Anon _) _) = 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 (ForAllTy (Anon 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 `getNth` 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 ty = repSplitTyConApp_maybe ty
repSplitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
repSplitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
repSplitTyConApp_maybe (ForAllTy (Anon arg) res) = Just (funTyCon, [arg,res])
repSplitTyConApp_maybe _ = Nothing
splitListTyConApp_maybe :: Type -> Maybe Type
splitListTyConApp_maybe ty = case splitTyConApp_maybe ty of
Just (tc,[e]) | tc == listTyCon -> Just e
_other -> 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
splitCastTy_maybe :: Type -> Maybe (Type, Coercion)
splitCastTy_maybe ty | Just ty' <- coreView ty = splitCastTy_maybe ty'
splitCastTy_maybe (CastTy ty co) = Just (ty, co)
splitCastTy_maybe _ = Nothing
mkCastTy :: Type -> Coercion -> Type
mkCastTy ty co | isReflexiveCo co = ty
mkCastTy (CastTy ty co1) co2 = mkCastTy ty (co1 `mkTransCo` co2)
mkCastTy outer_ty@(ForAllTy (Named tv vis) inner_ty) co
=
let fvs = tyCoVarsOfCo co `unionVarSet` tyCoVarsOfType outer_ty
empty_subst = mkEmptyTCvSubst (mkInScopeSet fvs)
(subst, tv') = substTyVarBndr empty_subst tv
in
ForAllTy (Named tv' vis) (substTy subst inner_ty `mkCastTy` co)
mkCastTy ty co =
let result = split_apps [] ty co in
ASSERT2( CastTy ty co `eqType` result
, ppr ty <+> dcolon <+> ppr (typeKind ty) $$
ppr co <+> dcolon <+> ppr (coercionKind co) $$
ppr result <+> dcolon <+> ppr (typeKind result) )
result
where
split_apps args (AppTy t1 t2) co
= split_apps (t2:args) t1 co
split_apps args (TyConApp tc tc_args) co
| mightBeUnsaturatedTyCon tc
= affix_co (tyConBinders tc) (mkTyConTy tc) (tc_args `chkAppend` args) co
| otherwise
= let (non_decomp_args, decomp_args) = splitAt (tyConArity tc) tc_args
saturated_tc = mkTyConApp tc non_decomp_args
in
affix_co (fst $ splitPiTys $ typeKind saturated_tc)
saturated_tc (decomp_args `chkAppend` args) co
split_apps args (ForAllTy (Anon arg) res) co
= affix_co (tyConBinders funTyCon) (mkTyConTy funTyCon)
(arg : res : args) co
split_apps args ty co
= affix_co (fst $ splitPiTys $ typeKind ty)
ty args co
affix_co _ ty [] co = no_double_casts ty co
affix_co bndrs ty args co
= let (no_dep_bndrs, some_dep_bndrs) = spanEnd isAnonBinder bndrs
(some_dep_args, rest_args) = splitAtList some_dep_bndrs args
dep_subst = zipTyBinderSubst some_dep_bndrs some_dep_args
used_no_dep_bndrs = takeList rest_args no_dep_bndrs
rest_arg_tys = substTys dep_subst (map binderType used_no_dep_bndrs)
co' = mkFunCos Nominal
(map (mkReflCo Nominal) rest_arg_tys)
co
in
((ty `mkAppTys` some_dep_args) `no_double_casts` co') `mkAppTys` rest_args
no_double_casts (CastTy ty co1) co2 = CastTy ty (co1 `mkTransCo` co2)
no_double_casts ty co = CastTy ty co
mkCoercionTy :: Coercion -> Type
mkCoercionTy = CoercionTy
isCoercionTy :: Type -> Bool
isCoercionTy (CoercionTy _) = True
isCoercionTy _ = False
isCoercionTy_maybe :: Type -> Maybe Coercion
isCoercionTy_maybe (CoercionTy co) = Just co
isCoercionTy_maybe _ = Nothing
stripCoercionTy :: Type -> Coercion
stripCoercionTy (CoercionTy co) = co
stripCoercionTy ty = pprPanic "stripCoercionTy" (ppr ty)
type UnaryType = Type
data RepType = UbxTupleRep [UnaryType]
| UnaryRep UnaryType
instance Outputable RepType where
ppr (UbxTupleRep tys) = text "UbxTupleRep" <+> ppr tys
ppr (UnaryRep ty) = text "UnaryRep" <+> ppr ty
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 (Named {}) ty2)
= go rec_nts ty2
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) non_rr_tys)
where
non_rr_tys = dropRuntimeRepArgs tys
go rec_nts (CastTy ty _)
= go rec_nts ty
go _ ty@(CoercionTy _)
= pprPanic "repType" (ppr ty)
go _ ty = UnaryRep ty
typePrimRep :: UnaryType -> PrimRep
typePrimRep ty = kindPrimRep (typeKind ty)
tyConPrimRep :: TyCon -> PrimRep
tyConPrimRep tc = kindPrimRep res_kind
where
res_kind = tyConResKind tc
kindPrimRep :: Kind -> PrimRep
kindPrimRep ki | Just ki' <- coreViewOneStarKind ki = kindPrimRep ki'
kindPrimRep (TyConApp typ [runtime_rep])
= ASSERT( typ `hasKey` tYPETyConKey )
go runtime_rep
where
go rr | Just rr' <- coreView rr = go rr'
go (TyConApp rr_dc args)
| RuntimeRep fun <- tyConRuntimeRepInfo rr_dc
= fun args
go rr = pprPanic "kindPrimRep.go" (ppr rr)
kindPrimRep ki = WARN( True
, text "kindPrimRep defaulting to PtrRep on" <+> ppr ki )
PtrRep
typeRepArity :: Arity -> Type -> RepArity
typeRepArity 0 _ = 0
typeRepArity n ty = case repType ty of
UnaryRep (ForAllTy bndr ty) -> length (flattenRepType (repType (binderType bndr))) + typeRepArity (n 1) ty
_ -> pprPanic "typeRepArity: arity greater than type can handle" (ppr (n, ty, repType ty))
isVoidTy :: Type -> Bool
isVoidTy ty = case repType ty of
UnaryRep (TyConApp tc _) -> isUnliftedTyCon tc &&
isVoidRep (tyConPrimRep tc)
_ -> False
mkForAllTy :: TyBinder -> Type -> Type
mkForAllTy = ForAllTy
mkNamedForAllTy :: TyVar -> VisibilityFlag -> Type -> Type
mkNamedForAllTy tv vis = ASSERT( isTyVar tv )
ForAllTy (Named tv vis)
mkInvForAllTys :: [TyVar] -> Type -> Type
mkInvForAllTys tvs = ASSERT( all isTyVar tvs )
mkForAllTys (map (flip Named Invisible) tvs)
mkSpecForAllTys :: [TyVar] -> Type -> Type
mkSpecForAllTys tvs = ASSERT( all isTyVar tvs )
mkForAllTys (map (flip Named Specified) tvs)
mkVisForAllTys :: [TyVar] -> Type -> Type
mkVisForAllTys tvs = ASSERT( all isTyVar tvs )
mkForAllTys (map (flip Named Visible) tvs)
mkPiType :: Var -> Type -> Type
mkPiTypes :: [Var] -> Type -> Type
mkPiType v ty
| isTyVar v = mkForAllTy (Named v Invisible) ty
| otherwise = mkForAllTy (Anon (varType v)) ty
mkPiTypes vs ty = foldr mkPiType ty vs
mkTyBindersPreferAnon :: [TyVar] -> Type -> [TyBinder]
mkTyBindersPreferAnon vars inner_ty = fst $ go vars inner_ty
where
go :: [TyVar] -> Type -> ([TyBinder], VarSet)
go [] ty = ([], tyCoVarsOfType ty)
go (v:vs) ty | v `elemVarSet` fvs
= ( Named v Visible : binders
, fvs `delVarSet` v `unionVarSet` kind_vars )
| otherwise
= ( Anon (tyVarKind v) : binders
, fvs `unionVarSet` kind_vars )
where
(binders, fvs) = go vs ty
kind_vars = tyCoVarsOfType $ tyVarKind v
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 (Named tv _) ty) tvs = split ty ty (tv:tvs)
split orig_ty _ tvs = (reverse tvs, orig_ty)
splitPiTys :: Type -> ([TyBinder], Type)
splitPiTys ty = split ty ty []
where
split orig_ty ty bs | Just ty' <- coreView ty = split orig_ty ty' bs
split _ (ForAllTy b res) bs = split res res (b:bs)
split orig_ty _ bs = (reverse bs, orig_ty)
splitNamedPiTys :: Type -> ([TyBinder], Type)
splitNamedPiTys ty = split ty ty []
where
split orig_ty ty bs | Just ty' <- coreView ty = split orig_ty ty' bs
split _ (ForAllTy b@(Named {}) res) bs = split res res (b:bs)
split orig_ty _ bs = (reverse bs, orig_ty)
isForAllTy :: Type -> Bool
isForAllTy (ForAllTy (Named {}) _) = True
isForAllTy _ = False
isPiTy :: Type -> Bool
isPiTy (ForAllTy {}) = True
isPiTy _ = False
splitForAllTy :: Type -> (TyVar, Type)
splitForAllTy ty
| Just answer <- splitForAllTy_maybe ty = answer
| otherwise = pprPanic "splitForAllTy" (ppr ty)
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 (Named tv _) ty) = Just (tv, ty)
splitFAT_m _ = Nothing
splitPiTy_maybe :: Type -> Maybe (TyBinder, Type)
splitPiTy_maybe ty = go ty
where
go ty | Just ty' <- coreView ty = go ty'
go (ForAllTy bndr ty) = Just (bndr, ty)
go _ = Nothing
splitPiTy :: Type -> (TyBinder, Type)
splitPiTy ty
| Just answer <- splitPiTy_maybe ty = answer
| otherwise = pprPanic "splitPiTy" (ppr ty)
dropForAlls :: Type -> Type
dropForAlls ty | Just ty' <- coreView ty = dropForAlls ty'
| otherwise = go ty
where
go (ForAllTy (Named {}) res) = go res
go res = res
filterOutInvisibleTypes :: TyCon -> [Type] -> [Type]
filterOutInvisibleTypes tc tys = snd $ partitionInvisibles tc id tys
filterOutInvisibleTyVars :: TyCon -> [TyVar] -> [TyVar]
filterOutInvisibleTyVars tc tvs = snd $ partitionInvisibles tc mkTyVarTy tvs
partitionInvisibles :: TyCon -> (a -> Type) -> [a] -> ([a], [a])
partitionInvisibles tc get_ty = go emptyTCvSubst (tyConKind tc)
where
go _ _ [] = ([], [])
go subst (ForAllTy bndr res_ki) (x:xs)
| isVisibleBinder bndr = second (x :) (go subst' res_ki xs)
| otherwise = first (x :) (go subst' res_ki xs)
where
subst' = extendTvSubstBinder subst bndr (get_ty x)
go subst (TyVarTy tv) xs
| Just ki <- lookupTyVar subst tv = go subst ki xs
go _ _ xs = ([], xs)
splitPiTysInvisible :: Type -> ([TyBinder], Type)
splitPiTysInvisible ty = split ty ty []
where
split orig_ty ty bndrs
| Just ty' <- coreView ty = split orig_ty ty' bndrs
split _ (ForAllTy bndr ty) bndrs
| isInvisibleBinder bndr
= split ty ty (bndr:bndrs)
split orig_ty _ bndrs
= (reverse bndrs, orig_ty)
applyTysX :: [TyVar] -> Type -> [Type] -> Type
applyTysX tvs body_ty arg_tys
= ASSERT2( length arg_tys >= n_tvs, pp_stuff )
ASSERT2( tyCoVarsOfType body_ty `subVarSet` mkVarSet tvs, pp_stuff )
mkAppTys (substTyWith tvs (take n_tvs arg_tys) body_ty)
(drop n_tvs arg_tys)
where
pp_stuff = vcat [ppr tvs, ppr body_ty, ppr arg_tys]
n_tvs = length tvs
mkNamedBinder :: VisibilityFlag -> Var -> TyBinder
mkNamedBinder vis var = Named var vis
mkNamedBinders :: VisibilityFlag -> [TyVar] -> [TyBinder]
mkNamedBinders vis = map (mkNamedBinder vis)
mkAnonBinder :: Type -> TyBinder
mkAnonBinder = Anon
isIdLikeBinder :: TyBinder -> Bool
isIdLikeBinder (Named {}) = False
isIdLikeBinder (Anon {}) = True
isVisibleType :: Type -> Bool
isVisibleType = not . isPredTy
binderVisibility :: TyBinder -> VisibilityFlag
binderVisibility (Named _ vis) = vis
binderVisibility (Anon ty)
| isVisibleType ty = Visible
| otherwise = Invisible
binderVar_maybe :: TyBinder -> Maybe Var
binderVar_maybe (Named v _) = Just v
binderVar_maybe (Anon {}) = Nothing
binderVar :: String
-> TyBinder -> Var
binderVar _ (Named v _) = v
binderVar e (Anon t) = pprPanic ("binderVar (" ++ e ++ ")") (ppr t)
binderRelevantType_maybe :: TyBinder -> Maybe Type
binderRelevantType_maybe (Named {}) = Nothing
binderRelevantType_maybe (Anon ty) = Just ty
caseBinder :: TyBinder
-> (TyVar -> a)
-> (Type -> a)
-> a
caseBinder (Named v _) f _ = f v
caseBinder (Anon t) _ d = d t
partitionBinders :: [TyBinder] -> ([TyVar], [Type])
partitionBinders = partitionWith named_or_anon
where
named_or_anon bndr = caseBinder bndr Left Right
partitionBindersIntoBinders :: [TyBinder] -> ([TyBinder], [Type])
partitionBindersIntoBinders = partitionWith named_or_anon
where
named_or_anon bndr = caseBinder bndr (\_ -> Left bndr) Right
isPredTy :: Type -> Bool
isPredTy ty = go ty []
where
go :: Type -> [KindOrType] -> Bool
go (AppTy ty1 ty2) args = go ty1 (ty2 : args)
go (TyVarTy tv) args = go_k (tyVarKind tv) args
go (TyConApp tc tys) args = ASSERT( null args )
go_tc tc tys
go (ForAllTy (Anon arg) res) []
| isPredTy arg = isPredTy res
| otherwise = False
go (ForAllTy (Named {}) ty) [] = go ty []
go _ _ = False
go_tc :: TyCon -> [KindOrType] -> Bool
go_tc tc args
| tc `hasKey` eqPrimTyConKey || tc `hasKey` eqReprPrimTyConKey
= length args == 4
| otherwise = go_k (tyConKind tc) args
go_k :: Kind -> [KindOrType] -> Bool
go_k k args = isConstraintKind (piResultTys k args)
isClassPred, isEqPred, isNomEqPred, 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` eqPrimTyConKey
|| tyCon `hasKey` eqReprPrimTyConKey
_ -> False
isNomEqPred ty = case tyConAppTyCon_maybe ty of
Just tyCon -> tyCon `hasKey` eqPrimTyConKey
_ -> False
isIPPred ty = case tyConAppTyCon_maybe ty of
Just tc -> isIPTyCon tc
_ -> False
isIPTyCon :: TyCon -> Bool
isIPTyCon tc = tc `hasKey` ipClassKey
isIPClass :: Class -> Bool
isIPClass cls = cls `hasKey` ipClassKey
isCTupleClass :: Class -> Bool
isCTupleClass cls = isTupleTyCon (classTyCon cls)
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)
mkPrimEqPredRole :: Role -> Type -> Type -> PredType
mkPrimEqPredRole Nominal = mkPrimEqPred
mkPrimEqPredRole Representational = mkReprPrimEqPred
mkPrimEqPredRole Phantom = panic "mkPrimEqPredRole phantom"
mkPrimEqPred :: Type -> Type -> Type
mkPrimEqPred ty1 ty2
= TyConApp eqPrimTyCon [k1, k2, ty1, ty2]
where
k1 = typeKind ty1
k2 = typeKind ty2
mkHeteroPrimEqPred :: Kind -> Kind -> Type -> Type -> Type
mkHeteroPrimEqPred k1 k2 ty1 ty2 = TyConApp eqPrimTyCon [k1, k2, ty1, ty2]
mkHeteroReprPrimEqPred :: Kind -> Kind -> Type -> Type -> Type
mkHeteroReprPrimEqPred k1 k2 ty1 ty2
= TyConApp eqReprPrimTyCon [k1, k2, ty1, ty2]
splitCoercionType_maybe :: Type -> Maybe (Type, Type)
splitCoercionType_maybe ty
= do { (tc, [_, _, ty1, ty2]) <- splitTyConApp_maybe ty
; guard $ tc `hasKey` eqPrimTyConKey || tc `hasKey` eqReprPrimTyConKey
; return (ty1, ty2) }
mkReprPrimEqPred :: Type -> Type -> Type
mkReprPrimEqPred ty1 ty2
= TyConApp eqReprPrimTyCon [k1, k2, ty1, ty2]
where
k1 = typeKind ty1
k2 = typeKind ty2
equalityTyCon :: Role -> TyCon
equalityTyCon Nominal = eqPrimTyCon
equalityTyCon Representational = eqReprPrimTyCon
equalityTyCon Phantom = eqPhantPrimTyCon
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
| IrredPred PredType
classifyPredType :: PredType -> PredTree
classifyPredType ev_ty = case splitTyConApp_maybe ev_ty of
Just (tc, [_, _, ty1, ty2])
| tc `hasKey` eqReprPrimTyConKey -> EqPred ReprEq ty1 ty2
| tc `hasKey` eqPrimTyConKey -> EqPred NomEq ty1 ty2
Just (tc, tys)
| Just clas <- tyConClass_maybe tc -> ClassPred clas 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])
| tc `hasKey` eqPrimTyConKey
|| tc `hasKey` eqReprPrimTyConKey
-> (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` eqPrimTyConKey -> Just (Nominal, ty1, ty2)
| tc `hasKey` eqReprPrimTyConKey -> Just (Representational, ty1, ty2)
_ -> Nothing
getEqPredRole :: PredType -> Role
getEqPredRole ty = eqRelRole (predTypeEqRel ty)
predTypeEqRel :: PredType -> EqRel
predTypeEqRel ty
| Just (tc, _) <- splitTyConApp_maybe ty
, tc `hasKey` eqReprPrimTyConKey
= ReprEq
| otherwise
= NomEq
typeSize :: Type -> Int
typeSize (LitTy {}) = 1
typeSize (TyVarTy {}) = 1
typeSize (AppTy t1 t2) = typeSize t1 + typeSize t2
typeSize (ForAllTy b t) = typeSize (binderType b) + typeSize t
typeSize (TyConApp _ ts) = 1 + sum (map typeSize ts)
typeSize (CastTy ty co) = typeSize ty + coercionSize co
typeSize (CoercionTy co) = coercionSize co
toposortTyVars :: [TyVar] -> [TyVar]
toposortTyVars tvs = reverse $
[ tv | (tv, _, _) <- topologicalSortG $
graphFromEdgedVertices nodes ]
where
var_ids :: VarEnv Int
var_ids = mkVarEnv (zip tvs [1..])
nodes = [ ( tv
, lookupVarEnv_NF var_ids tv
, mapMaybe (lookupVarEnv var_ids)
(tyCoVarsOfTypeList (tyVarKind tv)) )
| tv <- tvs ]
varSetElemsWellScoped :: VarSet -> [Var]
varSetElemsWellScoped = toposortTyVars . varSetElems
tyCoVarsOfTypeWellScoped :: Type -> [TyVar]
tyCoVarsOfTypeWellScoped = toposortTyVars . tyCoVarsOfTypeList
tyCoVarsOfTypesWellScoped :: [Type] -> [TyVar]
tyCoVarsOfTypesWellScoped = toposortTyVars . tyCoVarsOfTypesList
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 )
zipTvSubst 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 (Named {}) ty) = isUnliftedType ty
isUnliftedType (TyConApp tc _) = isUnliftedTyCon tc
isUnliftedType _ = False
getRuntimeRep :: String
-> Type -> Type
getRuntimeRep err ty = getRuntimeRepFromKind err (typeKind ty)
getRuntimeRepFromKind :: String
-> Type -> Type
getRuntimeRepFromKind err = go
where
go k | Just k' <- coreViewOneStarKind k = go k'
go k
| Just (tc, [arg]) <- splitTyConApp_maybe k
, tc `hasKey` tYPETyConKey
= arg
go k = pprPanic "getRuntimeRep" (text err $$
ppr k <+> dcolon <+> ppr (typeKind k))
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 (TyConApp tc tys) = tc `seq` seqTypes tys
seqType (ForAllTy bndr ty) = seqType (binderType bndr) `seq` seqType ty
seqType (CastTy ty co) = seqType ty `seq` seqCo co
seqType (CoercionTy co) = seqCo co
seqTypes :: [Type] -> ()
seqTypes [] = ()
seqTypes (ty:tys) = seqType ty `seq` seqTypes tys
eqType :: Type -> Type -> Bool
eqType t1 t2 = isEqual $ cmpType t1 t2
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
eqVarBndrs :: RnEnv2 -> [Var] -> [Var] -> Maybe RnEnv2
eqVarBndrs env [] []
= Just env
eqVarBndrs env (tv1:tvs1) (tv2:tvs2)
| eqTypeX env (tyVarKind tv1) (tyVarKind tv2)
= eqVarBndrs (rnBndr2 env tv1 tv2) tvs1 tvs2
eqVarBndrs _ _ _= Nothing
cmpType :: Type -> Type -> Ordering
cmpType t1 t2
= cmpTypeX rn_env t1 t2
where
rn_env = mkRnEnv2 (mkInScopeSet (tyCoVarsOfTypes [t1, t2]))
cmpTypes :: [Type] -> [Type] -> Ordering
cmpTypes ts1 ts2 = cmpTypesX rn_env ts1 ts2
where
rn_env = mkRnEnv2 (mkInScopeSet (tyCoVarsOfTypes (ts1 ++ ts2)))
data TypeOrdering = TLT
| TEQ
| TEQX
| TGT
deriving (Eq, Ord, Enum, Bounded)
cmpTypeX :: RnEnv2 -> Type -> Type -> Ordering
cmpTypeX env orig_t1 orig_t2 =
case go env orig_t1 orig_t2 of
TEQX -> toOrdering $ go env k1 k2
ty_ordering -> toOrdering ty_ordering
where
k1 = typeKind orig_t1
k2 = typeKind orig_t2
toOrdering :: TypeOrdering -> Ordering
toOrdering TLT = LT
toOrdering TEQ = EQ
toOrdering TEQX = EQ
toOrdering TGT = GT
liftOrdering :: Ordering -> TypeOrdering
liftOrdering LT = TLT
liftOrdering EQ = TEQ
liftOrdering GT = TGT
thenCmpTy :: TypeOrdering -> TypeOrdering -> TypeOrdering
thenCmpTy TEQ rel = rel
thenCmpTy TEQX rel = hasCast rel
thenCmpTy rel _ = rel
hasCast :: TypeOrdering -> TypeOrdering
hasCast TEQ = TEQX
hasCast rel = rel
go :: RnEnv2 -> Type -> Type -> TypeOrdering
go env t1 t2
| Just t1' <- coreViewOneStarKind t1 = go env t1' t2
| Just t2' <- coreViewOneStarKind t2 = go env t1 t2'
go env (TyVarTy tv1) (TyVarTy tv2)
= liftOrdering $ rnOccL env tv1 `compare` rnOccR env tv2
go env (ForAllTy (Named tv1 _) t1) (ForAllTy (Named tv2 _) t2)
= go env (tyVarKind tv1) (tyVarKind tv2)
`thenCmpTy` go (rnBndr2 env tv1 tv2) t1 t2
go env (AppTy s1 t1) ty2
| Just (s2, t2) <- repSplitAppTy_maybe ty2
= go env s1 s2 `thenCmpTy` go env t1 t2
go env ty1 (AppTy s2 t2)
| Just (s1, t1) <- repSplitAppTy_maybe ty1
= go env s1 s2 `thenCmpTy` go env t1 t2
go env (ForAllTy (Anon s1) t1) (ForAllTy (Anon s2) t2)
= go env s1 s2 `thenCmpTy` go env t1 t2
go env (TyConApp tc1 tys1) (TyConApp tc2 tys2)
= liftOrdering (tc1 `cmpTc` tc2) `thenCmpTy` gos env tys1 tys2
go _ (LitTy l1) (LitTy l2) = liftOrdering (compare l1 l2)
go env (CastTy t1 _) t2 = hasCast $ go env t1 t2
go env t1 (CastTy t2 _) = hasCast $ go env t1 t2
go _ (CoercionTy {}) (CoercionTy {}) = TEQ
go _ ty1 ty2
= liftOrdering $ (get_rank ty1) `compare` (get_rank ty2)
where get_rank :: Type -> Int
get_rank (CastTy {})
= pprPanic "cmpTypeX.get_rank" (ppr [ty1,ty2])
get_rank (TyVarTy {}) = 0
get_rank (CoercionTy {}) = 1
get_rank (AppTy {}) = 3
get_rank (LitTy {}) = 4
get_rank (TyConApp {}) = 5
get_rank (ForAllTy (Anon {}) _) = 6
get_rank (ForAllTy (Named {}) _) = 7
gos :: RnEnv2 -> [Type] -> [Type] -> TypeOrdering
gos _ [] [] = TEQ
gos _ [] _ = TLT
gos _ _ [] = TGT
gos env (ty1:tys1) (ty2:tys2) = go env ty1 ty2 `thenCmpTy` gos env tys1 tys2
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
= ASSERT( not (isStarKindSynonymTyCon tc1) && not (isStarKindSynonymTyCon tc2) )
u1 `compare` u2
where
u1 = tyConUnique tc1
u2 = tyConUnique tc2
typeKind :: Type -> Kind
typeKind (TyConApp tc tys) = piResultTys (tyConKind tc) tys
typeKind (AppTy fun arg) = piResultTy (typeKind fun) arg
typeKind (LitTy l) = typeLiteralKind l
typeKind (ForAllTy (Anon _) _) = liftedTypeKind
typeKind (ForAllTy _ ty) = typeKind ty
typeKind (TyVarTy tyvar) = tyVarKind tyvar
typeKind (CastTy _ty co) = pSnd $ coercionKind co
typeKind (CoercionTy co) = coercionType co
typeLiteralKind :: TyLit -> Kind
typeLiteralKind l =
case l of
NumTyLit _ -> typeNatKind
StrTyLit _ -> typeSymbolKind
pprTyVar :: TyVar -> SDoc
pprTyVar tv = ppr tv <+> dcolon <+> ppr (tyVarKind tv)
tyConsOfType :: Type -> NameEnv TyCon
tyConsOfType ty
= go ty
where
go :: Type -> NameEnv TyCon
go ty | Just ty' <- coreView ty = go ty'
go (TyVarTy {}) = emptyNameEnv
go (LitTy {}) = emptyNameEnv
go (TyConApp tc tys) = go_tc tc `plusNameEnv` go_s tys
go (AppTy a b) = go a `plusNameEnv` go b
go (ForAllTy (Anon a) b) = go a `plusNameEnv` go b `plusNameEnv` go_tc funTyCon
go (ForAllTy (Named tv _) ty) = go ty `plusNameEnv` go (tyVarKind tv)
go (CastTy ty co) = go ty `plusNameEnv` go_co co
go (CoercionTy co) = go_co co
go_co (Refl _ ty) = go ty
go_co (TyConAppCo _ tc args) = go_tc tc `plusNameEnv` go_cos args
go_co (AppCo co arg) = go_co co `plusNameEnv` go_co arg
go_co (ForAllCo _ kind_co co) = go_co kind_co `plusNameEnv` go_co co
go_co (CoVarCo {}) = emptyNameEnv
go_co (AxiomInstCo ax _ args) = go_ax ax `plusNameEnv` go_cos args
go_co (UnivCo p _ t1 t2) = go_prov p `plusNameEnv` go t1 `plusNameEnv` go t2
go_co (SymCo co) = go_co co
go_co (TransCo co1 co2) = go_co co1 `plusNameEnv` go_co co2
go_co (NthCo _ co) = go_co co
go_co (LRCo _ co) = go_co co
go_co (InstCo co arg) = go_co co `plusNameEnv` go_co arg
go_co (CoherenceCo co1 co2) = go_co co1 `plusNameEnv` go_co co2
go_co (KindCo co) = go_co co
go_co (SubCo co) = go_co co
go_co (AxiomRuleCo _ cs) = go_cos cs
go_prov UnsafeCoerceProv = emptyNameEnv
go_prov (PhantomProv co) = go_co co
go_prov (ProofIrrelProv co) = go_co co
go_prov (PluginProv _) = emptyNameEnv
go_prov (HoleProv _) = emptyNameEnv
go_s tys = foldr (plusNameEnv . go) emptyNameEnv tys
go_cos cos = foldr (plusNameEnv . go_co) emptyNameEnv cos
go_tc tc = unitNameEnv (tyConName tc) tc
go_ax ax = go_tc $ coAxiomTyCon ax
synTyConResKind :: TyCon -> Kind
synTyConResKind tycon = piResultTys (tyConKind tycon) (mkTyVarTys (tyConTyVars tycon))
splitDepVarsOfType :: Type -> Pair TyCoVarSet
splitDepVarsOfType ty = Pair dep_vars final_nondep_vars
where
Pair dep_vars nondep_vars = split_dep_vars ty
final_nondep_vars = nondep_vars `minusVarSet` dep_vars
splitDepVarsOfTypes :: [Type] -> Pair TyCoVarSet
splitDepVarsOfTypes tys = Pair dep_vars final_nondep_vars
where
Pair dep_vars nondep_vars = foldMap split_dep_vars tys
final_nondep_vars = nondep_vars `minusVarSet` dep_vars
split_dep_vars :: Type -> Pair TyCoVarSet
split_dep_vars = go
where
go (TyVarTy tv) = Pair (tyCoVarsOfType $ tyVarKind tv)
(unitVarSet tv)
go (AppTy t1 t2) = go t1 `mappend` go t2
go (TyConApp _ tys) = foldMap go tys
go (ForAllTy (Anon arg) res) = go arg `mappend` go res
go (ForAllTy (Named tv _) ty)
= let Pair kvs tvs = go ty in
Pair (kvs `delVarSet` tv `unionVarSet` tyCoVarsOfType (tyVarKind tv))
(tvs `delVarSet` tv)
go (LitTy {}) = mempty
go (CastTy ty co) = go ty `mappend` Pair (tyCoVarsOfCo co)
emptyVarSet
go (CoercionTy co) = go_co co
go_co co = let Pair ty1 ty2 = coercionKind co in
go ty1 `mappend` go ty2
splitVisVarsOfType :: Type -> Pair TyCoVarSet
splitVisVarsOfType orig_ty = Pair invis_vars vis_vars
where
Pair invis_vars1 vis_vars = go orig_ty
invis_vars = invis_vars1 `minusVarSet` vis_vars
go (TyVarTy tv) = Pair (tyCoVarsOfType $ tyVarKind tv) (unitVarSet tv)
go (AppTy t1 t2) = go t1 `mappend` go t2
go (TyConApp tc tys) = go_tc tc tys
go (ForAllTy (Anon t1) t2) = go t1 `mappend` go t2
go (ForAllTy (Named tv _) ty)
= ((`delVarSet` tv) <$> go ty) `mappend`
(invisible (tyCoVarsOfType $ tyVarKind tv))
go (LitTy {}) = mempty
go (CastTy ty co) = go ty `mappend` invisible (tyCoVarsOfCo co)
go (CoercionTy co) = invisible $ tyCoVarsOfCo co
invisible vs = Pair vs emptyVarSet
go_tc tc tys = let (invis, vis) = partitionInvisibles tc id tys in
invisible (tyCoVarsOfTypes invis) `mappend` foldMap go vis
splitVisVarsOfTypes :: [Type] -> Pair TyCoVarSet
splitVisVarsOfTypes = foldMap splitVisVarsOfType