{-# LANGUAGE FlexibleContexts, PatternSynonyms, ViewPatterns, MultiWayIf #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module GHC.Core.Type (
Type, ForAllTyFlag(..), FunTyFlag(..),
Specificity(..),
KindOrType, PredType, ThetaType, FRRType,
Var, TyVar, isTyVar, TyCoVar, PiTyBinder, ForAllTyBinder, TyVarBinder,
Mult, Scaled,
KnotTied, RuntimeRepType,
mkTyVarTy, mkTyVarTys, getTyVar, getTyVar_maybe, repGetTyVar_maybe,
getCastedTyVar_maybe, tyVarKind, varType,
mkAppTy, mkAppTys, splitAppTy, splitAppTys, splitAppTysNoView,
splitAppTy_maybe, splitAppTyNoView_maybe, tcSplitAppTyNoView_maybe,
mkFunTy, mkVisFunTy,
mkVisFunTyMany, mkVisFunTysMany,
mkScaledFunTys,
mkInvisFunTy, mkInvisFunTys,
tcMkVisFunTy, tcMkScaledFunTys, tcMkInvisFunTy,
splitFunTy, splitFunTy_maybe,
splitFunTys, funResultTy, funArgTy,
funTyConAppTy_maybe, funTyFlagTyCon,
tyConAppFunTy_maybe, tyConAppFunCo_maybe,
mkFunctionType, mkScaledFunctionTys, chooseFunTyFlag,
mkTyConApp, mkTyConTy,
tyConAppTyCon_maybe, tyConAppTyConPicky_maybe,
tyConAppArgs_maybe, tyConAppTyCon, tyConAppArgs,
splitTyConApp_maybe, splitTyConAppNoView_maybe, splitTyConApp,
tcSplitTyConApp, tcSplitTyConApp_maybe,
mkForAllTy, mkForAllTys, mkInvisForAllTys, mkTyCoInvForAllTys,
mkSpecForAllTy, mkSpecForAllTys,
mkVisForAllTys, mkTyCoInvForAllTy,
mkInfForAllTy, mkInfForAllTys,
splitForAllTyCoVars, splitForAllTyVars,
splitForAllReqTyBinders, splitForAllInvisTyBinders,
splitForAllForAllTyBinders,
splitForAllTyCoVar_maybe, splitForAllTyCoVar,
splitForAllTyVar_maybe, splitForAllCoVar_maybe,
splitPiTy_maybe, splitPiTy, splitPiTys,
getRuntimeArgTys,
mkTyConBindersPreferAnon,
mkPiTy, mkPiTys,
piResultTy, piResultTys,
applyTysX, dropForAlls,
mkFamilyTyConApp,
buildSynTyCon,
mkNumLitTy, isNumLitTy,
mkStrLitTy, isStrLitTy,
mkCharLitTy, isCharLitTy,
isLitTy,
isPredTy,
getRuntimeRep, splitRuntimeRep_maybe, kindRep_maybe, kindRep,
getLevity, levityType_maybe,
mkCastTy, mkCoercionTy, splitCastTy_maybe,
userTypeError_maybe, pprUserTypeErrorTy,
coAxNthLHS,
stripCoercionTy,
splitInvisPiTys, splitInvisPiTysN,
invisibleTyBndrCount,
filterOutInvisibleTypes, filterOutInferredTypes,
partitionInvisibleTypes, partitionInvisibles,
tyConForAllTyFlags, appTyForAllTyFlags,
TyCoMapper(..), mapTyCo, mapTyCoX,
TyCoFolder(..), foldTyCo, noView,
newTyConInstRhs,
mkForAllTyBinder, mkForAllTyBinders,
mkTyVarBinder, mkTyVarBinders,
tyVarSpecToBinders,
isAnonPiTyBinder,
binderVar, binderVars, binderType, binderFlag, binderFlags,
piTyBinderType, namedPiTyBinder_maybe,
anonPiTyBinderType_maybe,
isVisibleForAllTyFlag, isInvisibleForAllTyFlag, isVisiblePiTyBinder,
isInvisiblePiTyBinder, isNamedPiTyBinder,
tyConBindersPiTyBinders,
isTyVarTy, isFunTy, isCoercionTy,
isCoercionTy_maybe, isForAllTy,
isForAllTy_ty, isForAllTy_co,
isPiTy, isTauTy, isFamFreeTy,
isCoVarType, isAtomicTy,
isValidJoinPointType,
tyConAppNeedsKindSig,
mkTYPEapp, mkTYPEapp_maybe,
mkCONSTRAINTapp, mkCONSTRAINTapp_maybe,
mkBoxedRepApp_maybe, mkTupleRepApp_maybe,
typeOrConstraintKind,
sORTKind_maybe, typeTypeOrConstraint,
typeLevity_maybe, tyConIsTYPEorCONSTRAINT,
isLiftedTypeKind, isUnliftedTypeKind, pickyIsLiftedTypeKind,
isLiftedRuntimeRep, isUnliftedRuntimeRep, runtimeRepLevity_maybe,
isBoxedRuntimeRep,
isLiftedLevity, isUnliftedLevity,
isUnliftedType, isBoxedType, isUnboxedTupleType, isUnboxedSumType,
kindBoxedRepLevity_maybe,
mightBeLiftedType, mightBeUnliftedType,
isAlgType, isDataFamilyAppType,
isPrimitiveType, isStrictType,
isLevityTy, isLevityVar,
isRuntimeRepTy, isRuntimeRepVar, isRuntimeRepKindedTy,
dropRuntimeRepArgs,
isMultiplicityTy, isMultiplicityVar,
unrestricted, linear, tymult,
mkScaled, irrelevantMult, scaledSet,
pattern OneTy, pattern ManyTy,
isOneTy, isManyTy,
isLinearType,
Kind,
typeKind, typeHasFixedRuntimeRep, argsHaveFixedRuntimeRep,
tcIsLiftedTypeKind,
isConstraintKind, isConstraintLikeKind, returnsConstraintKind,
tcIsBoxedTypeKind, isTypeLikeKind,
liftedTypeKind, unliftedTypeKind,
tyCoFVsOfType, tyCoFVsBndr, tyCoFVsVarBndr, tyCoFVsVarBndrs,
tyCoVarsOfType, tyCoVarsOfTypes,
tyCoVarsOfTypeDSet,
coVarsOfType,
coVarsOfTypes,
anyFreeVarsOfType, anyFreeVarsOfTypes,
noFreeVarsOfType,
expandTypeSynonyms,
typeSize, occCheckExpand,
closeOverKindsDSet, closeOverKindsList,
closeOverKinds,
scopedSort, tyCoVarsOfTypeWellScoped,
tyCoVarsOfTypesWellScoped,
seqType, seqTypes,
coreView,
tyConsOfType,
TvSubstEnv,
IdSubstEnv,
Subst(..),
emptyTvSubstEnv, emptySubst, mkEmptySubst,
mkSubst, zipTvSubst, mkTvSubstPrs,
zipTCvSubst,
notElemSubst,
getTvSubstEnv,
zapSubst, getSubstInScope, setInScope, getSubstRangeTyCoFVs,
extendSubstInScope, extendSubstInScopeList, extendSubstInScopeSet,
extendTCvSubst, extendCvSubst,
extendTvSubst, extendTvSubstBinderAndInScope,
extendTvSubstList, extendTvSubstAndInScope,
extendTCvSubstList,
extendTvSubstWithClone,
extendTCvSubstWithClone,
isInScope, composeTCvSubst, zipTyEnv, zipCoEnv,
isEmptySubst, unionSubst, isEmptyTCvSubst,
substTy, substTys, substScaledTy, substScaledTys, substTyWith, substTysWith, substTheta,
substTyAddInScope,
substTyUnchecked, substTysUnchecked, substScaledTyUnchecked, substScaledTysUnchecked,
substThetaUnchecked, substTyWithUnchecked,
substCo, substCoUnchecked, substCoWithUnchecked,
substTyVarBndr, substTyVarBndrs, substTyVar, substTyVars,
substVarBndr, substVarBndrs,
substTyCoBndr, substTyVarToTyVar,
cloneTyVarBndr, cloneTyVarBndrs, lookupTyVar,
tidyType, tidyTypes,
tidyOpenType, tidyOpenTypes,
tidyVarBndr, tidyVarBndrs, tidyFreeTyCoVars,
tidyOpenTyCoVar, tidyOpenTyCoVars,
tidyTyCoVarOcc,
tidyTopType,
tidyForAllTyBinder, tidyForAllTyBinders,
isTYPEorCONSTRAINT,
isConcrete, isFixedRuntimeRepKind,
) where
import GHC.Prelude
import GHC.Types.Basic
import GHC.Core.TyCo.Rep
import GHC.Core.TyCo.Subst
import GHC.Core.TyCo.Tidy
import GHC.Core.TyCo.FVs
import GHC.Types.Var
import GHC.Types.Var.Env
import GHC.Types.Var.Set
import GHC.Types.Unique.Set
import GHC.Core.TyCon
import GHC.Builtin.Types.Prim
import {-# SOURCE #-} GHC.Builtin.Types
( charTy, naturalTy
, typeSymbolKind, liftedTypeKind, unliftedTypeKind
, constraintKind, zeroBitTypeKind
, manyDataConTy, oneDataConTy
, liftedRepTy, unliftedRepTy, zeroBitRepTy )
import GHC.Types.Name( Name )
import GHC.Builtin.Names
import GHC.Core.Coercion.Axiom
import {-# SOURCE #-} GHC.Core.Coercion
( mkNomReflCo, mkGReflCo, mkReflCo
, mkTyConAppCo, mkAppCo
, mkForAllCo, mkFunCo2, mkAxiomInstCo, mkUnivCo
, mkSymCo, mkTransCo, mkSelCo, mkLRCo, mkInstCo
, mkKindCo, mkSubCo, mkFunCo1
, decomposePiCos, coercionKind
, coercionRKind, coercionType
, isReflexiveCo, seqCo
, topNormaliseNewType_maybe
)
import {-# SOURCE #-} GHC.Tc.Utils.TcType ( isConcreteTyVar )
import GHC.Utils.Misc
import GHC.Utils.FV
import GHC.Utils.Outputable
import GHC.Utils.Panic
import GHC.Utils.Panic.Plain
import GHC.Data.FastString
import Control.Monad ( guard )
import GHC.Data.Maybe ( orElse, isJust )
coreView :: Type -> Maybe Type
coreView :: Type -> Maybe Type
coreView (TyConApp TyCon
tc [Type]
tys) = TyCon -> [Type] -> Maybe Type
expandSynTyConApp_maybe TyCon
tc [Type]
tys
coreView Type
_ = Maybe Type
forall a. Maybe a
Nothing
{-# INLINE coreView #-}
coreFullView, core_full_view :: Type -> Type
coreFullView :: Type -> Type
coreFullView ty :: Type
ty@(TyConApp TyCon
tc [Type]
_)
| TyCon -> Bool
isTypeSynonymTyCon TyCon
tc = Type -> Type
core_full_view Type
ty
coreFullView Type
ty = Type
ty
{-# INLINE coreFullView #-}
core_full_view :: Type -> Type
core_full_view Type
ty
| Just Type
ty' <- Type -> Maybe Type
coreView Type
ty = Type -> Type
core_full_view Type
ty'
| Bool
otherwise = Type
ty
expandSynTyConApp_maybe :: TyCon -> [Type] -> Maybe Type
{-# INLINE expandSynTyConApp_maybe #-}
expandSynTyConApp_maybe :: TyCon -> [Type] -> Maybe Type
expandSynTyConApp_maybe TyCon
tc [Type]
arg_tys
| Just ([TyVar]
tvs, Type
rhs) <- TyCon -> Maybe ([TyVar], Type)
synTyConDefn_maybe TyCon
tc
, [Type]
arg_tys [Type] -> Arity -> Bool
`saturates` TyCon -> Arity
tyConArity TyCon
tc
= Type -> Maybe Type
forall a. a -> Maybe a
Just ([TyVar] -> Type -> [Type] -> Type
expand_syn [TyVar]
tvs Type
rhs [Type]
arg_tys)
| Bool
otherwise
= Maybe Type
forall a. Maybe a
Nothing
saturates :: [Type] -> Arity -> Bool
saturates :: [Type] -> Arity -> Bool
saturates [Type]
_ Arity
0 = Bool
True
saturates [] Arity
_ = Bool
False
saturates (Type
_:[Type]
tys) Arity
n = Bool -> Bool -> Bool
forall a. HasCallStack => Bool -> a -> a
assert( Arity
n Arity -> Arity -> Bool
forall a. Ord a => a -> a -> Bool
>= Arity
0 ) (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [Type] -> Arity -> Bool
saturates [Type]
tys (Arity
nArity -> Arity -> Arity
forall a. Num a => a -> a -> a
-Arity
1)
expand_syn :: [TyVar]
-> Type
-> [Type]
-> Type
{-# NOINLINE expand_syn #-}
expand_syn :: [TyVar] -> Type -> [Type] -> Type
expand_syn [TyVar]
tvs Type
rhs [Type]
arg_tys
| [Type] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
arg_tys = Bool -> Type -> Type
forall a. HasCallStack => Bool -> a -> a
assert ([TyVar] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TyVar]
tvs) Type
rhs
| [TyVar] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TyVar]
tvs = Type -> [Type] -> Type
mkAppTys Type
rhs [Type]
arg_tys
| Bool
otherwise = Subst -> [TyVar] -> [Type] -> Type
go Subst
empty_subst [TyVar]
tvs [Type]
arg_tys
where
empty_subst :: Subst
empty_subst = InScopeSet -> Subst
mkEmptySubst InScopeSet
in_scope
in_scope :: InScopeSet
in_scope = VarSet -> InScopeSet
mkInScopeSet (VarSet -> InScopeSet) -> VarSet -> InScopeSet
forall a b. (a -> b) -> a -> b
$ [Type] -> VarSet
shallowTyCoVarsOfTypes ([Type] -> VarSet) -> [Type] -> VarSet
forall a b. (a -> b) -> a -> b
$ [Type]
arg_tys
go :: Subst -> [TyVar] -> [Type] -> Type
go Subst
subst [] [Type]
tys
| [Type] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
tys = Type
rhs'
| Bool
otherwise = Type -> [Type] -> Type
mkAppTys Type
rhs' [Type]
tys
where
rhs' :: Type
rhs' = (() :: Constraint) => Subst -> Type -> Type
Subst -> Type -> Type
substTy Subst
subst Type
rhs
go Subst
subst (TyVar
tv:[TyVar]
tvs) (Type
ty:[Type]
tys) = Subst -> [TyVar] -> [Type] -> Type
go (Subst -> TyVar -> Type -> Subst
extendTvSubst Subst
subst TyVar
tv Type
ty) [TyVar]
tvs [Type]
tys
go Subst
_ (TyVar
_:[TyVar]
_) [] = String -> SDoc -> Type
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"expand_syn" ([TyVar] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [TyVar]
tvs SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
rhs SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
arg_tys)
expandTypeSynonyms :: Type -> Type
expandTypeSynonyms :: Type -> Type
expandTypeSynonyms Type
ty
= Subst -> Type -> Type
go (InScopeSet -> Subst
mkEmptySubst InScopeSet
in_scope) Type
ty
where
in_scope :: InScopeSet
in_scope = VarSet -> InScopeSet
mkInScopeSet (Type -> VarSet
tyCoVarsOfType Type
ty)
go :: Subst -> Type -> Type
go Subst
subst (TyConApp TyCon
tc [Type]
tys)
| ExpandsSyn [(TyVar, Type)]
tenv Type
rhs [Type]
tys' <- TyCon -> [Type] -> ExpandSynResult Type
forall tyco. TyCon -> [tyco] -> ExpandSynResult tyco
expandSynTyCon_maybe TyCon
tc [Type]
expanded_tys
= let subst' :: Subst
subst' = InScopeSet -> TvSubstEnv -> Subst
mkTvSubst InScopeSet
in_scope ([(TyVar, Type)] -> TvSubstEnv
forall a. [(TyVar, a)] -> VarEnv a
mkVarEnv [(TyVar, Type)]
tenv)
in Type -> [Type] -> Type
mkAppTys (Subst -> Type -> Type
go Subst
subst' Type
rhs) [Type]
tys'
| Bool
otherwise
= TyCon -> [Type] -> Type
TyConApp TyCon
tc [Type]
expanded_tys
where
expanded_tys :: [Type]
expanded_tys = ((Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Subst -> Type -> Type
go Subst
subst) [Type]
tys)
go Subst
_ (LitTy TyLit
l) = TyLit -> Type
LitTy TyLit
l
go Subst
subst (TyVarTy TyVar
tv) = Subst -> TyVar -> Type
substTyVar Subst
subst TyVar
tv
go Subst
subst (AppTy Type
t1 Type
t2) = Type -> Type -> Type
mkAppTy (Subst -> Type -> Type
go Subst
subst Type
t1) (Subst -> Type -> Type
go Subst
subst Type
t2)
go Subst
subst ty :: Type
ty@(FunTy FunTyFlag
_ Type
mult Type
arg Type
res)
= Type
ty { ft_mult = go subst mult, ft_arg = go subst arg, ft_res = go subst res }
go Subst
subst (ForAllTy (Bndr TyVar
tv ForAllTyFlag
vis) Type
t)
= let (Subst
subst', TyVar
tv') = (Subst -> Type -> Type) -> Subst -> TyVar -> (Subst, TyVar)
substVarBndrUsing Subst -> Type -> Type
go Subst
subst TyVar
tv in
VarBndr TyVar ForAllTyFlag -> Type -> Type
ForAllTy (TyVar -> ForAllTyFlag -> VarBndr TyVar ForAllTyFlag
forall var argf. var -> argf -> VarBndr var argf
Bndr TyVar
tv' ForAllTyFlag
vis) (Subst -> Type -> Type
go Subst
subst' Type
t)
go Subst
subst (CastTy Type
ty KindCoercion
co) = Type -> KindCoercion -> Type
mkCastTy (Subst -> Type -> Type
go Subst
subst Type
ty) (Subst -> KindCoercion -> KindCoercion
go_co Subst
subst KindCoercion
co)
go Subst
subst (CoercionTy KindCoercion
co) = KindCoercion -> Type
mkCoercionTy (Subst -> KindCoercion -> KindCoercion
go_co Subst
subst KindCoercion
co)
go_mco :: Subst -> MCoercionN -> MCoercionN
go_mco Subst
_ MCoercionN
MRefl = MCoercionN
MRefl
go_mco Subst
subst (MCo KindCoercion
co) = KindCoercion -> MCoercionN
MCo (Subst -> KindCoercion -> KindCoercion
go_co Subst
subst KindCoercion
co)
go_co :: Subst -> KindCoercion -> KindCoercion
go_co Subst
subst (Refl Type
ty)
= Type -> KindCoercion
mkNomReflCo (Subst -> Type -> Type
go Subst
subst Type
ty)
go_co Subst
subst (GRefl Role
r Type
ty MCoercionN
mco)
= Role -> Type -> MCoercionN -> KindCoercion
mkGReflCo Role
r (Subst -> Type -> Type
go Subst
subst Type
ty) (Subst -> MCoercionN -> MCoercionN
go_mco Subst
subst MCoercionN
mco)
go_co Subst
subst (TyConAppCo Role
r TyCon
tc [KindCoercion]
args)
= (() :: Constraint) =>
Role -> TyCon -> [KindCoercion] -> KindCoercion
Role -> TyCon -> [KindCoercion] -> KindCoercion
mkTyConAppCo Role
r TyCon
tc ((KindCoercion -> KindCoercion) -> [KindCoercion] -> [KindCoercion]
forall a b. (a -> b) -> [a] -> [b]
map (Subst -> KindCoercion -> KindCoercion
go_co Subst
subst) [KindCoercion]
args)
go_co Subst
subst (AppCo KindCoercion
co KindCoercion
arg)
= KindCoercion -> KindCoercion -> KindCoercion
mkAppCo (Subst -> KindCoercion -> KindCoercion
go_co Subst
subst KindCoercion
co) (Subst -> KindCoercion -> KindCoercion
go_co Subst
subst KindCoercion
arg)
go_co Subst
subst (ForAllCo TyVar
tv KindCoercion
kind_co KindCoercion
co)
= let (Subst
subst', TyVar
tv', KindCoercion
kind_co') = Subst -> TyVar -> KindCoercion -> (Subst, TyVar, KindCoercion)
go_cobndr Subst
subst TyVar
tv KindCoercion
kind_co in
TyVar -> KindCoercion -> KindCoercion -> KindCoercion
mkForAllCo TyVar
tv' KindCoercion
kind_co' (Subst -> KindCoercion -> KindCoercion
go_co Subst
subst' KindCoercion
co)
go_co Subst
subst (FunCo Role
r FunTyFlag
afl FunTyFlag
afr KindCoercion
w KindCoercion
co1 KindCoercion
co2)
= (() :: Constraint) =>
Role
-> FunTyFlag
-> FunTyFlag
-> KindCoercion
-> KindCoercion
-> KindCoercion
-> KindCoercion
Role
-> FunTyFlag
-> FunTyFlag
-> KindCoercion
-> KindCoercion
-> KindCoercion
-> KindCoercion
mkFunCo2 Role
r FunTyFlag
afl FunTyFlag
afr (Subst -> KindCoercion -> KindCoercion
go_co Subst
subst KindCoercion
w) (Subst -> KindCoercion -> KindCoercion
go_co Subst
subst KindCoercion
co1) (Subst -> KindCoercion -> KindCoercion
go_co Subst
subst KindCoercion
co2)
go_co Subst
subst (CoVarCo TyVar
cv)
= Subst -> TyVar -> KindCoercion
substCoVar Subst
subst TyVar
cv
go_co Subst
subst (AxiomInstCo CoAxiom Branched
ax Arity
ind [KindCoercion]
args)
= CoAxiom Branched -> Arity -> [KindCoercion] -> KindCoercion
mkAxiomInstCo CoAxiom Branched
ax Arity
ind ((KindCoercion -> KindCoercion) -> [KindCoercion] -> [KindCoercion]
forall a b. (a -> b) -> [a] -> [b]
map (Subst -> KindCoercion -> KindCoercion
go_co Subst
subst) [KindCoercion]
args)
go_co Subst
subst (UnivCo UnivCoProvenance
p Role
r Type
t1 Type
t2)
= UnivCoProvenance -> Role -> Type -> Type -> KindCoercion
mkUnivCo (Subst -> UnivCoProvenance -> UnivCoProvenance
go_prov Subst
subst UnivCoProvenance
p) Role
r (Subst -> Type -> Type
go Subst
subst Type
t1) (Subst -> Type -> Type
go Subst
subst Type
t2)
go_co Subst
subst (SymCo KindCoercion
co)
= KindCoercion -> KindCoercion
mkSymCo (Subst -> KindCoercion -> KindCoercion
go_co Subst
subst KindCoercion
co)
go_co Subst
subst (TransCo KindCoercion
co1 KindCoercion
co2)
= KindCoercion -> KindCoercion -> KindCoercion
mkTransCo (Subst -> KindCoercion -> KindCoercion
go_co Subst
subst KindCoercion
co1) (Subst -> KindCoercion -> KindCoercion
go_co Subst
subst KindCoercion
co2)
go_co Subst
subst (SelCo CoSel
n KindCoercion
co)
= (() :: Constraint) => CoSel -> KindCoercion -> KindCoercion
CoSel -> KindCoercion -> KindCoercion
mkSelCo CoSel
n (Subst -> KindCoercion -> KindCoercion
go_co Subst
subst KindCoercion
co)
go_co Subst
subst (LRCo LeftOrRight
lr KindCoercion
co)
= LeftOrRight -> KindCoercion -> KindCoercion
mkLRCo LeftOrRight
lr (Subst -> KindCoercion -> KindCoercion
go_co Subst
subst KindCoercion
co)
go_co Subst
subst (InstCo KindCoercion
co KindCoercion
arg)
= KindCoercion -> KindCoercion -> KindCoercion
mkInstCo (Subst -> KindCoercion -> KindCoercion
go_co Subst
subst KindCoercion
co) (Subst -> KindCoercion -> KindCoercion
go_co Subst
subst KindCoercion
arg)
go_co Subst
subst (KindCo KindCoercion
co)
= KindCoercion -> KindCoercion
mkKindCo (Subst -> KindCoercion -> KindCoercion
go_co Subst
subst KindCoercion
co)
go_co Subst
subst (SubCo KindCoercion
co)
= (() :: Constraint) => KindCoercion -> KindCoercion
KindCoercion -> KindCoercion
mkSubCo (Subst -> KindCoercion -> KindCoercion
go_co Subst
subst KindCoercion
co)
go_co Subst
subst (AxiomRuleCo CoAxiomRule
ax [KindCoercion]
cs)
= CoAxiomRule -> [KindCoercion] -> KindCoercion
AxiomRuleCo CoAxiomRule
ax ((KindCoercion -> KindCoercion) -> [KindCoercion] -> [KindCoercion]
forall a b. (a -> b) -> [a] -> [b]
map (Subst -> KindCoercion -> KindCoercion
go_co Subst
subst) [KindCoercion]
cs)
go_co Subst
_ (HoleCo CoercionHole
h)
= String -> SDoc -> KindCoercion
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"expandTypeSynonyms hit a hole" (CoercionHole -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoercionHole
h)
go_prov :: Subst -> UnivCoProvenance -> UnivCoProvenance
go_prov Subst
subst (PhantomProv KindCoercion
co) = KindCoercion -> UnivCoProvenance
PhantomProv (Subst -> KindCoercion -> KindCoercion
go_co Subst
subst KindCoercion
co)
go_prov Subst
subst (ProofIrrelProv KindCoercion
co) = KindCoercion -> UnivCoProvenance
ProofIrrelProv (Subst -> KindCoercion -> KindCoercion
go_co Subst
subst KindCoercion
co)
go_prov Subst
_ p :: UnivCoProvenance
p@(PluginProv String
_) = UnivCoProvenance
p
go_prov Subst
_ p :: UnivCoProvenance
p@(CorePrepProv Bool
_) = UnivCoProvenance
p
go_cobndr :: Subst -> TyVar -> KindCoercion -> (Subst, TyVar, KindCoercion)
go_cobndr Subst
subst = Bool
-> (KindCoercion -> KindCoercion)
-> Subst
-> TyVar
-> KindCoercion
-> (Subst, TyVar, KindCoercion)
substForAllCoBndrUsing Bool
False (Subst -> KindCoercion -> KindCoercion
go_co Subst
subst) Subst
subst
isTyConKeyApp_maybe :: Unique -> Type -> Maybe [Type]
isTyConKeyApp_maybe :: Unique -> Type -> Maybe [Type]
isTyConKeyApp_maybe Unique
key Type
ty
| TyConApp TyCon
tc [Type]
args <- Type -> Type
coreFullView Type
ty
, TyCon
tc TyCon -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
key
= [Type] -> Maybe [Type]
forall a. a -> Maybe a
Just [Type]
args
| Bool
otherwise
= Maybe [Type]
forall a. Maybe a
Nothing
{-# INLINE isTyConKeyApp_maybe #-}
kindRep :: HasDebugCallStack => Kind -> RuntimeRepType
kindRep :: (() :: Constraint) => Type -> Type
kindRep Type
k = case (() :: Constraint) => Type -> Maybe Type
Type -> Maybe Type
kindRep_maybe Type
k of
Just Type
r -> Type
r
Maybe Type
Nothing -> String -> SDoc -> Type
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"kindRep" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
k)
kindRep_maybe :: HasDebugCallStack => Kind -> Maybe RuntimeRepType
kindRep_maybe :: (() :: Constraint) => Type -> Maybe Type
kindRep_maybe Type
kind
| Just (TypeOrConstraint
_, Type
rep) <- Type -> Maybe (TypeOrConstraint, Type)
sORTKind_maybe Type
kind = Type -> Maybe Type
forall a. a -> Maybe a
Just Type
rep
| Bool
otherwise = Maybe Type
forall a. Maybe a
Nothing
isLiftedTypeKind :: Kind -> Bool
isLiftedTypeKind :: Type -> Bool
isLiftedTypeKind Type
kind
= case (() :: Constraint) => Type -> Maybe Type
Type -> Maybe Type
kindRep_maybe Type
kind of
Just Type
rep -> Type -> Bool
isLiftedRuntimeRep Type
rep
Maybe Type
Nothing -> Bool
False
isUnliftedTypeKind :: Kind -> Bool
isUnliftedTypeKind :: Type -> Bool
isUnliftedTypeKind Type
kind
= case (() :: Constraint) => Type -> Maybe Type
Type -> Maybe Type
kindRep_maybe Type
kind of
Just Type
rep -> Type -> Bool
isUnliftedRuntimeRep Type
rep
Maybe Type
Nothing -> Bool
False
pickyIsLiftedTypeKind :: Kind -> Bool
pickyIsLiftedTypeKind :: Type -> Bool
pickyIsLiftedTypeKind Type
kind
| TyConApp TyCon
tc [Type
arg] <- Type
kind
, TyCon
tc TyCon -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
tYPETyConKey
, TyConApp TyCon
rr_tc [Type]
rr_args <- Type
arg = case [Type]
rr_args of
[] -> TyCon
rr_tc TyCon -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
liftedRepTyConKey
[Type
rr_arg]
| TyCon
rr_tc TyCon -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
boxedRepDataConKey
, TyConApp TyCon
lev [] <- Type
rr_arg
, TyCon
lev TyCon -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
liftedDataConKey -> Bool
True
[Type]
_ -> Bool
False
| TyConApp TyCon
tc [] <- Type
kind
, TyCon
tc TyCon -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
liftedTypeKindTyConKey = Bool
True
| Bool
otherwise = Bool
False
kindBoxedRepLevity_maybe :: Type -> Maybe Levity
kindBoxedRepLevity_maybe :: Type -> Maybe Levity
kindBoxedRepLevity_maybe Type
ty
| Just Type
rep <- (() :: Constraint) => Type -> Maybe Type
Type -> Maybe Type
kindRep_maybe Type
ty
, Type -> Bool
isBoxedRuntimeRep Type
rep
= Type -> Maybe Levity
runtimeRepLevity_maybe Type
rep
| Bool
otherwise
= Maybe Levity
forall a. Maybe a
Nothing
isLiftedRuntimeRep :: RuntimeRepType -> Bool
isLiftedRuntimeRep :: Type -> Bool
isLiftedRuntimeRep Type
rep =
Type -> Maybe Levity
runtimeRepLevity_maybe Type
rep Maybe Levity -> Maybe Levity -> Bool
forall a. Eq a => a -> a -> Bool
== Levity -> Maybe Levity
forall a. a -> Maybe a
Just Levity
Lifted
isUnliftedRuntimeRep :: RuntimeRepType -> Bool
isUnliftedRuntimeRep :: Type -> Bool
isUnliftedRuntimeRep Type
rep =
Type -> Maybe Levity
runtimeRepLevity_maybe Type
rep Maybe Levity -> Maybe Levity -> Bool
forall a. Eq a => a -> a -> Bool
== Levity -> Maybe Levity
forall a. a -> Maybe a
Just Levity
Unlifted
isNullaryTyConKeyApp :: Unique -> Type -> Bool
isNullaryTyConKeyApp :: Unique -> Type -> Bool
isNullaryTyConKeyApp Unique
key Type
ty
| Just [Type]
args <- Unique -> Type -> Maybe [Type]
isTyConKeyApp_maybe Unique
key Type
ty
= Bool -> Bool -> Bool
forall a. HasCallStack => Bool -> a -> a
assert ([Type] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
args) Bool
True
| Bool
otherwise
= Bool
False
{-# INLINE isNullaryTyConKeyApp #-}
isLiftedLevity :: Type -> Bool
isLiftedLevity :: Type -> Bool
isLiftedLevity = Unique -> Type -> Bool
isNullaryTyConKeyApp Unique
liftedDataConKey
isUnliftedLevity :: Type -> Bool
isUnliftedLevity :: Type -> Bool
isUnliftedLevity = Unique -> Type -> Bool
isNullaryTyConKeyApp Unique
unliftedDataConKey
isLevityTy :: Type -> Bool
isLevityTy :: Type -> Bool
isLevityTy = Unique -> Type -> Bool
isNullaryTyConKeyApp Unique
levityTyConKey
isRuntimeRepTy :: Type -> Bool
isRuntimeRepTy :: Type -> Bool
isRuntimeRepTy = Unique -> Type -> Bool
isNullaryTyConKeyApp Unique
runtimeRepTyConKey
isRuntimeRepVar :: TyVar -> Bool
isRuntimeRepVar :: TyVar -> Bool
isRuntimeRepVar = Type -> Bool
isRuntimeRepTy (Type -> Bool) -> (TyVar -> Type) -> TyVar -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVar -> Type
tyVarKind
isLevityVar :: TyVar -> Bool
isLevityVar :: TyVar -> Bool
isLevityVar = Type -> Bool
isLevityTy (Type -> Bool) -> (TyVar -> Type) -> TyVar -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVar -> Type
tyVarKind
isMultiplicityTy :: Type -> Bool
isMultiplicityTy :: Type -> Bool
isMultiplicityTy = Unique -> Type -> Bool
isNullaryTyConKeyApp Unique
multiplicityTyConKey
isMultiplicityVar :: TyVar -> Bool
isMultiplicityVar :: TyVar -> Bool
isMultiplicityVar = Type -> Bool
isMultiplicityTy (Type -> Bool) -> (TyVar -> Type) -> TyVar -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVar -> Type
tyVarKind
splitRuntimeRep_maybe :: RuntimeRepType -> Maybe (TyCon, [Type])
splitRuntimeRep_maybe :: Type -> Maybe (TyCon, [Type])
splitRuntimeRep_maybe Type
rep
| TyConApp TyCon
rr_tc [Type]
args <- Type -> Type
coreFullView Type
rep
, TyCon -> Bool
isPromotedDataCon TyCon
rr_tc
= (TyCon, [Type]) -> Maybe (TyCon, [Type])
forall a. a -> Maybe a
Just (TyCon
rr_tc, [Type]
args)
| Bool
otherwise
= Maybe (TyCon, [Type])
forall a. Maybe a
Nothing
isBoxedRuntimeRep :: RuntimeRepType -> Bool
isBoxedRuntimeRep :: Type -> Bool
isBoxedRuntimeRep Type
rep = Maybe Type -> Bool
forall a. Maybe a -> Bool
isJust (Type -> Maybe Type
isBoxedRuntimeRep_maybe Type
rep)
isBoxedRuntimeRep_maybe :: RuntimeRepType -> Maybe Type
isBoxedRuntimeRep_maybe :: Type -> Maybe Type
isBoxedRuntimeRep_maybe Type
rep
| Just (TyCon
rr_tc, [Type]
args) <- Type -> Maybe (TyCon, [Type])
splitRuntimeRep_maybe Type
rep
, TyCon
rr_tc TyCon -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
boxedRepDataConKey
, [Type
lev] <- [Type]
args
= Type -> Maybe Type
forall a. a -> Maybe a
Just Type
lev
| Bool
otherwise
= Maybe Type
forall a. Maybe a
Nothing
runtimeRepLevity_maybe :: RuntimeRepType -> Maybe Levity
runtimeRepLevity_maybe :: Type -> Maybe Levity
runtimeRepLevity_maybe Type
rep
| Just (TyCon
rr_tc, [Type]
args) <- Type -> Maybe (TyCon, [Type])
splitRuntimeRep_maybe Type
rep
=
if (TyCon
rr_tc TyCon -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
boxedRepDataConKey)
then case [Type]
args of
[Type
lev] -> Type -> Maybe Levity
levityType_maybe Type
lev
[Type]
_ -> String -> SDoc -> Maybe Levity
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"runtimeRepLevity_maybe" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
rep)
else Levity -> Maybe Levity
forall a. a -> Maybe a
Just Levity
Unlifted
| Bool
otherwise
= Maybe Levity
forall a. Maybe a
Nothing
levityType_maybe :: LevityType -> Maybe Levity
levityType_maybe :: Type -> Maybe Levity
levityType_maybe Type
lev
| TyConApp TyCon
lev_tc [Type]
args <- Type -> Type
coreFullView Type
lev
= if | TyCon
lev_tc TyCon -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
liftedDataConKey -> Bool -> Maybe Levity -> Maybe Levity
forall a. HasCallStack => Bool -> a -> a
assert( [Type] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
args) (Maybe Levity -> Maybe Levity) -> Maybe Levity -> Maybe Levity
forall a b. (a -> b) -> a -> b
$ Levity -> Maybe Levity
forall a. a -> Maybe a
Just Levity
Lifted
| TyCon
lev_tc TyCon -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
unliftedDataConKey -> Bool -> Maybe Levity -> Maybe Levity
forall a. HasCallStack => Bool -> a -> a
assert( [Type] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
args) (Maybe Levity -> Maybe Levity) -> Maybe Levity -> Maybe Levity
forall a b. (a -> b) -> a -> b
$ Levity -> Maybe Levity
forall a. a -> Maybe a
Just Levity
Unlifted
| Bool
otherwise -> Maybe Levity
forall a. Maybe a
Nothing
| Bool
otherwise
= Maybe Levity
forall a. Maybe a
Nothing
data TyCoMapper env m
= TyCoMapper
{ forall env (m :: * -> *).
TyCoMapper env m -> env -> TyVar -> m Type
tcm_tyvar :: env -> TyVar -> m Type
, forall env (m :: * -> *).
TyCoMapper env m -> env -> TyVar -> m KindCoercion
tcm_covar :: env -> CoVar -> m Coercion
, forall env (m :: * -> *).
TyCoMapper env m -> env -> CoercionHole -> m KindCoercion
tcm_hole :: env -> CoercionHole -> m Coercion
, forall env (m :: * -> *).
TyCoMapper env m -> env -> TyVar -> ForAllTyFlag -> m (env, TyVar)
tcm_tycobinder :: env -> TyCoVar -> ForAllTyFlag -> m (env, TyCoVar)
, forall env (m :: * -> *). TyCoMapper env m -> TyCon -> m TyCon
tcm_tycon :: TyCon -> m TyCon
}
{-# INLINE mapTyCo #-}
mapTyCo :: Monad m => TyCoMapper () m
-> ( Type -> m Type
, [Type] -> m [Type]
, Coercion -> m Coercion
, [Coercion] -> m[Coercion])
mapTyCo :: forall (m :: * -> *).
Monad m =>
TyCoMapper () m
-> (Type -> m Type, [Type] -> m [Type],
KindCoercion -> m KindCoercion, [KindCoercion] -> m [KindCoercion])
mapTyCo TyCoMapper () m
mapper
= case TyCoMapper () m
-> (() -> Type -> m Type, () -> [Type] -> m [Type],
() -> KindCoercion -> m KindCoercion,
() -> [KindCoercion] -> m [KindCoercion])
forall (m :: * -> *) env.
Monad m =>
TyCoMapper env m
-> (env -> Type -> m Type, env -> [Type] -> m [Type],
env -> KindCoercion -> m KindCoercion,
env -> [KindCoercion] -> m [KindCoercion])
mapTyCoX TyCoMapper () m
mapper of
(() -> Type -> m Type
go_ty, () -> [Type] -> m [Type]
go_tys, () -> KindCoercion -> m KindCoercion
go_co, () -> [KindCoercion] -> m [KindCoercion]
go_cos)
-> (() -> Type -> m Type
go_ty (), () -> [Type] -> m [Type]
go_tys (), () -> KindCoercion -> m KindCoercion
go_co (), () -> [KindCoercion] -> m [KindCoercion]
go_cos ())
{-# INLINE mapTyCoX #-}
mapTyCoX :: Monad m => TyCoMapper env m
-> ( env -> Type -> m Type
, env -> [Type] -> m [Type]
, env -> Coercion -> m Coercion
, env -> [Coercion] -> m[Coercion])
mapTyCoX :: forall (m :: * -> *) env.
Monad m =>
TyCoMapper env m
-> (env -> Type -> m Type, env -> [Type] -> m [Type],
env -> KindCoercion -> m KindCoercion,
env -> [KindCoercion] -> m [KindCoercion])
mapTyCoX (TyCoMapper { tcm_tyvar :: forall env (m :: * -> *).
TyCoMapper env m -> env -> TyVar -> m Type
tcm_tyvar = env -> TyVar -> m Type
tyvar
, tcm_tycobinder :: forall env (m :: * -> *).
TyCoMapper env m -> env -> TyVar -> ForAllTyFlag -> m (env, TyVar)
tcm_tycobinder = env -> TyVar -> ForAllTyFlag -> m (env, TyVar)
tycobinder
, tcm_tycon :: forall env (m :: * -> *). TyCoMapper env m -> TyCon -> m TyCon
tcm_tycon = TyCon -> m TyCon
tycon
, tcm_covar :: forall env (m :: * -> *).
TyCoMapper env m -> env -> TyVar -> m KindCoercion
tcm_covar = env -> TyVar -> m KindCoercion
covar
, tcm_hole :: forall env (m :: * -> *).
TyCoMapper env m -> env -> CoercionHole -> m KindCoercion
tcm_hole = env -> CoercionHole -> m KindCoercion
cohole })
= (env -> Type -> m Type
go_ty, env -> [Type] -> m [Type]
go_tys, env -> KindCoercion -> m KindCoercion
go_co, env -> [KindCoercion] -> m [KindCoercion]
go_cos)
where
go_tys :: env -> [Type] -> m [Type]
go_tys env
_ [] = [Type] -> m [Type]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return []
go_tys env
env (Type
ty:[Type]
tys) = (:) (Type -> [Type] -> [Type]) -> m Type -> m ([Type] -> [Type])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> env -> Type -> m Type
go_ty env
env Type
ty m ([Type] -> [Type]) -> m [Type] -> m [Type]
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> env -> [Type] -> m [Type]
go_tys env
env [Type]
tys
go_ty :: env -> Type -> m Type
go_ty env
env (TyVarTy TyVar
tv) = env -> TyVar -> m Type
tyvar env
env TyVar
tv
go_ty env
env (AppTy Type
t1 Type
t2) = Type -> Type -> Type
mkAppTy (Type -> Type -> Type) -> m Type -> m (Type -> Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> env -> Type -> m Type
go_ty env
env Type
t1 m (Type -> Type) -> m Type -> m Type
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> env -> Type -> m Type
go_ty env
env Type
t2
go_ty env
_ ty :: Type
ty@(LitTy {}) = Type -> m Type
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Type
ty
go_ty env
env (CastTy Type
ty KindCoercion
co) = Type -> KindCoercion -> Type
mkCastTy (Type -> KindCoercion -> Type)
-> m Type -> m (KindCoercion -> Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> env -> Type -> m Type
go_ty env
env Type
ty m (KindCoercion -> Type) -> m KindCoercion -> m Type
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> env -> KindCoercion -> m KindCoercion
go_co env
env KindCoercion
co
go_ty env
env (CoercionTy KindCoercion
co) = KindCoercion -> Type
CoercionTy (KindCoercion -> Type) -> m KindCoercion -> m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> env -> KindCoercion -> m KindCoercion
go_co env
env KindCoercion
co
go_ty env
env ty :: Type
ty@(FunTy FunTyFlag
_ Type
w Type
arg Type
res)
= do { Type
w' <- env -> Type -> m Type
go_ty env
env Type
w; Type
arg' <- env -> Type -> m Type
go_ty env
env Type
arg; Type
res' <- env -> Type -> m Type
go_ty env
env Type
res
; Type -> m Type
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
ty { ft_mult = w', ft_arg = arg', ft_res = res' }) }
go_ty env
env ty :: Type
ty@(TyConApp TyCon
tc [Type]
tys)
| TyCon -> Bool
isTcTyCon TyCon
tc
= do { TyCon
tc' <- TyCon -> m TyCon
tycon TyCon
tc
; TyCon -> [Type] -> Type
mkTyConApp TyCon
tc' ([Type] -> Type) -> m [Type] -> m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> env -> [Type] -> m [Type]
go_tys env
env [Type]
tys }
| [Type] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
tys
= Type -> m Type
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Type
ty
| Bool
otherwise
= TyCon -> [Type] -> Type
mkTyConApp TyCon
tc ([Type] -> Type) -> m [Type] -> m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> env -> [Type] -> m [Type]
go_tys env
env [Type]
tys
go_ty env
env (ForAllTy (Bndr TyVar
tv ForAllTyFlag
vis) Type
inner)
= do { (env
env', TyVar
tv') <- env -> TyVar -> ForAllTyFlag -> m (env, TyVar)
tycobinder env
env TyVar
tv ForAllTyFlag
vis
; Type
inner' <- env -> Type -> m Type
go_ty env
env' Type
inner
; Type -> m Type
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ VarBndr TyVar ForAllTyFlag -> Type -> Type
ForAllTy (TyVar -> ForAllTyFlag -> VarBndr TyVar ForAllTyFlag
forall var argf. var -> argf -> VarBndr var argf
Bndr TyVar
tv' ForAllTyFlag
vis) Type
inner' }
go_cos :: env -> [KindCoercion] -> m [KindCoercion]
go_cos env
_ [] = [KindCoercion] -> m [KindCoercion]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return []
go_cos env
env (KindCoercion
co:[KindCoercion]
cos) = (:) (KindCoercion -> [KindCoercion] -> [KindCoercion])
-> m KindCoercion -> m ([KindCoercion] -> [KindCoercion])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> env -> KindCoercion -> m KindCoercion
go_co env
env KindCoercion
co m ([KindCoercion] -> [KindCoercion])
-> m [KindCoercion] -> m [KindCoercion]
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> env -> [KindCoercion] -> m [KindCoercion]
go_cos env
env [KindCoercion]
cos
go_mco :: env -> MCoercionN -> m MCoercionN
go_mco env
_ MCoercionN
MRefl = MCoercionN -> m MCoercionN
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return MCoercionN
MRefl
go_mco env
env (MCo KindCoercion
co) = KindCoercion -> MCoercionN
MCo (KindCoercion -> MCoercionN) -> m KindCoercion -> m MCoercionN
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (env -> KindCoercion -> m KindCoercion
go_co env
env KindCoercion
co)
go_co :: env -> KindCoercion -> m KindCoercion
go_co env
env (Refl Type
ty) = Type -> KindCoercion
Refl (Type -> KindCoercion) -> m Type -> m KindCoercion
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> env -> Type -> m Type
go_ty env
env Type
ty
go_co env
env (GRefl Role
r Type
ty MCoercionN
mco) = Role -> Type -> MCoercionN -> KindCoercion
mkGReflCo Role
r (Type -> MCoercionN -> KindCoercion)
-> m Type -> m (MCoercionN -> KindCoercion)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> env -> Type -> m Type
go_ty env
env Type
ty m (MCoercionN -> KindCoercion) -> m MCoercionN -> m KindCoercion
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> env -> MCoercionN -> m MCoercionN
go_mco env
env MCoercionN
mco
go_co env
env (AppCo KindCoercion
c1 KindCoercion
c2) = KindCoercion -> KindCoercion -> KindCoercion
mkAppCo (KindCoercion -> KindCoercion -> KindCoercion)
-> m KindCoercion -> m (KindCoercion -> KindCoercion)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> env -> KindCoercion -> m KindCoercion
go_co env
env KindCoercion
c1 m (KindCoercion -> KindCoercion)
-> m KindCoercion -> m KindCoercion
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> env -> KindCoercion -> m KindCoercion
go_co env
env KindCoercion
c2
go_co env
env (FunCo Role
r FunTyFlag
afl FunTyFlag
afr KindCoercion
cw KindCoercion
c1 KindCoercion
c2) = (() :: Constraint) =>
Role
-> FunTyFlag
-> FunTyFlag
-> KindCoercion
-> KindCoercion
-> KindCoercion
-> KindCoercion
Role
-> FunTyFlag
-> FunTyFlag
-> KindCoercion
-> KindCoercion
-> KindCoercion
-> KindCoercion
mkFunCo2 Role
r FunTyFlag
afl FunTyFlag
afr (KindCoercion -> KindCoercion -> KindCoercion -> KindCoercion)
-> m KindCoercion
-> m (KindCoercion -> KindCoercion -> KindCoercion)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> env -> KindCoercion -> m KindCoercion
go_co env
env KindCoercion
cw
m (KindCoercion -> KindCoercion -> KindCoercion)
-> m KindCoercion -> m (KindCoercion -> KindCoercion)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> env -> KindCoercion -> m KindCoercion
go_co env
env KindCoercion
c1 m (KindCoercion -> KindCoercion)
-> m KindCoercion -> m KindCoercion
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> env -> KindCoercion -> m KindCoercion
go_co env
env KindCoercion
c2
go_co env
env (CoVarCo TyVar
cv) = env -> TyVar -> m KindCoercion
covar env
env TyVar
cv
go_co env
env (HoleCo CoercionHole
hole) = env -> CoercionHole -> m KindCoercion
cohole env
env CoercionHole
hole
go_co env
env (UnivCo UnivCoProvenance
p Role
r Type
t1 Type
t2) = UnivCoProvenance -> Role -> Type -> Type -> KindCoercion
mkUnivCo (UnivCoProvenance -> Role -> Type -> Type -> KindCoercion)
-> m UnivCoProvenance -> m (Role -> Type -> Type -> KindCoercion)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> env -> UnivCoProvenance -> m UnivCoProvenance
go_prov env
env UnivCoProvenance
p m (Role -> Type -> Type -> KindCoercion)
-> m Role -> m (Type -> Type -> KindCoercion)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Role -> m Role
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Role
r
m (Type -> Type -> KindCoercion)
-> m Type -> m (Type -> KindCoercion)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> env -> Type -> m Type
go_ty env
env Type
t1 m (Type -> KindCoercion) -> m Type -> m KindCoercion
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> env -> Type -> m Type
go_ty env
env Type
t2
go_co env
env (SymCo KindCoercion
co) = KindCoercion -> KindCoercion
mkSymCo (KindCoercion -> KindCoercion) -> m KindCoercion -> m KindCoercion
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> env -> KindCoercion -> m KindCoercion
go_co env
env KindCoercion
co
go_co env
env (TransCo KindCoercion
c1 KindCoercion
c2) = KindCoercion -> KindCoercion -> KindCoercion
mkTransCo (KindCoercion -> KindCoercion -> KindCoercion)
-> m KindCoercion -> m (KindCoercion -> KindCoercion)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> env -> KindCoercion -> m KindCoercion
go_co env
env KindCoercion
c1 m (KindCoercion -> KindCoercion)
-> m KindCoercion -> m KindCoercion
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> env -> KindCoercion -> m KindCoercion
go_co env
env KindCoercion
c2
go_co env
env (AxiomRuleCo CoAxiomRule
r [KindCoercion]
cos) = CoAxiomRule -> [KindCoercion] -> KindCoercion
AxiomRuleCo CoAxiomRule
r ([KindCoercion] -> KindCoercion)
-> m [KindCoercion] -> m KindCoercion
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> env -> [KindCoercion] -> m [KindCoercion]
go_cos env
env [KindCoercion]
cos
go_co env
env (SelCo CoSel
i KindCoercion
co) = (() :: Constraint) => CoSel -> KindCoercion -> KindCoercion
CoSel -> KindCoercion -> KindCoercion
mkSelCo CoSel
i (KindCoercion -> KindCoercion) -> m KindCoercion -> m KindCoercion
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> env -> KindCoercion -> m KindCoercion
go_co env
env KindCoercion
co
go_co env
env (LRCo LeftOrRight
lr KindCoercion
co) = LeftOrRight -> KindCoercion -> KindCoercion
mkLRCo LeftOrRight
lr (KindCoercion -> KindCoercion) -> m KindCoercion -> m KindCoercion
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> env -> KindCoercion -> m KindCoercion
go_co env
env KindCoercion
co
go_co env
env (InstCo KindCoercion
co KindCoercion
arg) = KindCoercion -> KindCoercion -> KindCoercion
mkInstCo (KindCoercion -> KindCoercion -> KindCoercion)
-> m KindCoercion -> m (KindCoercion -> KindCoercion)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> env -> KindCoercion -> m KindCoercion
go_co env
env KindCoercion
co m (KindCoercion -> KindCoercion)
-> m KindCoercion -> m KindCoercion
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> env -> KindCoercion -> m KindCoercion
go_co env
env KindCoercion
arg
go_co env
env (KindCo KindCoercion
co) = KindCoercion -> KindCoercion
mkKindCo (KindCoercion -> KindCoercion) -> m KindCoercion -> m KindCoercion
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> env -> KindCoercion -> m KindCoercion
go_co env
env KindCoercion
co
go_co env
env (SubCo KindCoercion
co) = (() :: Constraint) => KindCoercion -> KindCoercion
KindCoercion -> KindCoercion
mkSubCo (KindCoercion -> KindCoercion) -> m KindCoercion -> m KindCoercion
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> env -> KindCoercion -> m KindCoercion
go_co env
env KindCoercion
co
go_co env
env (AxiomInstCo CoAxiom Branched
ax Arity
i [KindCoercion]
cos) = CoAxiom Branched -> Arity -> [KindCoercion] -> KindCoercion
mkAxiomInstCo CoAxiom Branched
ax Arity
i ([KindCoercion] -> KindCoercion)
-> m [KindCoercion] -> m KindCoercion
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> env -> [KindCoercion] -> m [KindCoercion]
go_cos env
env [KindCoercion]
cos
go_co env
env co :: KindCoercion
co@(TyConAppCo Role
r TyCon
tc [KindCoercion]
cos)
| TyCon -> Bool
isTcTyCon TyCon
tc
= do { TyCon
tc' <- TyCon -> m TyCon
tycon TyCon
tc
; (() :: Constraint) =>
Role -> TyCon -> [KindCoercion] -> KindCoercion
Role -> TyCon -> [KindCoercion] -> KindCoercion
mkTyConAppCo Role
r TyCon
tc' ([KindCoercion] -> KindCoercion)
-> m [KindCoercion] -> m KindCoercion
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> env -> [KindCoercion] -> m [KindCoercion]
go_cos env
env [KindCoercion]
cos }
| [KindCoercion] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [KindCoercion]
cos
= KindCoercion -> m KindCoercion
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return KindCoercion
co
| Bool
otherwise
= (() :: Constraint) =>
Role -> TyCon -> [KindCoercion] -> KindCoercion
Role -> TyCon -> [KindCoercion] -> KindCoercion
mkTyConAppCo Role
r TyCon
tc ([KindCoercion] -> KindCoercion)
-> m [KindCoercion] -> m KindCoercion
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> env -> [KindCoercion] -> m [KindCoercion]
go_cos env
env [KindCoercion]
cos
go_co env
env (ForAllCo TyVar
tv KindCoercion
kind_co KindCoercion
co)
= do { KindCoercion
kind_co' <- env -> KindCoercion -> m KindCoercion
go_co env
env KindCoercion
kind_co
; (env
env', TyVar
tv') <- env -> TyVar -> ForAllTyFlag -> m (env, TyVar)
tycobinder env
env TyVar
tv ForAllTyFlag
Inferred
; KindCoercion
co' <- env -> KindCoercion -> m KindCoercion
go_co env
env' KindCoercion
co
; KindCoercion -> m KindCoercion
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (KindCoercion -> m KindCoercion) -> KindCoercion -> m KindCoercion
forall a b. (a -> b) -> a -> b
$ TyVar -> KindCoercion -> KindCoercion -> KindCoercion
mkForAllCo TyVar
tv' KindCoercion
kind_co' KindCoercion
co' }
go_prov :: env -> UnivCoProvenance -> m UnivCoProvenance
go_prov env
env (PhantomProv KindCoercion
co) = KindCoercion -> UnivCoProvenance
PhantomProv (KindCoercion -> UnivCoProvenance)
-> m KindCoercion -> m UnivCoProvenance
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> env -> KindCoercion -> m KindCoercion
go_co env
env KindCoercion
co
go_prov env
env (ProofIrrelProv KindCoercion
co) = KindCoercion -> UnivCoProvenance
ProofIrrelProv (KindCoercion -> UnivCoProvenance)
-> m KindCoercion -> m UnivCoProvenance
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> env -> KindCoercion -> m KindCoercion
go_co env
env KindCoercion
co
go_prov env
_ p :: UnivCoProvenance
p@(PluginProv String
_) = UnivCoProvenance -> m UnivCoProvenance
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return UnivCoProvenance
p
go_prov env
_ p :: UnivCoProvenance
p@(CorePrepProv Bool
_) = UnivCoProvenance -> m UnivCoProvenance
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return UnivCoProvenance
p
getTyVar :: HasDebugCallStack => Type -> TyVar
getTyVar :: (() :: Constraint) => Type -> TyVar
getTyVar Type
ty = case Type -> Maybe TyVar
getTyVar_maybe Type
ty of
Just TyVar
tv -> TyVar
tv
Maybe TyVar
Nothing -> String -> SDoc -> TyVar
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"getTyVar" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty)
getTyVar_maybe :: Type -> Maybe TyVar
getTyVar_maybe :: Type -> Maybe TyVar
getTyVar_maybe = Type -> Maybe TyVar
repGetTyVar_maybe (Type -> Maybe TyVar) -> (Type -> Type) -> Type -> Maybe TyVar
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Type
coreFullView
repGetTyVar_maybe :: Type -> Maybe TyVar
repGetTyVar_maybe :: Type -> Maybe TyVar
repGetTyVar_maybe (TyVarTy TyVar
tv) = TyVar -> Maybe TyVar
forall a. a -> Maybe a
Just TyVar
tv
repGetTyVar_maybe Type
_ = Maybe TyVar
forall a. Maybe a
Nothing
isTyVarTy :: Type -> Bool
isTyVarTy :: Type -> Bool
isTyVarTy Type
ty = Maybe TyVar -> Bool
forall a. Maybe a -> Bool
isJust (Type -> Maybe TyVar
getTyVar_maybe Type
ty)
getCastedTyVar_maybe :: Type -> Maybe (TyVar, CoercionN)
getCastedTyVar_maybe :: Type -> Maybe (TyVar, KindCoercion)
getCastedTyVar_maybe Type
ty = case Type -> Type
coreFullView Type
ty of
CastTy (TyVarTy TyVar
tv) KindCoercion
co -> (TyVar, KindCoercion) -> Maybe (TyVar, KindCoercion)
forall a. a -> Maybe a
Just (TyVar
tv, KindCoercion
co)
TyVarTy TyVar
tv -> (TyVar, KindCoercion) -> Maybe (TyVar, KindCoercion)
forall a. a -> Maybe a
Just (TyVar
tv, Role -> Type -> KindCoercion
mkReflCo Role
Nominal (TyVar -> Type
tyVarKind TyVar
tv))
Type
_ -> Maybe (TyVar, KindCoercion)
forall a. Maybe a
Nothing
mkAppTy :: Type -> Type -> Type
mkAppTy :: Type -> Type -> Type
mkAppTy (CastTy Type
fun_ty KindCoercion
co) Type
arg_ty
| ([KindCoercion
arg_co], KindCoercion
res_co) <- (() :: Constraint) =>
KindCoercion
-> Pair Type -> [Type] -> ([KindCoercion], KindCoercion)
KindCoercion
-> Pair Type -> [Type] -> ([KindCoercion], KindCoercion)
decomposePiCos KindCoercion
co (KindCoercion -> Pair Type
coercionKind KindCoercion
co) [Type
arg_ty]
= (Type
fun_ty Type -> Type -> Type
`mkAppTy` (Type
arg_ty Type -> KindCoercion -> Type
`mkCastTy` KindCoercion
arg_co)) Type -> KindCoercion -> Type
`mkCastTy` KindCoercion
res_co
mkAppTy (TyConApp TyCon
tc [Type]
tys) Type
ty2 = TyCon -> [Type] -> Type
mkTyConApp TyCon
tc ([Type]
tys [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type
ty2])
mkAppTy Type
ty1 Type
ty2 = Type -> Type -> Type
AppTy Type
ty1 Type
ty2
mkAppTys :: Type -> [Type] -> Type
mkAppTys :: Type -> [Type] -> Type
mkAppTys Type
ty1 [] = Type
ty1
mkAppTys (CastTy Type
fun_ty KindCoercion
co) [Type]
arg_tys
= (Type -> Type -> Type) -> Type -> [Type] -> Type
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Type -> Type -> Type
AppTy ((Type -> [Type] -> Type
mkAppTys Type
fun_ty [Type]
casted_arg_tys) Type -> KindCoercion -> Type
`mkCastTy` KindCoercion
res_co) [Type]
leftovers
where
([KindCoercion]
arg_cos, KindCoercion
res_co) = (() :: Constraint) =>
KindCoercion
-> Pair Type -> [Type] -> ([KindCoercion], KindCoercion)
KindCoercion
-> Pair Type -> [Type] -> ([KindCoercion], KindCoercion)
decomposePiCos KindCoercion
co (KindCoercion -> Pair Type
coercionKind KindCoercion
co) [Type]
arg_tys
([Type]
args_to_cast, [Type]
leftovers) = [KindCoercion] -> [Type] -> ([Type], [Type])
forall b a. [b] -> [a] -> ([a], [a])
splitAtList [KindCoercion]
arg_cos [Type]
arg_tys
casted_arg_tys :: [Type]
casted_arg_tys = (Type -> KindCoercion -> Type)
-> [Type] -> [KindCoercion] -> [Type]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Type -> KindCoercion -> Type
mkCastTy [Type]
args_to_cast [KindCoercion]
arg_cos
mkAppTys (TyConApp TyCon
tc [Type]
tys1) [Type]
tys2 = TyCon -> [Type] -> Type
mkTyConApp TyCon
tc ([Type]
tys1 [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type]
tys2)
mkAppTys Type
ty1 [Type]
tys2 = (Type -> Type -> Type) -> Type -> [Type] -> Type
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Type -> Type -> Type
AppTy Type
ty1 [Type]
tys2
splitAppTy_maybe :: Type -> Maybe (Type, Type)
splitAppTy_maybe :: Type -> Maybe (Type, Type)
splitAppTy_maybe = (() :: Constraint) => Type -> Maybe (Type, Type)
Type -> Maybe (Type, Type)
splitAppTyNoView_maybe (Type -> Maybe (Type, Type))
-> (Type -> Type) -> Type -> Maybe (Type, Type)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Type
coreFullView
splitAppTy :: Type -> (Type, Type)
splitAppTy :: Type -> (Type, Type)
splitAppTy Type
ty = Type -> Maybe (Type, Type)
splitAppTy_maybe Type
ty Maybe (Type, Type) -> (Type, Type) -> (Type, Type)
forall a. Maybe a -> a -> a
`orElse` String -> SDoc -> (Type, Type)
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"splitAppTy" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty)
splitAppTyNoView_maybe :: HasDebugCallStack => Type -> Maybe (Type,Type)
splitAppTyNoView_maybe :: (() :: Constraint) => Type -> Maybe (Type, Type)
splitAppTyNoView_maybe (AppTy Type
ty1 Type
ty2)
= (Type, Type) -> Maybe (Type, Type)
forall a. a -> Maybe a
Just (Type
ty1, Type
ty2)
splitAppTyNoView_maybe (FunTy FunTyFlag
af Type
w Type
ty1 Type
ty2)
| Just (TyCon
tc, [Type]
tys) <- FunTyFlag -> Type -> Type -> Type -> Maybe (TyCon, [Type])
funTyConAppTy_maybe FunTyFlag
af Type
w Type
ty1 Type
ty2
, Just ([Type]
tys', Type
ty') <- [Type] -> Maybe ([Type], Type)
forall a. [a] -> Maybe ([a], a)
snocView [Type]
tys
= (Type, Type) -> Maybe (Type, Type)
forall a. a -> Maybe a
Just (TyCon -> [Type] -> Type
TyConApp TyCon
tc [Type]
tys', Type
ty')
splitAppTyNoView_maybe (TyConApp TyCon
tc [Type]
tys)
| Bool -> Bool
not (TyCon -> Bool
tyConMustBeSaturated TyCon
tc) Bool -> Bool -> Bool
|| [Type]
tys [Type] -> Arity -> Bool
forall a. [a] -> Arity -> Bool
`lengthExceeds` TyCon -> Arity
tyConArity TyCon
tc
, Just ([Type]
tys', Type
ty') <- [Type] -> Maybe ([Type], Type)
forall a. [a] -> Maybe ([a], a)
snocView [Type]
tys
= (Type, Type) -> Maybe (Type, Type)
forall a. a -> Maybe a
Just (TyCon -> [Type] -> Type
TyConApp TyCon
tc [Type]
tys', Type
ty')
splitAppTyNoView_maybe Type
_other = Maybe (Type, Type)
forall a. Maybe a
Nothing
tcSplitAppTyNoView_maybe :: Type -> Maybe (Type,Type)
tcSplitAppTyNoView_maybe :: Type -> Maybe (Type, Type)
tcSplitAppTyNoView_maybe Type
ty
| FunTy { ft_af :: Type -> FunTyFlag
ft_af = FunTyFlag
af } <- Type
ty
, Bool -> Bool
not (FunTyFlag -> Bool
isVisibleFunArg FunTyFlag
af)
= Maybe (Type, Type)
forall a. Maybe a
Nothing
| Bool
otherwise
= (() :: Constraint) => Type -> Maybe (Type, Type)
Type -> Maybe (Type, Type)
splitAppTyNoView_maybe Type
ty
splitAppTys :: Type -> (Type, [Type])
splitAppTys :: Type -> (Type, [Type])
splitAppTys Type
ty = Type -> Type -> [Type] -> (Type, [Type])
split Type
ty Type
ty []
where
split :: Type -> Type -> [Type] -> (Type, [Type])
split Type
orig_ty Type
ty [Type]
args | Just Type
ty' <- Type -> Maybe Type
coreView Type
ty = Type -> Type -> [Type] -> (Type, [Type])
split Type
orig_ty Type
ty' [Type]
args
split Type
_ (AppTy Type
ty Type
arg) [Type]
args = Type -> Type -> [Type] -> (Type, [Type])
split Type
ty Type
ty (Type
argType -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:[Type]
args)
split Type
_ (TyConApp TyCon
tc [Type]
tc_args) [Type]
args
= let
n :: Arity
n | TyCon -> Bool
tyConMustBeSaturated TyCon
tc = TyCon -> Arity
tyConArity TyCon
tc
| Bool
otherwise = Arity
0
([Type]
tc_args1, [Type]
tc_args2) = Arity -> [Type] -> ([Type], [Type])
forall a. Arity -> [a] -> ([a], [a])
splitAt Arity
n [Type]
tc_args
in
(TyCon -> [Type] -> Type
TyConApp TyCon
tc [Type]
tc_args1, [Type]
tc_args2 [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type]
args)
split Type
_ (FunTy FunTyFlag
af Type
w Type
ty1 Type
ty2) [Type]
args
| Just (TyCon
tc,[Type]
tys) <- FunTyFlag -> Type -> Type -> Type -> Maybe (TyCon, [Type])
funTyConAppTy_maybe FunTyFlag
af Type
w Type
ty1 Type
ty2
= Bool -> (Type, [Type]) -> (Type, [Type])
forall a. HasCallStack => Bool -> a -> a
assert ([Type] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
args )
(TyCon -> [Type] -> Type
TyConApp TyCon
tc [], [Type]
tys)
split Type
orig_ty Type
_ [Type]
args = (Type
orig_ty, [Type]
args)
splitAppTysNoView :: HasDebugCallStack => Type -> (Type, [Type])
splitAppTysNoView :: (() :: Constraint) => Type -> (Type, [Type])
splitAppTysNoView Type
ty = Type -> [Type] -> (Type, [Type])
split Type
ty []
where
split :: Type -> [Type] -> (Type, [Type])
split (AppTy Type
ty Type
arg) [Type]
args = Type -> [Type] -> (Type, [Type])
split Type
ty (Type
argType -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:[Type]
args)
split (TyConApp TyCon
tc [Type]
tc_args) [Type]
args
= let n :: Arity
n | TyCon -> Bool
tyConMustBeSaturated TyCon
tc = TyCon -> Arity
tyConArity TyCon
tc
| Bool
otherwise = Arity
0
([Type]
tc_args1, [Type]
tc_args2) = Arity -> [Type] -> ([Type], [Type])
forall a. Arity -> [a] -> ([a], [a])
splitAt Arity
n [Type]
tc_args
in
(TyCon -> [Type] -> Type
TyConApp TyCon
tc [Type]
tc_args1, [Type]
tc_args2 [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type]
args)
split (FunTy FunTyFlag
af Type
w Type
ty1 Type
ty2) [Type]
args
| Just (TyCon
tc, [Type]
tys) <- FunTyFlag -> Type -> Type -> Type -> Maybe (TyCon, [Type])
funTyConAppTy_maybe FunTyFlag
af Type
w Type
ty1 Type
ty2
= Bool -> (Type, [Type]) -> (Type, [Type])
forall a. HasCallStack => Bool -> a -> a
assert ([Type] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
args )
(TyCon -> [Type] -> Type
TyConApp TyCon
tc [], [Type]
tys)
split Type
ty [Type]
args = (Type
ty, [Type]
args)
mkNumLitTy :: Integer -> Type
mkNumLitTy :: Integer -> Type
mkNumLitTy Integer
n = TyLit -> Type
LitTy (Integer -> TyLit
NumTyLit Integer
n)
isNumLitTy :: Type -> Maybe Integer
isNumLitTy :: Type -> Maybe Integer
isNumLitTy Type
ty
| LitTy (NumTyLit Integer
n) <- Type -> Type
coreFullView Type
ty = Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
n
| Bool
otherwise = Maybe Integer
forall a. Maybe a
Nothing
mkStrLitTy :: FastString -> Type
mkStrLitTy :: FastString -> Type
mkStrLitTy FastString
s = TyLit -> Type
LitTy (FastString -> TyLit
StrTyLit FastString
s)
isStrLitTy :: Type -> Maybe FastString
isStrLitTy :: Type -> Maybe FastString
isStrLitTy Type
ty
| LitTy (StrTyLit FastString
s) <- Type -> Type
coreFullView Type
ty = FastString -> Maybe FastString
forall a. a -> Maybe a
Just FastString
s
| Bool
otherwise = Maybe FastString
forall a. Maybe a
Nothing
mkCharLitTy :: Char -> Type
mkCharLitTy :: Char -> Type
mkCharLitTy Char
c = TyLit -> Type
LitTy (Char -> TyLit
CharTyLit Char
c)
isCharLitTy :: Type -> Maybe Char
isCharLitTy :: Type -> Maybe Char
isCharLitTy Type
ty
| LitTy (CharTyLit Char
s) <- Type -> Type
coreFullView Type
ty = Char -> Maybe Char
forall a. a -> Maybe a
Just Char
s
| Bool
otherwise = Maybe Char
forall a. Maybe a
Nothing
isLitTy :: Type -> Maybe TyLit
isLitTy :: Type -> Maybe TyLit
isLitTy Type
ty
| LitTy TyLit
l <- Type -> Type
coreFullView Type
ty = TyLit -> Maybe TyLit
forall a. a -> Maybe a
Just TyLit
l
| Bool
otherwise = Maybe TyLit
forall a. Maybe a
Nothing
userTypeError_maybe :: Type -> Maybe Type
userTypeError_maybe :: Type -> Maybe Type
userTypeError_maybe Type
t
= do { (TyCon
tc, Type
_kind : Type
msg : [Type]
_) <- (() :: Constraint) => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
t
; Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (TyCon -> Name
tyConName TyCon
tc Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
errorMessageTypeErrorFamName)
; Type -> Maybe Type
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return Type
msg }
pprUserTypeErrorTy :: Type -> SDoc
pprUserTypeErrorTy :: Type -> SDoc
pprUserTypeErrorTy Type
ty =
case (() :: Constraint) => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
ty of
Just (TyCon
tc,[Type
txt])
| TyCon -> Name
tyConName TyCon
tc Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
typeErrorTextDataConName
, Just FastString
str <- Type -> Maybe FastString
isStrLitTy Type
txt -> FastString -> SDoc
forall doc. IsLine doc => FastString -> doc
ftext FastString
str
Just (TyCon
tc,[Type
_k,Type
t])
| TyCon -> Name
tyConName TyCon
tc Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
typeErrorShowTypeDataConName -> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
t
Just (TyCon
tc,[Type
t1,Type
t2])
| TyCon -> Name
tyConName TyCon
tc Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
typeErrorAppendDataConName ->
Type -> SDoc
pprUserTypeErrorTy Type
t1 SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> Type -> SDoc
pprUserTypeErrorTy Type
t2
Just (TyCon
tc,[Type
t1,Type
t2])
| TyCon -> Name
tyConName TyCon
tc Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
typeErrorVAppendDataConName ->
Type -> SDoc
pprUserTypeErrorTy Type
t1 SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ Type -> SDoc
pprUserTypeErrorTy Type
t2
Maybe (TyCon, [Type])
_ -> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty
funTyConAppTy_maybe :: FunTyFlag -> Type -> Type -> Type
-> Maybe (TyCon, [Type])
funTyConAppTy_maybe :: FunTyFlag -> Type -> Type -> Type -> Maybe (TyCon, [Type])
funTyConAppTy_maybe FunTyFlag
af Type
mult Type
arg Type
res
| Just Type
arg_rep <- (() :: Constraint) => Type -> Maybe Type
Type -> Maybe Type
getRuntimeRep_maybe Type
arg
, Just Type
res_rep <- (() :: Constraint) => Type -> Maybe Type
Type -> Maybe Type
getRuntimeRep_maybe Type
res
, let args :: [Type]
args | FunTyFlag -> Bool
isFUNArg FunTyFlag
af = [Type
mult, Type
arg_rep, Type
res_rep, Type
arg, Type
res]
| Bool
otherwise = [ Type
arg_rep, Type
res_rep, Type
arg, Type
res]
= (TyCon, [Type]) -> Maybe (TyCon, [Type])
forall a. a -> Maybe a
Just ((TyCon, [Type]) -> Maybe (TyCon, [Type]))
-> (TyCon, [Type]) -> Maybe (TyCon, [Type])
forall a b. (a -> b) -> a -> b
$ (FunTyFlag -> TyCon
funTyFlagTyCon FunTyFlag
af, [Type]
args)
| Bool
otherwise
= Maybe (TyCon, [Type])
forall a. Maybe a
Nothing
tyConAppFunTy_maybe :: HasDebugCallStack => TyCon -> [Type] -> Maybe Type
tyConAppFunTy_maybe :: (() :: Constraint) => TyCon -> [Type] -> Maybe Type
tyConAppFunTy_maybe TyCon
tc [Type]
tys
| Just (FunTyFlag
af, Type
mult, Type
arg, Type
res) <- Type -> TyCon -> [Type] -> Maybe (FunTyFlag, Type, Type, Type)
forall a.
(() :: Constraint, Outputable a) =>
a -> TyCon -> [a] -> Maybe (FunTyFlag, a, a, a)
ty_con_app_fun_maybe Type
manyDataConTy TyCon
tc [Type]
tys
= Type -> Maybe Type
forall a. a -> Maybe a
Just (FunTy { ft_af :: FunTyFlag
ft_af = FunTyFlag
af, ft_mult :: Type
ft_mult = Type
mult, ft_arg :: Type
ft_arg = Type
arg, ft_res :: Type
ft_res = Type
res })
| Bool
otherwise = Maybe Type
forall a. Maybe a
Nothing
tyConAppFunCo_maybe :: HasDebugCallStack => Role -> TyCon -> [Coercion]
-> Maybe Coercion
tyConAppFunCo_maybe :: (() :: Constraint) =>
Role -> TyCon -> [KindCoercion] -> Maybe KindCoercion
tyConAppFunCo_maybe Role
r TyCon
tc [KindCoercion]
cos
| Just (FunTyFlag
af, KindCoercion
mult, KindCoercion
arg, KindCoercion
res) <- KindCoercion
-> TyCon
-> [KindCoercion]
-> Maybe (FunTyFlag, KindCoercion, KindCoercion, KindCoercion)
forall a.
(() :: Constraint, Outputable a) =>
a -> TyCon -> [a] -> Maybe (FunTyFlag, a, a, a)
ty_con_app_fun_maybe (Role -> Type -> KindCoercion
mkReflCo Role
r Type
manyDataConTy) TyCon
tc [KindCoercion]
cos
= KindCoercion -> Maybe KindCoercion
forall a. a -> Maybe a
Just ((() :: Constraint) =>
Role
-> FunTyFlag
-> KindCoercion
-> KindCoercion
-> KindCoercion
-> KindCoercion
Role
-> FunTyFlag
-> KindCoercion
-> KindCoercion
-> KindCoercion
-> KindCoercion
mkFunCo1 Role
r FunTyFlag
af KindCoercion
mult KindCoercion
arg KindCoercion
res)
| Bool
otherwise = Maybe KindCoercion
forall a. Maybe a
Nothing
ty_con_app_fun_maybe :: (HasDebugCallStack, Outputable a) => a -> TyCon -> [a]
-> Maybe (FunTyFlag, a, a, a)
{-# INLINE ty_con_app_fun_maybe #-}
ty_con_app_fun_maybe :: forall a.
(() :: Constraint, Outputable a) =>
a -> TyCon -> [a] -> Maybe (FunTyFlag, a, a, a)
ty_con_app_fun_maybe a
many_ty_co TyCon
tc [a]
args
| Unique
tc_uniq Unique -> Unique -> Bool
forall a. Eq a => a -> a -> Bool
== Unique
fUNTyConKey = Maybe (FunTyFlag, a, a, a)
fUN_case
| Unique
tc_uniq Unique -> Unique -> Bool
forall a. Eq a => a -> a -> Bool
== Unique
tcArrowTyConKey = FunTyFlag -> Maybe (FunTyFlag, a, a, a)
non_FUN_case FunTyFlag
FTF_T_C
| Unique
tc_uniq Unique -> Unique -> Bool
forall a. Eq a => a -> a -> Bool
== Unique
ctArrowTyConKey = FunTyFlag -> Maybe (FunTyFlag, a, a, a)
non_FUN_case FunTyFlag
FTF_C_T
| Unique
tc_uniq Unique -> Unique -> Bool
forall a. Eq a => a -> a -> Bool
== Unique
ccArrowTyConKey = FunTyFlag -> Maybe (FunTyFlag, a, a, a)
non_FUN_case FunTyFlag
FTF_C_C
| Bool
otherwise = Maybe (FunTyFlag, a, a, a)
forall a. Maybe a
Nothing
where
tc_uniq :: Unique
tc_uniq = TyCon -> Unique
tyConUnique TyCon
tc
fUN_case :: Maybe (FunTyFlag, a, a, a)
fUN_case
| (a
w:a
_r1:a
_r2:a
a1:a
a2:[a]
rest) <- [a]
args
= Bool
-> SDoc -> Maybe (FunTyFlag, a, a, a) -> Maybe (FunTyFlag, a, a, a)
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr ([a] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [a]
rest) (TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCon
tc SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [a] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [a]
args) (Maybe (FunTyFlag, a, a, a) -> Maybe (FunTyFlag, a, a, a))
-> Maybe (FunTyFlag, a, a, a) -> Maybe (FunTyFlag, a, a, a)
forall a b. (a -> b) -> a -> b
$
(FunTyFlag, a, a, a) -> Maybe (FunTyFlag, a, a, a)
forall a. a -> Maybe a
Just (FunTyFlag
FTF_T_T, a
w, a
a1, a
a2)
| Bool
otherwise = Maybe (FunTyFlag, a, a, a)
forall a. Maybe a
Nothing
non_FUN_case :: FunTyFlag -> Maybe (FunTyFlag, a, a, a)
non_FUN_case FunTyFlag
ftf
| (a
_r1:a
_r2:a
a1:a
a2:[a]
rest) <- [a]
args
= Bool
-> SDoc -> Maybe (FunTyFlag, a, a, a) -> Maybe (FunTyFlag, a, a, a)
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr ([a] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [a]
rest) (TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCon
tc SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [a] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [a]
args) (Maybe (FunTyFlag, a, a, a) -> Maybe (FunTyFlag, a, a, a))
-> Maybe (FunTyFlag, a, a, a) -> Maybe (FunTyFlag, a, a, a)
forall a b. (a -> b) -> a -> b
$
(FunTyFlag, a, a, a) -> Maybe (FunTyFlag, a, a, a)
forall a. a -> Maybe a
Just (FunTyFlag
ftf, a
many_ty_co, a
a1, a
a2)
| Bool
otherwise
= Maybe (FunTyFlag, a, a, a)
forall a. Maybe a
Nothing
mkFunctionType :: HasDebugCallStack => Mult -> Type -> Type -> Type
mkFunctionType :: (() :: Constraint) => Type -> Type -> Type -> Type
mkFunctionType Type
mult Type
arg_ty Type
res_ty
= FunTy { ft_af :: FunTyFlag
ft_af = FunTyFlag
af, ft_arg :: Type
ft_arg = Type
arg_ty, ft_res :: Type
ft_res = Type
res_ty
, ft_mult :: Type
ft_mult = Bool -> SDoc -> Type -> Type
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr Bool
mult_ok ([Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type
mult, Type
arg_ty, Type
res_ty]) (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$
Type
mult }
where
af :: FunTyFlag
af = (() :: Constraint) => Type -> Type -> FunTyFlag
Type -> Type -> FunTyFlag
chooseFunTyFlag Type
arg_ty Type
res_ty
mult_ok :: Bool
mult_ok = FunTyFlag -> Bool
isVisibleFunArg FunTyFlag
af Bool -> Bool -> Bool
|| Type -> Bool
isManyTy Type
mult
mkScaledFunctionTys :: [Scaled Type] -> Type -> Type
mkScaledFunctionTys :: [Scaled Type] -> Type -> Type
mkScaledFunctionTys [Scaled Type]
arg_tys Type
res_ty
= (Scaled Type -> Type -> Type) -> Type -> [Scaled Type] -> Type
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Scaled Type -> Type -> Type
mk Type
res_ty [Scaled Type]
arg_tys
where
mk :: Scaled Type -> Type -> Type
mk (Scaled Type
mult Type
arg_ty) Type
res_ty
= (() :: Constraint) => FunTyFlag -> Type -> Type -> Type -> Type
FunTyFlag -> Type -> Type -> Type -> Type
mkFunTy ((() :: Constraint) => Type -> Type -> FunTyFlag
Type -> Type -> FunTyFlag
chooseFunTyFlag Type
arg_ty Type
res_ty)
Type
mult Type
arg_ty Type
res_ty
chooseFunTyFlag :: HasDebugCallStack => Type -> Type -> FunTyFlag
chooseFunTyFlag :: (() :: Constraint) => Type -> Type -> FunTyFlag
chooseFunTyFlag Type
arg_ty Type
res_ty
= TypeOrConstraint -> TypeOrConstraint -> FunTyFlag
mkFunTyFlag ((() :: Constraint) => Type -> TypeOrConstraint
Type -> TypeOrConstraint
typeTypeOrConstraint Type
arg_ty) ((() :: Constraint) => Type -> TypeOrConstraint
Type -> TypeOrConstraint
typeTypeOrConstraint Type
res_ty)
splitFunTy :: Type -> (Mult, Type, Type)
splitFunTy :: Type -> (Type, Type, Type)
splitFunTy Type
ty = case Type -> Maybe (FunTyFlag, Type, Type, Type)
splitFunTy_maybe Type
ty of
Just (FunTyFlag
_af, Type
mult, Type
arg, Type
res) -> (Type
mult,Type
arg,Type
res)
Maybe (FunTyFlag, Type, Type, Type)
Nothing -> String -> SDoc -> (Type, Type, Type)
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"splitFunTy" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty)
{-# INLINE splitFunTy_maybe #-}
splitFunTy_maybe :: Type -> Maybe (FunTyFlag, Mult, Type, Type)
splitFunTy_maybe :: Type -> Maybe (FunTyFlag, Type, Type, Type)
splitFunTy_maybe Type
ty
| FunTy FunTyFlag
af Type
w Type
arg Type
res <- Type -> Type
coreFullView Type
ty = (FunTyFlag, Type, Type, Type)
-> Maybe (FunTyFlag, Type, Type, Type)
forall a. a -> Maybe a
Just (FunTyFlag
af, Type
w, Type
arg, Type
res)
| Bool
otherwise = Maybe (FunTyFlag, Type, Type, Type)
forall a. Maybe a
Nothing
splitFunTys :: Type -> ([Scaled Type], Type)
splitFunTys :: Type -> ([Scaled Type], Type)
splitFunTys Type
ty = [Scaled Type] -> Type -> Type -> ([Scaled Type], Type)
split [] Type
ty Type
ty
where
split :: [Scaled Type] -> Type -> Type -> ([Scaled Type], Type)
split [Scaled Type]
args Type
_ (FunTy FunTyFlag
_ Type
w Type
arg Type
res) = [Scaled Type] -> Type -> Type -> ([Scaled Type], Type)
split (Type -> Type -> Scaled Type
forall a. Type -> a -> Scaled a
Scaled Type
w Type
arg Scaled Type -> [Scaled Type] -> [Scaled Type]
forall a. a -> [a] -> [a]
: [Scaled Type]
args) Type
res Type
res
split [Scaled Type]
args Type
orig_ty Type
ty | Just Type
ty' <- Type -> Maybe Type
coreView Type
ty = [Scaled Type] -> Type -> Type -> ([Scaled Type], Type)
split [Scaled Type]
args Type
orig_ty Type
ty'
split [Scaled Type]
args Type
orig_ty Type
_ = ([Scaled Type] -> [Scaled Type]
forall a. [a] -> [a]
reverse [Scaled Type]
args, Type
orig_ty)
funResultTy :: HasDebugCallStack => Type -> Type
funResultTy :: (() :: Constraint) => Type -> Type
funResultTy Type
ty
| FunTy { ft_res :: Type -> Type
ft_res = Type
res } <- Type -> Type
coreFullView Type
ty = Type
res
| Bool
otherwise = String -> SDoc -> Type
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"funResultTy" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty)
funArgTy :: Type -> Type
funArgTy :: Type -> Type
funArgTy Type
ty
| FunTy { ft_arg :: Type -> Type
ft_arg = Type
arg } <- Type -> Type
coreFullView Type
ty = Type
arg
| Bool
otherwise = String -> SDoc -> Type
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"funArgTy" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty)
piResultTy :: HasDebugCallStack => Type -> Type -> Type
piResultTy :: (() :: Constraint) => Type -> Type -> Type
piResultTy Type
ty Type
arg = case Type -> Type -> Maybe Type
piResultTy_maybe Type
ty Type
arg of
Just Type
res -> Type
res
Maybe Type
Nothing -> String -> SDoc -> Type
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"piResultTy" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
arg)
piResultTy_maybe :: Type -> Type -> Maybe Type
piResultTy_maybe :: Type -> Type -> Maybe Type
piResultTy_maybe Type
ty Type
arg = case Type -> Type
coreFullView Type
ty of
FunTy { ft_res :: Type -> Type
ft_res = Type
res } -> Type -> Maybe Type
forall a. a -> Maybe a
Just Type
res
ForAllTy (Bndr TyVar
tv ForAllTyFlag
_) Type
res
-> let empty_subst :: Subst
empty_subst = InScopeSet -> Subst
mkEmptySubst (InScopeSet -> Subst) -> InScopeSet -> Subst
forall a b. (a -> b) -> a -> b
$ VarSet -> InScopeSet
mkInScopeSet (VarSet -> InScopeSet) -> VarSet -> InScopeSet
forall a b. (a -> b) -> a -> b
$
[Type] -> VarSet
tyCoVarsOfTypes [Type
arg,Type
res]
in Type -> Maybe Type
forall a. a -> Maybe a
Just ((() :: Constraint) => Subst -> Type -> Type
Subst -> Type -> Type
substTy (Subst -> TyVar -> Type -> Subst
extendTCvSubst Subst
empty_subst TyVar
tv Type
arg) Type
res)
Type
_ -> Maybe Type
forall a. Maybe a
Nothing
piResultTys :: HasDebugCallStack => Type -> [Type] -> Type
piResultTys :: (() :: Constraint) => Type -> [Type] -> Type
piResultTys Type
ty [] = Type
ty
piResultTys Type
ty orig_args :: [Type]
orig_args@(Type
arg:[Type]
args)
| FunTy { ft_res :: Type -> Type
ft_res = Type
res } <- Type
ty
= (() :: Constraint) => Type -> [Type] -> Type
Type -> [Type] -> Type
piResultTys Type
res [Type]
args
| ForAllTy (Bndr TyVar
tv ForAllTyFlag
_) Type
res <- Type
ty
= Subst -> Type -> [Type] -> Type
go (Subst -> TyVar -> Type -> Subst
extendTCvSubst Subst
init_subst TyVar
tv Type
arg) Type
res [Type]
args
| Just Type
ty' <- Type -> Maybe Type
coreView Type
ty
= (() :: Constraint) => Type -> [Type] -> Type
Type -> [Type] -> Type
piResultTys Type
ty' [Type]
orig_args
| Bool
otherwise
= String -> SDoc -> Type
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"piResultTys1" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
orig_args)
where
init_subst :: Subst
init_subst = InScopeSet -> Subst
mkEmptySubst (InScopeSet -> Subst) -> InScopeSet -> Subst
forall a b. (a -> b) -> a -> b
$ VarSet -> InScopeSet
mkInScopeSet ([Type] -> VarSet
tyCoVarsOfTypes (Type
tyType -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:[Type]
orig_args))
go :: Subst -> Type -> [Type] -> Type
go :: Subst -> Type -> [Type] -> Type
go Subst
subst Type
ty [] = Subst -> Type -> Type
substTyUnchecked Subst
subst Type
ty
go Subst
subst Type
ty all_args :: [Type]
all_args@(Type
arg:[Type]
args)
| FunTy { ft_res :: Type -> Type
ft_res = Type
res } <- Type
ty
= Subst -> Type -> [Type] -> Type
go Subst
subst Type
res [Type]
args
| ForAllTy (Bndr TyVar
tv ForAllTyFlag
_) Type
res <- Type
ty
= Subst -> Type -> [Type] -> Type
go (Subst -> TyVar -> Type -> Subst
extendTCvSubst Subst
subst TyVar
tv Type
arg) Type
res [Type]
args
| Just Type
ty' <- Type -> Maybe Type
coreView Type
ty
= Subst -> Type -> [Type] -> Type
go Subst
subst Type
ty' [Type]
all_args
| Bool -> Bool
not (Subst -> Bool
isEmptyTCvSubst Subst
subst)
= Subst -> Type -> [Type] -> Type
go Subst
init_subst
((() :: Constraint) => Subst -> Type -> Type
Subst -> Type -> Type
substTy Subst
subst Type
ty)
[Type]
all_args
| Bool
otherwise
=
String -> SDoc -> Type
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"piResultTys2" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
orig_args SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
all_args)
applyTysX :: HasDebugCallStack => [TyVar] -> Type -> [Type] -> Type
applyTysX :: (() :: Constraint) => [TyVar] -> Type -> [Type] -> Type
applyTysX [TyVar]
tvs Type
body_ty [Type]
arg_tys
= Bool -> SDoc -> Type -> Type
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr ([TyVar]
tvs [TyVar] -> [Type] -> Bool
forall a b. [a] -> [b] -> Bool
`leLength` [Type]
arg_tys) SDoc
pp_stuff (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$
Bool -> SDoc -> Type -> Type
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (Type -> VarSet
tyCoVarsOfType Type
body_ty VarSet -> VarSet -> Bool
`subVarSet` [TyVar] -> VarSet
mkVarSet [TyVar]
tvs) SDoc
pp_stuff (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$
Type -> [Type] -> Type
mkAppTys ([TyVar] -> [Type] -> Type -> Type
(() :: Constraint) => [TyVar] -> [Type] -> Type -> Type
substTyWith [TyVar]
tvs [Type]
arg_tys_prefix Type
body_ty)
[Type]
arg_tys_rest
where
pp_stuff :: SDoc
pp_stuff = [SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [[TyVar] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [TyVar]
tvs, Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
body_ty, [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
arg_tys]
([Type]
arg_tys_prefix, [Type]
arg_tys_rest) = [TyVar] -> [Type] -> ([Type], [Type])
forall b a. [b] -> [a] -> ([a], [a])
splitAtList [TyVar]
tvs [Type]
arg_tys
tyConAppTyConPicky_maybe :: Type -> Maybe TyCon
tyConAppTyConPicky_maybe :: Type -> Maybe TyCon
tyConAppTyConPicky_maybe (TyConApp TyCon
tc [Type]
_) = TyCon -> Maybe TyCon
forall a. a -> Maybe a
Just TyCon
tc
tyConAppTyConPicky_maybe (FunTy { ft_af :: Type -> FunTyFlag
ft_af = FunTyFlag
af }) = TyCon -> Maybe TyCon
forall a. a -> Maybe a
Just (FunTyFlag -> TyCon
funTyFlagTyCon FunTyFlag
af)
tyConAppTyConPicky_maybe Type
_ = Maybe TyCon
forall a. Maybe a
Nothing
{-# INLINE tyConAppTyCon_maybe #-}
tyConAppTyCon_maybe :: Type -> Maybe TyCon
tyConAppTyCon_maybe :: Type -> Maybe TyCon
tyConAppTyCon_maybe Type
ty = case Type -> Type
coreFullView Type
ty of
TyConApp TyCon
tc [Type]
_ -> TyCon -> Maybe TyCon
forall a. a -> Maybe a
Just TyCon
tc
FunTy { ft_af :: Type -> FunTyFlag
ft_af = FunTyFlag
af } -> TyCon -> Maybe TyCon
forall a. a -> Maybe a
Just (FunTyFlag -> TyCon
funTyFlagTyCon FunTyFlag
af)
Type
_ -> Maybe TyCon
forall a. Maybe a
Nothing
tyConAppTyCon :: HasDebugCallStack => Type -> TyCon
tyConAppTyCon :: (() :: Constraint) => Type -> TyCon
tyConAppTyCon Type
ty = Type -> Maybe TyCon
tyConAppTyCon_maybe Type
ty Maybe TyCon -> TyCon -> TyCon
forall a. Maybe a -> a -> a
`orElse` String -> SDoc -> TyCon
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"tyConAppTyCon" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty)
tyConAppArgs_maybe :: Type -> Maybe [Type]
tyConAppArgs_maybe :: Type -> Maybe [Type]
tyConAppArgs_maybe Type
ty = case (() :: Constraint) => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
ty of
Just (TyCon
_, [Type]
tys) -> [Type] -> Maybe [Type]
forall a. a -> Maybe a
Just [Type]
tys
Maybe (TyCon, [Type])
Nothing -> Maybe [Type]
forall a. Maybe a
Nothing
tyConAppArgs :: HasCallStack => Type -> [Type]
tyConAppArgs :: HasCallStack => Type -> [Type]
tyConAppArgs Type
ty = Type -> Maybe [Type]
tyConAppArgs_maybe Type
ty Maybe [Type] -> [Type] -> [Type]
forall a. Maybe a -> a -> a
`orElse` String -> SDoc -> [Type]
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"tyConAppArgs" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty)
splitTyConApp :: Type -> (TyCon, [Type])
splitTyConApp :: Type -> (TyCon, [Type])
splitTyConApp Type
ty = (() :: Constraint) => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
ty Maybe (TyCon, [Type]) -> (TyCon, [Type]) -> (TyCon, [Type])
forall a. Maybe a -> a -> a
`orElse` String -> SDoc -> (TyCon, [Type])
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"splitTyConApp" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty)
splitTyConApp_maybe :: HasDebugCallStack => Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe :: (() :: Constraint) => Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
ty = Type -> Maybe (TyCon, [Type])
splitTyConAppNoView_maybe (Type -> Type
coreFullView Type
ty)
splitTyConAppNoView_maybe :: Type -> Maybe (TyCon, [Type])
splitTyConAppNoView_maybe :: Type -> Maybe (TyCon, [Type])
splitTyConAppNoView_maybe Type
ty
= case Type
ty of
FunTy { ft_af :: Type -> FunTyFlag
ft_af = FunTyFlag
af, ft_mult :: Type -> Type
ft_mult = Type
w, ft_arg :: Type -> Type
ft_arg = Type
arg, ft_res :: Type -> Type
ft_res = Type
res}
-> FunTyFlag -> Type -> Type -> Type -> Maybe (TyCon, [Type])
funTyConAppTy_maybe FunTyFlag
af Type
w Type
arg Type
res
TyConApp TyCon
tc [Type]
tys -> (TyCon, [Type]) -> Maybe (TyCon, [Type])
forall a. a -> Maybe a
Just (TyCon
tc, [Type]
tys)
Type
_ -> Maybe (TyCon, [Type])
forall a. Maybe a
Nothing
tcSplitTyConApp_maybe :: HasCallStack => Type -> Maybe (TyCon, [Type])
tcSplitTyConApp_maybe :: HasCallStack => Type -> Maybe (TyCon, [Type])
tcSplitTyConApp_maybe Type
ty
= case Type -> Type
coreFullView Type
ty of
FunTy { ft_af :: Type -> FunTyFlag
ft_af = FunTyFlag
af, ft_mult :: Type -> Type
ft_mult = Type
w, ft_arg :: Type -> Type
ft_arg = Type
arg, ft_res :: Type -> Type
ft_res = Type
res}
| FunTyFlag -> Bool
isVisibleFunArg FunTyFlag
af
-> FunTyFlag -> Type -> Type -> Type -> Maybe (TyCon, [Type])
funTyConAppTy_maybe FunTyFlag
af Type
w Type
arg Type
res
TyConApp TyCon
tc [Type]
tys -> (TyCon, [Type]) -> Maybe (TyCon, [Type])
forall a. a -> Maybe a
Just (TyCon
tc, [Type]
tys)
Type
_ -> Maybe (TyCon, [Type])
forall a. Maybe a
Nothing
tcSplitTyConApp :: Type -> (TyCon, [Type])
tcSplitTyConApp :: Type -> (TyCon, [Type])
tcSplitTyConApp Type
ty
= HasCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
tcSplitTyConApp_maybe Type
ty Maybe (TyCon, [Type]) -> (TyCon, [Type]) -> (TyCon, [Type])
forall a. Maybe a -> a -> a
`orElse` String -> SDoc -> (TyCon, [Type])
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"tcSplitTyConApp" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty)
newTyConInstRhs :: TyCon -> [Type] -> Type
newTyConInstRhs :: TyCon -> [Type] -> Type
newTyConInstRhs TyCon
tycon [Type]
tys
= Bool -> SDoc -> Type -> Type
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr ([TyVar]
tvs [TyVar] -> [Type] -> Bool
forall a b. [a] -> [b] -> Bool
`leLength` [Type]
tys) (TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCon
tycon SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
tys SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ [TyVar] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [TyVar]
tvs) (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$
[TyVar] -> Type -> [Type] -> Type
(() :: Constraint) => [TyVar] -> Type -> [Type] -> Type
applyTysX [TyVar]
tvs Type
rhs [Type]
tys
where
([TyVar]
tvs, Type
rhs) = TyCon -> ([TyVar], Type)
newTyConEtadRhs TyCon
tycon
splitCastTy_maybe :: Type -> Maybe (Type, Coercion)
splitCastTy_maybe :: Type -> Maybe (Type, KindCoercion)
splitCastTy_maybe Type
ty
| CastTy Type
ty' KindCoercion
co <- Type -> Type
coreFullView Type
ty = (Type, KindCoercion) -> Maybe (Type, KindCoercion)
forall a. a -> Maybe a
Just (Type
ty', KindCoercion
co)
| Bool
otherwise = Maybe (Type, KindCoercion)
forall a. Maybe a
Nothing
mkCastTy :: Type -> Coercion -> Type
mkCastTy :: Type -> KindCoercion -> Type
mkCastTy Type
orig_ty KindCoercion
co | KindCoercion -> Bool
isReflexiveCo KindCoercion
co = Type
orig_ty
mkCastTy Type
orig_ty KindCoercion
co = Type -> KindCoercion -> Type
mk_cast_ty Type
orig_ty KindCoercion
co
mk_cast_ty :: Type -> Coercion -> Type
mk_cast_ty :: Type -> KindCoercion -> Type
mk_cast_ty Type
orig_ty KindCoercion
co = Type -> Type
go Type
orig_ty
where
go :: Type -> Type
go :: Type -> Type
go Type
ty | Just Type
ty' <- Type -> Maybe Type
coreView Type
ty = Type -> Type
go Type
ty'
go (CastTy Type
ty KindCoercion
co1)
= Type -> KindCoercion -> Type
mkCastTy Type
ty (KindCoercion
co1 KindCoercion -> KindCoercion -> KindCoercion
`mkTransCo` KindCoercion
co)
go (ForAllTy (Bndr TyVar
tv ForAllTyFlag
vis) Type
inner_ty)
| TyVar -> Bool
isTyVar TyVar
tv
, let fvs :: VarSet
fvs = KindCoercion -> VarSet
tyCoVarsOfCo KindCoercion
co
=
if TyVar
tv TyVar -> VarSet -> Bool
`elemVarSet` VarSet
fvs
then let empty_subst :: Subst
empty_subst = InScopeSet -> Subst
mkEmptySubst (VarSet -> InScopeSet
mkInScopeSet VarSet
fvs)
(Subst
subst, TyVar
tv') = (() :: Constraint) => Subst -> TyVar -> (Subst, TyVar)
Subst -> TyVar -> (Subst, TyVar)
substVarBndr Subst
empty_subst TyVar
tv
in VarBndr TyVar ForAllTyFlag -> Type -> Type
ForAllTy (TyVar -> ForAllTyFlag -> VarBndr TyVar ForAllTyFlag
forall var argf. var -> argf -> VarBndr var argf
Bndr TyVar
tv' ForAllTyFlag
vis) ((() :: Constraint) => Subst -> Type -> Type
Subst -> Type -> Type
substTy Subst
subst Type
inner_ty Type -> KindCoercion -> Type
`mk_cast_ty` KindCoercion
co)
else VarBndr TyVar ForAllTyFlag -> Type -> Type
ForAllTy (TyVar -> ForAllTyFlag -> VarBndr TyVar ForAllTyFlag
forall var argf. var -> argf -> VarBndr var argf
Bndr TyVar
tv ForAllTyFlag
vis) (Type
inner_ty Type -> KindCoercion -> Type
`mk_cast_ty` KindCoercion
co)
go Type
_ = Type -> KindCoercion -> Type
CastTy Type
orig_ty KindCoercion
co
mkCoercionTy :: Coercion -> Type
mkCoercionTy :: KindCoercion -> Type
mkCoercionTy = KindCoercion -> Type
CoercionTy
isCoercionTy :: Type -> Bool
isCoercionTy :: Type -> Bool
isCoercionTy (CoercionTy KindCoercion
_) = Bool
True
isCoercionTy Type
_ = Bool
False
isCoercionTy_maybe :: Type -> Maybe Coercion
isCoercionTy_maybe :: Type -> Maybe KindCoercion
isCoercionTy_maybe (CoercionTy KindCoercion
co) = KindCoercion -> Maybe KindCoercion
forall a. a -> Maybe a
Just KindCoercion
co
isCoercionTy_maybe Type
_ = Maybe KindCoercion
forall a. Maybe a
Nothing
stripCoercionTy :: Type -> Coercion
stripCoercionTy :: Type -> KindCoercion
stripCoercionTy (CoercionTy KindCoercion
co) = KindCoercion
co
stripCoercionTy Type
ty = String -> SDoc -> KindCoercion
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"stripCoercionTy" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty)
tyConBindersPiTyBinders :: [TyConBinder] -> [PiTyBinder]
tyConBindersPiTyBinders :: [TyConBinder] -> [PiTyBinder]
tyConBindersPiTyBinders = (TyConBinder -> PiTyBinder) -> [TyConBinder] -> [PiTyBinder]
forall a b. (a -> b) -> [a] -> [b]
map TyConBinder -> PiTyBinder
to_tyb
where
to_tyb :: TyConBinder -> PiTyBinder
to_tyb (Bndr TyVar
tv (NamedTCB ForAllTyFlag
vis)) = VarBndr TyVar ForAllTyFlag -> PiTyBinder
Named (TyVar -> ForAllTyFlag -> VarBndr TyVar ForAllTyFlag
forall var argf. var -> argf -> VarBndr var argf
Bndr TyVar
tv ForAllTyFlag
vis)
to_tyb (Bndr TyVar
tv (AnonTCB FunTyFlag
af)) = Scaled Type -> FunTyFlag -> PiTyBinder
Anon (Type -> Scaled Type
forall a. a -> Scaled a
tymult (TyVar -> Type
varType TyVar
tv)) FunTyFlag
af
mkTyCoInvForAllTy :: TyCoVar -> Type -> Type
mkTyCoInvForAllTy :: TyVar -> Type -> Type
mkTyCoInvForAllTy TyVar
tv Type
ty
| TyVar -> Bool
isCoVar TyVar
tv
, Bool -> Bool
not (TyVar
tv TyVar -> VarSet -> Bool
`elemVarSet` Type -> VarSet
tyCoVarsOfType Type
ty)
= (() :: Constraint) => Type -> Type -> Type
Type -> Type -> Type
mkVisFunTyMany (TyVar -> Type
varType TyVar
tv) Type
ty
| Bool
otherwise
= VarBndr TyVar ForAllTyFlag -> Type -> Type
ForAllTy (TyVar -> ForAllTyFlag -> VarBndr TyVar ForAllTyFlag
forall var argf. var -> argf -> VarBndr var argf
Bndr TyVar
tv ForAllTyFlag
Inferred) Type
ty
mkInfForAllTy :: TyVar -> Type -> Type
mkInfForAllTy :: TyVar -> Type -> Type
mkInfForAllTy TyVar
tv Type
ty = Bool
-> (VarBndr TyVar ForAllTyFlag -> Type -> Type)
-> VarBndr TyVar ForAllTyFlag
-> Type
-> Type
forall a. HasCallStack => Bool -> a -> a
assert (TyVar -> Bool
isTyVar TyVar
tv )
VarBndr TyVar ForAllTyFlag -> Type -> Type
ForAllTy (TyVar -> ForAllTyFlag -> VarBndr TyVar ForAllTyFlag
forall var argf. var -> argf -> VarBndr var argf
Bndr TyVar
tv ForAllTyFlag
Inferred) Type
ty
mkTyCoInvForAllTys :: [TyCoVar] -> Type -> Type
mkTyCoInvForAllTys :: [TyVar] -> Type -> Type
mkTyCoInvForAllTys [TyVar]
tvs Type
ty = (TyVar -> Type -> Type) -> Type -> [TyVar] -> Type
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr TyVar -> Type -> Type
mkTyCoInvForAllTy Type
ty [TyVar]
tvs
mkInfForAllTys :: [TyVar] -> Type -> Type
mkInfForAllTys :: [TyVar] -> Type -> Type
mkInfForAllTys [TyVar]
tvs Type
ty = (TyVar -> Type -> Type) -> Type -> [TyVar] -> Type
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr TyVar -> Type -> Type
mkInfForAllTy Type
ty [TyVar]
tvs
mkSpecForAllTy :: TyVar -> Type -> Type
mkSpecForAllTy :: TyVar -> Type -> Type
mkSpecForAllTy TyVar
tv Type
ty = Bool
-> (VarBndr TyVar ForAllTyFlag -> Type -> Type)
-> VarBndr TyVar ForAllTyFlag
-> Type
-> Type
forall a. HasCallStack => Bool -> a -> a
assert (TyVar -> Bool
isTyVar TyVar
tv )
VarBndr TyVar ForAllTyFlag -> Type -> Type
ForAllTy (TyVar -> ForAllTyFlag -> VarBndr TyVar ForAllTyFlag
forall var argf. var -> argf -> VarBndr var argf
Bndr TyVar
tv ForAllTyFlag
Specified) Type
ty
mkSpecForAllTys :: [TyVar] -> Type -> Type
mkSpecForAllTys :: [TyVar] -> Type -> Type
mkSpecForAllTys [TyVar]
tvs Type
ty = (TyVar -> Type -> Type) -> Type -> [TyVar] -> Type
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr TyVar -> Type -> Type
mkSpecForAllTy Type
ty [TyVar]
tvs
mkVisForAllTys :: [TyVar] -> Type -> Type
mkVisForAllTys :: [TyVar] -> Type -> Type
mkVisForAllTys [TyVar]
tvs = Bool
-> ([VarBndr TyVar ForAllTyFlag] -> Type -> Type)
-> [VarBndr TyVar ForAllTyFlag]
-> Type
-> Type
forall a. HasCallStack => Bool -> a -> a
assert ((TyVar -> Bool) -> [TyVar] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all TyVar -> Bool
isTyVar [TyVar]
tvs )
[VarBndr TyVar ForAllTyFlag] -> Type -> Type
mkForAllTys [ TyVar -> ForAllTyFlag -> VarBndr TyVar ForAllTyFlag
forall var argf. var -> argf -> VarBndr var argf
Bndr TyVar
tv ForAllTyFlag
Required | TyVar
tv <- [TyVar]
tvs ]
mkTyConBindersPreferAnon :: [TyVar]
-> TyCoVarSet
-> [TyConBinder]
mkTyConBindersPreferAnon :: [TyVar] -> VarSet -> [TyConBinder]
mkTyConBindersPreferAnon [TyVar]
vars VarSet
inner_tkvs = Bool
-> (([TyConBinder], VarSet) -> [TyConBinder])
-> ([TyConBinder], VarSet)
-> [TyConBinder]
forall a. HasCallStack => Bool -> a -> a
assert ((TyVar -> Bool) -> [TyVar] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all TyVar -> Bool
isTyVar [TyVar]
vars)
([TyConBinder], VarSet) -> [TyConBinder]
forall a b. (a, b) -> a
fst ([TyVar] -> ([TyConBinder], VarSet)
go [TyVar]
vars)
where
go :: [TyVar] -> ([TyConBinder], VarSet)
go :: [TyVar] -> ([TyConBinder], VarSet)
go [] = ([], VarSet
inner_tkvs)
go (TyVar
v:[TyVar]
vs) | TyVar
v TyVar -> VarSet -> Bool
`elemVarSet` VarSet
fvs
= ( TyVar -> TyConBndrVis -> TyConBinder
forall var argf. var -> argf -> VarBndr var argf
Bndr TyVar
v (ForAllTyFlag -> TyConBndrVis
NamedTCB ForAllTyFlag
Required) TyConBinder -> [TyConBinder] -> [TyConBinder]
forall a. a -> [a] -> [a]
: [TyConBinder]
binders
, VarSet
fvs VarSet -> TyVar -> VarSet
`delVarSet` TyVar
v VarSet -> VarSet -> VarSet
`unionVarSet` VarSet
kind_vars )
| Bool
otherwise
= ( TyVar -> TyConBndrVis -> TyConBinder
forall var argf. var -> argf -> VarBndr var argf
Bndr TyVar
v (FunTyFlag -> TyConBndrVis
AnonTCB FunTyFlag
visArgTypeLike) TyConBinder -> [TyConBinder] -> [TyConBinder]
forall a. a -> [a] -> [a]
: [TyConBinder]
binders
, VarSet
fvs VarSet -> VarSet -> VarSet
`unionVarSet` VarSet
kind_vars )
where
([TyConBinder]
binders, VarSet
fvs) = [TyVar] -> ([TyConBinder], VarSet)
go [TyVar]
vs
kind_vars :: VarSet
kind_vars = Type -> VarSet
tyCoVarsOfType (Type -> VarSet) -> Type -> VarSet
forall a b. (a -> b) -> a -> b
$ TyVar -> Type
tyVarKind TyVar
v
splitForAllForAllTyBinders :: Type -> ([ForAllTyBinder], Type)
splitForAllForAllTyBinders :: Type -> ([VarBndr TyVar ForAllTyFlag], Type)
splitForAllForAllTyBinders Type
ty = Type
-> Type
-> [VarBndr TyVar ForAllTyFlag]
-> ([VarBndr TyVar ForAllTyFlag], Type)
split Type
ty Type
ty []
where
split :: Type
-> Type
-> [VarBndr TyVar ForAllTyFlag]
-> ([VarBndr TyVar ForAllTyFlag], Type)
split Type
_ (ForAllTy VarBndr TyVar ForAllTyFlag
b Type
res) [VarBndr TyVar ForAllTyFlag]
bs = Type
-> Type
-> [VarBndr TyVar ForAllTyFlag]
-> ([VarBndr TyVar ForAllTyFlag], Type)
split Type
res Type
res (VarBndr TyVar ForAllTyFlag
bVarBndr TyVar ForAllTyFlag
-> [VarBndr TyVar ForAllTyFlag] -> [VarBndr TyVar ForAllTyFlag]
forall a. a -> [a] -> [a]
:[VarBndr TyVar ForAllTyFlag]
bs)
split Type
orig_ty Type
ty [VarBndr TyVar ForAllTyFlag]
bs | Just Type
ty' <- Type -> Maybe Type
coreView Type
ty = Type
-> Type
-> [VarBndr TyVar ForAllTyFlag]
-> ([VarBndr TyVar ForAllTyFlag], Type)
split Type
orig_ty Type
ty' [VarBndr TyVar ForAllTyFlag]
bs
split Type
orig_ty Type
_ [VarBndr TyVar ForAllTyFlag]
bs = ([VarBndr TyVar ForAllTyFlag] -> [VarBndr TyVar ForAllTyFlag]
forall a. [a] -> [a]
reverse [VarBndr TyVar ForAllTyFlag]
bs, Type
orig_ty)
{-# INLINE splitForAllForAllTyBinders #-}
splitForAllTyCoVars :: Type -> ([TyCoVar], Type)
splitForAllTyCoVars :: Type -> ([TyVar], Type)
splitForAllTyCoVars Type
ty = Type -> Type -> [TyVar] -> ([TyVar], Type)
split Type
ty Type
ty []
where
split :: Type -> Type -> [TyVar] -> ([TyVar], Type)
split Type
_ (ForAllTy (Bndr TyVar
tv ForAllTyFlag
_) Type
ty) [TyVar]
tvs = Type -> Type -> [TyVar] -> ([TyVar], Type)
split Type
ty Type
ty (TyVar
tvTyVar -> [TyVar] -> [TyVar]
forall a. a -> [a] -> [a]
:[TyVar]
tvs)
split Type
orig_ty Type
ty [TyVar]
tvs | Just Type
ty' <- Type -> Maybe Type
coreView Type
ty = Type -> Type -> [TyVar] -> ([TyVar], Type)
split Type
orig_ty Type
ty' [TyVar]
tvs
split Type
orig_ty Type
_ [TyVar]
tvs = ([TyVar] -> [TyVar]
forall a. [a] -> [a]
reverse [TyVar]
tvs, Type
orig_ty)
splitForAllTyVars :: Type -> ([TyVar], Type)
splitForAllTyVars :: Type -> ([TyVar], Type)
splitForAllTyVars Type
ty = Type -> Type -> [TyVar] -> ([TyVar], Type)
split Type
ty Type
ty []
where
split :: Type -> Type -> [TyVar] -> ([TyVar], Type)
split Type
_ (ForAllTy (Bndr TyVar
tv ForAllTyFlag
_) Type
ty) [TyVar]
tvs | TyVar -> Bool
isTyVar TyVar
tv = Type -> Type -> [TyVar] -> ([TyVar], Type)
split Type
ty Type
ty (TyVar
tvTyVar -> [TyVar] -> [TyVar]
forall a. a -> [a] -> [a]
:[TyVar]
tvs)
split Type
orig_ty Type
ty [TyVar]
tvs | Just Type
ty' <- Type -> Maybe Type
coreView Type
ty = Type -> Type -> [TyVar] -> ([TyVar], Type)
split Type
orig_ty Type
ty' [TyVar]
tvs
split Type
orig_ty Type
_ [TyVar]
tvs = ([TyVar] -> [TyVar]
forall a. [a] -> [a]
reverse [TyVar]
tvs, Type
orig_ty)
splitForAllReqTyBinders :: Type -> ([ReqTyBinder], Type)
splitForAllReqTyBinders :: Type -> ([ReqTyBinder], Type)
splitForAllReqTyBinders Type
ty = Type -> Type -> [ReqTyBinder] -> ([ReqTyBinder], Type)
split Type
ty Type
ty []
where
split :: Type -> Type -> [ReqTyBinder] -> ([ReqTyBinder], Type)
split Type
_ (ForAllTy (Bndr TyVar
tv ForAllTyFlag
Required) Type
ty) [ReqTyBinder]
tvs = Type -> Type -> [ReqTyBinder] -> ([ReqTyBinder], Type)
split Type
ty Type
ty (TyVar -> () -> ReqTyBinder
forall var argf. var -> argf -> VarBndr var argf
Bndr TyVar
tv ()ReqTyBinder -> [ReqTyBinder] -> [ReqTyBinder]
forall a. a -> [a] -> [a]
:[ReqTyBinder]
tvs)
split Type
orig_ty Type
ty [ReqTyBinder]
tvs | Just Type
ty' <- Type -> Maybe Type
coreView Type
ty = Type -> Type -> [ReqTyBinder] -> ([ReqTyBinder], Type)
split Type
orig_ty Type
ty' [ReqTyBinder]
tvs
split Type
orig_ty Type
_ [ReqTyBinder]
tvs = ([ReqTyBinder] -> [ReqTyBinder]
forall a. [a] -> [a]
reverse [ReqTyBinder]
tvs, Type
orig_ty)
splitForAllInvisTyBinders :: Type -> ([InvisTyBinder], Type)
splitForAllInvisTyBinders :: Type -> ([InvisTyBinder], Type)
splitForAllInvisTyBinders Type
ty = Type -> Type -> [InvisTyBinder] -> ([InvisTyBinder], Type)
split Type
ty Type
ty []
where
split :: Type -> Type -> [InvisTyBinder] -> ([InvisTyBinder], Type)
split Type
_ (ForAllTy (Bndr TyVar
tv (Invisible Specificity
spec)) Type
ty) [InvisTyBinder]
tvs = Type -> Type -> [InvisTyBinder] -> ([InvisTyBinder], Type)
split Type
ty Type
ty (TyVar -> Specificity -> InvisTyBinder
forall var argf. var -> argf -> VarBndr var argf
Bndr TyVar
tv Specificity
specInvisTyBinder -> [InvisTyBinder] -> [InvisTyBinder]
forall a. a -> [a] -> [a]
:[InvisTyBinder]
tvs)
split Type
orig_ty Type
ty [InvisTyBinder]
tvs | Just Type
ty' <- Type -> Maybe Type
coreView Type
ty = Type -> Type -> [InvisTyBinder] -> ([InvisTyBinder], Type)
split Type
orig_ty Type
ty' [InvisTyBinder]
tvs
split Type
orig_ty Type
_ [InvisTyBinder]
tvs = ([InvisTyBinder] -> [InvisTyBinder]
forall a. [a] -> [a]
reverse [InvisTyBinder]
tvs, Type
orig_ty)
isForAllTy :: Type -> Bool
isForAllTy :: Type -> Bool
isForAllTy Type
ty
| ForAllTy {} <- Type -> Type
coreFullView Type
ty = Bool
True
| Bool
otherwise = Bool
False
isForAllTy_ty :: Type -> Bool
isForAllTy_ty :: Type -> Bool
isForAllTy_ty Type
ty
| ForAllTy (Bndr TyVar
tv ForAllTyFlag
_) Type
_ <- Type -> Type
coreFullView Type
ty
, TyVar -> Bool
isTyVar TyVar
tv
= Bool
True
| Bool
otherwise = Bool
False
isForAllTy_co :: Type -> Bool
isForAllTy_co :: Type -> Bool
isForAllTy_co Type
ty
| ForAllTy (Bndr TyVar
tv ForAllTyFlag
_) Type
_ <- Type -> Type
coreFullView Type
ty
, TyVar -> Bool
isCoVar TyVar
tv
= Bool
True
| Bool
otherwise = Bool
False
isPiTy :: Type -> Bool
isPiTy :: Type -> Bool
isPiTy Type
ty = case Type -> Type
coreFullView Type
ty of
ForAllTy {} -> Bool
True
FunTy {} -> Bool
True
Type
_ -> Bool
False
isFunTy :: Type -> Bool
isFunTy :: Type -> Bool
isFunTy Type
ty
| FunTy {} <- Type -> Type
coreFullView Type
ty = Bool
True
| Bool
otherwise = Bool
False
splitForAllTyCoVar :: Type -> (TyCoVar, Type)
splitForAllTyCoVar :: Type -> (TyVar, Type)
splitForAllTyCoVar Type
ty
| Just (TyVar, Type)
answer <- Type -> Maybe (TyVar, Type)
splitForAllTyCoVar_maybe Type
ty = (TyVar, Type)
answer
| Bool
otherwise = String -> SDoc -> (TyVar, Type)
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"splitForAllTyCoVar" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty)
dropForAlls :: Type -> Type
dropForAlls :: Type -> Type
dropForAlls Type
ty = Type -> Type
go Type
ty
where
go :: Type -> Type
go (ForAllTy VarBndr TyVar ForAllTyFlag
_ Type
res) = Type -> Type
go Type
res
go Type
ty | Just Type
ty' <- Type -> Maybe Type
coreView Type
ty = Type -> Type
go Type
ty'
go Type
res = Type
res
splitForAllTyCoVar_maybe :: Type -> Maybe (TyCoVar, Type)
splitForAllTyCoVar_maybe :: Type -> Maybe (TyVar, Type)
splitForAllTyCoVar_maybe Type
ty
| ForAllTy (Bndr TyVar
tv ForAllTyFlag
_) Type
inner_ty <- Type -> Type
coreFullView Type
ty = (TyVar, Type) -> Maybe (TyVar, Type)
forall a. a -> Maybe a
Just (TyVar
tv, Type
inner_ty)
| Bool
otherwise = Maybe (TyVar, Type)
forall a. Maybe a
Nothing
splitForAllTyVar_maybe :: Type -> Maybe (TyVar, Type)
splitForAllTyVar_maybe :: Type -> Maybe (TyVar, Type)
splitForAllTyVar_maybe Type
ty
| ForAllTy (Bndr TyVar
tv ForAllTyFlag
_) Type
inner_ty <- Type -> Type
coreFullView Type
ty
, TyVar -> Bool
isTyVar TyVar
tv
= (TyVar, Type) -> Maybe (TyVar, Type)
forall a. a -> Maybe a
Just (TyVar
tv, Type
inner_ty)
| Bool
otherwise = Maybe (TyVar, Type)
forall a. Maybe a
Nothing
splitForAllCoVar_maybe :: Type -> Maybe (CoVar, Type)
splitForAllCoVar_maybe :: Type -> Maybe (TyVar, Type)
splitForAllCoVar_maybe Type
ty
| ForAllTy (Bndr TyVar
tv ForAllTyFlag
_) Type
inner_ty <- Type -> Type
coreFullView Type
ty
, TyVar -> Bool
isCoVar TyVar
tv
= (TyVar, Type) -> Maybe (TyVar, Type)
forall a. a -> Maybe a
Just (TyVar
tv, Type
inner_ty)
| Bool
otherwise = Maybe (TyVar, Type)
forall a. Maybe a
Nothing
{-# INLINE splitPiTy_maybe #-}
splitPiTy_maybe :: Type -> Maybe (PiTyBinder, Type)
splitPiTy_maybe :: Type -> Maybe (PiTyBinder, Type)
splitPiTy_maybe Type
ty = case Type -> Type
coreFullView Type
ty of
ForAllTy VarBndr TyVar ForAllTyFlag
bndr Type
ty -> (PiTyBinder, Type) -> Maybe (PiTyBinder, Type)
forall a. a -> Maybe a
Just (VarBndr TyVar ForAllTyFlag -> PiTyBinder
Named VarBndr TyVar ForAllTyFlag
bndr, Type
ty)
FunTy { ft_af :: Type -> FunTyFlag
ft_af = FunTyFlag
af, ft_mult :: Type -> Type
ft_mult = Type
w, ft_arg :: Type -> Type
ft_arg = Type
arg, ft_res :: Type -> Type
ft_res = Type
res}
-> (PiTyBinder, Type) -> Maybe (PiTyBinder, Type)
forall a. a -> Maybe a
Just (Scaled Type -> FunTyFlag -> PiTyBinder
Anon (Type -> Type -> Scaled Type
forall a. Type -> a -> Scaled a
mkScaled Type
w Type
arg) FunTyFlag
af, Type
res)
Type
_ -> Maybe (PiTyBinder, Type)
forall a. Maybe a
Nothing
splitPiTy :: Type -> (PiTyBinder, Type)
splitPiTy :: Type -> (PiTyBinder, Type)
splitPiTy Type
ty
| Just (PiTyBinder, Type)
answer <- Type -> Maybe (PiTyBinder, Type)
splitPiTy_maybe Type
ty = (PiTyBinder, Type)
answer
| Bool
otherwise = String -> SDoc -> (PiTyBinder, Type)
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"splitPiTy" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty)
splitPiTys :: Type -> ([PiTyBinder], Type)
splitPiTys :: Type -> ([PiTyBinder], Type)
splitPiTys Type
ty = Type -> Type -> [PiTyBinder] -> ([PiTyBinder], Type)
split Type
ty Type
ty []
where
split :: Type -> Type -> [PiTyBinder] -> ([PiTyBinder], Type)
split Type
_ (ForAllTy VarBndr TyVar ForAllTyFlag
b Type
res) [PiTyBinder]
bs = Type -> Type -> [PiTyBinder] -> ([PiTyBinder], Type)
split Type
res Type
res (VarBndr TyVar ForAllTyFlag -> PiTyBinder
Named VarBndr TyVar ForAllTyFlag
b PiTyBinder -> [PiTyBinder] -> [PiTyBinder]
forall a. a -> [a] -> [a]
: [PiTyBinder]
bs)
split Type
_ (FunTy { ft_af :: Type -> FunTyFlag
ft_af = FunTyFlag
af, ft_mult :: Type -> Type
ft_mult = Type
w, ft_arg :: Type -> Type
ft_arg = Type
arg, ft_res :: Type -> Type
ft_res = Type
res }) [PiTyBinder]
bs
= Type -> Type -> [PiTyBinder] -> ([PiTyBinder], Type)
split Type
res Type
res (Scaled Type -> FunTyFlag -> PiTyBinder
Anon (Type -> Type -> Scaled Type
forall a. Type -> a -> Scaled a
Scaled Type
w Type
arg) FunTyFlag
af PiTyBinder -> [PiTyBinder] -> [PiTyBinder]
forall a. a -> [a] -> [a]
: [PiTyBinder]
bs)
split Type
orig_ty Type
ty [PiTyBinder]
bs | Just Type
ty' <- Type -> Maybe Type
coreView Type
ty = Type -> Type -> [PiTyBinder] -> ([PiTyBinder], Type)
split Type
orig_ty Type
ty' [PiTyBinder]
bs
split Type
orig_ty Type
_ [PiTyBinder]
bs = ([PiTyBinder] -> [PiTyBinder]
forall a. [a] -> [a]
reverse [PiTyBinder]
bs, Type
orig_ty)
getRuntimeArgTys :: Type -> [(Scaled Type, FunTyFlag)]
getRuntimeArgTys :: Type -> [(Scaled Type, FunTyFlag)]
getRuntimeArgTys = Type -> [(Scaled Type, FunTyFlag)]
go
where
go :: Type -> [(Scaled Type, FunTyFlag)]
go :: Type -> [(Scaled Type, FunTyFlag)]
go (ForAllTy VarBndr TyVar ForAllTyFlag
_ Type
res)
= Type -> [(Scaled Type, FunTyFlag)]
go Type
res
go (FunTy { ft_mult :: Type -> Type
ft_mult = Type
w, ft_arg :: Type -> Type
ft_arg = Type
arg, ft_res :: Type -> Type
ft_res = Type
res, ft_af :: Type -> FunTyFlag
ft_af = FunTyFlag
af })
= (Type -> Type -> Scaled Type
forall a. Type -> a -> Scaled a
Scaled Type
w Type
arg, FunTyFlag
af) (Scaled Type, FunTyFlag)
-> [(Scaled Type, FunTyFlag)] -> [(Scaled Type, FunTyFlag)]
forall a. a -> [a] -> [a]
: Type -> [(Scaled Type, FunTyFlag)]
go Type
res
go Type
ty
| Just Type
ty' <- Type -> Maybe Type
coreView Type
ty
= Type -> [(Scaled Type, FunTyFlag)]
go Type
ty'
| Just (KindCoercion
_,Type
ty') <- Type -> Maybe (KindCoercion, Type)
topNormaliseNewType_maybe Type
ty
= Type -> [(Scaled Type, FunTyFlag)]
go Type
ty'
| Bool
otherwise
= []
invisibleTyBndrCount :: Type -> Int
invisibleTyBndrCount :: Type -> Arity
invisibleTyBndrCount Type
ty = [PiTyBinder] -> Arity
forall a. [a] -> Arity
forall (t :: * -> *) a. Foldable t => t a -> Arity
length (([PiTyBinder], Type) -> [PiTyBinder]
forall a b. (a, b) -> a
fst (Type -> ([PiTyBinder], Type)
splitInvisPiTys Type
ty))
splitInvisPiTys :: Type -> ([PiTyBinder], Type)
splitInvisPiTys :: Type -> ([PiTyBinder], Type)
splitInvisPiTys Type
ty = Type -> Type -> [PiTyBinder] -> ([PiTyBinder], Type)
split Type
ty Type
ty []
where
split :: Type -> Type -> [PiTyBinder] -> ([PiTyBinder], Type)
split Type
_ (ForAllTy VarBndr TyVar ForAllTyFlag
b Type
res) [PiTyBinder]
bs
| Bndr TyVar
_ ForAllTyFlag
vis <- VarBndr TyVar ForAllTyFlag
b
, ForAllTyFlag -> Bool
isInvisibleForAllTyFlag ForAllTyFlag
vis = Type -> Type -> [PiTyBinder] -> ([PiTyBinder], Type)
split Type
res Type
res (VarBndr TyVar ForAllTyFlag -> PiTyBinder
Named VarBndr TyVar ForAllTyFlag
b PiTyBinder -> [PiTyBinder] -> [PiTyBinder]
forall a. a -> [a] -> [a]
: [PiTyBinder]
bs)
split Type
_ (FunTy { ft_af :: Type -> FunTyFlag
ft_af = FunTyFlag
af, ft_mult :: Type -> Type
ft_mult = Type
mult, ft_arg :: Type -> Type
ft_arg = Type
arg, ft_res :: Type -> Type
ft_res = Type
res }) [PiTyBinder]
bs
| FunTyFlag -> Bool
isInvisibleFunArg FunTyFlag
af = Type -> Type -> [PiTyBinder] -> ([PiTyBinder], Type)
split Type
res Type
res (Scaled Type -> FunTyFlag -> PiTyBinder
Anon (Type -> Type -> Scaled Type
forall a. Type -> a -> Scaled a
mkScaled Type
mult Type
arg) FunTyFlag
af PiTyBinder -> [PiTyBinder] -> [PiTyBinder]
forall a. a -> [a] -> [a]
: [PiTyBinder]
bs)
split Type
orig_ty Type
ty [PiTyBinder]
bs
| Just Type
ty' <- Type -> Maybe Type
coreView Type
ty = Type -> Type -> [PiTyBinder] -> ([PiTyBinder], Type)
split Type
orig_ty Type
ty' [PiTyBinder]
bs
split Type
orig_ty Type
_ [PiTyBinder]
bs = ([PiTyBinder] -> [PiTyBinder]
forall a. [a] -> [a]
reverse [PiTyBinder]
bs, Type
orig_ty)
splitInvisPiTysN :: Int -> Type -> ([PiTyBinder], Type)
splitInvisPiTysN :: Arity -> Type -> ([PiTyBinder], Type)
splitInvisPiTysN Arity
n Type
ty = Arity -> Type -> Type -> [PiTyBinder] -> ([PiTyBinder], Type)
forall {t}.
(Eq t, Num t) =>
t -> Type -> Type -> [PiTyBinder] -> ([PiTyBinder], Type)
split Arity
n Type
ty Type
ty []
where
split :: t -> Type -> Type -> [PiTyBinder] -> ([PiTyBinder], Type)
split t
n Type
orig_ty Type
ty [PiTyBinder]
bs
| t
n t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
0 = ([PiTyBinder] -> [PiTyBinder]
forall a. [a] -> [a]
reverse [PiTyBinder]
bs, Type
orig_ty)
| Just Type
ty' <- Type -> Maybe Type
coreView Type
ty = t -> Type -> Type -> [PiTyBinder] -> ([PiTyBinder], Type)
split t
n Type
orig_ty Type
ty' [PiTyBinder]
bs
| ForAllTy VarBndr TyVar ForAllTyFlag
b Type
res <- Type
ty
, Bndr TyVar
_ ForAllTyFlag
vis <- VarBndr TyVar ForAllTyFlag
b
, ForAllTyFlag -> Bool
isInvisibleForAllTyFlag ForAllTyFlag
vis = t -> Type -> Type -> [PiTyBinder] -> ([PiTyBinder], Type)
split (t
nt -> t -> t
forall a. Num a => a -> a -> a
-t
1) Type
res Type
res (VarBndr TyVar ForAllTyFlag -> PiTyBinder
Named VarBndr TyVar ForAllTyFlag
b PiTyBinder -> [PiTyBinder] -> [PiTyBinder]
forall a. a -> [a] -> [a]
: [PiTyBinder]
bs)
| FunTy { ft_af :: Type -> FunTyFlag
ft_af = FunTyFlag
af, ft_mult :: Type -> Type
ft_mult = Type
mult, ft_arg :: Type -> Type
ft_arg = Type
arg, ft_res :: Type -> Type
ft_res = Type
res } <- Type
ty
, FunTyFlag -> Bool
isInvisibleFunArg FunTyFlag
af = t -> Type -> Type -> [PiTyBinder] -> ([PiTyBinder], Type)
split (t
nt -> t -> t
forall a. Num a => a -> a -> a
-t
1) Type
res Type
res (Scaled Type -> FunTyFlag -> PiTyBinder
Anon (Type -> Type -> Scaled Type
forall a. Type -> a -> Scaled a
Scaled Type
mult Type
arg) FunTyFlag
af PiTyBinder -> [PiTyBinder] -> [PiTyBinder]
forall a. a -> [a] -> [a]
: [PiTyBinder]
bs)
| Bool
otherwise = ([PiTyBinder] -> [PiTyBinder]
forall a. [a] -> [a]
reverse [PiTyBinder]
bs, Type
orig_ty)
filterOutInvisibleTypes :: TyCon -> [Type] -> [Type]
filterOutInvisibleTypes :: TyCon -> [Type] -> [Type]
filterOutInvisibleTypes TyCon
tc [Type]
tys = ([Type], [Type]) -> [Type]
forall a b. (a, b) -> b
snd (([Type], [Type]) -> [Type]) -> ([Type], [Type]) -> [Type]
forall a b. (a -> b) -> a -> b
$ TyCon -> [Type] -> ([Type], [Type])
partitionInvisibleTypes TyCon
tc [Type]
tys
filterOutInferredTypes :: TyCon -> [Type] -> [Type]
filterOutInferredTypes :: TyCon -> [Type] -> [Type]
filterOutInferredTypes TyCon
tc [Type]
tys =
[Bool] -> [Type] -> [Type]
forall a. [Bool] -> [a] -> [a]
filterByList ((ForAllTyFlag -> Bool) -> [ForAllTyFlag] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map (ForAllTyFlag -> ForAllTyFlag -> Bool
forall a. Eq a => a -> a -> Bool
/= ForAllTyFlag
Inferred) ([ForAllTyFlag] -> [Bool]) -> [ForAllTyFlag] -> [Bool]
forall a b. (a -> b) -> a -> b
$ TyCon -> [Type] -> [ForAllTyFlag]
tyConForAllTyFlags TyCon
tc [Type]
tys) [Type]
tys
partitionInvisibleTypes :: TyCon -> [Type] -> ([Type], [Type])
partitionInvisibleTypes :: TyCon -> [Type] -> ([Type], [Type])
partitionInvisibleTypes TyCon
tc [Type]
tys =
[Bool] -> [Type] -> ([Type], [Type])
forall a. [Bool] -> [a] -> ([a], [a])
partitionByList ((ForAllTyFlag -> Bool) -> [ForAllTyFlag] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map ForAllTyFlag -> Bool
isInvisibleForAllTyFlag ([ForAllTyFlag] -> [Bool]) -> [ForAllTyFlag] -> [Bool]
forall a b. (a -> b) -> a -> b
$ TyCon -> [Type] -> [ForAllTyFlag]
tyConForAllTyFlags TyCon
tc [Type]
tys) [Type]
tys
partitionInvisibles :: [(a, ForAllTyFlag)] -> ([a], [a])
partitionInvisibles :: forall a. [(a, ForAllTyFlag)] -> ([a], [a])
partitionInvisibles = ((a, ForAllTyFlag) -> Either a a)
-> [(a, ForAllTyFlag)] -> ([a], [a])
forall a b c. (a -> Either b c) -> [a] -> ([b], [c])
partitionWith (a, ForAllTyFlag) -> Either a a
forall a. (a, ForAllTyFlag) -> Either a a
pick_invis
where
pick_invis :: (a, ForAllTyFlag) -> Either a a
pick_invis :: forall a. (a, ForAllTyFlag) -> Either a a
pick_invis (a
thing, ForAllTyFlag
vis) | ForAllTyFlag -> Bool
isInvisibleForAllTyFlag ForAllTyFlag
vis = a -> Either a a
forall a b. a -> Either a b
Left a
thing
| Bool
otherwise = a -> Either a a
forall a b. b -> Either a b
Right a
thing
tyConForAllTyFlags :: TyCon -> [Type] -> [ForAllTyFlag]
tyConForAllTyFlags :: TyCon -> [Type] -> [ForAllTyFlag]
tyConForAllTyFlags TyCon
tc = Type -> [Type] -> [ForAllTyFlag]
fun_kind_arg_flags (TyCon -> Type
tyConKind TyCon
tc)
appTyForAllTyFlags :: Type -> [Type] -> [ForAllTyFlag]
appTyForAllTyFlags :: Type -> [Type] -> [ForAllTyFlag]
appTyForAllTyFlags Type
ty = Type -> [Type] -> [ForAllTyFlag]
fun_kind_arg_flags ((() :: Constraint) => Type -> Type
Type -> Type
typeKind Type
ty)
fun_kind_arg_flags :: Kind -> [Type] -> [ForAllTyFlag]
fun_kind_arg_flags :: Type -> [Type] -> [ForAllTyFlag]
fun_kind_arg_flags = Subst -> Type -> [Type] -> [ForAllTyFlag]
go Subst
emptySubst
where
go :: Subst -> Type -> [Type] -> [ForAllTyFlag]
go Subst
subst Type
ki [Type]
arg_tys
| Just Type
ki' <- Type -> Maybe Type
coreView Type
ki = Subst -> Type -> [Type] -> [ForAllTyFlag]
go Subst
subst Type
ki' [Type]
arg_tys
go Subst
_ Type
_ [] = []
go Subst
subst (ForAllTy (Bndr TyVar
tv ForAllTyFlag
argf) Type
res_ki) (Type
arg_ty:[Type]
arg_tys)
= ForAllTyFlag
argf ForAllTyFlag -> [ForAllTyFlag] -> [ForAllTyFlag]
forall a. a -> [a] -> [a]
: Subst -> Type -> [Type] -> [ForAllTyFlag]
go Subst
subst' Type
res_ki [Type]
arg_tys
where
subst' :: Subst
subst' = Subst -> TyVar -> Type -> Subst
extendTvSubst Subst
subst TyVar
tv Type
arg_ty
go Subst
subst (TyVarTy TyVar
tv) [Type]
arg_tys
| Just Type
ki <- Subst -> TyVar -> Maybe Type
lookupTyVar Subst
subst TyVar
tv = Subst -> Type -> [Type] -> [ForAllTyFlag]
go Subst
subst Type
ki [Type]
arg_tys
go Subst
subst (FunTy{ft_af :: Type -> FunTyFlag
ft_af = FunTyFlag
af, ft_res :: Type -> Type
ft_res = Type
res_ki}) (Type
_:[Type]
arg_tys)
= ForAllTyFlag
argf ForAllTyFlag -> [ForAllTyFlag] -> [ForAllTyFlag]
forall a. a -> [a] -> [a]
: Subst -> Type -> [Type] -> [ForAllTyFlag]
go Subst
subst Type
res_ki [Type]
arg_tys
where
argf :: ForAllTyFlag
argf | FunTyFlag -> Bool
isVisibleFunArg FunTyFlag
af = ForAllTyFlag
Required
| Bool
otherwise = ForAllTyFlag
Inferred
go Subst
_ Type
_ [Type]
arg_tys = (Type -> ForAllTyFlag) -> [Type] -> [ForAllTyFlag]
forall a b. (a -> b) -> [a] -> [b]
map (ForAllTyFlag -> Type -> ForAllTyFlag
forall a b. a -> b -> a
const ForAllTyFlag
Required) [Type]
arg_tys
isTauTy :: Type -> Bool
isTauTy :: Type -> Bool
isTauTy Type
ty | Just Type
ty' <- Type -> Maybe Type
coreView Type
ty = Type -> Bool
isTauTy Type
ty'
isTauTy (TyVarTy TyVar
_) = Bool
True
isTauTy (LitTy {}) = Bool
True
isTauTy (TyConApp TyCon
tc [Type]
tys) = (Type -> Bool) -> [Type] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Type -> Bool
isTauTy [Type]
tys Bool -> Bool -> Bool
&& TyCon -> Bool
isTauTyCon TyCon
tc
isTauTy (AppTy Type
a Type
b) = Type -> Bool
isTauTy Type
a Bool -> Bool -> Bool
&& Type -> Bool
isTauTy Type
b
isTauTy (FunTy { ft_af :: Type -> FunTyFlag
ft_af = FunTyFlag
af, ft_mult :: Type -> Type
ft_mult = Type
w, ft_arg :: Type -> Type
ft_arg = Type
a, ft_res :: Type -> Type
ft_res = Type
b })
| FunTyFlag -> Bool
isInvisibleFunArg FunTyFlag
af = Bool
False
| Bool
otherwise = Type -> Bool
isTauTy Type
w Bool -> Bool -> Bool
&& Type -> Bool
isTauTy Type
a Bool -> Bool -> Bool
&& Type -> Bool
isTauTy Type
b
isTauTy (ForAllTy {}) = Bool
False
isTauTy (CastTy Type
ty KindCoercion
_) = Type -> Bool
isTauTy Type
ty
isTauTy (CoercionTy KindCoercion
_) = Bool
False
isAtomicTy :: Type -> Bool
isAtomicTy :: Type -> Bool
isAtomicTy (TyVarTy {}) = Bool
True
isAtomicTy (LitTy {}) = Bool
True
isAtomicTy (TyConApp TyCon
_ []) = Bool
True
isAtomicTy Type
ty | Type -> Bool
isLiftedTypeKind Type
ty = Bool
True
isAtomicTy Type
_ = Bool
False
mkFamilyTyConApp :: TyCon -> [Type] -> Type
mkFamilyTyConApp :: TyCon -> [Type] -> Type
mkFamilyTyConApp TyCon
tc [Type]
tys
| Just (TyCon
fam_tc, [Type]
fam_tys) <- TyCon -> Maybe (TyCon, [Type])
tyConFamInst_maybe TyCon
tc
, let tvs :: [TyVar]
tvs = TyCon -> [TyVar]
tyConTyVars TyCon
tc
fam_subst :: Subst
fam_subst = Bool -> SDoc -> Subst -> Subst
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr ([TyVar]
tvs [TyVar] -> [Type] -> Bool
forall a b. [a] -> [b] -> Bool
`equalLength` [Type]
tys) (TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCon
tc SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
tys) (Subst -> Subst) -> Subst -> Subst
forall a b. (a -> b) -> a -> b
$
[TyVar] -> [Type] -> Subst
(() :: Constraint) => [TyVar] -> [Type] -> Subst
zipTvSubst [TyVar]
tvs [Type]
tys
= TyCon -> [Type] -> Type
mkTyConApp TyCon
fam_tc ((() :: Constraint) => Subst -> [Type] -> [Type]
Subst -> [Type] -> [Type]
substTys Subst
fam_subst [Type]
fam_tys)
| Bool
otherwise
= TyCon -> [Type] -> Type
mkTyConApp TyCon
tc [Type]
tys
coAxNthLHS :: CoAxiom br -> Int -> Type
coAxNthLHS :: forall (br :: BranchFlag). CoAxiom br -> Arity -> Type
coAxNthLHS CoAxiom br
ax Arity
ind =
TyCon -> [Type] -> Type
mkTyConApp (CoAxiom br -> TyCon
forall (br :: BranchFlag). CoAxiom br -> TyCon
coAxiomTyCon CoAxiom br
ax) (CoAxBranch -> [Type]
coAxBranchLHS (CoAxiom br -> Arity -> CoAxBranch
forall (br :: BranchFlag). CoAxiom br -> Arity -> CoAxBranch
coAxiomNthBranch CoAxiom br
ax Arity
ind))
isFamFreeTy :: Type -> Bool
isFamFreeTy :: Type -> Bool
isFamFreeTy Type
ty | Just Type
ty' <- Type -> Maybe Type
coreView Type
ty = Type -> Bool
isFamFreeTy Type
ty'
isFamFreeTy (TyVarTy TyVar
_) = Bool
True
isFamFreeTy (LitTy {}) = Bool
True
isFamFreeTy (TyConApp TyCon
tc [Type]
tys) = (Type -> Bool) -> [Type] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Type -> Bool
isFamFreeTy [Type]
tys Bool -> Bool -> Bool
&& TyCon -> Bool
isFamFreeTyCon TyCon
tc
isFamFreeTy (AppTy Type
a Type
b) = Type -> Bool
isFamFreeTy Type
a Bool -> Bool -> Bool
&& Type -> Bool
isFamFreeTy Type
b
isFamFreeTy (FunTy FunTyFlag
_ Type
w Type
a Type
b) = Type -> Bool
isFamFreeTy Type
w Bool -> Bool -> Bool
&& Type -> Bool
isFamFreeTy Type
a Bool -> Bool -> Bool
&& Type -> Bool
isFamFreeTy Type
b
isFamFreeTy (ForAllTy VarBndr TyVar ForAllTyFlag
_ Type
ty) = Type -> Bool
isFamFreeTy Type
ty
isFamFreeTy (CastTy Type
ty KindCoercion
_) = Type -> Bool
isFamFreeTy Type
ty
isFamFreeTy (CoercionTy KindCoercion
_) = Bool
False
isCoVarType :: Type -> Bool
isCoVarType :: Type -> Bool
isCoVarType Type
ty
| Just TyCon
tc <- Type -> Maybe TyCon
tyConAppTyCon_maybe Type
ty
= TyCon
tc TyCon -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
eqPrimTyConKey Bool -> Bool -> Bool
|| TyCon
tc TyCon -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
eqReprPrimTyConKey
| Bool
otherwise
= Bool
False
buildSynTyCon :: Name -> [KnotTied TyConBinder] -> Kind
-> [Role] -> KnotTied Type -> TyCon
buildSynTyCon :: Name -> [TyConBinder] -> Type -> [Role] -> Type -> TyCon
buildSynTyCon Name
name [TyConBinder]
binders Type
res_kind [Role]
roles Type
rhs
= Name
-> [TyConBinder]
-> Type
-> [Role]
-> Type
-> Bool
-> Bool
-> Bool
-> TyCon
mkSynonymTyCon Name
name [TyConBinder]
binders Type
res_kind [Role]
roles Type
rhs Bool
is_tau Bool
is_fam_free Bool
is_forgetful
where
is_tau :: Bool
is_tau = Type -> Bool
isTauTy Type
rhs
is_fam_free :: Bool
is_fam_free = Type -> Bool
isFamFreeTy Type
rhs
is_forgetful :: Bool
is_forgetful = (TyConBinder -> Bool) -> [TyConBinder] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Bool -> Bool
not (Bool -> Bool) -> (TyConBinder -> Bool) -> TyConBinder -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TyVar -> VarSet -> Bool
`elemVarSet` Type -> VarSet
tyCoVarsOfType Type
rhs) (TyVar -> Bool) -> (TyConBinder -> TyVar) -> TyConBinder -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyConBinder -> TyVar
forall tv argf. VarBndr tv argf -> tv
binderVar) [TyConBinder]
binders Bool -> Bool -> Bool
||
(TyCon -> Bool) -> UniqSet TyCon -> Bool
forall a. (a -> Bool) -> UniqSet a -> Bool
uniqSetAny TyCon -> Bool
isForgetfulSynTyCon (Type -> UniqSet TyCon
tyConsOfType Type
rhs)
typeLevity_maybe :: HasDebugCallStack => Type -> Maybe Levity
typeLevity_maybe :: (() :: Constraint) => Type -> Maybe Levity
typeLevity_maybe Type
ty = Type -> Maybe Levity
runtimeRepLevity_maybe ((() :: Constraint) => Type -> Type
Type -> Type
getRuntimeRep Type
ty)
isUnliftedType :: HasDebugCallStack => Type -> Bool
isUnliftedType :: (() :: Constraint) => Type -> Bool
isUnliftedType Type
ty =
case (() :: Constraint) => Type -> Maybe Levity
Type -> Maybe Levity
typeLevity_maybe Type
ty of
Just Levity
Lifted -> Bool
False
Just Levity
Unlifted -> Bool
True
Maybe Levity
Nothing ->
String -> SDoc -> Bool
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"isUnliftedType" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr ((() :: Constraint) => Type -> Type
Type -> Type
typeKind Type
ty))
mightBeLiftedType :: Type -> Bool
mightBeLiftedType :: Type -> Bool
mightBeLiftedType = Maybe Levity -> Bool
mightBeLifted (Maybe Levity -> Bool) -> (Type -> Maybe Levity) -> Type -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (() :: Constraint) => Type -> Maybe Levity
Type -> Maybe Levity
typeLevity_maybe
mightBeUnliftedType :: Type -> Bool
mightBeUnliftedType :: Type -> Bool
mightBeUnliftedType = Maybe Levity -> Bool
mightBeUnlifted (Maybe Levity -> Bool) -> (Type -> Maybe Levity) -> Type -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (() :: Constraint) => Type -> Maybe Levity
Type -> Maybe Levity
typeLevity_maybe
isBoxedType :: Type -> Bool
isBoxedType :: Type -> Bool
isBoxedType Type
ty = Type -> Bool
isBoxedRuntimeRep ((() :: Constraint) => Type -> Type
Type -> Type
getRuntimeRep Type
ty)
isRuntimeRepKindedTy :: Type -> Bool
isRuntimeRepKindedTy :: Type -> Bool
isRuntimeRepKindedTy = Type -> Bool
isRuntimeRepTy (Type -> Bool) -> (Type -> Type) -> Type -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (() :: Constraint) => Type -> Type
Type -> Type
typeKind
dropRuntimeRepArgs :: [Type] -> [Type]
dropRuntimeRepArgs :: [Type] -> [Type]
dropRuntimeRepArgs = (Type -> Bool) -> [Type] -> [Type]
forall a. (a -> Bool) -> [a] -> [a]
dropWhile Type -> Bool
isRuntimeRepKindedTy
getRuntimeRep_maybe :: HasDebugCallStack
=> Type -> Maybe RuntimeRepType
getRuntimeRep_maybe :: (() :: Constraint) => Type -> Maybe Type
getRuntimeRep_maybe = (() :: Constraint) => Type -> Maybe Type
Type -> Maybe Type
kindRep_maybe (Type -> Maybe Type) -> (Type -> Type) -> Type -> Maybe Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (() :: Constraint) => Type -> Type
Type -> Type
typeKind
getRuntimeRep :: HasDebugCallStack => Type -> RuntimeRepType
getRuntimeRep :: (() :: Constraint) => Type -> Type
getRuntimeRep Type
ty
= case (() :: Constraint) => Type -> Maybe Type
Type -> Maybe Type
getRuntimeRep_maybe Type
ty of
Just Type
r -> Type
r
Maybe Type
Nothing -> String -> SDoc -> Type
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"getRuntimeRep" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr ((() :: Constraint) => Type -> Type
Type -> Type
typeKind Type
ty))
getLevity_maybe :: HasDebugCallStack => Type -> Maybe Type
getLevity_maybe :: (() :: Constraint) => Type -> Maybe Type
getLevity_maybe Type
ty
| Just Type
rep <- (() :: Constraint) => Type -> Maybe Type
Type -> Maybe Type
getRuntimeRep_maybe Type
ty
, Just [Type
lev] <- Unique -> Type -> Maybe [Type]
isTyConKeyApp_maybe Unique
boxedRepDataConKey Type
rep
= Type -> Maybe Type
forall a. a -> Maybe a
Just Type
lev
| Bool
otherwise
= Maybe Type
forall a. Maybe a
Nothing
getLevity :: HasDebugCallStack => Type -> Type
getLevity :: (() :: Constraint) => Type -> Type
getLevity Type
ty
| Just Type
lev <- (() :: Constraint) => Type -> Maybe Type
Type -> Maybe Type
getLevity_maybe Type
ty
= Type
lev
| Bool
otherwise
= String -> SDoc -> Type
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"getLevity" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr ((() :: Constraint) => Type -> Type
Type -> Type
typeKind Type
ty))
isUnboxedTupleType :: Type -> Bool
isUnboxedTupleType :: Type -> Bool
isUnboxedTupleType Type
ty
= (() :: Constraint) => Type -> TyCon
Type -> TyCon
tyConAppTyCon ((() :: Constraint) => Type -> Type
Type -> Type
getRuntimeRep Type
ty) TyCon -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
tupleRepDataConKey
isUnboxedSumType :: Type -> Bool
isUnboxedSumType :: Type -> Bool
isUnboxedSumType Type
ty
= (() :: Constraint) => Type -> TyCon
Type -> TyCon
tyConAppTyCon ((() :: Constraint) => Type -> Type
Type -> Type
getRuntimeRep Type
ty) TyCon -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
sumRepDataConKey
isAlgType :: Type -> Bool
isAlgType :: Type -> Bool
isAlgType Type
ty
= case (() :: Constraint) => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
ty of
Just (TyCon
tc, [Type]
ty_args) -> Bool -> (TyCon -> Bool) -> TyCon -> Bool
forall a. HasCallStack => Bool -> a -> a
assert ([Type]
ty_args [Type] -> Arity -> Bool
forall a. [a] -> Arity -> Bool
`lengthIs` TyCon -> Arity
tyConArity TyCon
tc )
TyCon -> Bool
isAlgTyCon TyCon
tc
Maybe (TyCon, [Type])
_other -> Bool
False
isDataFamilyAppType :: Type -> Bool
isDataFamilyAppType :: Type -> Bool
isDataFamilyAppType Type
ty = case Type -> Maybe TyCon
tyConAppTyCon_maybe Type
ty of
Just TyCon
tc -> TyCon -> Bool
isDataFamilyTyCon TyCon
tc
Maybe TyCon
_ -> Bool
False
isStrictType :: HasDebugCallStack => Type -> Bool
isStrictType :: (() :: Constraint) => Type -> Bool
isStrictType = (() :: Constraint) => Type -> Bool
Type -> Bool
isUnliftedType
isPrimitiveType :: Type -> Bool
isPrimitiveType :: Type -> Bool
isPrimitiveType Type
ty = case (() :: Constraint) => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
ty of
Just (TyCon
tc, [Type]
ty_args) -> Bool -> (TyCon -> Bool) -> TyCon -> Bool
forall a. HasCallStack => Bool -> a -> a
assert ([Type]
ty_args [Type] -> Arity -> Bool
forall a. [a] -> Arity -> Bool
`lengthIs` TyCon -> Arity
tyConArity TyCon
tc )
TyCon -> Bool
isPrimTyCon TyCon
tc
Maybe (TyCon, [Type])
_ -> Bool
False
isValidJoinPointType :: JoinArity -> Type -> Bool
isValidJoinPointType :: Arity -> Type -> Bool
isValidJoinPointType Arity
arity Type
ty
= VarSet -> Arity -> Type -> Bool
forall {t}. (Eq t, Num t) => VarSet -> t -> Type -> Bool
valid_under VarSet
emptyVarSet Arity
arity Type
ty
where
valid_under :: VarSet -> t -> Type -> Bool
valid_under VarSet
tvs t
arity Type
ty
| t
arity t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
0
= VarSet
tvs VarSet -> VarSet -> Bool
`disjointVarSet` Type -> VarSet
tyCoVarsOfType Type
ty
| Just (TyVar
t, Type
ty') <- Type -> Maybe (TyVar, Type)
splitForAllTyCoVar_maybe Type
ty
= VarSet -> t -> Type -> Bool
valid_under (VarSet
tvs VarSet -> TyVar -> VarSet
`extendVarSet` TyVar
t) (t
arityt -> t -> t
forall a. Num a => a -> a -> a
-t
1) Type
ty'
| Just (FunTyFlag
_, Type
_, Type
_, Type
res_ty) <- Type -> Maybe (FunTyFlag, Type, Type, Type)
splitFunTy_maybe Type
ty
= VarSet -> t -> Type -> Bool
valid_under VarSet
tvs (t
arityt -> t -> t
forall a. Num a => a -> a -> a
-t
1) Type
res_ty
| Bool
otherwise
= Bool
False
seqType :: Type -> ()
seqType :: Type -> ()
seqType (LitTy TyLit
n) = TyLit
n TyLit -> () -> ()
forall a b. a -> b -> b
`seq` ()
seqType (TyVarTy TyVar
tv) = TyVar
tv TyVar -> () -> ()
forall a b. a -> b -> b
`seq` ()
seqType (AppTy Type
t1 Type
t2) = Type -> ()
seqType Type
t1 () -> () -> ()
forall a b. a -> b -> b
`seq` Type -> ()
seqType Type
t2
seqType (FunTy FunTyFlag
_ Type
w Type
t1 Type
t2) = Type -> ()
seqType Type
w () -> () -> ()
forall a b. a -> b -> b
`seq` Type -> ()
seqType Type
t1 () -> () -> ()
forall a b. a -> b -> b
`seq` Type -> ()
seqType Type
t2
seqType (TyConApp TyCon
tc [Type]
tys) = TyCon
tc TyCon -> () -> ()
forall a b. a -> b -> b
`seq` [Type] -> ()
seqTypes [Type]
tys
seqType (ForAllTy (Bndr TyVar
tv ForAllTyFlag
_) Type
ty) = Type -> ()
seqType (TyVar -> Type
varType TyVar
tv) () -> () -> ()
forall a b. a -> b -> b
`seq` Type -> ()
seqType Type
ty
seqType (CastTy Type
ty KindCoercion
co) = Type -> ()
seqType Type
ty () -> () -> ()
forall a b. a -> b -> b
`seq` KindCoercion -> ()
seqCo KindCoercion
co
seqType (CoercionTy KindCoercion
co) = KindCoercion -> ()
seqCo KindCoercion
co
seqTypes :: [Type] -> ()
seqTypes :: [Type] -> ()
seqTypes [] = ()
seqTypes (Type
ty:[Type]
tys) = Type -> ()
seqType Type
ty () -> () -> ()
forall a b. a -> b -> b
`seq` [Type] -> ()
seqTypes [Type]
tys
typeKind :: HasDebugCallStack => Type -> Kind
typeKind :: (() :: Constraint) => Type -> Type
typeKind (TyConApp TyCon
tc [Type]
tys) = (() :: Constraint) => Type -> [Type] -> Type
Type -> [Type] -> Type
piResultTys (TyCon -> Type
tyConKind TyCon
tc) [Type]
tys
typeKind (LitTy TyLit
l) = TyLit -> Type
typeLiteralKind TyLit
l
typeKind (FunTy { ft_af :: Type -> FunTyFlag
ft_af = FunTyFlag
af }) = case FunTyFlag -> TypeOrConstraint
funTyFlagResultTypeOrConstraint FunTyFlag
af of
TypeOrConstraint
TypeLike -> Type
liftedTypeKind
TypeOrConstraint
ConstraintLike -> Type
constraintKind
typeKind (TyVarTy TyVar
tyvar) = TyVar -> Type
tyVarKind TyVar
tyvar
typeKind (CastTy Type
_ty KindCoercion
co) = KindCoercion -> Type
coercionRKind KindCoercion
co
typeKind (CoercionTy KindCoercion
co) = KindCoercion -> Type
coercionType KindCoercion
co
typeKind (AppTy Type
fun Type
arg)
= Type -> [Type] -> Type
go Type
fun [Type
arg]
where
go :: Type -> [Type] -> Type
go (AppTy Type
fun Type
arg) [Type]
args = Type -> [Type] -> Type
go Type
fun (Type
argType -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:[Type]
args)
go Type
fun [Type]
args = (() :: Constraint) => Type -> [Type] -> Type
Type -> [Type] -> Type
piResultTys ((() :: Constraint) => Type -> Type
Type -> Type
typeKind Type
fun) [Type]
args
typeKind ty :: Type
ty@(ForAllTy {})
= case [TyVar] -> Type -> Maybe Type
occCheckExpand [TyVar]
tvs Type
body_kind of
Maybe Type
Nothing -> String -> SDoc -> Type
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"typeKind"
(Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ [TyVar] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [TyVar]
tvs SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
body SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
body_kind)
Just Type
k' | (TyVar -> Bool) -> [TyVar] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all TyVar -> Bool
isTyVar [TyVar]
tvs -> Type
k'
| Bool
otherwise -> Type
lifted_kind_from_body
where
([TyVar]
tvs, Type
body) = Type -> ([TyVar], Type)
splitForAllTyVars Type
ty
body_kind :: Type
body_kind = (() :: Constraint) => Type -> Type
Type -> Type
typeKind Type
body
lifted_kind_from_body :: Type
lifted_kind_from_body
= case Type -> Maybe (TypeOrConstraint, Type)
sORTKind_maybe Type
body_kind of
Just (TypeOrConstraint
ConstraintLike, Type
_) -> Type
constraintKind
Just (TypeOrConstraint
TypeLike, Type
_) -> Type
liftedTypeKind
Maybe (TypeOrConstraint, Type)
Nothing -> String -> SDoc -> Type
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"typeKind" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
body_kind)
sORTKind_maybe :: Kind -> Maybe (TypeOrConstraint, Type)
sORTKind_maybe :: Type -> Maybe (TypeOrConstraint, Type)
sORTKind_maybe (TyConApp TyCon
tc [Type]
tys)
| Unique
tc_uniq Unique -> Unique -> Bool
forall a. Eq a => a -> a -> Bool
== Unique
liftedTypeKindTyConKey = Bool
-> Maybe (TypeOrConstraint, Type) -> Maybe (TypeOrConstraint, Type)
forall a. HasCallStack => Bool -> a -> a
assert( [Type] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
tys ) (Maybe (TypeOrConstraint, Type) -> Maybe (TypeOrConstraint, Type))
-> Maybe (TypeOrConstraint, Type) -> Maybe (TypeOrConstraint, Type)
forall a b. (a -> b) -> a -> b
$ (TypeOrConstraint, Type) -> Maybe (TypeOrConstraint, Type)
forall a. a -> Maybe a
Just (TypeOrConstraint
TypeLike, Type
liftedRepTy)
| Unique
tc_uniq Unique -> Unique -> Bool
forall a. Eq a => a -> a -> Bool
== Unique
constraintKindTyConKey = Bool
-> Maybe (TypeOrConstraint, Type) -> Maybe (TypeOrConstraint, Type)
forall a. HasCallStack => Bool -> a -> a
assert( [Type] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
tys ) (Maybe (TypeOrConstraint, Type) -> Maybe (TypeOrConstraint, Type))
-> Maybe (TypeOrConstraint, Type) -> Maybe (TypeOrConstraint, Type)
forall a b. (a -> b) -> a -> b
$ (TypeOrConstraint, Type) -> Maybe (TypeOrConstraint, Type)
forall a. a -> Maybe a
Just (TypeOrConstraint
ConstraintLike, Type
liftedRepTy)
| Unique
tc_uniq Unique -> Unique -> Bool
forall a. Eq a => a -> a -> Bool
== Unique
tYPETyConKey = TypeOrConstraint -> Maybe (TypeOrConstraint, Type)
get_rep TypeOrConstraint
TypeLike
| Unique
tc_uniq Unique -> Unique -> Bool
forall a. Eq a => a -> a -> Bool
== Unique
cONSTRAINTTyConKey = TypeOrConstraint -> Maybe (TypeOrConstraint, Type)
get_rep TypeOrConstraint
ConstraintLike
| Just Type
ty' <- TyCon -> [Type] -> Maybe Type
expandSynTyConApp_maybe TyCon
tc [Type]
tys = Type -> Maybe (TypeOrConstraint, Type)
sORTKind_maybe Type
ty'
where
!tc_uniq :: Unique
tc_uniq = TyCon -> Unique
tyConUnique TyCon
tc
get_rep :: TypeOrConstraint -> Maybe (TypeOrConstraint, Type)
get_rep TypeOrConstraint
torc = case [Type]
tys of
(Type
rep:[Type]
_reps) -> Bool
-> Maybe (TypeOrConstraint, Type) -> Maybe (TypeOrConstraint, Type)
forall a. HasCallStack => Bool -> a -> a
assert ([Type] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
_reps) (Maybe (TypeOrConstraint, Type) -> Maybe (TypeOrConstraint, Type))
-> Maybe (TypeOrConstraint, Type) -> Maybe (TypeOrConstraint, Type)
forall a b. (a -> b) -> a -> b
$ (TypeOrConstraint, Type) -> Maybe (TypeOrConstraint, Type)
forall a. a -> Maybe a
Just (TypeOrConstraint
torc, Type
rep)
[] -> Maybe (TypeOrConstraint, Type)
forall a. Maybe a
Nothing
sORTKind_maybe Type
_ = Maybe (TypeOrConstraint, Type)
forall a. Maybe a
Nothing
typeTypeOrConstraint :: HasDebugCallStack => Type -> TypeOrConstraint
typeTypeOrConstraint :: (() :: Constraint) => Type -> TypeOrConstraint
typeTypeOrConstraint Type
ty
= case Type -> Type
coreFullView Type
ty of
FunTy { ft_af :: Type -> FunTyFlag
ft_af = FunTyFlag
af } -> FunTyFlag -> TypeOrConstraint
funTyFlagResultTypeOrConstraint FunTyFlag
af
Type
ty' | Just (TypeOrConstraint
torc, Type
_) <- Type -> Maybe (TypeOrConstraint, Type)
sORTKind_maybe ((() :: Constraint) => Type -> Type
Type -> Type
typeKind Type
ty')
-> TypeOrConstraint
torc
| Bool
otherwise
-> String -> SDoc -> TypeOrConstraint
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"typeOrConstraint" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr ((() :: Constraint) => Type -> Type
Type -> Type
typeKind Type
ty))
isPredTy :: HasDebugCallStack => Type -> Bool
isPredTy :: (() :: Constraint) => Type -> Bool
isPredTy Type
ty = case (() :: Constraint) => Type -> TypeOrConstraint
Type -> TypeOrConstraint
typeTypeOrConstraint Type
ty of
TypeOrConstraint
TypeLike -> Bool
False
TypeOrConstraint
ConstraintLike -> Bool
True
isTYPEorCONSTRAINT :: Kind -> Bool
isTYPEorCONSTRAINT :: Type -> Bool
isTYPEorCONSTRAINT Type
k = Maybe (TypeOrConstraint, Type) -> Bool
forall a. Maybe a -> Bool
isJust (Type -> Maybe (TypeOrConstraint, Type)
sORTKind_maybe Type
k)
tyConIsTYPEorCONSTRAINT :: TyCon -> Bool
tyConIsTYPEorCONSTRAINT :: TyCon -> Bool
tyConIsTYPEorCONSTRAINT TyCon
tc
= Unique
tc_uniq Unique -> Unique -> Bool
forall a. Eq a => a -> a -> Bool
== Unique
tYPETyConKey Bool -> Bool -> Bool
|| Unique
tc_uniq Unique -> Unique -> Bool
forall a. Eq a => a -> a -> Bool
== Unique
cONSTRAINTTyConKey
where
!tc_uniq :: Unique
tc_uniq = TyCon -> Unique
tyConUnique TyCon
tc
isConstraintLikeKind :: Kind -> Bool
isConstraintLikeKind :: Type -> Bool
isConstraintLikeKind Type
kind
= case Type -> Maybe (TypeOrConstraint, Type)
sORTKind_maybe Type
kind of
Just (TypeOrConstraint
ConstraintLike, Type
_) -> Bool
True
Maybe (TypeOrConstraint, Type)
_ -> Bool
False
isConstraintKind :: Kind -> Bool
isConstraintKind :: Type -> Bool
isConstraintKind Type
kind
= case Type -> Maybe (TypeOrConstraint, Type)
sORTKind_maybe Type
kind of
Just (TypeOrConstraint
ConstraintLike, Type
rep) -> Type -> Bool
isLiftedRuntimeRep Type
rep
Maybe (TypeOrConstraint, Type)
_ -> Bool
False
tcIsLiftedTypeKind :: Kind -> Bool
tcIsLiftedTypeKind :: Type -> Bool
tcIsLiftedTypeKind Type
kind
| Just (TypeOrConstraint
TypeLike, Type
rep) <- Type -> Maybe (TypeOrConstraint, Type)
sORTKind_maybe Type
kind
= Type -> Bool
isLiftedRuntimeRep Type
rep
| Bool
otherwise
= Bool
False
tcIsBoxedTypeKind :: Kind -> Bool
tcIsBoxedTypeKind :: Type -> Bool
tcIsBoxedTypeKind Type
kind
| Just (TypeOrConstraint
TypeLike, Type
rep) <- Type -> Maybe (TypeOrConstraint, Type)
sORTKind_maybe Type
kind
= Type -> Bool
isBoxedRuntimeRep Type
rep
| Bool
otherwise
= Bool
False
isTypeLikeKind :: Kind -> Bool
isTypeLikeKind :: Type -> Bool
isTypeLikeKind Type
kind
= case Type -> Maybe (TypeOrConstraint, Type)
sORTKind_maybe Type
kind of
Just (TypeOrConstraint
TypeLike, Type
_) -> Bool
True
Maybe (TypeOrConstraint, Type)
_ -> Bool
False
returnsConstraintKind :: Kind -> Bool
returnsConstraintKind :: Type -> Bool
returnsConstraintKind Type
kind
| Just Type
kind' <- Type -> Maybe Type
coreView Type
kind = Type -> Bool
returnsConstraintKind Type
kind'
returnsConstraintKind (ForAllTy VarBndr TyVar ForAllTyFlag
_ Type
ty) = Type -> Bool
returnsConstraintKind Type
ty
returnsConstraintKind (FunTy { ft_res :: Type -> Type
ft_res = Type
ty }) = Type -> Bool
returnsConstraintKind Type
ty
returnsConstraintKind Type
kind = Type -> Bool
isConstraintLikeKind Type
kind
typeLiteralKind :: TyLit -> Kind
typeLiteralKind :: TyLit -> Type
typeLiteralKind (NumTyLit {}) = Type
naturalTy
typeLiteralKind (StrTyLit {}) = Type
typeSymbolKind
typeLiteralKind (CharTyLit {}) = Type
charTy
typeHasFixedRuntimeRep :: HasDebugCallStack => Type -> Bool
typeHasFixedRuntimeRep :: (() :: Constraint) => Type -> Bool
typeHasFixedRuntimeRep = Type -> Bool
go
where
go :: Type -> Bool
go (TyConApp TyCon
tc [Type]
_)
| TyCon -> Bool
tcHasFixedRuntimeRep TyCon
tc = Bool
True
go (FunTy {}) = Bool
True
go (LitTy {}) = Bool
True
go (ForAllTy VarBndr TyVar ForAllTyFlag
_ Type
ty) = Type -> Bool
go Type
ty
go Type
ty = (() :: Constraint) => Type -> Bool
Type -> Bool
isFixedRuntimeRepKind ((() :: Constraint) => Type -> Type
Type -> Type
typeKind Type
ty)
argsHaveFixedRuntimeRep :: Type -> Bool
argsHaveFixedRuntimeRep :: Type -> Bool
argsHaveFixedRuntimeRep Type
ty
= (PiTyBinder -> Bool) -> [PiTyBinder] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all PiTyBinder -> Bool
ok [PiTyBinder]
bndrs
where
ok :: PiTyBinder -> Bool
ok :: PiTyBinder -> Bool
ok (Anon Scaled Type
ty FunTyFlag
_) = (() :: Constraint) => Type -> Bool
Type -> Bool
typeHasFixedRuntimeRep (Scaled Type -> Type
forall a. Scaled a -> a
scaledThing Scaled Type
ty)
ok PiTyBinder
_ = Bool
True
bndrs :: [PiTyBinder]
([PiTyBinder]
bndrs, Type
_) = Type -> ([PiTyBinder], Type)
splitPiTys Type
ty
isFixedRuntimeRepKind :: HasDebugCallStack => Kind -> Bool
isFixedRuntimeRepKind :: (() :: Constraint) => Type -> Bool
isFixedRuntimeRepKind Type
k
= Bool -> SDoc -> Bool -> Bool
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (Type -> Bool
isTYPEorCONSTRAINT Type
k) (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
k) (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$
Type -> Bool
isConcrete Type
k
isConcrete :: Type -> Bool
isConcrete :: Type -> Bool
isConcrete = Type -> Bool
go
where
go :: Type -> Bool
go Type
ty | Just Type
ty' <- Type -> Maybe Type
coreView Type
ty = Type -> Bool
go Type
ty'
go (TyVarTy TyVar
tv) = TyVar -> Bool
isConcreteTyVar TyVar
tv
go (AppTy Type
ty1 Type
ty2) = Type -> Bool
go Type
ty1 Bool -> Bool -> Bool
&& Type -> Bool
go Type
ty2
go (TyConApp TyCon
tc [Type]
tys)
| TyCon -> Bool
isConcreteTyCon TyCon
tc = (Type -> Bool) -> [Type] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Type -> Bool
go [Type]
tys
| Bool
otherwise = Bool
False
go ForAllTy{} = Bool
False
go (FunTy FunTyFlag
_ Type
w Type
t1 Type
t2) = Type -> Bool
go Type
w
Bool -> Bool -> Bool
&& Type -> Bool
go ((() :: Constraint) => Type -> Type
Type -> Type
typeKind Type
t1) Bool -> Bool -> Bool
&& Type -> Bool
go Type
t1
Bool -> Bool -> Bool
&& Type -> Bool
go ((() :: Constraint) => Type -> Type
Type -> Type
typeKind Type
t2) Bool -> Bool -> Bool
&& Type -> Bool
go Type
t2
go LitTy{} = Bool
True
go CastTy{} = Bool
False
go CoercionTy{} = Bool
False
tyConAppNeedsKindSig
:: Bool
-> TyCon
-> Int
-> Bool
tyConAppNeedsKindSig :: Bool -> TyCon -> Arity -> Bool
tyConAppNeedsKindSig Bool
spec_inj_pos TyCon
tc Arity
n_args
| Ordering
LT <- [TyConBinder] -> Arity -> Ordering
forall a. [a] -> Arity -> Ordering
listLengthCmp [TyConBinder]
tc_binders Arity
n_args
= Bool
False
| Bool
otherwise
= let ([TyConBinder]
dropped_binders, [TyConBinder]
remaining_binders)
= Arity -> [TyConBinder] -> ([TyConBinder], [TyConBinder])
forall a. Arity -> [a] -> ([a], [a])
splitAt Arity
n_args [TyConBinder]
tc_binders
result_kind :: Type
result_kind = [TyConBinder] -> Type -> Type
mkTyConKind [TyConBinder]
remaining_binders Type
tc_res_kind
result_vars :: VarSet
result_vars = Type -> VarSet
tyCoVarsOfType Type
result_kind
dropped_vars :: VarSet
dropped_vars = FV -> VarSet
fvVarSet (FV -> VarSet) -> FV -> VarSet
forall a b. (a -> b) -> a -> b
$
(TyConBinder -> FV) -> [TyConBinder] -> FV
forall a. (a -> FV) -> [a] -> FV
mapUnionFV TyConBinder -> FV
injective_vars_of_binder [TyConBinder]
dropped_binders
in Bool -> Bool
not (VarSet -> VarSet -> Bool
subVarSet VarSet
result_vars VarSet
dropped_vars)
where
tc_binders :: [TyConBinder]
tc_binders = TyCon -> [TyConBinder]
tyConBinders TyCon
tc
tc_res_kind :: Type
tc_res_kind = TyCon -> Type
tyConResKind TyCon
tc
injective_vars_of_binder :: TyConBinder -> FV
injective_vars_of_binder :: TyConBinder -> FV
injective_vars_of_binder (Bndr TyVar
tv TyConBndrVis
vis) =
case TyConBndrVis
vis of
AnonTCB FunTyFlag
af | FunTyFlag -> Bool
isVisibleFunArg FunTyFlag
af
-> Bool -> Type -> FV
injectiveVarsOfType Bool
False
(TyVar -> Type
varType TyVar
tv)
NamedTCB ForAllTyFlag
argf | ForAllTyFlag -> Bool
source_of_injectivity ForAllTyFlag
argf
-> TyVar -> FV
unitFV TyVar
tv FV -> FV -> FV
`unionFV`
Bool -> Type -> FV
injectiveVarsOfType Bool
False (TyVar -> Type
varType TyVar
tv)
TyConBndrVis
_ -> FV
emptyFV
source_of_injectivity :: ForAllTyFlag -> Bool
source_of_injectivity ForAllTyFlag
Required = Bool
True
source_of_injectivity ForAllTyFlag
Specified = Bool
spec_inj_pos
source_of_injectivity ForAllTyFlag
Inferred = Bool
False
unrestricted, linear, tymult :: a -> Scaled a
unrestricted :: forall a. a -> Scaled a
unrestricted = Type -> a -> Scaled a
forall a. Type -> a -> Scaled a
Scaled Type
ManyTy
linear :: forall a. a -> Scaled a
linear = Type -> a -> Scaled a
forall a. Type -> a -> Scaled a
Scaled Type
OneTy
tymult :: forall a. a -> Scaled a
tymult = Type -> a -> Scaled a
forall a. Type -> a -> Scaled a
Scaled Type
ManyTy
irrelevantMult :: Scaled a -> a
irrelevantMult :: forall a. Scaled a -> a
irrelevantMult = Scaled a -> a
forall a. Scaled a -> a
scaledThing
mkScaled :: Mult -> a -> Scaled a
mkScaled :: forall a. Type -> a -> Scaled a
mkScaled = Type -> a -> Scaled a
forall a. Type -> a -> Scaled a
Scaled
scaledSet :: Scaled a -> b -> Scaled b
scaledSet :: forall a b. Scaled a -> b -> Scaled b
scaledSet (Scaled Type
m a
_) b
b = Type -> b -> Scaled b
forall a. Type -> a -> Scaled a
Scaled Type
m b
b
pattern OneTy :: Mult
pattern $mOneTy :: forall {r}. Type -> ((# #) -> r) -> ((# #) -> r) -> r
$bOneTy :: Type
OneTy <- (isOneTy -> True)
where OneTy = Type
oneDataConTy
pattern ManyTy :: Mult
pattern $mManyTy :: forall {r}. Type -> ((# #) -> r) -> ((# #) -> r) -> r
$bManyTy :: Type
ManyTy <- (isManyTy -> True)
where ManyTy = Type
manyDataConTy
isManyTy :: Mult -> Bool
isManyTy :: Type -> Bool
isManyTy Type
ty
| Just TyCon
tc <- Type -> Maybe TyCon
tyConAppTyCon_maybe Type
ty
= TyCon
tc TyCon -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
manyDataConKey
isManyTy Type
_ = Bool
False
isOneTy :: Mult -> Bool
isOneTy :: Type -> Bool
isOneTy Type
ty
| Just TyCon
tc <- Type -> Maybe TyCon
tyConAppTyCon_maybe Type
ty
= TyCon
tc TyCon -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
oneDataConKey
isOneTy Type
_ = Bool
False
isLinearType :: Type -> Bool
isLinearType :: Type -> Bool
isLinearType Type
ty = case Type
ty of
FunTy FunTyFlag
_ Type
ManyTy Type
_ Type
res -> Type -> Bool
isLinearType Type
res
FunTy FunTyFlag
_ Type
_ Type
_ Type
_ -> Bool
True
ForAllTy VarBndr TyVar ForAllTyFlag
_ Type
res -> Type -> Bool
isLinearType Type
res
Type
_ -> Bool
False
mkTyConApp :: TyCon -> [Type] -> Type
mkTyConApp :: TyCon -> [Type] -> Type
mkTyConApp TyCon
tycon []
=
TyCon -> Type
mkTyConTy TyCon
tycon
mkTyConApp TyCon
tycon tys :: [Type]
tys@(Type
ty1:[Type]
rest)
| Just Type
fun_ty <- (() :: Constraint) => TyCon -> [Type] -> Maybe Type
TyCon -> [Type] -> Maybe Type
tyConAppFunTy_maybe TyCon
tycon [Type]
tys
= Type
fun_ty
| Unique
key Unique -> Unique -> Bool
forall a. Eq a => a -> a -> Bool
== Unique
tYPETyConKey
, Just Type
ty <- Type -> Maybe Type
mkTYPEapp_maybe Type
ty1
= Bool -> Type -> Type
forall a. HasCallStack => Bool -> a -> a
assert ([Type] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
rest) Type
ty
| Unique
key Unique -> Unique -> Bool
forall a. Eq a => a -> a -> Bool
== Unique
cONSTRAINTTyConKey
, Just Type
ty <- Type -> Maybe Type
mkCONSTRAINTapp_maybe Type
ty1
= Bool -> Type -> Type
forall a. HasCallStack => Bool -> a -> a
assert ([Type] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
rest) Type
ty
| Unique
key Unique -> Unique -> Bool
forall a. Eq a => a -> a -> Bool
== Unique
boxedRepDataConTyConKey
, Just Type
ty <- Type -> Maybe Type
mkBoxedRepApp_maybe Type
ty1
= Bool -> Type -> Type
forall a. HasCallStack => Bool -> a -> a
assert ([Type] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
rest) Type
ty
| Unique
key Unique -> Unique -> Bool
forall a. Eq a => a -> a -> Bool
== Unique
tupleRepDataConTyConKey
, Just Type
ty <- Type -> Maybe Type
mkTupleRepApp_maybe Type
ty1
= Bool -> Type -> Type
forall a. HasCallStack => Bool -> a -> a
assert ([Type] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
rest) Type
ty
| Bool
otherwise
= TyCon -> [Type] -> Type
TyConApp TyCon
tycon [Type]
tys
where
key :: Unique
key = TyCon -> Unique
tyConUnique TyCon
tycon
mkTYPEapp :: RuntimeRepType -> Type
mkTYPEapp :: Type -> Type
mkTYPEapp Type
rr
= case Type -> Maybe Type
mkTYPEapp_maybe Type
rr of
Just Type
ty -> Type
ty
Maybe Type
Nothing -> TyCon -> [Type] -> Type
TyConApp TyCon
tYPETyCon [Type
rr]
mkTYPEapp_maybe :: RuntimeRepType -> Maybe Type
{-# NOINLINE mkTYPEapp_maybe #-}
mkTYPEapp_maybe :: Type -> Maybe Type
mkTYPEapp_maybe (TyConApp TyCon
tc [Type]
args)
| Unique
key Unique -> Unique -> Bool
forall a. Eq a => a -> a -> Bool
== Unique
liftedRepTyConKey = Bool -> Maybe Type -> Maybe Type
forall a. HasCallStack => Bool -> a -> a
assert ([Type] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
args) (Maybe Type -> Maybe Type) -> Maybe Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$ Type -> Maybe Type
forall a. a -> Maybe a
Just Type
liftedTypeKind
| Unique
key Unique -> Unique -> Bool
forall a. Eq a => a -> a -> Bool
== Unique
unliftedRepTyConKey = Bool -> Maybe Type -> Maybe Type
forall a. HasCallStack => Bool -> a -> a
assert ([Type] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
args) (Maybe Type -> Maybe Type) -> Maybe Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$ Type -> Maybe Type
forall a. a -> Maybe a
Just Type
unliftedTypeKind
| Unique
key Unique -> Unique -> Bool
forall a. Eq a => a -> a -> Bool
== Unique
zeroBitRepTyConKey = Bool -> Maybe Type -> Maybe Type
forall a. HasCallStack => Bool -> a -> a
assert ([Type] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
args) (Maybe Type -> Maybe Type) -> Maybe Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$ Type -> Maybe Type
forall a. a -> Maybe a
Just Type
zeroBitTypeKind
where
key :: Unique
key = TyCon -> Unique
tyConUnique TyCon
tc
mkTYPEapp_maybe Type
_ = Maybe Type
forall a. Maybe a
Nothing
mkCONSTRAINTapp :: RuntimeRepType -> Type
mkCONSTRAINTapp :: Type -> Type
mkCONSTRAINTapp Type
rr
= case Type -> Maybe Type
mkCONSTRAINTapp_maybe Type
rr of
Just Type
ty -> Type
ty
Maybe Type
Nothing -> TyCon -> [Type] -> Type
TyConApp TyCon
cONSTRAINTTyCon [Type
rr]
mkCONSTRAINTapp_maybe :: RuntimeRepType -> Maybe Type
{-# NOINLINE mkCONSTRAINTapp_maybe #-}
mkCONSTRAINTapp_maybe :: Type -> Maybe Type
mkCONSTRAINTapp_maybe (TyConApp TyCon
tc [Type]
args)
| TyCon
tc TyCon -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
liftedRepTyConKey = Bool -> Maybe Type -> Maybe Type
forall a. HasCallStack => Bool -> a -> a
assert ([Type] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
args) (Maybe Type -> Maybe Type) -> Maybe Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$
Type -> Maybe Type
forall a. a -> Maybe a
Just Type
constraintKind
mkCONSTRAINTapp_maybe Type
_ = Maybe Type
forall a. Maybe a
Nothing
mkBoxedRepApp_maybe :: LevityType -> Maybe Type
{-# NOINLINE mkBoxedRepApp_maybe #-}
mkBoxedRepApp_maybe :: Type -> Maybe Type
mkBoxedRepApp_maybe (TyConApp TyCon
tc [Type]
args)
| Unique
key Unique -> Unique -> Bool
forall a. Eq a => a -> a -> Bool
== Unique
liftedDataConKey = Bool -> Maybe Type -> Maybe Type
forall a. HasCallStack => Bool -> a -> a
assert ([Type] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
args) (Maybe Type -> Maybe Type) -> Maybe Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$ Type -> Maybe Type
forall a. a -> Maybe a
Just Type
liftedRepTy
| Unique
key Unique -> Unique -> Bool
forall a. Eq a => a -> a -> Bool
== Unique
unliftedDataConKey = Bool -> Maybe Type -> Maybe Type
forall a. HasCallStack => Bool -> a -> a
assert ([Type] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
args) (Maybe Type -> Maybe Type) -> Maybe Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$ Type -> Maybe Type
forall a. a -> Maybe a
Just Type
unliftedRepTy
where
key :: Unique
key = TyCon -> Unique
tyConUnique TyCon
tc
mkBoxedRepApp_maybe Type
_ = Maybe Type
forall a. Maybe a
Nothing
mkTupleRepApp_maybe :: Type -> Maybe Type
{-# NOINLINE mkTupleRepApp_maybe #-}
mkTupleRepApp_maybe :: Type -> Maybe Type
mkTupleRepApp_maybe (TyConApp TyCon
tc [Type]
args)
| Unique
key Unique -> Unique -> Bool
forall a. Eq a => a -> a -> Bool
== Unique
nilDataConKey = Bool -> Maybe Type -> Maybe Type
forall a. HasCallStack => Bool -> a -> a
assert ([Type] -> Bool
forall a. [a] -> Bool
isSingleton [Type]
args) (Maybe Type -> Maybe Type) -> Maybe Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$ Type -> Maybe Type
forall a. a -> Maybe a
Just Type
zeroBitRepTy
where
key :: Unique
key = TyCon -> Unique
tyConUnique TyCon
tc
mkTupleRepApp_maybe Type
_ = Maybe Type
forall a. Maybe a
Nothing
typeOrConstraintKind :: TypeOrConstraint -> RuntimeRepType -> Kind
typeOrConstraintKind :: TypeOrConstraint -> Type -> Type
typeOrConstraintKind TypeOrConstraint
TypeLike Type
rep = Type -> Type
mkTYPEapp Type
rep
typeOrConstraintKind TypeOrConstraint
ConstraintLike Type
rep = Type -> Type
mkCONSTRAINTapp Type
rep