{-# LANGUAGE DerivingStrategies #-}
module GHC.Core.Predicate (
Pred(..), classifyPredType,
isPredTy, isEvVarType,
EqRel(..), eqRelRole,
isEqPrimPred, isEqPred,
getEqPredTys, getEqPredTys_maybe, getEqPredRole,
predTypeEqRel,
mkPrimEqPred, mkReprPrimEqPred, mkPrimEqPredRole,
mkHeteroPrimEqPred, mkHeteroReprPrimEqPred,
mkClassPred, isDictTy, typeDeterminesValue,
isClassPred, isEqPredClass, isCTupleClass,
getClassPredTys, getClassPredTys_maybe,
classMethodTy, classMethodInstTy,
isIPLikePred, hasIPSuperClasses, isIPTyCon, isIPClass,
isCallStackTy, isCallStackPred, isCallStackPredTy,
isIPPred_maybe,
DictId, isEvVar, isDictId
) where
import GHC.Prelude
import GHC.Core.Type
import GHC.Core.Class
import GHC.Core.TyCon
import GHC.Core.TyCon.RecWalk
import GHC.Types.Var
import GHC.Core.Coercion
import GHC.Core.Multiplicity ( scaledThing )
import GHC.Builtin.Names
import GHC.Utils.Outputable
import GHC.Utils.Misc
import GHC.Utils.Panic
import GHC.Data.FastString
import Control.Monad ( guard )
data Pred
= ClassPred Class [Type]
| EqPred EqRel Type Type
| IrredPred PredType
| ForAllPred [TyVar] [PredType] PredType
classifyPredType :: PredType -> Pred
classifyPredType :: PredType -> Pred
classifyPredType PredType
ev_ty = case HasDebugCallStack => PredType -> Maybe (TyCon, [PredType])
splitTyConApp_maybe PredType
ev_ty of
Just (TyCon
tc, [PredType
_, PredType
_, PredType
ty1, PredType
ty2])
| TyCon
tc forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
eqReprPrimTyConKey -> EqRel -> PredType -> PredType -> Pred
EqPred EqRel
ReprEq PredType
ty1 PredType
ty2
| TyCon
tc forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
eqPrimTyConKey -> EqRel -> PredType -> PredType -> Pred
EqPred EqRel
NomEq PredType
ty1 PredType
ty2
Just (TyCon
tc, [PredType]
tys)
| Just Class
clas <- TyCon -> Maybe Class
tyConClass_maybe TyCon
tc
-> Class -> [PredType] -> Pred
ClassPred Class
clas [PredType]
tys
Maybe (TyCon, [PredType])
_ | ([TyCoVar]
tvs, PredType
rho) <- PredType -> ([TyCoVar], PredType)
splitForAllTyCoVars PredType
ev_ty
, ([Scaled PredType]
theta, PredType
pred) <- PredType -> ([Scaled PredType], PredType)
splitFunTys PredType
rho
, Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TyCoVar]
tvs Bool -> Bool -> Bool
&& forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Scaled PredType]
theta)
-> [TyCoVar] -> [PredType] -> PredType -> Pred
ForAllPred [TyCoVar]
tvs (forall a b. (a -> b) -> [a] -> [b]
map forall a. Scaled a -> a
scaledThing [Scaled PredType]
theta) PredType
pred
| Bool
otherwise
-> PredType -> Pred
IrredPred PredType
ev_ty
mkClassPred :: Class -> [Type] -> PredType
mkClassPred :: Class -> [PredType] -> PredType
mkClassPred Class
clas [PredType]
tys = TyCon -> [PredType] -> PredType
mkTyConApp (Class -> TyCon
classTyCon Class
clas) [PredType]
tys
isDictTy :: Type -> Bool
isDictTy :: PredType -> Bool
isDictTy = PredType -> Bool
isClassPred
typeDeterminesValue :: Type -> Bool
typeDeterminesValue :: PredType -> Bool
typeDeterminesValue PredType
ty = PredType -> Bool
isDictTy PredType
ty Bool -> Bool -> Bool
&& Bool -> Bool
not (PredType -> Bool
isIPLikePred PredType
ty)
getClassPredTys :: HasDebugCallStack => PredType -> (Class, [Type])
getClassPredTys :: HasDebugCallStack => PredType -> (Class, [PredType])
getClassPredTys PredType
ty = case PredType -> Maybe (Class, [PredType])
getClassPredTys_maybe PredType
ty of
Just (Class
clas, [PredType]
tys) -> (Class
clas, [PredType]
tys)
Maybe (Class, [PredType])
Nothing -> forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"getClassPredTys" (forall a. Outputable a => a -> SDoc
ppr PredType
ty)
getClassPredTys_maybe :: PredType -> Maybe (Class, [Type])
getClassPredTys_maybe :: PredType -> Maybe (Class, [PredType])
getClassPredTys_maybe PredType
ty = case HasDebugCallStack => PredType -> Maybe (TyCon, [PredType])
splitTyConApp_maybe PredType
ty of
Just (TyCon
tc, [PredType]
tys) | Just Class
clas <- TyCon -> Maybe Class
tyConClass_maybe TyCon
tc -> forall a. a -> Maybe a
Just (Class
clas, [PredType]
tys)
Maybe (TyCon, [PredType])
_ -> forall a. Maybe a
Nothing
classMethodTy :: Id -> Type
classMethodTy :: TyCoVar -> PredType
classMethodTy TyCoVar
sel_id
= HasDebugCallStack => PredType -> PredType
funResultTy forall a b. (a -> b) -> a -> b
$
PredType -> PredType
dropForAlls forall a b. (a -> b) -> a -> b
$
TyCoVar -> PredType
varType TyCoVar
sel_id
classMethodInstTy :: Id -> [Type] -> Type
classMethodInstTy :: TyCoVar -> [PredType] -> PredType
classMethodInstTy TyCoVar
sel_id [PredType]
arg_tys
= HasDebugCallStack => PredType -> PredType
funResultTy forall a b. (a -> b) -> a -> b
$
HasDebugCallStack => PredType -> [PredType] -> PredType
piResultTys (TyCoVar -> PredType
varType TyCoVar
sel_id) [PredType]
arg_tys
data EqRel = NomEq | ReprEq
deriving (EqRel -> EqRel -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: EqRel -> EqRel -> Bool
$c/= :: EqRel -> EqRel -> Bool
== :: EqRel -> EqRel -> Bool
$c== :: EqRel -> EqRel -> Bool
Eq, Eq EqRel
EqRel -> EqRel -> Bool
EqRel -> EqRel -> Ordering
EqRel -> EqRel -> EqRel
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
min :: EqRel -> EqRel -> EqRel
$cmin :: EqRel -> EqRel -> EqRel
max :: EqRel -> EqRel -> EqRel
$cmax :: EqRel -> EqRel -> EqRel
>= :: EqRel -> EqRel -> Bool
$c>= :: EqRel -> EqRel -> Bool
> :: EqRel -> EqRel -> Bool
$c> :: EqRel -> EqRel -> Bool
<= :: EqRel -> EqRel -> Bool
$c<= :: EqRel -> EqRel -> Bool
< :: EqRel -> EqRel -> Bool
$c< :: EqRel -> EqRel -> Bool
compare :: EqRel -> EqRel -> Ordering
$ccompare :: EqRel -> EqRel -> Ordering
Ord)
instance Outputable EqRel where
ppr :: EqRel -> SDoc
ppr EqRel
NomEq = forall doc. IsLine doc => String -> doc
text String
"nominal equality"
ppr EqRel
ReprEq = forall doc. IsLine doc => String -> doc
text String
"representational equality"
eqRelRole :: EqRel -> Role
eqRelRole :: EqRel -> Role
eqRelRole EqRel
NomEq = Role
Nominal
eqRelRole EqRel
ReprEq = Role
Representational
getEqPredTys :: PredType -> (Type, Type)
getEqPredTys :: PredType -> (PredType, PredType)
getEqPredTys PredType
ty
= case HasDebugCallStack => PredType -> Maybe (TyCon, [PredType])
splitTyConApp_maybe PredType
ty of
Just (TyCon
tc, [PredType
_, PredType
_, PredType
ty1, PredType
ty2])
| TyCon
tc forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
eqPrimTyConKey
Bool -> Bool -> Bool
|| TyCon
tc forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
eqReprPrimTyConKey
-> (PredType
ty1, PredType
ty2)
Maybe (TyCon, [PredType])
_ -> forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"getEqPredTys" (forall a. Outputable a => a -> SDoc
ppr PredType
ty)
getEqPredTys_maybe :: PredType -> Maybe (Role, Type, Type)
getEqPredTys_maybe :: PredType -> Maybe (Role, PredType, PredType)
getEqPredTys_maybe PredType
ty
= case HasDebugCallStack => PredType -> Maybe (TyCon, [PredType])
splitTyConApp_maybe PredType
ty of
Just (TyCon
tc, [PredType
_, PredType
_, PredType
ty1, PredType
ty2])
| TyCon
tc forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
eqPrimTyConKey -> forall a. a -> Maybe a
Just (Role
Nominal, PredType
ty1, PredType
ty2)
| TyCon
tc forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
eqReprPrimTyConKey -> forall a. a -> Maybe a
Just (Role
Representational, PredType
ty1, PredType
ty2)
Maybe (TyCon, [PredType])
_ -> forall a. Maybe a
Nothing
getEqPredRole :: PredType -> Role
getEqPredRole :: PredType -> Role
getEqPredRole PredType
ty = EqRel -> Role
eqRelRole (PredType -> EqRel
predTypeEqRel PredType
ty)
predTypeEqRel :: PredType -> EqRel
predTypeEqRel :: PredType -> EqRel
predTypeEqRel PredType
ty
| Just (TyCon
tc, [PredType]
_) <- HasDebugCallStack => PredType -> Maybe (TyCon, [PredType])
splitTyConApp_maybe PredType
ty
, TyCon
tc forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
eqReprPrimTyConKey
= EqRel
ReprEq
| Bool
otherwise
= EqRel
NomEq
isEvVarType :: Type -> Bool
isEvVarType :: PredType -> Bool
isEvVarType PredType
ty = PredType -> Bool
isCoVarType PredType
ty Bool -> Bool -> Bool
|| HasDebugCallStack => PredType -> Bool
isPredTy PredType
ty
isEqPredClass :: Class -> Bool
isEqPredClass :: Class -> Bool
isEqPredClass Class
cls = Class
cls forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
eqTyConKey
Bool -> Bool -> Bool
|| Class
cls forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
heqTyConKey
isClassPred, isEqPred, isEqPrimPred :: PredType -> Bool
isClassPred :: PredType -> Bool
isClassPred PredType
ty = case PredType -> Maybe TyCon
tyConAppTyCon_maybe PredType
ty of
Just TyCon
tyCon | TyCon -> Bool
isClassTyCon TyCon
tyCon -> Bool
True
Maybe TyCon
_ -> Bool
False
isEqPred :: PredType -> Bool
isEqPred PredType
ty
| Just TyCon
tc <- PredType -> Maybe TyCon
tyConAppTyCon_maybe PredType
ty
, Just Class
cls <- TyCon -> Maybe Class
tyConClass_maybe TyCon
tc
= Class -> Bool
isEqPredClass Class
cls
| Bool
otherwise
= Bool
False
isEqPrimPred :: PredType -> Bool
isEqPrimPred PredType
ty = PredType -> Bool
isCoVarType PredType
ty
isCTupleClass :: Class -> Bool
isCTupleClass :: Class -> Bool
isCTupleClass Class
cls = TyCon -> Bool
isTupleTyCon (Class -> TyCon
classTyCon Class
cls)
isIPTyCon :: TyCon -> Bool
isIPTyCon :: TyCon -> Bool
isIPTyCon TyCon
tc = TyCon
tc forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
ipClassKey
isIPClass :: Class -> Bool
isIPClass :: Class -> Bool
isIPClass Class
cls = Class
cls forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
ipClassKey
isIPLikePred :: Type -> Bool
isIPLikePred :: PredType -> Bool
isIPLikePred = RecTcChecker -> PredType -> Bool
is_ip_like_pred RecTcChecker
initIPRecTc
is_ip_like_pred :: RecTcChecker -> Type -> Bool
is_ip_like_pred :: RecTcChecker -> PredType -> Bool
is_ip_like_pred RecTcChecker
rec_clss PredType
ty
| Just (TyCon
tc, [PredType]
tys) <- HasDebugCallStack => PredType -> Maybe (TyCon, [PredType])
splitTyConApp_maybe PredType
ty
, Just RecTcChecker
rec_clss' <- if TyCon -> Bool
isTupleTyCon TyCon
tc
then forall a. a -> Maybe a
Just RecTcChecker
rec_clss
else RecTcChecker -> TyCon -> Maybe RecTcChecker
checkRecTc RecTcChecker
rec_clss TyCon
tc
, Just Class
cls <- TyCon -> Maybe Class
tyConClass_maybe TyCon
tc
= Class -> Bool
isIPClass Class
cls Bool -> Bool -> Bool
|| RecTcChecker -> Class -> [PredType] -> Bool
has_ip_super_classes RecTcChecker
rec_clss' Class
cls [PredType]
tys
| Bool
otherwise
= Bool
False
hasIPSuperClasses :: Class -> [Type] -> Bool
hasIPSuperClasses :: Class -> [PredType] -> Bool
hasIPSuperClasses = RecTcChecker -> Class -> [PredType] -> Bool
has_ip_super_classes RecTcChecker
initIPRecTc
has_ip_super_classes :: RecTcChecker -> Class -> [Type] -> Bool
has_ip_super_classes :: RecTcChecker -> Class -> [PredType] -> Bool
has_ip_super_classes RecTcChecker
rec_clss Class
cls [PredType]
tys
= forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any TyCoVar -> Bool
ip_ish (Class -> [TyCoVar]
classSCSelIds Class
cls)
where
ip_ish :: TyCoVar -> Bool
ip_ish TyCoVar
sc_sel_id = RecTcChecker -> PredType -> Bool
is_ip_like_pred RecTcChecker
rec_clss forall a b. (a -> b) -> a -> b
$
TyCoVar -> [PredType] -> PredType
classMethodInstTy TyCoVar
sc_sel_id [PredType]
tys
initIPRecTc :: RecTcChecker
initIPRecTc :: RecTcChecker
initIPRecTc = Int -> RecTcChecker -> RecTcChecker
setRecTcMaxBound Int
1 RecTcChecker
initRecTc
isCallStackPredTy :: Type -> Bool
isCallStackPredTy :: PredType -> Bool
isCallStackPredTy PredType
ty
| Just (TyCon
tc, [PredType]
tys) <- HasDebugCallStack => PredType -> Maybe (TyCon, [PredType])
splitTyConApp_maybe PredType
ty
, Just Class
cls <- TyCon -> Maybe Class
tyConClass_maybe TyCon
tc
, Just {} <- Class -> [PredType] -> Maybe FastString
isCallStackPred Class
cls [PredType]
tys
= Bool
True
| Bool
otherwise
= Bool
False
isCallStackPred :: Class -> [Type] -> Maybe FastString
isCallStackPred :: Class -> [PredType] -> Maybe FastString
isCallStackPred Class
cls [PredType]
tys
| [PredType
ty1, PredType
ty2] <- [PredType]
tys
, Class -> Bool
isIPClass Class
cls
, PredType -> Bool
isCallStackTy PredType
ty2
= PredType -> Maybe FastString
isStrLitTy PredType
ty1
| Bool
otherwise
= forall a. Maybe a
Nothing
isCallStackTy :: Type -> Bool
isCallStackTy :: PredType -> Bool
isCallStackTy PredType
ty
| Just TyCon
tc <- PredType -> Maybe TyCon
tyConAppTyCon_maybe PredType
ty
= TyCon
tc forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
callStackTyConKey
| Bool
otherwise
= Bool
False
isIPPred_maybe :: Type -> Maybe (FastString, Type)
isIPPred_maybe :: PredType -> Maybe (FastString, PredType)
isIPPred_maybe PredType
ty =
do (TyCon
tc,[PredType
t1,PredType
t2]) <- HasDebugCallStack => PredType -> Maybe (TyCon, [PredType])
splitTyConApp_maybe PredType
ty
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (TyCon -> Bool
isIPTyCon TyCon
tc)
FastString
x <- PredType -> Maybe FastString
isStrLitTy PredType
t1
forall (m :: * -> *) a. Monad m => a -> m a
return (FastString
x,PredType
t2)
isEvVar :: Var -> Bool
isEvVar :: TyCoVar -> Bool
isEvVar TyCoVar
var = PredType -> Bool
isEvVarType (TyCoVar -> PredType
varType TyCoVar
var)
isDictId :: Id -> Bool
isDictId :: TyCoVar -> Bool
isDictId TyCoVar
id = PredType -> Bool
isDictTy (TyCoVar -> PredType
varType TyCoVar
id)