{-# LANGUAGE FlexibleContexts, PatternSynonyms, ViewPatterns #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
{-# OPTIONS_GHC -Wno-incomplete-record-updates #-}
module GHC.Core.Type (
Type, ArgFlag(..), AnonArgFlag(..),
Specificity(..),
KindOrType, PredType, ThetaType, FRRType,
Var, TyVar, isTyVar, TyCoVar, TyCoBinder, TyCoVarBinder, TyVarBinder,
Mult, Scaled,
KnotTied,
mkTyVarTy, mkTyVarTys, getTyVar, getTyVar_maybe, repGetTyVar_maybe,
getCastedTyVar_maybe, tyVarKind, varType,
mkAppTy, mkAppTys, splitAppTy, splitAppTys, repSplitAppTys,
splitAppTy_maybe, repSplitAppTy_maybe, tcRepSplitAppTy_maybe,
mkFunTy, mkVisFunTy, mkInvisFunTy,
mkVisFunTys,
mkVisFunTyMany, mkInvisFunTyMany,
mkVisFunTysMany, mkInvisFunTysMany,
splitFunTy, splitFunTy_maybe,
splitFunTys, funResultTy, funArgTy,
mkTyConApp, mkTyConTy, mkTYPEapp,
tyConAppTyCon_maybe, tyConAppTyConPicky_maybe,
tyConAppArgs_maybe, tyConAppTyCon, tyConAppArgs,
splitTyConApp_maybe, splitTyConApp, tyConAppArgN,
tcSplitTyConApp_maybe,
splitListTyConApp_maybe,
repSplitTyConApp_maybe,
tcRepSplitTyConApp_maybe,
mkForAllTy, mkForAllTys, mkInvisForAllTys, mkTyCoInvForAllTys,
mkSpecForAllTy, mkSpecForAllTys,
mkVisForAllTys, mkTyCoInvForAllTy,
mkInfForAllTy, mkInfForAllTys,
splitForAllTyCoVars, splitForAllTyVars,
splitForAllReqTVBinders, splitForAllInvisTVBinders,
splitForAllTyCoVarBinders,
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_maybe, kindRep_maybe, kindRep,
mkCastTy, mkCoercionTy, splitCastTy_maybe,
userTypeError_maybe, pprUserTypeErrorTy,
coAxNthLHS,
stripCoercionTy,
splitInvisPiTys, splitInvisPiTysN,
invisibleTyBndrCount,
filterOutInvisibleTypes, filterOutInferredTypes,
partitionInvisibleTypes, partitionInvisibles,
tyConArgFlags, appTyArgFlags,
TyCoMapper(..), mapTyCo, mapTyCoX,
TyCoFolder(..), foldTyCo, noView,
newTyConInstRhs,
sameVis,
mkTyCoVarBinder, mkTyCoVarBinders,
mkTyVarBinder, mkTyVarBinders,
tyVarSpecToBinders,
mkAnonBinder,
isAnonTyCoBinder,
binderVar, binderVars, binderType, binderArgFlag,
tyCoBinderType, tyCoBinderVar_maybe,
tyBinderType,
binderRelevantType_maybe,
isVisibleArgFlag, isInvisibleArgFlag, isVisibleBinder,
isInvisibleBinder, isNamedBinder,
tyConBindersTyCoBinders,
funTyCon, unrestrictedFunTyCon,
isTyVarTy, isFunTy, isCoercionTy,
isCoercionTy_maybe, isForAllTy,
isForAllTy_ty, isForAllTy_co,
isPiTy, isTauTy, isFamFreeTy,
isCoVarType, isAtomicTy,
isValidJoinPointType,
tyConAppNeedsKindSig,
typeLevity_maybe,
isLiftedTypeKind, isUnliftedTypeKind, isBoxedTypeKind, pickyIsLiftedTypeKind,
isLiftedRuntimeRep, isUnliftedRuntimeRep, runtimeRepLevity_maybe,
isBoxedRuntimeRep,
isLiftedLevity, isUnliftedLevity,
isUnliftedType, isBoxedType, isUnboxedTupleType, isUnboxedSumType,
mightBeLiftedType, mightBeUnliftedType,
isStateType,
isAlgType, isDataFamilyAppType,
isPrimitiveType, isStrictType,
isLevityTy, isLevityVar,
isRuntimeRepTy, isRuntimeRepVar, isRuntimeRepKindedTy,
dropRuntimeRepArgs,
getRuntimeRep, getLevity, getLevity_maybe,
isMultiplicityTy, isMultiplicityVar,
unrestricted, linear, tymult,
mkScaled, irrelevantMult, scaledSet,
pattern One, pattern Many,
isOneDataConTy, isManyDataConTy,
isLinearType,
Kind,
typeKind, tcTypeKind, typeHasFixedRuntimeRep, resultHasFixedRuntimeRep,
tcIsLiftedTypeKind, tcIsConstraintKind, tcReturnsConstraintKind,
tcIsBoxedTypeKind, tcIsRuntimeTypeKind,
liftedTypeKind, unliftedTypeKind,
tyCoFVsOfType, tyCoFVsBndr, tyCoFVsVarBndr, tyCoFVsVarBndrs,
tyCoVarsOfType, tyCoVarsOfTypes,
tyCoVarsOfTypeDSet,
coVarsOfType,
coVarsOfTypes,
anyFreeVarsOfType, anyFreeVarsOfTypes,
noFreeVarsOfType,
splitVisVarsOfType, splitVisVarsOfTypes,
expandTypeSynonyms,
typeSize, occCheckExpand,
closeOverKindsDSet, closeOverKindsList,
closeOverKinds,
scopedSort, tyCoVarsOfTypeWellScoped,
tyCoVarsOfTypesWellScoped,
eqType, eqTypeX, eqTypes, nonDetCmpType, nonDetCmpTypes, nonDetCmpTypeX,
nonDetCmpTypesX, nonDetCmpTc,
eqVarBndrs,
seqType, seqTypes,
coreView, tcView,
tyConsOfType,
TvSubstEnv,
TCvSubst(..),
emptyTvSubstEnv, emptyTCvSubst, mkEmptyTCvSubst,
mkTCvSubst, zipTvSubst, mkTvSubstPrs,
zipTCvSubst,
notElemTCvSubst,
getTvSubstEnv, setTvSubstEnv,
zapTCvSubst, getTCvInScope, getTCvSubstRangeFVs,
extendTCvInScope, extendTCvInScopeList, extendTCvInScopeSet,
extendTCvSubst, extendCvSubst,
extendTvSubst, extendTvSubstBinderAndInScope,
extendTvSubstList, extendTvSubstAndInScope,
extendTCvSubstList,
extendTvSubstWithClone,
extendTCvSubstWithClone,
isInScope, composeTCvSubstEnv, composeTCvSubst, zipTyEnv, zipCoEnv,
isEmptyTCvSubst, unionTCvSubst,
substTy, substTys, substScaledTy, substScaledTys, substTyWith, substTysWith, substTheta,
substTyAddInScope,
substTyUnchecked, substTysUnchecked, substScaledTyUnchecked, substScaledTysUnchecked,
substThetaUnchecked, substTyWithUnchecked,
substCoUnchecked, substCoWithUnchecked,
substTyVarBndr, substTyVarBndrs, substTyVar, substTyVars,
substVarBndr, substVarBndrs,
substTyCoBndr,
cloneTyVarBndr, cloneTyVarBndrs, lookupTyVar,
tidyType, tidyTypes,
tidyOpenType, tidyOpenTypes,
tidyVarBndr, tidyVarBndrs, tidyFreeTyCoVars,
tidyOpenTyCoVar, tidyOpenTyCoVars,
tidyTyCoVarOcc,
tidyTopType,
tidyTyCoVarBinder, tidyTyCoVarBinders,
isConstraintKindCon,
classifiesTypeWithValues,
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, listTyCon
, typeSymbolKind, liftedTypeKind, unliftedTypeKind
, liftedRepTy, unliftedRepTy, zeroBitRepTy
, boxedRepDataConTyCon
, constraintKind, zeroBitTypeKind
, unrestrictedFunTyCon
, manyDataConTy, oneDataConTy )
import GHC.Types.Name( Name )
import GHC.Builtin.Names
import GHC.Core.Coercion.Axiom
import {-# SOURCE #-} GHC.Core.Coercion
( mkNomReflCo, mkGReflCo, mkReflCo
, mkTyConAppCo, mkAppCo, mkCoVarCo, mkAxiomRuleCo
, mkForAllCo, mkFunCo, mkAxiomInstCo, mkUnivCo
, mkSymCo, mkTransCo, mkNthCo, mkLRCo, mkInstCo
, mkKindCo, mkSubCo
, decomposePiCos, coercionKind, coercionLKind
, 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 GHC.Data.Pair
import GHC.Data.List.SetOps
import GHC.Types.Unique ( nonDetCmpUnique )
import GHC.Data.Maybe ( orElse, expectJust )
import Data.Maybe ( isJust )
import Control.Monad ( guard )
tcView :: Type -> Maybe Type
tcView :: Type -> Maybe Type
tcView (TyConApp TyCon
tc [Type]
tys)
| res :: Maybe Type
res@(Just Type
_) <- TyCon -> [Type] -> Maybe Type
expandSynTyConApp_maybe TyCon
tc [Type]
tys
= Maybe Type
res
tcView Type
_ = Maybe Type
forall a. Maybe a
Nothing
{-# INLINE tcView #-}
coreView :: Type -> Maybe Type
coreView :: Type -> Maybe Type
coreView ty :: Type
ty@(TyConApp TyCon
tc [Type]
tys)
| res :: Maybe Type
res@(Just Type
_) <- TyCon -> [Type] -> Maybe Type
expandSynTyConApp_maybe TyCon
tc [Type]
tys
= Maybe Type
res
| TyCon -> Bool
isConstraintKindCon TyCon
tc
= Bool -> SDoc -> Maybe Type -> Maybe Type
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr ([Type] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
tys) (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty) (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
coreView Type
_ = Maybe Type
forall a. Maybe a
Nothing
{-# INLINE coreView #-}
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] -> Int -> Bool
forall a. [a] -> Int -> Bool
`lengthAtLeast` (TyCon -> Int
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
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 = TCvSubst -> [TyVar] -> [Type] -> Type
go TCvSubst
empty_subst [TyVar]
tvs [Type]
arg_tys
where
empty_subst :: TCvSubst
empty_subst = InScopeSet -> TCvSubst
mkEmptyTCvSubst InScopeSet
in_scope
in_scope :: InScopeSet
in_scope = TyCoVarSet -> InScopeSet
mkInScopeSet (TyCoVarSet -> InScopeSet) -> TyCoVarSet -> InScopeSet
forall a b. (a -> b) -> a -> b
$ [Type] -> TyCoVarSet
shallowTyCoVarsOfTypes ([Type] -> TyCoVarSet) -> [Type] -> TyCoVarSet
forall a b. (a -> b) -> a -> b
$ [Type]
arg_tys
go :: TCvSubst -> [TyVar] -> [Type] -> Type
go TCvSubst
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) => TCvSubst -> Type -> Type
TCvSubst -> Type -> Type
substTy TCvSubst
subst Type
rhs
go TCvSubst
subst (TyVar
tv:[TyVar]
tvs) (Type
ty:[Type]
tys) = TCvSubst -> [TyVar] -> [Type] -> Type
go (TCvSubst -> TyVar -> Type -> TCvSubst
extendTvSubst TCvSubst
subst TyVar
tv Type
ty) [TyVar]
tvs [Type]
tys
go TCvSubst
_ (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
$$ Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
rhs SDoc -> SDoc -> SDoc
$$ [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
arg_tys)
coreFullView :: Type -> Type
coreFullView :: Type -> Type
coreFullView ty :: Type
ty@(TyConApp TyCon
tc [Type]
_)
| TyCon -> Bool
isTypeSynonymTyCon TyCon
tc Bool -> Bool -> Bool
|| TyCon -> Bool
isConstraintKindCon TyCon
tc = Type -> Type
go Type
ty
where
go :: Type -> Type
go Type
ty
| Just Type
ty' <- Type -> Maybe Type
coreView Type
ty = Type -> Type
go Type
ty'
| Bool
otherwise = Type
ty
coreFullView Type
ty = Type
ty
{-# INLINE coreFullView #-}
expandTypeSynonyms :: Type -> Type
expandTypeSynonyms :: Type -> Type
expandTypeSynonyms Type
ty
= TCvSubst -> Type -> Type
go (InScopeSet -> TCvSubst
mkEmptyTCvSubst InScopeSet
in_scope) Type
ty
where
in_scope :: InScopeSet
in_scope = TyCoVarSet -> InScopeSet
mkInScopeSet (Type -> TyCoVarSet
tyCoVarsOfType Type
ty)
go :: TCvSubst -> Type -> Type
go TCvSubst
subst (TyConApp TyCon
tc [Type]
tys)
| Just ([(TyVar, Type)]
tenv, Type
rhs, [Type]
tys') <- TyCon -> [Type] -> Maybe ([(TyVar, Type)], Type, [Type])
forall tyco.
TyCon -> [tyco] -> Maybe ([(TyVar, tyco)], Type, [tyco])
expandSynTyCon_maybe TyCon
tc [Type]
expanded_tys
= let subst' :: TCvSubst
subst' = InScopeSet -> TvSubstEnv -> TCvSubst
mkTvSubst InScopeSet
in_scope ([(TyVar, Type)] -> TvSubstEnv
forall a. [(TyVar, a)] -> VarEnv a
mkVarEnv [(TyVar, Type)]
tenv)
in Type -> [Type] -> Type
mkAppTys (TCvSubst -> Type -> Type
go TCvSubst
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 (TCvSubst -> Type -> Type
go TCvSubst
subst) [Type]
tys)
go TCvSubst
_ (LitTy TyLit
l) = TyLit -> Type
LitTy TyLit
l
go TCvSubst
subst (TyVarTy TyVar
tv) = TCvSubst -> TyVar -> Type
substTyVar TCvSubst
subst TyVar
tv
go TCvSubst
subst (AppTy Type
t1 Type
t2) = Type -> Type -> Type
mkAppTy (TCvSubst -> Type -> Type
go TCvSubst
subst Type
t1) (TCvSubst -> Type -> Type
go TCvSubst
subst Type
t2)
go TCvSubst
subst ty :: Type
ty@(FunTy AnonArgFlag
_ Type
mult Type
arg Type
res)
= Type
ty { ft_mult :: Type
ft_mult = TCvSubst -> Type -> Type
go TCvSubst
subst Type
mult, ft_arg :: Type
ft_arg = TCvSubst -> Type -> Type
go TCvSubst
subst Type
arg, ft_res :: Type
ft_res = TCvSubst -> Type -> Type
go TCvSubst
subst Type
res }
go TCvSubst
subst (ForAllTy (Bndr TyVar
tv ArgFlag
vis) Type
t)
= let (TCvSubst
subst', TyVar
tv') = (TCvSubst -> Type -> Type)
-> TCvSubst -> TyVar -> (TCvSubst, TyVar)
substVarBndrUsing TCvSubst -> Type -> Type
go TCvSubst
subst TyVar
tv in
VarBndr TyVar ArgFlag -> Type -> Type
ForAllTy (TyVar -> ArgFlag -> VarBndr TyVar ArgFlag
forall var argf. var -> argf -> VarBndr var argf
Bndr TyVar
tv' ArgFlag
vis) (TCvSubst -> Type -> Type
go TCvSubst
subst' Type
t)
go TCvSubst
subst (CastTy Type
ty KindCoercion
co) = Type -> KindCoercion -> Type
mkCastTy (TCvSubst -> Type -> Type
go TCvSubst
subst Type
ty) (TCvSubst -> KindCoercion -> KindCoercion
go_co TCvSubst
subst KindCoercion
co)
go TCvSubst
subst (CoercionTy KindCoercion
co) = KindCoercion -> Type
mkCoercionTy (TCvSubst -> KindCoercion -> KindCoercion
go_co TCvSubst
subst KindCoercion
co)
go_mco :: TCvSubst -> MCoercionN -> MCoercionN
go_mco TCvSubst
_ MCoercionN
MRefl = MCoercionN
MRefl
go_mco TCvSubst
subst (MCo KindCoercion
co) = KindCoercion -> MCoercionN
MCo (TCvSubst -> KindCoercion -> KindCoercion
go_co TCvSubst
subst KindCoercion
co)
go_co :: TCvSubst -> KindCoercion -> KindCoercion
go_co TCvSubst
subst (Refl Type
ty)
= Type -> KindCoercion
mkNomReflCo (TCvSubst -> Type -> Type
go TCvSubst
subst Type
ty)
go_co TCvSubst
subst (GRefl Role
r Type
ty MCoercionN
mco)
= Role -> Type -> MCoercionN -> KindCoercion
mkGReflCo Role
r (TCvSubst -> Type -> Type
go TCvSubst
subst Type
ty) (TCvSubst -> MCoercionN -> MCoercionN
go_mco TCvSubst
subst MCoercionN
mco)
go_co TCvSubst
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 (TCvSubst -> KindCoercion -> KindCoercion
go_co TCvSubst
subst) [KindCoercion]
args)
go_co TCvSubst
subst (AppCo KindCoercion
co KindCoercion
arg)
= KindCoercion -> KindCoercion -> KindCoercion
mkAppCo (TCvSubst -> KindCoercion -> KindCoercion
go_co TCvSubst
subst KindCoercion
co) (TCvSubst -> KindCoercion -> KindCoercion
go_co TCvSubst
subst KindCoercion
arg)
go_co TCvSubst
subst (ForAllCo TyVar
tv KindCoercion
kind_co KindCoercion
co)
= let (TCvSubst
subst', TyVar
tv', KindCoercion
kind_co') = TCvSubst
-> TyVar -> KindCoercion -> (TCvSubst, TyVar, KindCoercion)
go_cobndr TCvSubst
subst TyVar
tv KindCoercion
kind_co in
TyVar -> KindCoercion -> KindCoercion -> KindCoercion
mkForAllCo TyVar
tv' KindCoercion
kind_co' (TCvSubst -> KindCoercion -> KindCoercion
go_co TCvSubst
subst' KindCoercion
co)
go_co TCvSubst
subst (FunCo Role
r KindCoercion
w KindCoercion
co1 KindCoercion
co2)
= Role
-> KindCoercion -> KindCoercion -> KindCoercion -> KindCoercion
mkFunCo Role
r (TCvSubst -> KindCoercion -> KindCoercion
go_co TCvSubst
subst KindCoercion
w) (TCvSubst -> KindCoercion -> KindCoercion
go_co TCvSubst
subst KindCoercion
co1) (TCvSubst -> KindCoercion -> KindCoercion
go_co TCvSubst
subst KindCoercion
co2)
go_co TCvSubst
subst (CoVarCo TyVar
cv)
= TCvSubst -> TyVar -> KindCoercion
substCoVar TCvSubst
subst TyVar
cv
go_co TCvSubst
subst (AxiomInstCo CoAxiom Branched
ax Int
ind [KindCoercion]
args)
= CoAxiom Branched -> Int -> [KindCoercion] -> KindCoercion
mkAxiomInstCo CoAxiom Branched
ax Int
ind ((KindCoercion -> KindCoercion) -> [KindCoercion] -> [KindCoercion]
forall a b. (a -> b) -> [a] -> [b]
map (TCvSubst -> KindCoercion -> KindCoercion
go_co TCvSubst
subst) [KindCoercion]
args)
go_co TCvSubst
subst (UnivCo UnivCoProvenance
p Role
r Type
t1 Type
t2)
= UnivCoProvenance -> Role -> Type -> Type -> KindCoercion
mkUnivCo (TCvSubst -> UnivCoProvenance -> UnivCoProvenance
go_prov TCvSubst
subst UnivCoProvenance
p) Role
r (TCvSubst -> Type -> Type
go TCvSubst
subst Type
t1) (TCvSubst -> Type -> Type
go TCvSubst
subst Type
t2)
go_co TCvSubst
subst (SymCo KindCoercion
co)
= KindCoercion -> KindCoercion
mkSymCo (TCvSubst -> KindCoercion -> KindCoercion
go_co TCvSubst
subst KindCoercion
co)
go_co TCvSubst
subst (TransCo KindCoercion
co1 KindCoercion
co2)
= KindCoercion -> KindCoercion -> KindCoercion
mkTransCo (TCvSubst -> KindCoercion -> KindCoercion
go_co TCvSubst
subst KindCoercion
co1) (TCvSubst -> KindCoercion -> KindCoercion
go_co TCvSubst
subst KindCoercion
co2)
go_co TCvSubst
subst (NthCo Role
r Int
n KindCoercion
co)
= (() :: Constraint) => Role -> Int -> KindCoercion -> KindCoercion
Role -> Int -> KindCoercion -> KindCoercion
mkNthCo Role
r Int
n (TCvSubst -> KindCoercion -> KindCoercion
go_co TCvSubst
subst KindCoercion
co)
go_co TCvSubst
subst (LRCo LeftOrRight
lr KindCoercion
co)
= LeftOrRight -> KindCoercion -> KindCoercion
mkLRCo LeftOrRight
lr (TCvSubst -> KindCoercion -> KindCoercion
go_co TCvSubst
subst KindCoercion
co)
go_co TCvSubst
subst (InstCo KindCoercion
co KindCoercion
arg)
= KindCoercion -> KindCoercion -> KindCoercion
mkInstCo (TCvSubst -> KindCoercion -> KindCoercion
go_co TCvSubst
subst KindCoercion
co) (TCvSubst -> KindCoercion -> KindCoercion
go_co TCvSubst
subst KindCoercion
arg)
go_co TCvSubst
subst (KindCo KindCoercion
co)
= KindCoercion -> KindCoercion
mkKindCo (TCvSubst -> KindCoercion -> KindCoercion
go_co TCvSubst
subst KindCoercion
co)
go_co TCvSubst
subst (SubCo KindCoercion
co)
= (() :: Constraint) => KindCoercion -> KindCoercion
KindCoercion -> KindCoercion
mkSubCo (TCvSubst -> KindCoercion -> KindCoercion
go_co TCvSubst
subst KindCoercion
co)
go_co TCvSubst
subst (AxiomRuleCo CoAxiomRule
ax [KindCoercion]
cs)
= CoAxiomRule -> [KindCoercion] -> KindCoercion
AxiomRuleCo CoAxiomRule
ax ((KindCoercion -> KindCoercion) -> [KindCoercion] -> [KindCoercion]
forall a b. (a -> b) -> [a] -> [b]
map (TCvSubst -> KindCoercion -> KindCoercion
go_co TCvSubst
subst) [KindCoercion]
cs)
go_co TCvSubst
_ (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 :: TCvSubst -> UnivCoProvenance -> UnivCoProvenance
go_prov TCvSubst
subst (PhantomProv KindCoercion
co) = KindCoercion -> UnivCoProvenance
PhantomProv (TCvSubst -> KindCoercion -> KindCoercion
go_co TCvSubst
subst KindCoercion
co)
go_prov TCvSubst
subst (ProofIrrelProv KindCoercion
co) = KindCoercion -> UnivCoProvenance
ProofIrrelProv (TCvSubst -> KindCoercion -> KindCoercion
go_co TCvSubst
subst KindCoercion
co)
go_prov TCvSubst
_ p :: UnivCoProvenance
p@(PluginProv String
_) = UnivCoProvenance
p
go_prov TCvSubst
_ p :: UnivCoProvenance
p@(CorePrepProv Bool
_) = UnivCoProvenance
p
go_cobndr :: TCvSubst
-> TyVar -> KindCoercion -> (TCvSubst, TyVar, KindCoercion)
go_cobndr TCvSubst
subst = Bool
-> (KindCoercion -> KindCoercion)
-> TCvSubst
-> TyVar
-> KindCoercion
-> (TCvSubst, TyVar, KindCoercion)
substForAllCoBndrUsing Bool
False (TCvSubst -> KindCoercion -> KindCoercion
go_co TCvSubst
subst) TCvSubst
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 -> Type
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 Type
kindRep_maybe :: (() :: Constraint) => Type -> Maybe Type
kindRep_maybe Type
kind
| Just [Type
arg] <- Unique -> Type -> Maybe [Type]
isTyConKeyApp_maybe Unique
tYPETyConKey Type
kind = Type -> Maybe Type
forall a. a -> Maybe a
Just Type
arg
| Bool
otherwise = Maybe Type
forall a. Maybe a
Nothing
isBoxedTypeKind :: Kind -> Bool
isBoxedTypeKind :: Type -> Bool
isBoxedTypeKind Type
kind
= case (() :: Constraint) => Type -> Maybe Type
Type -> Maybe Type
kindRep_maybe Type
kind of
Just Type
rep -> Type -> Bool
isBoxedRuntimeRep Type
rep
Maybe Type
Nothing -> Bool
False
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
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
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
isBoxedRuntimeRep :: Type -> 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 :: Type -> Maybe Type
isBoxedRuntimeRep_maybe :: Type -> Maybe Type
isBoxedRuntimeRep_maybe Type
rep
| 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
runtimeRepLevity_maybe :: Type -> Maybe Levity
runtimeRepLevity_maybe :: Type -> Maybe Levity
runtimeRepLevity_maybe Type
rep
| TyConApp TyCon
rr_tc [Type]
args <- Type -> Type
coreFullView Type
rep
, TyCon -> Bool
isPromotedDataCon TyCon
rr_tc =
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 -> Bool
isLiftedLevity Type
lev -> Levity -> Maybe Levity
forall a. a -> Maybe a
Just Levity
Lifted
| Type -> Bool
isUnliftedLevity Type
lev -> Levity -> Maybe Levity
forall a. a -> Maybe a
Just Levity
Unlifted
[Type]
_ -> Maybe Levity
forall a. Maybe a
Nothing
else Levity -> Maybe Levity
forall a. a -> Maybe a
Just Levity
Unlifted
runtimeRepLevity_maybe Type
_ = Maybe Levity
forall a. Maybe a
Nothing
isLiftedRuntimeRep :: Type -> 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 :: Type -> 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
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 -> ArgFlag -> m (env, TyVar)
tcm_tycobinder :: env -> TyCoVar -> ArgFlag -> 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 -> ArgFlag -> m (env, TyVar)
tcm_tycobinder = env -> TyVar -> ArgFlag -> 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 AnonArgFlag
_ 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 :: Type
ft_mult = Type
w', ft_arg :: Type
ft_arg = Type
arg', ft_res :: Type
ft_res = Type
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 ArgFlag
vis) Type
inner)
= do { (env
env', TyVar
tv') <- env -> TyVar -> ArgFlag -> m (env, TyVar)
tycobinder env
env TyVar
tv ArgFlag
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 ArgFlag -> Type -> Type
ForAllTy (TyVar -> ArgFlag -> VarBndr TyVar ArgFlag
forall var argf. var -> argf -> VarBndr var argf
Bndr TyVar
tv' ArgFlag
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 KindCoercion
cw KindCoercion
c1 KindCoercion
c2) = Role
-> KindCoercion -> KindCoercion -> KindCoercion -> KindCoercion
mkFunCo Role
r (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 (NthCo Role
r Int
i KindCoercion
co) = (() :: Constraint) => Role -> Int -> KindCoercion -> KindCoercion
Role -> Int -> KindCoercion -> KindCoercion
mkNthCo Role
r Int
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 Int
i [KindCoercion]
cos) = CoAxiom Branched -> Int -> [KindCoercion] -> KindCoercion
mkAxiomInstCo CoAxiom Branched
ax Int
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 -> ArgFlag -> m (env, TyVar)
tycobinder env
env TyVar
tv ArgFlag
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 :: String -> Type -> TyVar
getTyVar :: String -> Type -> TyVar
getTyVar String
msg Type
ty = case Type -> Maybe TyVar
getTyVar_maybe Type
ty of
Just TyVar
tv -> TyVar
tv
Maybe TyVar
Nothing -> String -> TyVar
forall a. String -> a
panic (String
"getTyVar: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
msg)
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)
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
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
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
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)
repSplitAppTy_maybe (Type -> Maybe (Type, Type))
-> (Type -> Type) -> Type -> Maybe (Type, Type)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Type
coreFullView
repSplitAppTy_maybe :: HasDebugCallStack => Type -> Maybe (Type,Type)
repSplitAppTy_maybe :: (() :: Constraint) => Type -> Maybe (Type, Type)
repSplitAppTy_maybe (FunTy AnonArgFlag
_ Type
w Type
ty1 Type
ty2)
= (Type, Type) -> Maybe (Type, Type)
forall a. a -> Maybe a
Just (TyCon -> [Type] -> Type
TyConApp TyCon
funTyCon [Type
w, Type
rep1, Type
rep2, Type
ty1], Type
ty2)
where
rep1 :: Type
rep1 = (() :: Constraint) => Type -> Type
Type -> Type
getRuntimeRep Type
ty1
rep2 :: Type
rep2 = (() :: Constraint) => Type -> Type
Type -> Type
getRuntimeRep Type
ty2
repSplitAppTy_maybe (AppTy Type
ty1 Type
ty2)
= (Type, Type) -> Maybe (Type, Type)
forall a. a -> Maybe a
Just (Type
ty1, Type
ty2)
repSplitAppTy_maybe (TyConApp TyCon
tc [Type]
tys)
| Bool -> Bool
not (TyCon -> Bool
mustBeSaturated TyCon
tc) Bool -> Bool -> Bool
|| [Type]
tys [Type] -> Int -> Bool
forall a. [a] -> Int -> Bool
`lengthExceeds` TyCon -> Int
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')
repSplitAppTy_maybe Type
_other = Maybe (Type, Type)
forall a. Maybe a
Nothing
tcRepSplitAppTy_maybe :: Type -> Maybe (Type,Type)
tcRepSplitAppTy_maybe :: Type -> Maybe (Type, Type)
tcRepSplitAppTy_maybe (FunTy { ft_af :: Type -> AnonArgFlag
ft_af = AnonArgFlag
af, ft_mult :: Type -> Type
ft_mult = Type
w, ft_arg :: Type -> Type
ft_arg = Type
ty1, ft_res :: Type -> Type
ft_res = Type
ty2 })
| AnonArgFlag
VisArg <- AnonArgFlag
af
, Just Type
rep1 <- (() :: Constraint) => Type -> Maybe Type
Type -> Maybe Type
getRuntimeRep_maybe Type
ty1
, Just Type
rep2 <- (() :: Constraint) => Type -> Maybe Type
Type -> Maybe Type
getRuntimeRep_maybe Type
ty2
= (Type, Type) -> Maybe (Type, Type)
forall a. a -> Maybe a
Just (TyCon -> [Type] -> Type
TyConApp TyCon
funTyCon [Type
w, Type
rep1, Type
rep2, Type
ty1], Type
ty2)
| Bool
otherwise
= Maybe (Type, Type)
forall a. Maybe a
Nothing
tcRepSplitAppTy_maybe (AppTy Type
ty1 Type
ty2) = (Type, Type) -> Maybe (Type, Type)
forall a. a -> Maybe a
Just (Type
ty1, Type
ty2)
tcRepSplitAppTy_maybe (TyConApp TyCon
tc [Type]
tys)
| Bool -> Bool
not (TyCon -> Bool
mustBeSaturated TyCon
tc) Bool -> Bool -> Bool
|| [Type]
tys [Type] -> Int -> Bool
forall a. [a] -> Int -> Bool
`lengthExceeds` TyCon -> Int
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')
tcRepSplitAppTy_maybe Type
_other = Maybe (Type, Type)
forall a. Maybe a
Nothing
splitAppTy :: Type -> (Type, Type)
splitAppTy :: Type -> (Type, Type)
splitAppTy Type
ty = case Type -> Maybe (Type, Type)
splitAppTy_maybe Type
ty of
Just (Type, Type)
pr -> (Type, Type)
pr
Maybe (Type, Type)
Nothing -> String -> (Type, Type)
forall a. String -> a
panic String
"splitAppTy"
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 :: Int
n | TyCon -> Bool
mustBeSaturated TyCon
tc = TyCon -> Int
tyConArity TyCon
tc
| Bool
otherwise = Int
0
([Type]
tc_args1, [Type]
tc_args2) = Int -> [Type] -> ([Type], [Type])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
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 AnonArgFlag
_ Type
w Type
ty1 Type
ty2) [Type]
args
= 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
funTyCon [], [Type
w, Type
rep1, Type
rep2, Type
ty1, Type
ty2])
where
rep1 :: Type
rep1 = (() :: Constraint) => Type -> Type
Type -> Type
getRuntimeRep Type
ty1
rep2 :: Type
rep2 = (() :: Constraint) => Type -> Type
Type -> Type
getRuntimeRep Type
ty2
split Type
orig_ty Type
_ [Type]
args = (Type
orig_ty, [Type]
args)
repSplitAppTys :: HasDebugCallStack => Type -> (Type, [Type])
repSplitAppTys :: (() :: Constraint) => Type -> (Type, [Type])
repSplitAppTys 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 :: Int
n | TyCon -> Bool
mustBeSaturated TyCon
tc = TyCon -> Int
tyConArity TyCon
tc
| Bool
otherwise = Int
0
([Type]
tc_args1, [Type]
tc_args2) = Int -> [Type] -> ([Type], [Type])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
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 AnonArgFlag
_ Type
w Type
ty1 Type
ty2) [Type]
args
= 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
funTyCon [], [Type
w, Type
rep1, Type
rep2, Type
ty1, Type
ty2])
where
rep1 :: Type
rep1 = (() :: Constraint) => Type -> Type
Type -> Type
getRuntimeRep Type
ty1
rep2 :: Type
rep2 = (() :: Constraint) => Type -> Type
Type -> Type
getRuntimeRep Type
ty2
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
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
<> 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
$$ Type -> SDoc
pprUserTypeErrorTy Type
t2
Maybe (TyCon, [Type])
_ -> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty
splitFunTy :: Type -> (Mult, Type, Type)
splitFunTy :: Type -> (Type, Type, Type)
splitFunTy = String -> Maybe (Type, Type, Type) -> (Type, Type, Type)
forall a. HasCallStack => String -> Maybe a -> a
expectJust String
"splitFunTy" (Maybe (Type, Type, Type) -> (Type, Type, Type))
-> (Type -> Maybe (Type, Type, Type)) -> Type -> (Type, Type, Type)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Maybe (Type, Type, Type)
splitFunTy_maybe
{-# INLINE splitFunTy_maybe #-}
splitFunTy_maybe :: Type -> Maybe (Mult, Type, Type)
splitFunTy_maybe :: Type -> Maybe (Type, Type, Type)
splitFunTy_maybe Type
ty
| FunTy AnonArgFlag
_ Type
w Type
arg Type
res <- Type -> Type
coreFullView Type
ty = (Type, Type, Type) -> Maybe (Type, Type, Type)
forall a. a -> Maybe a
Just (Type
w, Type
arg, Type
res)
| Bool
otherwise = Maybe (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 AnonArgFlag
_ 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
$$ 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 ArgFlag
_) Type
res
-> let empty_subst :: TCvSubst
empty_subst = InScopeSet -> TCvSubst
mkEmptyTCvSubst (InScopeSet -> TCvSubst) -> InScopeSet -> TCvSubst
forall a b. (a -> b) -> a -> b
$ TyCoVarSet -> InScopeSet
mkInScopeSet (TyCoVarSet -> InScopeSet) -> TyCoVarSet -> InScopeSet
forall a b. (a -> b) -> a -> b
$
[Type] -> TyCoVarSet
tyCoVarsOfTypes [Type
arg,Type
res]
in Type -> Maybe Type
forall a. a -> Maybe a
Just ((() :: Constraint) => TCvSubst -> Type -> Type
TCvSubst -> Type -> Type
substTy (TCvSubst -> TyVar -> Type -> TCvSubst
extendTCvSubst TCvSubst
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 ArgFlag
_) Type
res <- Type
ty
= TCvSubst -> Type -> [Type] -> Type
go (TCvSubst -> TyVar -> Type -> TCvSubst
extendTCvSubst TCvSubst
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
$$ [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
orig_args)
where
init_subst :: TCvSubst
init_subst = InScopeSet -> TCvSubst
mkEmptyTCvSubst (InScopeSet -> TCvSubst) -> InScopeSet -> TCvSubst
forall a b. (a -> b) -> a -> b
$ TyCoVarSet -> InScopeSet
mkInScopeSet ([Type] -> TyCoVarSet
tyCoVarsOfTypes (Type
tyType -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:[Type]
orig_args))
go :: TCvSubst -> Type -> [Type] -> Type
go :: TCvSubst -> Type -> [Type] -> Type
go TCvSubst
subst Type
ty [] = TCvSubst -> Type -> Type
substTyUnchecked TCvSubst
subst Type
ty
go TCvSubst
subst Type
ty all_args :: [Type]
all_args@(Type
arg:[Type]
args)
| FunTy { ft_res :: Type -> Type
ft_res = Type
res } <- Type
ty
= TCvSubst -> Type -> [Type] -> Type
go TCvSubst
subst Type
res [Type]
args
| ForAllTy (Bndr TyVar
tv ArgFlag
_) Type
res <- Type
ty
= TCvSubst -> Type -> [Type] -> Type
go (TCvSubst -> TyVar -> Type -> TCvSubst
extendTCvSubst TCvSubst
subst TyVar
tv Type
arg) Type
res [Type]
args
| Just Type
ty' <- Type -> Maybe Type
coreView Type
ty
= TCvSubst -> Type -> [Type] -> Type
go TCvSubst
subst Type
ty' [Type]
all_args
| Bool -> Bool
not (TCvSubst -> Bool
isEmptyTCvSubst TCvSubst
subst)
= TCvSubst -> Type -> [Type] -> Type
go TCvSubst
init_subst
((() :: Constraint) => TCvSubst -> Type -> Type
TCvSubst -> Type -> Type
substTy TCvSubst
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
$$ [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
orig_args SDoc -> SDoc -> SDoc
$$ [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
all_args)
applyTysX :: [TyVar] -> Type -> [Type] -> Type
applyTysX :: [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 -> TyCoVarSet
tyCoVarsOfType Type
body_ty TyCoVarSet -> TyCoVarSet -> Bool
`subVarSet` [TyVar] -> TyCoVarSet
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
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 {}) = TyCon -> Maybe TyCon
forall a. a -> Maybe a
Just TyCon
funTyCon
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 {} -> TyCon -> Maybe TyCon
forall a. a -> Maybe a
Just TyCon
funTyCon
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 Type -> Type
coreFullView Type
ty of
TyConApp TyCon
_ [Type]
tys -> [Type] -> Maybe [Type]
forall a. a -> Maybe a
Just [Type]
tys
FunTy AnonArgFlag
_ Type
w Type
arg Type
res
| Just Type
rep1 <- (() :: Constraint) => Type -> Maybe Type
Type -> Maybe Type
getRuntimeRep_maybe Type
arg
, Just Type
rep2 <- (() :: Constraint) => Type -> Maybe Type
Type -> Maybe Type
getRuntimeRep_maybe Type
res
-> [Type] -> Maybe [Type]
forall a. a -> Maybe a
Just [Type
w, Type
rep1, Type
rep2, Type
arg, Type
res]
Type
_ -> 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)
tyConAppArgN :: Int -> Type -> Type
tyConAppArgN :: Int -> Type -> Type
tyConAppArgN Int
n Type
ty
= case Type -> Maybe [Type]
tyConAppArgs_maybe Type
ty of
Just [Type]
tys -> [Type]
tys [Type] -> Int -> Type
forall a. Outputable a => [a] -> Int -> a
`getNth` Int
n
Maybe [Type]
Nothing -> String -> SDoc -> Type
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"tyConAppArgN" (Int -> SDoc
forall a. Outputable a => a -> SDoc
ppr Int
n SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty)
splitTyConApp :: Type -> (TyCon, [Type])
splitTyConApp :: Type -> (TyCon, [Type])
splitTyConApp Type
ty = case (() :: Constraint) => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
ty of
Just (TyCon, [Type])
stuff -> (TyCon, [Type])
stuff
Maybe (TyCon, [Type])
Nothing -> 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 = (() :: Constraint) => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
repSplitTyConApp_maybe (Type -> Maybe (TyCon, [Type]))
-> (Type -> Type) -> Type -> Maybe (TyCon, [Type])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Type
coreFullView
tcSplitTyConApp_maybe :: HasCallStack => Type -> Maybe (TyCon, [Type])
tcSplitTyConApp_maybe :: HasCallStack => Type -> Maybe (TyCon, [Type])
tcSplitTyConApp_maybe Type
ty | Just Type
ty' <- Type -> Maybe Type
tcView Type
ty = HasCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
tcSplitTyConApp_maybe Type
ty'
| Bool
otherwise = (() :: Constraint) => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
tcRepSplitTyConApp_maybe Type
ty
repSplitTyConApp_maybe :: HasDebugCallStack => Type -> Maybe (TyCon, [Type])
repSplitTyConApp_maybe :: (() :: Constraint) => Type -> Maybe (TyCon, [Type])
repSplitTyConApp_maybe (TyConApp TyCon
tc [Type]
tys) = (TyCon, [Type]) -> Maybe (TyCon, [Type])
forall a. a -> Maybe a
Just (TyCon
tc, [Type]
tys)
repSplitTyConApp_maybe (FunTy AnonArgFlag
_ Type
w Type
arg Type
res)
= (TyCon, [Type]) -> Maybe (TyCon, [Type])
forall a. a -> Maybe a
Just (TyCon
funTyCon, [Type
w, Type
arg_rep, Type
res_rep, Type
arg, Type
res])
where
arg_rep :: Type
arg_rep = (() :: Constraint) => Type -> Type
Type -> Type
getRuntimeRep Type
arg
res_rep :: Type
res_rep = (() :: Constraint) => Type -> Type
Type -> Type
getRuntimeRep Type
res
repSplitTyConApp_maybe Type
_ = Maybe (TyCon, [Type])
forall a. Maybe a
Nothing
tcRepSplitTyConApp_maybe :: HasDebugCallStack => Type -> Maybe (TyCon, [Type])
tcRepSplitTyConApp_maybe :: (() :: Constraint) => Type -> Maybe (TyCon, [Type])
tcRepSplitTyConApp_maybe (TyConApp TyCon
tc [Type]
tys) = (TyCon, [Type]) -> Maybe (TyCon, [Type])
forall a. a -> Maybe a
Just (TyCon
tc, [Type]
tys)
tcRepSplitTyConApp_maybe (FunTy AnonArgFlag
VisArg Type
w 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
= (TyCon, [Type]) -> Maybe (TyCon, [Type])
forall a. a -> Maybe a
Just (TyCon
funTyCon, [Type
w, Type
arg_rep, Type
res_rep, Type
arg, Type
res])
tcRepSplitTyConApp_maybe Type
_ = Maybe (TyCon, [Type])
forall a. Maybe a
Nothing
splitListTyConApp_maybe :: Type -> Maybe Type
splitListTyConApp_maybe :: Type -> Maybe Type
splitListTyConApp_maybe Type
ty = case (() :: Constraint) => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
ty of
Just (TyCon
tc,[Type
e]) | TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
listTyCon -> Type -> Maybe Type
forall a. a -> Maybe a
Just Type
e
Maybe (TyCon, [Type])
_other -> Maybe Type
forall a. Maybe a
Nothing
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
$$ [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
tys SDoc -> SDoc -> SDoc
$$ [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
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 ArgFlag
vis) Type
inner_ty)
| TyVar -> Bool
isTyVar TyVar
tv
, let fvs :: TyCoVarSet
fvs = KindCoercion -> TyCoVarSet
tyCoVarsOfCo KindCoercion
co
=
if TyVar
tv TyVar -> TyCoVarSet -> Bool
`elemVarSet` TyCoVarSet
fvs
then let empty_subst :: TCvSubst
empty_subst = InScopeSet -> TCvSubst
mkEmptyTCvSubst (TyCoVarSet -> InScopeSet
mkInScopeSet TyCoVarSet
fvs)
(TCvSubst
subst, TyVar
tv') = (() :: Constraint) => TCvSubst -> TyVar -> (TCvSubst, TyVar)
TCvSubst -> TyVar -> (TCvSubst, TyVar)
substVarBndr TCvSubst
empty_subst TyVar
tv
in VarBndr TyVar ArgFlag -> Type -> Type
ForAllTy (TyVar -> ArgFlag -> VarBndr TyVar ArgFlag
forall var argf. var -> argf -> VarBndr var argf
Bndr TyVar
tv' ArgFlag
vis) ((() :: Constraint) => TCvSubst -> Type -> Type
TCvSubst -> Type -> Type
substTy TCvSubst
subst Type
inner_ty Type -> KindCoercion -> Type
`mk_cast_ty` KindCoercion
co)
else VarBndr TyVar ArgFlag -> Type -> Type
ForAllTy (TyVar -> ArgFlag -> VarBndr TyVar ArgFlag
forall var argf. var -> argf -> VarBndr var argf
Bndr TyVar
tv ArgFlag
vis) (Type
inner_ty Type -> KindCoercion -> Type
`mk_cast_ty` KindCoercion
co)
go Type
_ = Type -> KindCoercion -> Type
CastTy Type
orig_ty KindCoercion
co
tyConBindersTyCoBinders :: [TyConBinder] -> [TyCoBinder]
tyConBindersTyCoBinders :: [TyConBinder] -> [TyCoBinder]
tyConBindersTyCoBinders = (TyConBinder -> TyCoBinder) -> [TyConBinder] -> [TyCoBinder]
forall a b. (a -> b) -> [a] -> [b]
map TyConBinder -> TyCoBinder
to_tyb
where
to_tyb :: TyConBinder -> TyCoBinder
to_tyb (Bndr TyVar
tv (NamedTCB ArgFlag
vis)) = VarBndr TyVar ArgFlag -> TyCoBinder
Named (TyVar -> ArgFlag -> VarBndr TyVar ArgFlag
forall var argf. var -> argf -> VarBndr var argf
Bndr TyVar
tv ArgFlag
vis)
to_tyb (Bndr TyVar
tv (AnonTCB AnonArgFlag
af)) = AnonArgFlag -> Scaled Type -> TyCoBinder
Anon AnonArgFlag
af (Type -> Scaled Type
forall a. a -> Scaled a
tymult (TyVar -> Type
varType TyVar
tv))
mkTyConTy :: TyCon -> Type
mkTyConTy :: TyCon -> Type
mkTyConTy TyCon
tycon = TyCon -> Type
tyConNullaryTy TyCon
tycon
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)
| Unique
key Unique -> Unique -> Bool
forall a. Eq a => a -> a -> Bool
== Unique
funTyConKey
= case [Type]
tys of
[Type
w, Type
_rep1,Type
_rep2,Type
arg,Type
res] -> FunTy { ft_af :: AnonArgFlag
ft_af = AnonArgFlag
VisArg, ft_mult :: Type
ft_mult = Type
w
, ft_arg :: Type
ft_arg = Type
arg, ft_res :: Type
ft_res = Type
res }
[Type]
_ -> Type
bale_out
| Unique
key Unique -> Unique -> Bool
forall a. Eq a => a -> a -> Bool
== Unique
tYPETyConKey
= 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 -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$
case Type -> Maybe Type
mkTYPEapp_maybe Type
ty1 of
Just Type
ty -> Type
ty
Maybe Type
Nothing -> Type
bale_out
| Unique
key Unique -> Unique -> Bool
forall a. Eq a => a -> a -> Bool
== Unique
boxedRepDataConTyConKey
= 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 -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$
case Type -> Maybe Type
mkBoxedRepApp_maybe Type
ty1 of
Just Type
ty -> Type
ty
Maybe Type
Nothing -> Type
bale_out
| Unique
key Unique -> Unique -> Bool
forall a. Eq a => a -> a -> Bool
== Unique
tupleRepDataConTyConKey
= case Type -> Maybe Type
mkTupleRepApp_maybe Type
ty1 of
Just Type
ty -> Type
ty
Maybe Type
Nothing -> Type
bale_out
| Bool
otherwise
= Type
bale_out
where
key :: Unique
key = TyCon -> Unique
tyConUnique TyCon
tycon
bale_out :: Type
bale_out = TyCon -> [Type] -> Type
TyConApp TyCon
tycon [Type]
tys
mkTYPEapp :: Type -> 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 :: Type -> 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
mkBoxedRepApp_maybe :: Type -> 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
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)
mkTyCoInvForAllTy :: TyCoVar -> Type -> Type
mkTyCoInvForAllTy :: TyVar -> Type -> Type
mkTyCoInvForAllTy TyVar
tv Type
ty
| TyVar -> Bool
isCoVar TyVar
tv
, Bool -> Bool
not (TyVar
tv TyVar -> TyCoVarSet -> Bool
`elemVarSet` Type -> TyCoVarSet
tyCoVarsOfType Type
ty)
= Type -> Type -> Type
mkVisFunTyMany (TyVar -> Type
varType TyVar
tv) Type
ty
| Bool
otherwise
= VarBndr TyVar ArgFlag -> Type -> Type
ForAllTy (TyVar -> ArgFlag -> VarBndr TyVar ArgFlag
forall var argf. var -> argf -> VarBndr var argf
Bndr TyVar
tv ArgFlag
Inferred) Type
ty
mkInfForAllTy :: TyVar -> Type -> Type
mkInfForAllTy :: TyVar -> Type -> Type
mkInfForAllTy TyVar
tv Type
ty = Bool
-> (VarBndr TyVar ArgFlag -> Type -> Type)
-> VarBndr TyVar ArgFlag
-> Type
-> Type
forall a. HasCallStack => Bool -> a -> a
assert (TyVar -> Bool
isTyVar TyVar
tv )
VarBndr TyVar ArgFlag -> Type -> Type
ForAllTy (TyVar -> ArgFlag -> VarBndr TyVar ArgFlag
forall var argf. var -> argf -> VarBndr var argf
Bndr TyVar
tv ArgFlag
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 ArgFlag -> Type -> Type)
-> VarBndr TyVar ArgFlag
-> Type
-> Type
forall a. HasCallStack => Bool -> a -> a
assert (TyVar -> Bool
isTyVar TyVar
tv )
VarBndr TyVar ArgFlag -> Type -> Type
ForAllTy (TyVar -> ArgFlag -> VarBndr TyVar ArgFlag
forall var argf. var -> argf -> VarBndr var argf
Bndr TyVar
tv ArgFlag
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 ArgFlag] -> Type -> Type)
-> [VarBndr TyVar ArgFlag]
-> 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 ArgFlag] -> Type -> Type
mkForAllTys [ TyVar -> ArgFlag -> VarBndr TyVar ArgFlag
forall var argf. var -> argf -> VarBndr var argf
Bndr TyVar
tv ArgFlag
Required | TyVar
tv <- [TyVar]
tvs ]
mkTyConBindersPreferAnon :: [TyVar]
-> TyCoVarSet
-> [TyConBinder]
mkTyConBindersPreferAnon :: [TyVar] -> TyCoVarSet -> [TyConBinder]
mkTyConBindersPreferAnon [TyVar]
vars TyCoVarSet
inner_tkvs = Bool
-> (([TyConBinder], TyCoVarSet) -> [TyConBinder])
-> ([TyConBinder], TyCoVarSet)
-> [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], TyCoVarSet) -> [TyConBinder]
forall a b. (a, b) -> a
fst ([TyVar] -> ([TyConBinder], TyCoVarSet)
go [TyVar]
vars)
where
go :: [TyVar] -> ([TyConBinder], VarSet)
go :: [TyVar] -> ([TyConBinder], TyCoVarSet)
go [] = ([], TyCoVarSet
inner_tkvs)
go (TyVar
v:[TyVar]
vs) | TyVar
v TyVar -> TyCoVarSet -> Bool
`elemVarSet` TyCoVarSet
fvs
= ( TyVar -> TyConBndrVis -> TyConBinder
forall var argf. var -> argf -> VarBndr var argf
Bndr TyVar
v (ArgFlag -> TyConBndrVis
NamedTCB ArgFlag
Required) TyConBinder -> [TyConBinder] -> [TyConBinder]
forall a. a -> [a] -> [a]
: [TyConBinder]
binders
, TyCoVarSet
fvs TyCoVarSet -> TyVar -> TyCoVarSet
`delVarSet` TyVar
v TyCoVarSet -> TyCoVarSet -> TyCoVarSet
`unionVarSet` TyCoVarSet
kind_vars )
| Bool
otherwise
= ( TyVar -> TyConBndrVis -> TyConBinder
forall var argf. var -> argf -> VarBndr var argf
Bndr TyVar
v (AnonArgFlag -> TyConBndrVis
AnonTCB AnonArgFlag
VisArg) TyConBinder -> [TyConBinder] -> [TyConBinder]
forall a. a -> [a] -> [a]
: [TyConBinder]
binders
, TyCoVarSet
fvs TyCoVarSet -> TyCoVarSet -> TyCoVarSet
`unionVarSet` TyCoVarSet
kind_vars )
where
([TyConBinder]
binders, TyCoVarSet
fvs) = [TyVar] -> ([TyConBinder], TyCoVarSet)
go [TyVar]
vs
kind_vars :: TyCoVarSet
kind_vars = Type -> TyCoVarSet
tyCoVarsOfType (Type -> TyCoVarSet) -> Type -> TyCoVarSet
forall a b. (a -> b) -> a -> b
$ TyVar -> Type
tyVarKind TyVar
v
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 ArgFlag
_) 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)
splitSomeForAllTyCoVarBndrs :: (ArgFlag -> Maybe af) -> Type -> ([VarBndr TyCoVar af], Type)
splitSomeForAllTyCoVarBndrs :: forall af.
(ArgFlag -> Maybe af) -> Type -> ([VarBndr TyVar af], Type)
splitSomeForAllTyCoVarBndrs ArgFlag -> Maybe af
argf_pred Type
ty = Type -> Type -> [VarBndr TyVar af] -> ([VarBndr TyVar af], Type)
split Type
ty Type
ty []
where
split :: Type -> Type -> [VarBndr TyVar af] -> ([VarBndr TyVar af], Type)
split Type
_ (ForAllTy (Bndr TyVar
tcv ArgFlag
argf) Type
ty) [VarBndr TyVar af]
tvs
| Just af
argf' <- ArgFlag -> Maybe af
argf_pred ArgFlag
argf = Type -> Type -> [VarBndr TyVar af] -> ([VarBndr TyVar af], Type)
split Type
ty Type
ty (TyVar -> af -> VarBndr TyVar af
forall var argf. var -> argf -> VarBndr var argf
Bndr TyVar
tcv af
argf' VarBndr TyVar af -> [VarBndr TyVar af] -> [VarBndr TyVar af]
forall a. a -> [a] -> [a]
: [VarBndr TyVar af]
tvs)
split Type
orig_ty Type
ty [VarBndr TyVar af]
tvs | Just Type
ty' <- Type -> Maybe Type
coreView Type
ty = Type -> Type -> [VarBndr TyVar af] -> ([VarBndr TyVar af], Type)
split Type
orig_ty Type
ty' [VarBndr TyVar af]
tvs
split Type
orig_ty Type
_ [VarBndr TyVar af]
tvs = ([VarBndr TyVar af] -> [VarBndr TyVar af]
forall a. [a] -> [a]
reverse [VarBndr TyVar af]
tvs, Type
orig_ty)
splitForAllReqTVBinders :: Type -> ([ReqTVBinder], Type)
splitForAllReqTVBinders :: Type -> ([ReqTVBinder], Type)
splitForAllReqTVBinders Type
ty = (ArgFlag -> Maybe ()) -> Type -> ([ReqTVBinder], Type)
forall af.
(ArgFlag -> Maybe af) -> Type -> ([VarBndr TyVar af], Type)
splitSomeForAllTyCoVarBndrs ArgFlag -> Maybe ()
argf_pred Type
ty
where
argf_pred :: ArgFlag -> Maybe ()
argf_pred :: ArgFlag -> Maybe ()
argf_pred ArgFlag
Required = () -> Maybe ()
forall a. a -> Maybe a
Just ()
argf_pred (Invisible {}) = Maybe ()
forall a. Maybe a
Nothing
splitForAllInvisTVBinders :: Type -> ([InvisTVBinder], Type)
splitForAllInvisTVBinders :: Type -> ([InvisTVBinder], Type)
splitForAllInvisTVBinders Type
ty = (ArgFlag -> Maybe Specificity) -> Type -> ([InvisTVBinder], Type)
forall af.
(ArgFlag -> Maybe af) -> Type -> ([VarBndr TyVar af], Type)
splitSomeForAllTyCoVarBndrs ArgFlag -> Maybe Specificity
argf_pred Type
ty
where
argf_pred :: ArgFlag -> Maybe Specificity
argf_pred :: ArgFlag -> Maybe Specificity
argf_pred ArgFlag
Required = Maybe Specificity
forall a. Maybe a
Nothing
argf_pred (Invisible Specificity
spec) = Specificity -> Maybe Specificity
forall a. a -> Maybe a
Just Specificity
spec
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 ArgFlag
_) 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)
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 ArgFlag
_) 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 ArgFlag
_) 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 ArgFlag
_ 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 ArgFlag
_) 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 (TyCoVar, Type)
splitForAllTyVar_maybe :: Type -> Maybe (TyVar, Type)
splitForAllTyVar_maybe Type
ty
| ForAllTy (Bndr TyVar
tv ArgFlag
_) 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 (TyCoVar, Type)
splitForAllCoVar_maybe :: Type -> Maybe (TyVar, Type)
splitForAllCoVar_maybe Type
ty
| ForAllTy (Bndr TyVar
tv ArgFlag
_) 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 (TyCoBinder, Type)
splitPiTy_maybe :: Type -> Maybe (TyCoBinder, Type)
splitPiTy_maybe Type
ty = case Type -> Type
coreFullView Type
ty of
ForAllTy VarBndr TyVar ArgFlag
bndr Type
ty -> (TyCoBinder, Type) -> Maybe (TyCoBinder, Type)
forall a. a -> Maybe a
Just (VarBndr TyVar ArgFlag -> TyCoBinder
Named VarBndr TyVar ArgFlag
bndr, Type
ty)
FunTy { ft_af :: Type -> AnonArgFlag
ft_af = AnonArgFlag
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}
-> (TyCoBinder, Type) -> Maybe (TyCoBinder, Type)
forall a. a -> Maybe a
Just (AnonArgFlag -> Scaled Type -> TyCoBinder
Anon AnonArgFlag
af (Type -> Type -> Scaled Type
forall a. Type -> a -> Scaled a
mkScaled Type
w Type
arg), Type
res)
Type
_ -> Maybe (TyCoBinder, Type)
forall a. Maybe a
Nothing
splitPiTy :: Type -> (TyCoBinder, Type)
splitPiTy :: Type -> (TyCoBinder, Type)
splitPiTy Type
ty
| Just (TyCoBinder, Type)
answer <- Type -> Maybe (TyCoBinder, Type)
splitPiTy_maybe Type
ty = (TyCoBinder, Type)
answer
| Bool
otherwise = String -> SDoc -> (TyCoBinder, Type)
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"splitPiTy" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty)
splitPiTys :: Type -> ([TyCoBinder], Type)
splitPiTys :: Type -> ([TyCoBinder], Type)
splitPiTys Type
ty = Type -> Type -> [TyCoBinder] -> ([TyCoBinder], Type)
split Type
ty Type
ty []
where
split :: Type -> Type -> [TyCoBinder] -> ([TyCoBinder], Type)
split Type
_ (ForAllTy VarBndr TyVar ArgFlag
b Type
res) [TyCoBinder]
bs = Type -> Type -> [TyCoBinder] -> ([TyCoBinder], Type)
split Type
res Type
res (VarBndr TyVar ArgFlag -> TyCoBinder
Named VarBndr TyVar ArgFlag
b TyCoBinder -> [TyCoBinder] -> [TyCoBinder]
forall a. a -> [a] -> [a]
: [TyCoBinder]
bs)
split Type
_ (FunTy { ft_af :: Type -> AnonArgFlag
ft_af = AnonArgFlag
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 }) [TyCoBinder]
bs
= Type -> Type -> [TyCoBinder] -> ([TyCoBinder], Type)
split Type
res Type
res (AnonArgFlag -> Scaled Type -> TyCoBinder
Anon AnonArgFlag
af (Type -> Type -> Scaled Type
forall a. Type -> a -> Scaled a
Scaled Type
w Type
arg) TyCoBinder -> [TyCoBinder] -> [TyCoBinder]
forall a. a -> [a] -> [a]
: [TyCoBinder]
bs)
split Type
orig_ty Type
ty [TyCoBinder]
bs | Just Type
ty' <- Type -> Maybe Type
coreView Type
ty = Type -> Type -> [TyCoBinder] -> ([TyCoBinder], Type)
split Type
orig_ty Type
ty' [TyCoBinder]
bs
split Type
orig_ty Type
_ [TyCoBinder]
bs = ([TyCoBinder] -> [TyCoBinder]
forall a. [a] -> [a]
reverse [TyCoBinder]
bs, Type
orig_ty)
getRuntimeArgTys :: Type -> [(Type, AnonArgFlag)]
getRuntimeArgTys :: Type -> [(Type, AnonArgFlag)]
getRuntimeArgTys = Type -> [(Type, AnonArgFlag)]
go
where
go :: Type -> [(Type, AnonArgFlag)]
go :: Type -> [(Type, AnonArgFlag)]
go (ForAllTy VarBndr TyVar ArgFlag
_ Type
res)
= Type -> [(Type, AnonArgFlag)]
go Type
res
go (FunTy { ft_arg :: Type -> Type
ft_arg = Type
arg, ft_res :: Type -> Type
ft_res = Type
res, ft_af :: Type -> AnonArgFlag
ft_af = AnonArgFlag
af })
= (Type
arg, AnonArgFlag
af) (Type, AnonArgFlag)
-> [(Type, AnonArgFlag)] -> [(Type, AnonArgFlag)]
forall a. a -> [a] -> [a]
: Type -> [(Type, AnonArgFlag)]
go Type
res
go Type
ty
| Just Type
ty' <- Type -> Maybe Type
coreView Type
ty
= Type -> [(Type, AnonArgFlag)]
go Type
ty'
| Just (KindCoercion
_,Type
ty') <- Type -> Maybe (KindCoercion, Type)
topNormaliseNewType_maybe Type
ty
= Type -> [(Type, AnonArgFlag)]
go Type
ty'
| Bool
otherwise
= []
splitForAllTyCoVarBinders :: Type -> ([TyCoVarBinder], Type)
splitForAllTyCoVarBinders :: Type -> ([VarBndr TyVar ArgFlag], Type)
splitForAllTyCoVarBinders Type
ty = Type
-> Type
-> [VarBndr TyVar ArgFlag]
-> ([VarBndr TyVar ArgFlag], Type)
split Type
ty Type
ty []
where
split :: Type
-> Type
-> [VarBndr TyVar ArgFlag]
-> ([VarBndr TyVar ArgFlag], Type)
split Type
orig_ty Type
ty [VarBndr TyVar ArgFlag]
bs | Just Type
ty' <- Type -> Maybe Type
coreView Type
ty = Type
-> Type
-> [VarBndr TyVar ArgFlag]
-> ([VarBndr TyVar ArgFlag], Type)
split Type
orig_ty Type
ty' [VarBndr TyVar ArgFlag]
bs
split Type
_ (ForAllTy VarBndr TyVar ArgFlag
b Type
res) [VarBndr TyVar ArgFlag]
bs = Type
-> Type
-> [VarBndr TyVar ArgFlag]
-> ([VarBndr TyVar ArgFlag], Type)
split Type
res Type
res (VarBndr TyVar ArgFlag
bVarBndr TyVar ArgFlag
-> [VarBndr TyVar ArgFlag] -> [VarBndr TyVar ArgFlag]
forall a. a -> [a] -> [a]
:[VarBndr TyVar ArgFlag]
bs)
split Type
orig_ty Type
_ [VarBndr TyVar ArgFlag]
bs = ([VarBndr TyVar ArgFlag] -> [VarBndr TyVar ArgFlag]
forall a. [a] -> [a]
reverse [VarBndr TyVar ArgFlag]
bs, Type
orig_ty)
{-# INLINE splitForAllTyCoVarBinders #-}
invisibleTyBndrCount :: Type -> Int
invisibleTyBndrCount :: Type -> Int
invisibleTyBndrCount Type
ty = [TyCoBinder] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (([TyCoBinder], Type) -> [TyCoBinder]
forall a b. (a, b) -> a
fst (Type -> ([TyCoBinder], Type)
splitInvisPiTys Type
ty))
splitInvisPiTys :: Type -> ([TyCoBinder], Type)
splitInvisPiTys :: Type -> ([TyCoBinder], Type)
splitInvisPiTys Type
ty = Type -> Type -> [TyCoBinder] -> ([TyCoBinder], Type)
split Type
ty Type
ty []
where
split :: Type -> Type -> [TyCoBinder] -> ([TyCoBinder], Type)
split Type
_ (ForAllTy VarBndr TyVar ArgFlag
b Type
res) [TyCoBinder]
bs
| Bndr TyVar
_ ArgFlag
vis <- VarBndr TyVar ArgFlag
b
, ArgFlag -> Bool
isInvisibleArgFlag ArgFlag
vis = Type -> Type -> [TyCoBinder] -> ([TyCoBinder], Type)
split Type
res Type
res (VarBndr TyVar ArgFlag -> TyCoBinder
Named VarBndr TyVar ArgFlag
b TyCoBinder -> [TyCoBinder] -> [TyCoBinder]
forall a. a -> [a] -> [a]
: [TyCoBinder]
bs)
split Type
_ (FunTy { ft_af :: Type -> AnonArgFlag
ft_af = AnonArgFlag
InvisArg, ft_mult :: Type -> Type
ft_mult = Type
mult, ft_arg :: Type -> Type
ft_arg = Type
arg, ft_res :: Type -> Type
ft_res = Type
res }) [TyCoBinder]
bs
= Type -> Type -> [TyCoBinder] -> ([TyCoBinder], Type)
split Type
res Type
res (AnonArgFlag -> Scaled Type -> TyCoBinder
Anon AnonArgFlag
InvisArg (Type -> Type -> Scaled Type
forall a. Type -> a -> Scaled a
mkScaled Type
mult Type
arg) TyCoBinder -> [TyCoBinder] -> [TyCoBinder]
forall a. a -> [a] -> [a]
: [TyCoBinder]
bs)
split Type
orig_ty Type
ty [TyCoBinder]
bs
| Just Type
ty' <- Type -> Maybe Type
coreView Type
ty = Type -> Type -> [TyCoBinder] -> ([TyCoBinder], Type)
split Type
orig_ty Type
ty' [TyCoBinder]
bs
split Type
orig_ty Type
_ [TyCoBinder]
bs = ([TyCoBinder] -> [TyCoBinder]
forall a. [a] -> [a]
reverse [TyCoBinder]
bs, Type
orig_ty)
splitInvisPiTysN :: Int -> Type -> ([TyCoBinder], Type)
splitInvisPiTysN :: Int -> Type -> ([TyCoBinder], Type)
splitInvisPiTysN Int
n Type
ty = Int -> Type -> Type -> [TyCoBinder] -> ([TyCoBinder], Type)
forall {t}.
(Eq t, Num t) =>
t -> Type -> Type -> [TyCoBinder] -> ([TyCoBinder], Type)
split Int
n Type
ty Type
ty []
where
split :: t -> Type -> Type -> [TyCoBinder] -> ([TyCoBinder], Type)
split t
n Type
orig_ty Type
ty [TyCoBinder]
bs
| t
n t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
0 = ([TyCoBinder] -> [TyCoBinder]
forall a. [a] -> [a]
reverse [TyCoBinder]
bs, Type
orig_ty)
| Just Type
ty' <- Type -> Maybe Type
coreView Type
ty = t -> Type -> Type -> [TyCoBinder] -> ([TyCoBinder], Type)
split t
n Type
orig_ty Type
ty' [TyCoBinder]
bs
| ForAllTy VarBndr TyVar ArgFlag
b Type
res <- Type
ty
, Bndr TyVar
_ ArgFlag
vis <- VarBndr TyVar ArgFlag
b
, ArgFlag -> Bool
isInvisibleArgFlag ArgFlag
vis = t -> Type -> Type -> [TyCoBinder] -> ([TyCoBinder], Type)
split (t
nt -> t -> t
forall a. Num a => a -> a -> a
-t
1) Type
res Type
res (VarBndr TyVar ArgFlag -> TyCoBinder
Named VarBndr TyVar ArgFlag
b TyCoBinder -> [TyCoBinder] -> [TyCoBinder]
forall a. a -> [a] -> [a]
: [TyCoBinder]
bs)
| FunTy { ft_af :: Type -> AnonArgFlag
ft_af = AnonArgFlag
InvisArg, 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
= t -> Type -> Type -> [TyCoBinder] -> ([TyCoBinder], Type)
split (t
nt -> t -> t
forall a. Num a => a -> a -> a
-t
1) Type
res Type
res (AnonArgFlag -> Scaled Type -> TyCoBinder
Anon AnonArgFlag
InvisArg (Type -> Type -> Scaled Type
forall a. Type -> a -> Scaled a
Scaled Type
mult Type
arg) TyCoBinder -> [TyCoBinder] -> [TyCoBinder]
forall a. a -> [a] -> [a]
: [TyCoBinder]
bs)
| Bool
otherwise = ([TyCoBinder] -> [TyCoBinder]
forall a. [a] -> [a]
reverse [TyCoBinder]
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 ((ArgFlag -> Bool) -> [ArgFlag] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map (ArgFlag -> ArgFlag -> Bool
forall a. Eq a => a -> a -> Bool
/= ArgFlag
Inferred) ([ArgFlag] -> [Bool]) -> [ArgFlag] -> [Bool]
forall a b. (a -> b) -> a -> b
$ TyCon -> [Type] -> [ArgFlag]
tyConArgFlags 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 ((ArgFlag -> Bool) -> [ArgFlag] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map ArgFlag -> Bool
isInvisibleArgFlag ([ArgFlag] -> [Bool]) -> [ArgFlag] -> [Bool]
forall a b. (a -> b) -> a -> b
$ TyCon -> [Type] -> [ArgFlag]
tyConArgFlags TyCon
tc [Type]
tys) [Type]
tys
partitionInvisibles :: [(a, ArgFlag)] -> ([a], [a])
partitionInvisibles :: forall a. [(a, ArgFlag)] -> ([a], [a])
partitionInvisibles = ((a, ArgFlag) -> Either a a) -> [(a, ArgFlag)] -> ([a], [a])
forall a b c. (a -> Either b c) -> [a] -> ([b], [c])
partitionWith (a, ArgFlag) -> Either a a
forall a. (a, ArgFlag) -> Either a a
pick_invis
where
pick_invis :: (a, ArgFlag) -> Either a a
pick_invis :: forall a. (a, ArgFlag) -> Either a a
pick_invis (a
thing, ArgFlag
vis) | ArgFlag -> Bool
isInvisibleArgFlag ArgFlag
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
tyConArgFlags :: TyCon -> [Type] -> [ArgFlag]
tyConArgFlags :: TyCon -> [Type] -> [ArgFlag]
tyConArgFlags TyCon
tc = Type -> [Type] -> [ArgFlag]
fun_kind_arg_flags (TyCon -> Type
tyConKind TyCon
tc)
appTyArgFlags :: Type -> [Type] -> [ArgFlag]
appTyArgFlags :: Type -> [Type] -> [ArgFlag]
appTyArgFlags Type
ty = Type -> [Type] -> [ArgFlag]
fun_kind_arg_flags ((() :: Constraint) => Type -> Type
Type -> Type
typeKind Type
ty)
fun_kind_arg_flags :: Kind -> [Type] -> [ArgFlag]
fun_kind_arg_flags :: Type -> [Type] -> [ArgFlag]
fun_kind_arg_flags = TCvSubst -> Type -> [Type] -> [ArgFlag]
go TCvSubst
emptyTCvSubst
where
go :: TCvSubst -> Type -> [Type] -> [ArgFlag]
go TCvSubst
subst Type
ki [Type]
arg_tys
| Just Type
ki' <- Type -> Maybe Type
coreView Type
ki = TCvSubst -> Type -> [Type] -> [ArgFlag]
go TCvSubst
subst Type
ki' [Type]
arg_tys
go TCvSubst
_ Type
_ [] = []
go TCvSubst
subst (ForAllTy (Bndr TyVar
tv ArgFlag
argf) Type
res_ki) (Type
arg_ty:[Type]
arg_tys)
= ArgFlag
argf ArgFlag -> [ArgFlag] -> [ArgFlag]
forall a. a -> [a] -> [a]
: TCvSubst -> Type -> [Type] -> [ArgFlag]
go TCvSubst
subst' Type
res_ki [Type]
arg_tys
where
subst' :: TCvSubst
subst' = TCvSubst -> TyVar -> Type -> TCvSubst
extendTvSubst TCvSubst
subst TyVar
tv Type
arg_ty
go TCvSubst
subst (TyVarTy TyVar
tv) [Type]
arg_tys
| Just Type
ki <- TCvSubst -> TyVar -> Maybe Type
lookupTyVar TCvSubst
subst TyVar
tv = TCvSubst -> Type -> [Type] -> [ArgFlag]
go TCvSubst
subst Type
ki [Type]
arg_tys
go TCvSubst
subst (FunTy{ft_af :: Type -> AnonArgFlag
ft_af = AnonArgFlag
af, ft_res :: Type -> Type
ft_res = Type
res_ki}) (Type
_:[Type]
arg_tys)
= ArgFlag
argf ArgFlag -> [ArgFlag] -> [ArgFlag]
forall a. a -> [a] -> [a]
: TCvSubst -> Type -> [Type] -> [ArgFlag]
go TCvSubst
subst Type
res_ki [Type]
arg_tys
where
argf :: ArgFlag
argf = case AnonArgFlag
af of
AnonArgFlag
VisArg -> ArgFlag
Required
AnonArgFlag
InvisArg -> ArgFlag
Inferred
go TCvSubst
_ Type
_ [Type]
arg_tys = (Type -> ArgFlag) -> [Type] -> [ArgFlag]
forall a b. (a -> b) -> [a] -> [b]
map (ArgFlag -> Type -> ArgFlag
forall a b. a -> b -> a
const ArgFlag
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 AnonArgFlag
af Type
w Type
a Type
b) = case AnonArgFlag
af of
AnonArgFlag
InvisArg -> Bool
False
AnonArgFlag
VisArg -> 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
mkAnonBinder :: AnonArgFlag -> Scaled Type -> TyCoBinder
mkAnonBinder :: AnonArgFlag -> Scaled Type -> TyCoBinder
mkAnonBinder = AnonArgFlag -> Scaled Type -> TyCoBinder
Anon
isAnonTyCoBinder :: TyCoBinder -> Bool
isAnonTyCoBinder :: TyCoBinder -> Bool
isAnonTyCoBinder (Named {}) = Bool
False
isAnonTyCoBinder (Anon {}) = Bool
True
tyCoBinderVar_maybe :: TyCoBinder -> Maybe TyCoVar
tyCoBinderVar_maybe :: TyCoBinder -> Maybe TyVar
tyCoBinderVar_maybe (Named VarBndr TyVar ArgFlag
tv) = TyVar -> Maybe TyVar
forall a. a -> Maybe a
Just (TyVar -> Maybe TyVar) -> TyVar -> Maybe TyVar
forall a b. (a -> b) -> a -> b
$ VarBndr TyVar ArgFlag -> TyVar
forall tv argf. VarBndr tv argf -> tv
binderVar VarBndr TyVar ArgFlag
tv
tyCoBinderVar_maybe TyCoBinder
_ = Maybe TyVar
forall a. Maybe a
Nothing
tyCoBinderType :: TyCoBinder -> Type
tyCoBinderType :: TyCoBinder -> Type
tyCoBinderType (Named VarBndr TyVar ArgFlag
tvb) = VarBndr TyVar ArgFlag -> Type
forall argf. VarBndr TyVar argf -> Type
binderType VarBndr TyVar ArgFlag
tvb
tyCoBinderType (Anon AnonArgFlag
_ Scaled Type
ty) = Scaled Type -> Type
forall a. Scaled a -> a
scaledThing Scaled Type
ty
tyBinderType :: TyBinder -> Type
tyBinderType :: TyCoBinder -> Type
tyBinderType (Named (Bndr TyVar
tv ArgFlag
_))
= Bool -> (TyVar -> Type) -> TyVar -> Type
forall a. HasCallStack => Bool -> a -> a
assert (TyVar -> Bool
isTyVar TyVar
tv )
TyVar -> Type
tyVarKind TyVar
tv
tyBinderType (Anon AnonArgFlag
_ Scaled Type
ty) = Scaled Type -> Type
forall a. Scaled a -> a
scaledThing Scaled Type
ty
binderRelevantType_maybe :: TyCoBinder -> Maybe Type
binderRelevantType_maybe :: TyCoBinder -> Maybe Type
binderRelevantType_maybe (Named {}) = Maybe Type
forall a. Maybe a
Nothing
binderRelevantType_maybe (Anon AnonArgFlag
_ Scaled Type
ty) = Type -> Maybe Type
forall a. a -> Maybe a
Just (Scaled Type -> Type
forall a. Scaled a -> a
scaledThing Scaled Type
ty)
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 :: TCvSubst
fam_subst = Bool -> SDoc -> TCvSubst -> TCvSubst
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
<+> [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
tys) (TCvSubst -> TCvSubst) -> TCvSubst -> TCvSubst
forall a b. (a -> b) -> a -> b
$
[TyVar] -> [Type] -> TCvSubst
(() :: Constraint) => [TyVar] -> [Type] -> TCvSubst
zipTvSubst [TyVar]
tvs [Type]
tys
= TyCon -> [Type] -> Type
mkTyConApp TyCon
fam_tc ((() :: Constraint) => TCvSubst -> [Type] -> [Type]
TCvSubst -> [Type] -> [Type]
substTys TCvSubst
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 -> Int -> Type
coAxNthLHS CoAxiom br
ax Int
ind =
TyCon -> [Type] -> Type
mkTyConApp (CoAxiom br -> TyCon
forall (br :: BranchFlag). CoAxiom br -> TyCon
coAxiomTyCon CoAxiom br
ax) (CoAxBranch -> [Type]
coAxBranchLHS (CoAxiom br -> Int -> CoAxBranch
forall (br :: BranchFlag). CoAxiom br -> Int -> CoAxBranch
coAxiomNthBranch CoAxiom br
ax Int
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 AnonArgFlag
_ 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 ArgFlag
_ 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 -> TyCoVarSet -> Bool
`elemVarSet` Type -> TyCoVarSet
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
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr ((() :: Constraint) => Type -> Type
Type -> Type
typeKind Type
ty))
isStateType :: Type -> Bool
isStateType :: Type -> Bool
isStateType Type
ty
= case Type -> Maybe TyCon
tyConAppTyCon_maybe Type
ty of
Just TyCon
tycon -> TyCon
tycon TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
statePrimTyCon
Maybe TyCon
_ -> Bool
False
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 Type
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 -> Type
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
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
<+> 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 (TyCon
tc, [Type
lev]) <- (() :: Constraint) => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
rep
, TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
boxedRepDataConTyCon
= 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
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
<+> 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] -> Int -> Bool
forall a. [a] -> Int -> Bool
`lengthIs` TyCon -> Int
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] -> Int -> Bool
forall a. [a] -> Int -> Bool
`lengthIs` TyCon -> Int
tyConArity TyCon
tc )
TyCon -> Bool
isPrimTyCon TyCon
tc
Maybe (TyCon, [Type])
_ -> Bool
False
isValidJoinPointType :: JoinArity -> Type -> Bool
isValidJoinPointType :: Int -> Type -> Bool
isValidJoinPointType Int
arity Type
ty
= TyCoVarSet -> Int -> Type -> Bool
forall {t}. (Eq t, Num t) => TyCoVarSet -> t -> Type -> Bool
valid_under TyCoVarSet
emptyVarSet Int
arity Type
ty
where
valid_under :: TyCoVarSet -> t -> Type -> Bool
valid_under TyCoVarSet
tvs t
arity Type
ty
| t
arity t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
0
= TyCoVarSet
tvs TyCoVarSet -> TyCoVarSet -> Bool
`disjointVarSet` Type -> TyCoVarSet
tyCoVarsOfType Type
ty
| Just (TyVar
t, Type
ty') <- Type -> Maybe (TyVar, Type)
splitForAllTyCoVar_maybe Type
ty
= TyCoVarSet -> t -> Type -> Bool
valid_under (TyCoVarSet
tvs TyCoVarSet -> TyVar -> TyCoVarSet
`extendVarSet` TyVar
t) (t
arityt -> t -> t
forall a. Num a => a -> a -> a
-t
1) Type
ty'
| Just (Type
_, Type
_, Type
res_ty) <- Type -> Maybe (Type, Type, Type)
splitFunTy_maybe Type
ty
= TyCoVarSet -> t -> Type -> Bool
valid_under TyCoVarSet
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 AnonArgFlag
_ 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 ArgFlag
_) 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
eqType :: Type -> Type -> Bool
eqType :: Type -> Type -> Bool
eqType Type
t1 Type
t2 = Ordering -> Bool
isEqual (Ordering -> Bool) -> Ordering -> Bool
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Ordering
nonDetCmpType Type
t1 Type
t2
eqTypeX :: RnEnv2 -> Type -> Type -> Bool
eqTypeX :: RnEnv2 -> Type -> Type -> Bool
eqTypeX RnEnv2
env Type
t1 Type
t2 = Ordering -> Bool
isEqual (Ordering -> Bool) -> Ordering -> Bool
forall a b. (a -> b) -> a -> b
$ RnEnv2 -> Type -> Type -> Ordering
nonDetCmpTypeX RnEnv2
env Type
t1 Type
t2
eqTypes :: [Type] -> [Type] -> Bool
eqTypes :: [Type] -> [Type] -> Bool
eqTypes [Type]
tys1 [Type]
tys2 = Ordering -> Bool
isEqual (Ordering -> Bool) -> Ordering -> Bool
forall a b. (a -> b) -> a -> b
$ [Type] -> [Type] -> Ordering
nonDetCmpTypes [Type]
tys1 [Type]
tys2
eqVarBndrs :: RnEnv2 -> [Var] -> [Var] -> Maybe RnEnv2
eqVarBndrs :: RnEnv2 -> [TyVar] -> [TyVar] -> Maybe RnEnv2
eqVarBndrs RnEnv2
env [] []
= RnEnv2 -> Maybe RnEnv2
forall a. a -> Maybe a
Just RnEnv2
env
eqVarBndrs RnEnv2
env (TyVar
tv1:[TyVar]
tvs1) (TyVar
tv2:[TyVar]
tvs2)
| RnEnv2 -> Type -> Type -> Bool
eqTypeX RnEnv2
env (TyVar -> Type
varType TyVar
tv1) (TyVar -> Type
varType TyVar
tv2)
= RnEnv2 -> [TyVar] -> [TyVar] -> Maybe RnEnv2
eqVarBndrs (RnEnv2 -> TyVar -> TyVar -> RnEnv2
rnBndr2 RnEnv2
env TyVar
tv1 TyVar
tv2) [TyVar]
tvs1 [TyVar]
tvs2
eqVarBndrs RnEnv2
_ [TyVar]
_ [TyVar]
_= Maybe RnEnv2
forall a. Maybe a
Nothing
nonDetCmpType :: Type -> Type -> Ordering
nonDetCmpType :: Type -> Type -> Ordering
nonDetCmpType (TyConApp TyCon
tc1 []) (TyConApp TyCon
tc2 []) | TyCon
tc1 TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
tc2
= Ordering
EQ
nonDetCmpType Type
t1 Type
t2
= RnEnv2 -> Type -> Type -> Ordering
nonDetCmpTypeX RnEnv2
rn_env Type
t1 Type
t2
where
rn_env :: RnEnv2
rn_env = InScopeSet -> RnEnv2
mkRnEnv2 (TyCoVarSet -> InScopeSet
mkInScopeSet ([Type] -> TyCoVarSet
tyCoVarsOfTypes [Type
t1, Type
t2]))
{-# INLINE nonDetCmpType #-}
nonDetCmpTypes :: [Type] -> [Type] -> Ordering
nonDetCmpTypes :: [Type] -> [Type] -> Ordering
nonDetCmpTypes [Type]
ts1 [Type]
ts2 = RnEnv2 -> [Type] -> [Type] -> Ordering
nonDetCmpTypesX RnEnv2
rn_env [Type]
ts1 [Type]
ts2
where
rn_env :: RnEnv2
rn_env = InScopeSet -> RnEnv2
mkRnEnv2 (TyCoVarSet -> InScopeSet
mkInScopeSet ([Type] -> TyCoVarSet
tyCoVarsOfTypes ([Type]
ts1 [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type]
ts2)))
data TypeOrdering = TLT
| TEQ
| TEQX
| TGT
deriving (TypeOrdering -> TypeOrdering -> Bool
(TypeOrdering -> TypeOrdering -> Bool)
-> (TypeOrdering -> TypeOrdering -> Bool) -> Eq TypeOrdering
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: TypeOrdering -> TypeOrdering -> Bool
== :: TypeOrdering -> TypeOrdering -> Bool
$c/= :: TypeOrdering -> TypeOrdering -> Bool
/= :: TypeOrdering -> TypeOrdering -> Bool
Eq, Eq TypeOrdering
Eq TypeOrdering
-> (TypeOrdering -> TypeOrdering -> Ordering)
-> (TypeOrdering -> TypeOrdering -> Bool)
-> (TypeOrdering -> TypeOrdering -> Bool)
-> (TypeOrdering -> TypeOrdering -> Bool)
-> (TypeOrdering -> TypeOrdering -> Bool)
-> (TypeOrdering -> TypeOrdering -> TypeOrdering)
-> (TypeOrdering -> TypeOrdering -> TypeOrdering)
-> Ord TypeOrdering
TypeOrdering -> TypeOrdering -> Bool
TypeOrdering -> TypeOrdering -> Ordering
TypeOrdering -> TypeOrdering -> TypeOrdering
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: TypeOrdering -> TypeOrdering -> Ordering
compare :: TypeOrdering -> TypeOrdering -> Ordering
$c< :: TypeOrdering -> TypeOrdering -> Bool
< :: TypeOrdering -> TypeOrdering -> Bool
$c<= :: TypeOrdering -> TypeOrdering -> Bool
<= :: TypeOrdering -> TypeOrdering -> Bool
$c> :: TypeOrdering -> TypeOrdering -> Bool
> :: TypeOrdering -> TypeOrdering -> Bool
$c>= :: TypeOrdering -> TypeOrdering -> Bool
>= :: TypeOrdering -> TypeOrdering -> Bool
$cmax :: TypeOrdering -> TypeOrdering -> TypeOrdering
max :: TypeOrdering -> TypeOrdering -> TypeOrdering
$cmin :: TypeOrdering -> TypeOrdering -> TypeOrdering
min :: TypeOrdering -> TypeOrdering -> TypeOrdering
Ord, Int -> TypeOrdering
TypeOrdering -> Int
TypeOrdering -> [TypeOrdering]
TypeOrdering -> TypeOrdering
TypeOrdering -> TypeOrdering -> [TypeOrdering]
TypeOrdering -> TypeOrdering -> TypeOrdering -> [TypeOrdering]
(TypeOrdering -> TypeOrdering)
-> (TypeOrdering -> TypeOrdering)
-> (Int -> TypeOrdering)
-> (TypeOrdering -> Int)
-> (TypeOrdering -> [TypeOrdering])
-> (TypeOrdering -> TypeOrdering -> [TypeOrdering])
-> (TypeOrdering -> TypeOrdering -> [TypeOrdering])
-> (TypeOrdering -> TypeOrdering -> TypeOrdering -> [TypeOrdering])
-> Enum TypeOrdering
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: TypeOrdering -> TypeOrdering
succ :: TypeOrdering -> TypeOrdering
$cpred :: TypeOrdering -> TypeOrdering
pred :: TypeOrdering -> TypeOrdering
$ctoEnum :: Int -> TypeOrdering
toEnum :: Int -> TypeOrdering
$cfromEnum :: TypeOrdering -> Int
fromEnum :: TypeOrdering -> Int
$cenumFrom :: TypeOrdering -> [TypeOrdering]
enumFrom :: TypeOrdering -> [TypeOrdering]
$cenumFromThen :: TypeOrdering -> TypeOrdering -> [TypeOrdering]
enumFromThen :: TypeOrdering -> TypeOrdering -> [TypeOrdering]
$cenumFromTo :: TypeOrdering -> TypeOrdering -> [TypeOrdering]
enumFromTo :: TypeOrdering -> TypeOrdering -> [TypeOrdering]
$cenumFromThenTo :: TypeOrdering -> TypeOrdering -> TypeOrdering -> [TypeOrdering]
enumFromThenTo :: TypeOrdering -> TypeOrdering -> TypeOrdering -> [TypeOrdering]
Enum, TypeOrdering
TypeOrdering -> TypeOrdering -> Bounded TypeOrdering
forall a. a -> a -> Bounded a
$cminBound :: TypeOrdering
minBound :: TypeOrdering
$cmaxBound :: TypeOrdering
maxBound :: TypeOrdering
Bounded)
nonDetCmpTypeX :: RnEnv2 -> Type -> Type -> Ordering
nonDetCmpTypeX :: RnEnv2 -> Type -> Type -> Ordering
nonDetCmpTypeX RnEnv2
env Type
orig_t1 Type
orig_t2 =
case RnEnv2 -> Type -> Type -> TypeOrdering
go RnEnv2
env Type
orig_t1 Type
orig_t2 of
TypeOrdering
TEQX -> TypeOrdering -> Ordering
toOrdering (TypeOrdering -> Ordering) -> TypeOrdering -> Ordering
forall a b. (a -> b) -> a -> b
$ RnEnv2 -> Type -> Type -> TypeOrdering
go RnEnv2
env Type
k1 Type
k2
TypeOrdering
ty_ordering -> TypeOrdering -> Ordering
toOrdering TypeOrdering
ty_ordering
where
k1 :: Type
k1 = (() :: Constraint) => Type -> Type
Type -> Type
typeKind Type
orig_t1
k2 :: Type
k2 = (() :: Constraint) => Type -> Type
Type -> Type
typeKind Type
orig_t2
toOrdering :: TypeOrdering -> Ordering
toOrdering :: TypeOrdering -> Ordering
toOrdering TypeOrdering
TLT = Ordering
LT
toOrdering TypeOrdering
TEQ = Ordering
EQ
toOrdering TypeOrdering
TEQX = Ordering
EQ
toOrdering TypeOrdering
TGT = Ordering
GT
liftOrdering :: Ordering -> TypeOrdering
liftOrdering :: Ordering -> TypeOrdering
liftOrdering Ordering
LT = TypeOrdering
TLT
liftOrdering Ordering
EQ = TypeOrdering
TEQ
liftOrdering Ordering
GT = TypeOrdering
TGT
thenCmpTy :: TypeOrdering -> TypeOrdering -> TypeOrdering
thenCmpTy :: TypeOrdering -> TypeOrdering -> TypeOrdering
thenCmpTy TypeOrdering
TEQ TypeOrdering
rel = TypeOrdering
rel
thenCmpTy TypeOrdering
TEQX TypeOrdering
rel = TypeOrdering -> TypeOrdering
hasCast TypeOrdering
rel
thenCmpTy TypeOrdering
rel TypeOrdering
_ = TypeOrdering
rel
hasCast :: TypeOrdering -> TypeOrdering
hasCast :: TypeOrdering -> TypeOrdering
hasCast TypeOrdering
TEQ = TypeOrdering
TEQX
hasCast TypeOrdering
rel = TypeOrdering
rel
go :: RnEnv2 -> Type -> Type -> TypeOrdering
go :: RnEnv2 -> Type -> Type -> TypeOrdering
go RnEnv2
_ (TyConApp TyCon
tc1 []) (TyConApp TyCon
tc2 [])
| TyCon
tc1 TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
tc2
= TypeOrdering
TEQ
go RnEnv2
env Type
t1 Type
t2
| Just Type
t1' <- Type -> Maybe Type
coreView Type
t1 = RnEnv2 -> Type -> Type -> TypeOrdering
go RnEnv2
env Type
t1' Type
t2
| Just Type
t2' <- Type -> Maybe Type
coreView Type
t2 = RnEnv2 -> Type -> Type -> TypeOrdering
go RnEnv2
env Type
t1 Type
t2'
go RnEnv2
env (TyVarTy TyVar
tv1) (TyVarTy TyVar
tv2)
= Ordering -> TypeOrdering
liftOrdering (Ordering -> TypeOrdering) -> Ordering -> TypeOrdering
forall a b. (a -> b) -> a -> b
$ RnEnv2 -> TyVar -> TyVar
rnOccL RnEnv2
env TyVar
tv1 TyVar -> TyVar -> Ordering
`nonDetCmpVar` RnEnv2 -> TyVar -> TyVar
rnOccR RnEnv2
env TyVar
tv2
go RnEnv2
env (ForAllTy (Bndr TyVar
tv1 ArgFlag
_) Type
t1) (ForAllTy (Bndr TyVar
tv2 ArgFlag
_) Type
t2)
= RnEnv2 -> Type -> Type -> TypeOrdering
go RnEnv2
env (TyVar -> Type
varType TyVar
tv1) (TyVar -> Type
varType TyVar
tv2)
TypeOrdering -> TypeOrdering -> TypeOrdering
`thenCmpTy` RnEnv2 -> Type -> Type -> TypeOrdering
go (RnEnv2 -> TyVar -> TyVar -> RnEnv2
rnBndr2 RnEnv2
env TyVar
tv1 TyVar
tv2) Type
t1 Type
t2
go RnEnv2
env (AppTy Type
s1 Type
t1) Type
ty2
| Just (Type
s2, Type
t2) <- (() :: Constraint) => Type -> Maybe (Type, Type)
Type -> Maybe (Type, Type)
repSplitAppTy_maybe Type
ty2
= RnEnv2 -> Type -> Type -> TypeOrdering
go RnEnv2
env Type
s1 Type
s2 TypeOrdering -> TypeOrdering -> TypeOrdering
`thenCmpTy` RnEnv2 -> Type -> Type -> TypeOrdering
go RnEnv2
env Type
t1 Type
t2
go RnEnv2
env Type
ty1 (AppTy Type
s2 Type
t2)
| Just (Type
s1, Type
t1) <- (() :: Constraint) => Type -> Maybe (Type, Type)
Type -> Maybe (Type, Type)
repSplitAppTy_maybe Type
ty1
= RnEnv2 -> Type -> Type -> TypeOrdering
go RnEnv2
env Type
s1 Type
s2 TypeOrdering -> TypeOrdering -> TypeOrdering
`thenCmpTy` RnEnv2 -> Type -> Type -> TypeOrdering
go RnEnv2
env Type
t1 Type
t2
go RnEnv2
env (FunTy AnonArgFlag
_ Type
w1 Type
s1 Type
t1) (FunTy AnonArgFlag
_ Type
w2 Type
s2 Type
t2)
= Ordering -> TypeOrdering
liftOrdering (RnEnv2 -> Type -> Type -> Ordering
nonDetCmpTypeX RnEnv2
env Type
s1 Type
s2 Ordering -> Ordering -> Ordering
`thenCmp` RnEnv2 -> Type -> Type -> Ordering
nonDetCmpTypeX RnEnv2
env Type
t1 Type
t2)
TypeOrdering -> TypeOrdering -> TypeOrdering
`thenCmpTy` RnEnv2 -> Type -> Type -> TypeOrdering
go RnEnv2
env Type
w1 Type
w2
go RnEnv2
env (TyConApp TyCon
tc1 [Type]
tys1) (TyConApp TyCon
tc2 [Type]
tys2)
= Ordering -> TypeOrdering
liftOrdering (TyCon
tc1 TyCon -> TyCon -> Ordering
`nonDetCmpTc` TyCon
tc2) TypeOrdering -> TypeOrdering -> TypeOrdering
`thenCmpTy` RnEnv2 -> [Type] -> [Type] -> TypeOrdering
gos RnEnv2
env [Type]
tys1 [Type]
tys2
go RnEnv2
_ (LitTy TyLit
l1) (LitTy TyLit
l2) = Ordering -> TypeOrdering
liftOrdering (TyLit -> TyLit -> Ordering
nonDetCmpTyLit TyLit
l1 TyLit
l2)
go RnEnv2
env (CastTy Type
t1 KindCoercion
_) Type
t2 = TypeOrdering -> TypeOrdering
hasCast (TypeOrdering -> TypeOrdering) -> TypeOrdering -> TypeOrdering
forall a b. (a -> b) -> a -> b
$ RnEnv2 -> Type -> Type -> TypeOrdering
go RnEnv2
env Type
t1 Type
t2
go RnEnv2
env Type
t1 (CastTy Type
t2 KindCoercion
_) = TypeOrdering -> TypeOrdering
hasCast (TypeOrdering -> TypeOrdering) -> TypeOrdering -> TypeOrdering
forall a b. (a -> b) -> a -> b
$ RnEnv2 -> Type -> Type -> TypeOrdering
go RnEnv2
env Type
t1 Type
t2
go RnEnv2
_ (CoercionTy {}) (CoercionTy {}) = TypeOrdering
TEQ
go RnEnv2
_ Type
ty1 Type
ty2
= Ordering -> TypeOrdering
liftOrdering (Ordering -> TypeOrdering) -> Ordering -> TypeOrdering
forall a b. (a -> b) -> a -> b
$ (Type -> Int
get_rank Type
ty1) Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` (Type -> Int
get_rank Type
ty2)
where get_rank :: Type -> Int
get_rank :: Type -> Int
get_rank (CastTy {})
= String -> SDoc -> Int
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"nonDetCmpTypeX.get_rank" ([Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type
ty1,Type
ty2])
get_rank (TyVarTy {}) = Int
0
get_rank (CoercionTy {}) = Int
1
get_rank (AppTy {}) = Int
3
get_rank (LitTy {}) = Int
4
get_rank (TyConApp {}) = Int
5
get_rank (FunTy {}) = Int
6
get_rank (ForAllTy {}) = Int
7
gos :: RnEnv2 -> [Type] -> [Type] -> TypeOrdering
gos :: RnEnv2 -> [Type] -> [Type] -> TypeOrdering
gos RnEnv2
_ [] [] = TypeOrdering
TEQ
gos RnEnv2
_ [] [Type]
_ = TypeOrdering
TLT
gos RnEnv2
_ [Type]
_ [] = TypeOrdering
TGT
gos RnEnv2
env (Type
ty1:[Type]
tys1) (Type
ty2:[Type]
tys2) = RnEnv2 -> Type -> Type -> TypeOrdering
go RnEnv2
env Type
ty1 Type
ty2 TypeOrdering -> TypeOrdering -> TypeOrdering
`thenCmpTy` RnEnv2 -> [Type] -> [Type] -> TypeOrdering
gos RnEnv2
env [Type]
tys1 [Type]
tys2
nonDetCmpTypesX :: RnEnv2 -> [Type] -> [Type] -> Ordering
nonDetCmpTypesX :: RnEnv2 -> [Type] -> [Type] -> Ordering
nonDetCmpTypesX RnEnv2
_ [] [] = Ordering
EQ
nonDetCmpTypesX RnEnv2
env (Type
t1:[Type]
tys1) (Type
t2:[Type]
tys2) = RnEnv2 -> Type -> Type -> Ordering
nonDetCmpTypeX RnEnv2
env Type
t1 Type
t2
Ordering -> Ordering -> Ordering
`thenCmp`
RnEnv2 -> [Type] -> [Type] -> Ordering
nonDetCmpTypesX RnEnv2
env [Type]
tys1 [Type]
tys2
nonDetCmpTypesX RnEnv2
_ [] [Type]
_ = Ordering
LT
nonDetCmpTypesX RnEnv2
_ [Type]
_ [] = Ordering
GT
nonDetCmpTc :: TyCon -> TyCon -> Ordering
nonDetCmpTc :: TyCon -> TyCon -> Ordering
nonDetCmpTc TyCon
tc1 TyCon
tc2
= Bool -> Ordering -> Ordering
forall a. HasCallStack => Bool -> a -> a
assert (Bool -> Bool
not (TyCon -> Bool
isConstraintKindCon TyCon
tc1) Bool -> Bool -> Bool
&& Bool -> Bool
not (TyCon -> Bool
isConstraintKindCon TyCon
tc2)) (Ordering -> Ordering) -> Ordering -> Ordering
forall a b. (a -> b) -> a -> b
$
Unique
u1 Unique -> Unique -> Ordering
`nonDetCmpUnique` Unique
u2
where
u1 :: Unique
u1 = TyCon -> Unique
tyConUnique TyCon
tc1
u2 :: Unique
u2 = TyCon -> Unique
tyConUnique TyCon
tc2
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 {}) = Type
liftedTypeKind
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
Just Type
k' -> Type
k'
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
$$ [TyVar] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [TyVar]
tvs SDoc -> SDoc -> SDoc
$$ Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
body SDoc -> SDoc -> SDoc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
body_kind)
where
([TyVar]
tvs, Type
body) = Type -> ([TyVar], Type)
splitForAllTyVars Type
ty
body_kind :: Type
body_kind = (() :: Constraint) => Type -> Type
Type -> Type
typeKind Type
body
tcTypeKind :: HasDebugCallStack => Type -> Kind
tcTypeKind :: (() :: Constraint) => Type -> Type
tcTypeKind (TyConApp TyCon
tc [Type]
tys) = (() :: Constraint) => Type -> [Type] -> Type
Type -> [Type] -> Type
piResultTys (TyCon -> Type
tyConKind TyCon
tc) [Type]
tys
tcTypeKind (LitTy TyLit
l) = TyLit -> Type
typeLiteralKind TyLit
l
tcTypeKind (TyVarTy TyVar
tyvar) = TyVar -> Type
tyVarKind TyVar
tyvar
tcTypeKind (CastTy Type
_ty KindCoercion
co) = KindCoercion -> Type
coercionRKind KindCoercion
co
tcTypeKind (CoercionTy KindCoercion
co) = KindCoercion -> Type
coercionType KindCoercion
co
tcTypeKind (FunTy { ft_af :: Type -> AnonArgFlag
ft_af = AnonArgFlag
af, ft_res :: Type -> Type
ft_res = Type
res })
| AnonArgFlag
InvisArg <- AnonArgFlag
af
, Type -> Bool
tcIsConstraintKind ((() :: Constraint) => Type -> Type
Type -> Type
tcTypeKind Type
res)
= Type
constraintKind
| Bool
otherwise
= Type
liftedTypeKind
tcTypeKind (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
tcTypeKind Type
fun) [Type]
args
tcTypeKind ty :: Type
ty@(ForAllTy {})
| Type -> Bool
tcIsConstraintKind Type
body_kind
= Type
constraintKind
| Bool
otherwise
= case [TyVar] -> Type -> Maybe Type
occCheckExpand [TyVar]
tvs Type
body_kind of
Just Type
k' -> Type
k'
Maybe Type
Nothing -> String -> SDoc -> Type
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"tcTypeKind"
(Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty SDoc -> SDoc -> SDoc
$$ [TyVar] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [TyVar]
tvs SDoc -> SDoc -> SDoc
$$ Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
body SDoc -> SDoc -> SDoc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
body_kind)
where
([TyVar]
tvs, Type
body) = Type -> ([TyVar], Type)
splitForAllTyVars Type
ty
body_kind :: Type
body_kind = (() :: Constraint) => Type -> Type
Type -> Type
tcTypeKind Type
body
isPredTy :: HasDebugCallStack => Type -> Bool
isPredTy :: (() :: Constraint) => Type -> Bool
isPredTy Type
ty = Type -> Bool
tcIsConstraintKind ((() :: Constraint) => Type -> Type
Type -> Type
tcTypeKind Type
ty)
tcIsConstraintKind :: Kind -> Bool
tcIsConstraintKind :: Type -> Bool
tcIsConstraintKind Type
ty
| Just (TyCon
tc, [Type]
args) <- HasCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
tcSplitTyConApp_maybe Type
ty
, TyCon -> Bool
isConstraintKindCon TyCon
tc
= Bool -> SDoc -> Bool -> Bool
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr ([Type] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
args) (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty) Bool
True
| Bool
otherwise
= Bool
False
tcKindRep_maybe :: HasDebugCallStack => Kind -> Maybe Type
tcKindRep_maybe :: (() :: Constraint) => Type -> Maybe Type
tcKindRep_maybe Type
kind
| Just (TyCon
tc, [Type
arg]) <- HasCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
tcSplitTyConApp_maybe Type
kind
, TyCon
tc TyCon -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
tYPETyConKey = Type -> Maybe Type
forall a. a -> Maybe a
Just Type
arg
| Bool
otherwise = Maybe Type
forall a. Maybe a
Nothing
tcIsLiftedTypeKind :: Kind -> Bool
tcIsLiftedTypeKind :: Type -> Bool
tcIsLiftedTypeKind Type
kind
= case (() :: Constraint) => Type -> Maybe Type
Type -> Maybe Type
tcKindRep_maybe Type
kind of
Just Type
rep -> Type -> Bool
isLiftedRuntimeRep Type
rep
Maybe Type
Nothing -> Bool
False
tcIsBoxedTypeKind :: Kind -> Bool
tcIsBoxedTypeKind :: Type -> Bool
tcIsBoxedTypeKind Type
kind
= case (() :: Constraint) => Type -> Maybe Type
Type -> Maybe Type
tcKindRep_maybe Type
kind of
Just Type
rep -> Type -> Bool
isBoxedRuntimeRep Type
rep
Maybe Type
Nothing -> Bool
False
tcIsRuntimeTypeKind :: Kind -> Bool
tcIsRuntimeTypeKind :: Type -> Bool
tcIsRuntimeTypeKind Type
kind = Maybe Type -> Bool
forall a. Maybe a -> Bool
isJust ((() :: Constraint) => Type -> Maybe Type
Type -> Maybe Type
tcKindRep_maybe Type
kind)
tcReturnsConstraintKind :: Kind -> Bool
tcReturnsConstraintKind :: Type -> Bool
tcReturnsConstraintKind Type
kind
| Just Type
kind' <- Type -> Maybe Type
tcView Type
kind = Type -> Bool
tcReturnsConstraintKind Type
kind'
tcReturnsConstraintKind (ForAllTy VarBndr TyVar ArgFlag
_ Type
ty) = Type -> Bool
tcReturnsConstraintKind Type
ty
tcReturnsConstraintKind (FunTy { ft_res :: Type -> Type
ft_res = Type
ty }) = Type -> Bool
tcReturnsConstraintKind Type
ty
tcReturnsConstraintKind (TyConApp TyCon
tc [Type]
_) = TyCon -> Bool
isConstraintKindCon TyCon
tc
tcReturnsConstraintKind Type
_ = Bool
False
typeLiteralKind :: TyLit -> Kind
typeLiteralKind :: TyLit -> Type
typeLiteralKind (NumTyLit {}) = Type
naturalTy
typeLiteralKind (StrTyLit {}) = Type
typeSymbolKind
typeLiteralKind (CharTyLit {}) = Type
charTy
typeHasFixedRuntimeRep :: Type -> Bool
typeHasFixedRuntimeRep :: 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 ArgFlag
_ Type
ty) = Type -> Bool
go Type
ty
go Type
ty = (() :: Constraint) => Type -> Bool
Type -> Bool
isFixedRuntimeRepKind ((() :: Constraint) => Type -> Type
Type -> Type
typeKind Type
ty)
resultHasFixedRuntimeRep :: Type -> Bool
resultHasFixedRuntimeRep :: Type -> Bool
resultHasFixedRuntimeRep = Type -> Bool
typeHasFixedRuntimeRep (Type -> Bool) -> (Type -> Type) -> Type -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([TyCoBinder], Type) -> Type
forall a b. (a, b) -> b
snd (([TyCoBinder], Type) -> Type)
-> (Type -> ([TyCoBinder], Type)) -> Type -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> ([TyCoBinder], Type)
splitPiTys
occCheckExpand :: [Var] -> Type -> Maybe Type
occCheckExpand :: [TyVar] -> Type -> Maybe Type
occCheckExpand [TyVar]
vs_to_avoid Type
ty
| [TyVar] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TyVar]
vs_to_avoid
= Type -> Maybe Type
forall a. a -> Maybe a
Just Type
ty
| Bool
otherwise
= (TyCoVarSet, VarEnv TyVar) -> Type -> Maybe Type
go ([TyVar] -> TyCoVarSet
mkVarSet [TyVar]
vs_to_avoid, VarEnv TyVar
forall a. VarEnv a
emptyVarEnv) Type
ty
where
go :: (VarSet, VarEnv TyCoVar) -> Type -> Maybe Type
go :: (TyCoVarSet, VarEnv TyVar) -> Type -> Maybe Type
go (TyCoVarSet
as, VarEnv TyVar
env) ty :: Type
ty@(TyVarTy TyVar
tv)
| Just TyVar
tv' <- VarEnv TyVar -> TyVar -> Maybe TyVar
forall a. VarEnv a -> TyVar -> Maybe a
lookupVarEnv VarEnv TyVar
env TyVar
tv = Type -> Maybe Type
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (TyVar -> Type
mkTyVarTy TyVar
tv')
| TyCoVarSet -> TyVar -> Bool
bad_var_occ TyCoVarSet
as TyVar
tv = Maybe Type
forall a. Maybe a
Nothing
| Bool
otherwise = Type -> Maybe Type
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return Type
ty
go (TyCoVarSet, VarEnv TyVar)
_ ty :: Type
ty@(LitTy {}) = Type -> Maybe Type
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return Type
ty
go (TyCoVarSet, VarEnv TyVar)
cxt (AppTy Type
ty1 Type
ty2) = do { Type
ty1' <- (TyCoVarSet, VarEnv TyVar) -> Type -> Maybe Type
go (TyCoVarSet, VarEnv TyVar)
cxt Type
ty1
; Type
ty2' <- (TyCoVarSet, VarEnv TyVar) -> Type -> Maybe Type
go (TyCoVarSet, VarEnv TyVar)
cxt Type
ty2
; Type -> Maybe Type
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Type -> Type
mkAppTy Type
ty1' Type
ty2') }
go (TyCoVarSet, VarEnv TyVar)
cxt ty :: Type
ty@(FunTy AnonArgFlag
_ Type
w Type
ty1 Type
ty2)
= do { Type
w' <- (TyCoVarSet, VarEnv TyVar) -> Type -> Maybe Type
go (TyCoVarSet, VarEnv TyVar)
cxt Type
w
; Type
ty1' <- (TyCoVarSet, VarEnv TyVar) -> Type -> Maybe Type
go (TyCoVarSet, VarEnv TyVar)
cxt Type
ty1
; Type
ty2' <- (TyCoVarSet, VarEnv TyVar) -> Type -> Maybe Type
go (TyCoVarSet, VarEnv TyVar)
cxt Type
ty2
; Type -> Maybe Type
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
ty { ft_mult :: Type
ft_mult = Type
w', ft_arg :: Type
ft_arg = Type
ty1', ft_res :: Type
ft_res = Type
ty2' }) }
go cxt :: (TyCoVarSet, VarEnv TyVar)
cxt@(TyCoVarSet
as, VarEnv TyVar
env) (ForAllTy (Bndr TyVar
tv ArgFlag
vis) Type
body_ty)
= do { Type
ki' <- (TyCoVarSet, VarEnv TyVar) -> Type -> Maybe Type
go (TyCoVarSet, VarEnv TyVar)
cxt (TyVar -> Type
varType TyVar
tv)
; let tv' :: TyVar
tv' = TyVar -> Type -> TyVar
setVarType TyVar
tv Type
ki'
env' :: VarEnv TyVar
env' = VarEnv TyVar -> TyVar -> TyVar -> VarEnv TyVar
forall a. VarEnv a -> TyVar -> a -> VarEnv a
extendVarEnv VarEnv TyVar
env TyVar
tv TyVar
tv'
as' :: TyCoVarSet
as' = TyCoVarSet
as TyCoVarSet -> TyVar -> TyCoVarSet
`delVarSet` TyVar
tv
; Type
body' <- (TyCoVarSet, VarEnv TyVar) -> Type -> Maybe Type
go (TyCoVarSet
as', VarEnv TyVar
env') Type
body_ty
; Type -> Maybe Type
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (VarBndr TyVar ArgFlag -> Type -> Type
ForAllTy (TyVar -> ArgFlag -> VarBndr TyVar ArgFlag
forall var argf. var -> argf -> VarBndr var argf
Bndr TyVar
tv' ArgFlag
vis) Type
body') }
go (TyCoVarSet, VarEnv TyVar)
cxt ty :: Type
ty@(TyConApp TyCon
tc [Type]
tys)
= case (Type -> Maybe Type) -> [Type] -> Maybe [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((TyCoVarSet, VarEnv TyVar) -> Type -> Maybe Type
go (TyCoVarSet, VarEnv TyVar)
cxt) [Type]
tys of
Just [Type]
tys' -> Type -> Maybe Type
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (TyCon -> [Type] -> Type
mkTyConApp TyCon
tc [Type]
tys')
Maybe [Type]
Nothing | Just Type
ty' <- Type -> Maybe Type
tcView Type
ty -> (TyCoVarSet, VarEnv TyVar) -> Type -> Maybe Type
go (TyCoVarSet, VarEnv TyVar)
cxt Type
ty'
| Bool
otherwise -> Maybe Type
forall a. Maybe a
Nothing
go (TyCoVarSet, VarEnv TyVar)
cxt (CastTy Type
ty KindCoercion
co) = do { Type
ty' <- (TyCoVarSet, VarEnv TyVar) -> Type -> Maybe Type
go (TyCoVarSet, VarEnv TyVar)
cxt Type
ty
; KindCoercion
co' <- (TyCoVarSet, VarEnv TyVar) -> KindCoercion -> Maybe KindCoercion
go_co (TyCoVarSet, VarEnv TyVar)
cxt KindCoercion
co
; Type -> Maybe Type
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> KindCoercion -> Type
mkCastTy Type
ty' KindCoercion
co') }
go (TyCoVarSet, VarEnv TyVar)
cxt (CoercionTy KindCoercion
co) = do { KindCoercion
co' <- (TyCoVarSet, VarEnv TyVar) -> KindCoercion -> Maybe KindCoercion
go_co (TyCoVarSet, VarEnv TyVar)
cxt KindCoercion
co
; Type -> Maybe Type
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (KindCoercion -> Type
mkCoercionTy KindCoercion
co') }
bad_var_occ :: VarSet -> Var -> Bool
bad_var_occ :: TyCoVarSet -> TyVar -> Bool
bad_var_occ TyCoVarSet
vs_to_avoid TyVar
v
= TyVar
v TyVar -> TyCoVarSet -> Bool
`elemVarSet` TyCoVarSet
vs_to_avoid
Bool -> Bool -> Bool
|| Type -> TyCoVarSet
tyCoVarsOfType (TyVar -> Type
varType TyVar
v) TyCoVarSet -> TyCoVarSet -> Bool
`intersectsVarSet` TyCoVarSet
vs_to_avoid
go_mco :: (TyCoVarSet, VarEnv TyVar) -> MCoercionN -> Maybe MCoercionN
go_mco (TyCoVarSet, VarEnv TyVar)
_ MCoercionN
MRefl = MCoercionN -> Maybe MCoercionN
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return MCoercionN
MRefl
go_mco (TyCoVarSet, VarEnv TyVar)
ctx (MCo KindCoercion
co) = KindCoercion -> MCoercionN
MCo (KindCoercion -> MCoercionN)
-> Maybe KindCoercion -> Maybe MCoercionN
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TyCoVarSet, VarEnv TyVar) -> KindCoercion -> Maybe KindCoercion
go_co (TyCoVarSet, VarEnv TyVar)
ctx KindCoercion
co
go_co :: (TyCoVarSet, VarEnv TyVar) -> KindCoercion -> Maybe KindCoercion
go_co (TyCoVarSet, VarEnv TyVar)
cxt (Refl Type
ty) = do { Type
ty' <- (TyCoVarSet, VarEnv TyVar) -> Type -> Maybe Type
go (TyCoVarSet, VarEnv TyVar)
cxt Type
ty
; KindCoercion -> Maybe KindCoercion
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> KindCoercion
mkNomReflCo Type
ty') }
go_co (TyCoVarSet, VarEnv TyVar)
cxt (GRefl Role
r Type
ty MCoercionN
mco) = do { MCoercionN
mco' <- (TyCoVarSet, VarEnv TyVar) -> MCoercionN -> Maybe MCoercionN
go_mco (TyCoVarSet, VarEnv TyVar)
cxt MCoercionN
mco
; Type
ty' <- (TyCoVarSet, VarEnv TyVar) -> Type -> Maybe Type
go (TyCoVarSet, VarEnv TyVar)
cxt Type
ty
; KindCoercion -> Maybe KindCoercion
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Role -> Type -> MCoercionN -> KindCoercion
mkGReflCo Role
r Type
ty' MCoercionN
mco') }
go_co (TyCoVarSet, VarEnv TyVar)
cxt (TyConAppCo Role
r TyCon
tc [KindCoercion]
args) = do { [KindCoercion]
args' <- (KindCoercion -> Maybe KindCoercion)
-> [KindCoercion] -> Maybe [KindCoercion]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((TyCoVarSet, VarEnv TyVar) -> KindCoercion -> Maybe KindCoercion
go_co (TyCoVarSet, VarEnv TyVar)
cxt) [KindCoercion]
args
; KindCoercion -> Maybe KindCoercion
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return ((() :: Constraint) =>
Role -> TyCon -> [KindCoercion] -> KindCoercion
Role -> TyCon -> [KindCoercion] -> KindCoercion
mkTyConAppCo Role
r TyCon
tc [KindCoercion]
args') }
go_co (TyCoVarSet, VarEnv TyVar)
cxt (AppCo KindCoercion
co KindCoercion
arg) = do { KindCoercion
co' <- (TyCoVarSet, VarEnv TyVar) -> KindCoercion -> Maybe KindCoercion
go_co (TyCoVarSet, VarEnv TyVar)
cxt KindCoercion
co
; KindCoercion
arg' <- (TyCoVarSet, VarEnv TyVar) -> KindCoercion -> Maybe KindCoercion
go_co (TyCoVarSet, VarEnv TyVar)
cxt KindCoercion
arg
; KindCoercion -> Maybe KindCoercion
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (KindCoercion -> KindCoercion -> KindCoercion
mkAppCo KindCoercion
co' KindCoercion
arg') }
go_co cxt :: (TyCoVarSet, VarEnv TyVar)
cxt@(TyCoVarSet
as, VarEnv TyVar
env) (ForAllCo TyVar
tv KindCoercion
kind_co KindCoercion
body_co)
= do { KindCoercion
kind_co' <- (TyCoVarSet, VarEnv TyVar) -> KindCoercion -> Maybe KindCoercion
go_co (TyCoVarSet, VarEnv TyVar)
cxt KindCoercion
kind_co
; let tv' :: TyVar
tv' = TyVar -> Type -> TyVar
setVarType TyVar
tv (Type -> TyVar) -> Type -> TyVar
forall a b. (a -> b) -> a -> b
$
KindCoercion -> Type
coercionLKind KindCoercion
kind_co'
env' :: VarEnv TyVar
env' = VarEnv TyVar -> TyVar -> TyVar -> VarEnv TyVar
forall a. VarEnv a -> TyVar -> a -> VarEnv a
extendVarEnv VarEnv TyVar
env TyVar
tv TyVar
tv'
as' :: TyCoVarSet
as' = TyCoVarSet
as TyCoVarSet -> TyVar -> TyCoVarSet
`delVarSet` TyVar
tv
; KindCoercion
body' <- (TyCoVarSet, VarEnv TyVar) -> KindCoercion -> Maybe KindCoercion
go_co (TyCoVarSet
as', VarEnv TyVar
env') KindCoercion
body_co
; KindCoercion -> Maybe KindCoercion
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (TyVar -> KindCoercion -> KindCoercion -> KindCoercion
ForAllCo TyVar
tv' KindCoercion
kind_co' KindCoercion
body') }
go_co (TyCoVarSet, VarEnv TyVar)
cxt (FunCo Role
r KindCoercion
w KindCoercion
co1 KindCoercion
co2) = do { KindCoercion
co1' <- (TyCoVarSet, VarEnv TyVar) -> KindCoercion -> Maybe KindCoercion
go_co (TyCoVarSet, VarEnv TyVar)
cxt KindCoercion
co1
; KindCoercion
co2' <- (TyCoVarSet, VarEnv TyVar) -> KindCoercion -> Maybe KindCoercion
go_co (TyCoVarSet, VarEnv TyVar)
cxt KindCoercion
co2
; KindCoercion
w' <- (TyCoVarSet, VarEnv TyVar) -> KindCoercion -> Maybe KindCoercion
go_co (TyCoVarSet, VarEnv TyVar)
cxt KindCoercion
w
; KindCoercion -> Maybe KindCoercion
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Role
-> KindCoercion -> KindCoercion -> KindCoercion -> KindCoercion
mkFunCo Role
r KindCoercion
w' KindCoercion
co1' KindCoercion
co2') }
go_co (TyCoVarSet
as,VarEnv TyVar
env) co :: KindCoercion
co@(CoVarCo TyVar
c)
| Just TyVar
c' <- VarEnv TyVar -> TyVar -> Maybe TyVar
forall a. VarEnv a -> TyVar -> Maybe a
lookupVarEnv VarEnv TyVar
env TyVar
c = KindCoercion -> Maybe KindCoercion
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (TyVar -> KindCoercion
mkCoVarCo TyVar
c')
| TyCoVarSet -> TyVar -> Bool
bad_var_occ TyCoVarSet
as TyVar
c = Maybe KindCoercion
forall a. Maybe a
Nothing
| Bool
otherwise = KindCoercion -> Maybe KindCoercion
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return KindCoercion
co
go_co (TyCoVarSet
as,VarEnv TyVar
_) co :: KindCoercion
co@(HoleCo CoercionHole
h)
| TyCoVarSet -> TyVar -> Bool
bad_var_occ TyCoVarSet
as (CoercionHole -> TyVar
ch_co_var CoercionHole
h) = Maybe KindCoercion
forall a. Maybe a
Nothing
| Bool
otherwise = KindCoercion -> Maybe KindCoercion
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return KindCoercion
co
go_co (TyCoVarSet, VarEnv TyVar)
cxt (AxiomInstCo CoAxiom Branched
ax Int
ind [KindCoercion]
args) = do { [KindCoercion]
args' <- (KindCoercion -> Maybe KindCoercion)
-> [KindCoercion] -> Maybe [KindCoercion]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((TyCoVarSet, VarEnv TyVar) -> KindCoercion -> Maybe KindCoercion
go_co (TyCoVarSet, VarEnv TyVar)
cxt) [KindCoercion]
args
; KindCoercion -> Maybe KindCoercion
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (CoAxiom Branched -> Int -> [KindCoercion] -> KindCoercion
mkAxiomInstCo CoAxiom Branched
ax Int
ind [KindCoercion]
args') }
go_co (TyCoVarSet, VarEnv TyVar)
cxt (UnivCo UnivCoProvenance
p Role
r Type
ty1 Type
ty2) = do { UnivCoProvenance
p' <- (TyCoVarSet, VarEnv TyVar)
-> UnivCoProvenance -> Maybe UnivCoProvenance
go_prov (TyCoVarSet, VarEnv TyVar)
cxt UnivCoProvenance
p
; Type
ty1' <- (TyCoVarSet, VarEnv TyVar) -> Type -> Maybe Type
go (TyCoVarSet, VarEnv TyVar)
cxt Type
ty1
; Type
ty2' <- (TyCoVarSet, VarEnv TyVar) -> Type -> Maybe Type
go (TyCoVarSet, VarEnv TyVar)
cxt Type
ty2
; KindCoercion -> Maybe KindCoercion
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnivCoProvenance -> Role -> Type -> Type -> KindCoercion
mkUnivCo UnivCoProvenance
p' Role
r Type
ty1' Type
ty2') }
go_co (TyCoVarSet, VarEnv TyVar)
cxt (SymCo KindCoercion
co) = do { KindCoercion
co' <- (TyCoVarSet, VarEnv TyVar) -> KindCoercion -> Maybe KindCoercion
go_co (TyCoVarSet, VarEnv TyVar)
cxt KindCoercion
co
; KindCoercion -> Maybe KindCoercion
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (KindCoercion -> KindCoercion
mkSymCo KindCoercion
co') }
go_co (TyCoVarSet, VarEnv TyVar)
cxt (TransCo KindCoercion
co1 KindCoercion
co2) = do { KindCoercion
co1' <- (TyCoVarSet, VarEnv TyVar) -> KindCoercion -> Maybe KindCoercion
go_co (TyCoVarSet, VarEnv TyVar)
cxt KindCoercion
co1
; KindCoercion
co2' <- (TyCoVarSet, VarEnv TyVar) -> KindCoercion -> Maybe KindCoercion
go_co (TyCoVarSet, VarEnv TyVar)
cxt KindCoercion
co2
; KindCoercion -> Maybe KindCoercion
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (KindCoercion -> KindCoercion -> KindCoercion
mkTransCo KindCoercion
co1' KindCoercion
co2') }
go_co (TyCoVarSet, VarEnv TyVar)
cxt (NthCo Role
r Int
n KindCoercion
co) = do { KindCoercion
co' <- (TyCoVarSet, VarEnv TyVar) -> KindCoercion -> Maybe KindCoercion
go_co (TyCoVarSet, VarEnv TyVar)
cxt KindCoercion
co
; KindCoercion -> Maybe KindCoercion
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return ((() :: Constraint) => Role -> Int -> KindCoercion -> KindCoercion
Role -> Int -> KindCoercion -> KindCoercion
mkNthCo Role
r Int
n KindCoercion
co') }
go_co (TyCoVarSet, VarEnv TyVar)
cxt (LRCo LeftOrRight
lr KindCoercion
co) = do { KindCoercion
co' <- (TyCoVarSet, VarEnv TyVar) -> KindCoercion -> Maybe KindCoercion
go_co (TyCoVarSet, VarEnv TyVar)
cxt KindCoercion
co
; KindCoercion -> Maybe KindCoercion
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (LeftOrRight -> KindCoercion -> KindCoercion
mkLRCo LeftOrRight
lr KindCoercion
co') }
go_co (TyCoVarSet, VarEnv TyVar)
cxt (InstCo KindCoercion
co KindCoercion
arg) = do { KindCoercion
co' <- (TyCoVarSet, VarEnv TyVar) -> KindCoercion -> Maybe KindCoercion
go_co (TyCoVarSet, VarEnv TyVar)
cxt KindCoercion
co
; KindCoercion
arg' <- (TyCoVarSet, VarEnv TyVar) -> KindCoercion -> Maybe KindCoercion
go_co (TyCoVarSet, VarEnv TyVar)
cxt KindCoercion
arg
; KindCoercion -> Maybe KindCoercion
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (KindCoercion -> KindCoercion -> KindCoercion
mkInstCo KindCoercion
co' KindCoercion
arg') }
go_co (TyCoVarSet, VarEnv TyVar)
cxt (KindCo KindCoercion
co) = do { KindCoercion
co' <- (TyCoVarSet, VarEnv TyVar) -> KindCoercion -> Maybe KindCoercion
go_co (TyCoVarSet, VarEnv TyVar)
cxt KindCoercion
co
; KindCoercion -> Maybe KindCoercion
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (KindCoercion -> KindCoercion
mkKindCo KindCoercion
co') }
go_co (TyCoVarSet, VarEnv TyVar)
cxt (SubCo KindCoercion
co) = do { KindCoercion
co' <- (TyCoVarSet, VarEnv TyVar) -> KindCoercion -> Maybe KindCoercion
go_co (TyCoVarSet, VarEnv TyVar)
cxt KindCoercion
co
; KindCoercion -> Maybe KindCoercion
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return ((() :: Constraint) => KindCoercion -> KindCoercion
KindCoercion -> KindCoercion
mkSubCo KindCoercion
co') }
go_co (TyCoVarSet, VarEnv TyVar)
cxt (AxiomRuleCo CoAxiomRule
ax [KindCoercion]
cs) = do { [KindCoercion]
cs' <- (KindCoercion -> Maybe KindCoercion)
-> [KindCoercion] -> Maybe [KindCoercion]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((TyCoVarSet, VarEnv TyVar) -> KindCoercion -> Maybe KindCoercion
go_co (TyCoVarSet, VarEnv TyVar)
cxt) [KindCoercion]
cs
; KindCoercion -> Maybe KindCoercion
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (CoAxiomRule -> [KindCoercion] -> KindCoercion
mkAxiomRuleCo CoAxiomRule
ax [KindCoercion]
cs') }
go_prov :: (TyCoVarSet, VarEnv TyVar)
-> UnivCoProvenance -> Maybe UnivCoProvenance
go_prov (TyCoVarSet, VarEnv TyVar)
cxt (PhantomProv KindCoercion
co) = KindCoercion -> UnivCoProvenance
PhantomProv (KindCoercion -> UnivCoProvenance)
-> Maybe KindCoercion -> Maybe UnivCoProvenance
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TyCoVarSet, VarEnv TyVar) -> KindCoercion -> Maybe KindCoercion
go_co (TyCoVarSet, VarEnv TyVar)
cxt KindCoercion
co
go_prov (TyCoVarSet, VarEnv TyVar)
cxt (ProofIrrelProv KindCoercion
co) = KindCoercion -> UnivCoProvenance
ProofIrrelProv (KindCoercion -> UnivCoProvenance)
-> Maybe KindCoercion -> Maybe UnivCoProvenance
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TyCoVarSet, VarEnv TyVar) -> KindCoercion -> Maybe KindCoercion
go_co (TyCoVarSet, VarEnv TyVar)
cxt KindCoercion
co
go_prov (TyCoVarSet, VarEnv TyVar)
_ p :: UnivCoProvenance
p@(PluginProv String
_) = UnivCoProvenance -> Maybe UnivCoProvenance
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return UnivCoProvenance
p
go_prov (TyCoVarSet, VarEnv TyVar)
_ p :: UnivCoProvenance
p@(CorePrepProv Bool
_) = UnivCoProvenance -> Maybe UnivCoProvenance
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return UnivCoProvenance
p
tyConsOfType :: Type -> UniqSet TyCon
tyConsOfType :: Type -> UniqSet TyCon
tyConsOfType Type
ty
= Type -> UniqSet TyCon
go Type
ty
where
go :: Type -> UniqSet TyCon
go :: Type -> UniqSet TyCon
go Type
ty | Just Type
ty' <- Type -> Maybe Type
coreView Type
ty = Type -> UniqSet TyCon
go Type
ty'
go (TyVarTy {}) = UniqSet TyCon
forall a. UniqSet a
emptyUniqSet
go (LitTy {}) = UniqSet TyCon
forall a. UniqSet a
emptyUniqSet
go (TyConApp TyCon
tc [Type]
tys) = TyCon -> UniqSet TyCon
forall {a}. Uniquable a => a -> UniqSet a
go_tc TyCon
tc UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
forall a. UniqSet a -> UniqSet a -> UniqSet a
`unionUniqSets` [Type] -> UniqSet TyCon
forall {t :: * -> *}. Foldable t => t Type -> UniqSet TyCon
go_s [Type]
tys
go (AppTy Type
a Type
b) = Type -> UniqSet TyCon
go Type
a UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
forall a. UniqSet a -> UniqSet a -> UniqSet a
`unionUniqSets` Type -> UniqSet TyCon
go Type
b
go (FunTy AnonArgFlag
_ Type
w Type
a Type
b) = Type -> UniqSet TyCon
go Type
w UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
forall a. UniqSet a -> UniqSet a -> UniqSet a
`unionUniqSets`
Type -> UniqSet TyCon
go Type
a UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
forall a. UniqSet a -> UniqSet a -> UniqSet a
`unionUniqSets` Type -> UniqSet TyCon
go Type
b UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
forall a. UniqSet a -> UniqSet a -> UniqSet a
`unionUniqSets` TyCon -> UniqSet TyCon
forall {a}. Uniquable a => a -> UniqSet a
go_tc TyCon
funTyCon
go (ForAllTy (Bndr TyVar
tv ArgFlag
_) Type
ty) = Type -> UniqSet TyCon
go Type
ty UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
forall a. UniqSet a -> UniqSet a -> UniqSet a
`unionUniqSets` Type -> UniqSet TyCon
go (TyVar -> Type
varType TyVar
tv)
go (CastTy Type
ty KindCoercion
co) = Type -> UniqSet TyCon
go Type
ty UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
forall a. UniqSet a -> UniqSet a -> UniqSet a
`unionUniqSets` KindCoercion -> UniqSet TyCon
go_co KindCoercion
co
go (CoercionTy KindCoercion
co) = KindCoercion -> UniqSet TyCon
go_co KindCoercion
co
go_co :: KindCoercion -> UniqSet TyCon
go_co (Refl Type
ty) = Type -> UniqSet TyCon
go Type
ty
go_co (GRefl Role
_ Type
ty MCoercionN
mco) = Type -> UniqSet TyCon
go Type
ty UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
forall a. UniqSet a -> UniqSet a -> UniqSet a
`unionUniqSets` MCoercionN -> UniqSet TyCon
go_mco MCoercionN
mco
go_co (TyConAppCo Role
_ TyCon
tc [KindCoercion]
args) = TyCon -> UniqSet TyCon
forall {a}. Uniquable a => a -> UniqSet a
go_tc TyCon
tc UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
forall a. UniqSet a -> UniqSet a -> UniqSet a
`unionUniqSets` [KindCoercion] -> UniqSet TyCon
go_cos [KindCoercion]
args
go_co (AppCo KindCoercion
co KindCoercion
arg) = KindCoercion -> UniqSet TyCon
go_co KindCoercion
co UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
forall a. UniqSet a -> UniqSet a -> UniqSet a
`unionUniqSets` KindCoercion -> UniqSet TyCon
go_co KindCoercion
arg
go_co (ForAllCo TyVar
_ KindCoercion
kind_co KindCoercion
co) = KindCoercion -> UniqSet TyCon
go_co KindCoercion
kind_co UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
forall a. UniqSet a -> UniqSet a -> UniqSet a
`unionUniqSets` KindCoercion -> UniqSet TyCon
go_co KindCoercion
co
go_co (FunCo Role
_ KindCoercion
co_mult KindCoercion
co1 KindCoercion
co2) = KindCoercion -> UniqSet TyCon
go_co KindCoercion
co_mult UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
forall a. UniqSet a -> UniqSet a -> UniqSet a
`unionUniqSets` KindCoercion -> UniqSet TyCon
go_co KindCoercion
co1 UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
forall a. UniqSet a -> UniqSet a -> UniqSet a
`unionUniqSets` KindCoercion -> UniqSet TyCon
go_co KindCoercion
co2
go_co (AxiomInstCo CoAxiom Branched
ax Int
_ [KindCoercion]
args) = CoAxiom Branched -> UniqSet TyCon
forall {br :: BranchFlag}. CoAxiom br -> UniqSet TyCon
go_ax CoAxiom Branched
ax UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
forall a. UniqSet a -> UniqSet a -> UniqSet a
`unionUniqSets` [KindCoercion] -> UniqSet TyCon
go_cos [KindCoercion]
args
go_co (UnivCo UnivCoProvenance
p Role
_ Type
t1 Type
t2) = UnivCoProvenance -> UniqSet TyCon
go_prov UnivCoProvenance
p UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
forall a. UniqSet a -> UniqSet a -> UniqSet a
`unionUniqSets` Type -> UniqSet TyCon
go Type
t1 UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
forall a. UniqSet a -> UniqSet a -> UniqSet a
`unionUniqSets` Type -> UniqSet TyCon
go Type
t2
go_co (CoVarCo {}) = UniqSet TyCon
forall a. UniqSet a
emptyUniqSet
go_co (HoleCo {}) = UniqSet TyCon
forall a. UniqSet a
emptyUniqSet
go_co (SymCo KindCoercion
co) = KindCoercion -> UniqSet TyCon
go_co KindCoercion
co
go_co (TransCo KindCoercion
co1 KindCoercion
co2) = KindCoercion -> UniqSet TyCon
go_co KindCoercion
co1 UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
forall a. UniqSet a -> UniqSet a -> UniqSet a
`unionUniqSets` KindCoercion -> UniqSet TyCon
go_co KindCoercion
co2
go_co (NthCo Role
_ Int
_ KindCoercion
co) = KindCoercion -> UniqSet TyCon
go_co KindCoercion
co
go_co (LRCo LeftOrRight
_ KindCoercion
co) = KindCoercion -> UniqSet TyCon
go_co KindCoercion
co
go_co (InstCo KindCoercion
co KindCoercion
arg) = KindCoercion -> UniqSet TyCon
go_co KindCoercion
co UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
forall a. UniqSet a -> UniqSet a -> UniqSet a
`unionUniqSets` KindCoercion -> UniqSet TyCon
go_co KindCoercion
arg
go_co (KindCo KindCoercion
co) = KindCoercion -> UniqSet TyCon
go_co KindCoercion
co
go_co (SubCo KindCoercion
co) = KindCoercion -> UniqSet TyCon
go_co KindCoercion
co
go_co (AxiomRuleCo CoAxiomRule
_ [KindCoercion]
cs) = [KindCoercion] -> UniqSet TyCon
go_cos [KindCoercion]
cs
go_mco :: MCoercionN -> UniqSet TyCon
go_mco MCoercionN
MRefl = UniqSet TyCon
forall a. UniqSet a
emptyUniqSet
go_mco (MCo KindCoercion
co) = KindCoercion -> UniqSet TyCon
go_co KindCoercion
co
go_prov :: UnivCoProvenance -> UniqSet TyCon
go_prov (PhantomProv KindCoercion
co) = KindCoercion -> UniqSet TyCon
go_co KindCoercion
co
go_prov (ProofIrrelProv KindCoercion
co) = KindCoercion -> UniqSet TyCon
go_co KindCoercion
co
go_prov (PluginProv String
_) = UniqSet TyCon
forall a. UniqSet a
emptyUniqSet
go_prov (CorePrepProv Bool
_) = UniqSet TyCon
forall a. UniqSet a
emptyUniqSet
go_s :: t Type -> UniqSet TyCon
go_s t Type
tys = (Type -> UniqSet TyCon -> UniqSet TyCon)
-> UniqSet TyCon -> t Type -> UniqSet TyCon
forall a b. (a -> b -> b) -> b -> t a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
forall a. UniqSet a -> UniqSet a -> UniqSet a
unionUniqSets (UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon)
-> (Type -> UniqSet TyCon)
-> Type
-> UniqSet TyCon
-> UniqSet TyCon
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> UniqSet TyCon
go) UniqSet TyCon
forall a. UniqSet a
emptyUniqSet t Type
tys
go_cos :: [KindCoercion] -> UniqSet TyCon
go_cos [KindCoercion]
cos = (KindCoercion -> UniqSet TyCon -> UniqSet TyCon)
-> UniqSet TyCon -> [KindCoercion] -> UniqSet TyCon
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
forall a. UniqSet a -> UniqSet a -> UniqSet a
unionUniqSets (UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon)
-> (KindCoercion -> UniqSet TyCon)
-> KindCoercion
-> UniqSet TyCon
-> UniqSet TyCon
forall b c a. (b -> c) -> (a -> b) -> a -> c
. KindCoercion -> UniqSet TyCon
go_co) UniqSet TyCon
forall a. UniqSet a
emptyUniqSet [KindCoercion]
cos
go_tc :: a -> UniqSet a
go_tc a
tc = a -> UniqSet a
forall {a}. Uniquable a => a -> UniqSet a
unitUniqSet a
tc
go_ax :: CoAxiom br -> UniqSet TyCon
go_ax CoAxiom br
ax = TyCon -> UniqSet TyCon
forall {a}. Uniquable a => a -> UniqSet a
go_tc (TyCon -> UniqSet TyCon) -> TyCon -> UniqSet TyCon
forall a b. (a -> b) -> a -> b
$ CoAxiom br -> TyCon
forall (br :: BranchFlag). CoAxiom br -> TyCon
coAxiomTyCon CoAxiom br
ax
splitVisVarsOfType :: Type -> Pair TyCoVarSet
splitVisVarsOfType :: Type -> Pair TyCoVarSet
splitVisVarsOfType Type
orig_ty = TyCoVarSet -> TyCoVarSet -> Pair TyCoVarSet
forall a. a -> a -> Pair a
Pair TyCoVarSet
invis_vars TyCoVarSet
vis_vars
where
Pair TyCoVarSet
invis_vars1 TyCoVarSet
vis_vars = Type -> Pair TyCoVarSet
go Type
orig_ty
invis_vars :: TyCoVarSet
invis_vars = TyCoVarSet
invis_vars1 TyCoVarSet -> TyCoVarSet -> TyCoVarSet
`minusVarSet` TyCoVarSet
vis_vars
go :: Type -> Pair TyCoVarSet
go (TyVarTy TyVar
tv) = TyCoVarSet -> TyCoVarSet -> Pair TyCoVarSet
forall a. a -> a -> Pair a
Pair (Type -> TyCoVarSet
tyCoVarsOfType (Type -> TyCoVarSet) -> Type -> TyCoVarSet
forall a b. (a -> b) -> a -> b
$ TyVar -> Type
tyVarKind TyVar
tv) (TyVar -> TyCoVarSet
unitVarSet TyVar
tv)
go (AppTy Type
t1 Type
t2) = Type -> Pair TyCoVarSet
go Type
t1 Pair TyCoVarSet -> Pair TyCoVarSet -> Pair TyCoVarSet
forall a. Monoid a => a -> a -> a
`mappend` Type -> Pair TyCoVarSet
go Type
t2
go (TyConApp TyCon
tc [Type]
tys) = TyCon -> [Type] -> Pair TyCoVarSet
go_tc TyCon
tc [Type]
tys
go (FunTy AnonArgFlag
_ Type
w Type
t1 Type
t2) = Type -> Pair TyCoVarSet
go Type
w Pair TyCoVarSet -> Pair TyCoVarSet -> Pair TyCoVarSet
forall a. Monoid a => a -> a -> a
`mappend` Type -> Pair TyCoVarSet
go Type
t1 Pair TyCoVarSet -> Pair TyCoVarSet -> Pair TyCoVarSet
forall a. Monoid a => a -> a -> a
`mappend` Type -> Pair TyCoVarSet
go Type
t2
go (ForAllTy (Bndr TyVar
tv ArgFlag
_) Type
ty)
= ((TyCoVarSet -> TyVar -> TyCoVarSet
`delVarSet` TyVar
tv) (TyCoVarSet -> TyCoVarSet) -> Pair TyCoVarSet -> Pair TyCoVarSet
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Pair TyCoVarSet
go Type
ty) Pair TyCoVarSet -> Pair TyCoVarSet -> Pair TyCoVarSet
forall a. Monoid a => a -> a -> a
`mappend`
(TyCoVarSet -> Pair TyCoVarSet
invisible (Type -> TyCoVarSet
tyCoVarsOfType (Type -> TyCoVarSet) -> Type -> TyCoVarSet
forall a b. (a -> b) -> a -> b
$ TyVar -> Type
varType TyVar
tv))
go (LitTy {}) = Pair TyCoVarSet
forall a. Monoid a => a
mempty
go (CastTy Type
ty KindCoercion
co) = Type -> Pair TyCoVarSet
go Type
ty Pair TyCoVarSet -> Pair TyCoVarSet -> Pair TyCoVarSet
forall a. Monoid a => a -> a -> a
`mappend` TyCoVarSet -> Pair TyCoVarSet
invisible (KindCoercion -> TyCoVarSet
tyCoVarsOfCo KindCoercion
co)
go (CoercionTy KindCoercion
co) = TyCoVarSet -> Pair TyCoVarSet
invisible (TyCoVarSet -> Pair TyCoVarSet) -> TyCoVarSet -> Pair TyCoVarSet
forall a b. (a -> b) -> a -> b
$ KindCoercion -> TyCoVarSet
tyCoVarsOfCo KindCoercion
co
invisible :: TyCoVarSet -> Pair TyCoVarSet
invisible TyCoVarSet
vs = TyCoVarSet -> TyCoVarSet -> Pair TyCoVarSet
forall a. a -> a -> Pair a
Pair TyCoVarSet
vs TyCoVarSet
emptyVarSet
go_tc :: TyCon -> [Type] -> Pair TyCoVarSet
go_tc TyCon
tc [Type]
tys = let ([Type]
invis, [Type]
vis) = TyCon -> [Type] -> ([Type], [Type])
partitionInvisibleTypes TyCon
tc [Type]
tys in
TyCoVarSet -> Pair TyCoVarSet
invisible ([Type] -> TyCoVarSet
tyCoVarsOfTypes [Type]
invis) Pair TyCoVarSet -> Pair TyCoVarSet -> Pair TyCoVarSet
forall a. Monoid a => a -> a -> a
`mappend` (Type -> Pair TyCoVarSet) -> [Type] -> Pair TyCoVarSet
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Type -> Pair TyCoVarSet
go [Type]
vis
splitVisVarsOfTypes :: [Type] -> Pair TyCoVarSet
splitVisVarsOfTypes :: [Type] -> Pair TyCoVarSet
splitVisVarsOfTypes = (Type -> Pair TyCoVarSet) -> [Type] -> Pair TyCoVarSet
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Type -> Pair TyCoVarSet
splitVisVarsOfType
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
isLiftedTypeKind Type
k Bool -> Bool -> Bool
|| Bool
_is_type) (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
where
_is_type :: Bool
_is_type = Type -> Bool
classifiesTypeWithValues 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 AnonArgFlag
_ 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
classifiesTypeWithValues :: Kind -> Bool
classifiesTypeWithValues :: Type -> Bool
classifiesTypeWithValues Type
k = Maybe Type -> Bool
forall a. Maybe a -> Bool
isJust ((() :: Constraint) => Type -> Maybe Type
Type -> Maybe Type
kindRep_maybe Type
k)
tyConAppNeedsKindSig
:: Bool
-> TyCon
-> Int
-> Bool
tyConAppNeedsKindSig :: Bool -> TyCon -> Int -> Bool
tyConAppNeedsKindSig Bool
spec_inj_pos TyCon
tc Int
n_args
| Ordering
LT <- [TyConBinder] -> Int -> Ordering
forall a. [a] -> Int -> Ordering
listLengthCmp [TyConBinder]
tc_binders Int
n_args
= Bool
False
| Bool
otherwise
= let ([TyConBinder]
dropped_binders, [TyConBinder]
remaining_binders)
= Int -> [TyConBinder] -> ([TyConBinder], [TyConBinder])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
n_args [TyConBinder]
tc_binders
result_kind :: Type
result_kind = [TyConBinder] -> Type -> Type
mkTyConKind [TyConBinder]
remaining_binders Type
tc_res_kind
result_vars :: TyCoVarSet
result_vars = Type -> TyCoVarSet
tyCoVarsOfType Type
result_kind
dropped_vars :: TyCoVarSet
dropped_vars = FV -> TyCoVarSet
fvVarSet (FV -> TyCoVarSet) -> FV -> TyCoVarSet
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 (TyCoVarSet -> TyCoVarSet -> Bool
subVarSet TyCoVarSet
result_vars TyCoVarSet
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 AnonArgFlag
VisArg -> Bool -> Type -> FV
injectiveVarsOfType Bool
False
(TyVar -> Type
varType TyVar
tv)
NamedTCB ArgFlag
argf | ArgFlag -> Bool
source_of_injectivity ArgFlag
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 :: ArgFlag -> Bool
source_of_injectivity ArgFlag
Required = Bool
True
source_of_injectivity ArgFlag
Specified = Bool
spec_inj_pos
source_of_injectivity ArgFlag
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
Many
linear :: forall a. a -> Scaled a
linear = Type -> a -> Scaled a
forall a. Type -> a -> Scaled a
Scaled Type
One
tymult :: forall a. a -> Scaled a
tymult = Type -> a -> Scaled a
forall a. Type -> a -> Scaled a
Scaled Type
Many
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 One :: Mult
pattern $mOne :: forall {r}. Type -> ((# #) -> r) -> ((# #) -> r) -> r
$bOne :: Type
One <- (isOneDataConTy -> True)
where One = Type
oneDataConTy
pattern Many :: Mult
pattern $mMany :: forall {r}. Type -> ((# #) -> r) -> ((# #) -> r) -> r
$bMany :: Type
Many <- (isManyDataConTy -> True)
where Many = Type
manyDataConTy
isManyDataConTy :: Mult -> Bool
isManyDataConTy :: Type -> Bool
isManyDataConTy 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
isManyDataConTy Type
_ = Bool
False
isOneDataConTy :: Mult -> Bool
isOneDataConTy :: Type -> Bool
isOneDataConTy 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
isOneDataConTy Type
_ = Bool
False
isLinearType :: Type -> Bool
isLinearType :: Type -> Bool
isLinearType Type
ty = case Type
ty of
FunTy AnonArgFlag
_ Type
Many Type
_ Type
res -> Type -> Bool
isLinearType Type
res
FunTy AnonArgFlag
_ Type
_ Type
_ Type
_ -> Bool
True
ForAllTy VarBndr TyVar ArgFlag
_ Type
res -> Type -> Bool
isLinearType Type
res
Type
_ -> Bool
False