GHC.Core.Predicate

Documentation

data Pred

A predicate in the solver. The solver tries to prove Wanted predicates from Given ones.

Constructors

ClassPred Class [Type]

A typeclass predicate.

EqPred EqRel Type Type

A type equality predicate.

IrredPred PredType

An irreducible predicate.

ForAllPred [TyVar] [PredType] PredType

A quantified predicate.

See Note [Quantified constraints] in GHC.Tc.Solver.Canonical

SpecialPred SpecialPred

A special predicate, used internally in GHC.

See #20000.

classifyPredType :: PredType -> Pred

isPredTy :: HasDebugCallStack => Type -> Bool

isEvVarType :: Type -> Bool

data EqRel

A choice of equality relation. This is separate from the type Role because Phantom does not define a (non-trivial) equality relation.

Constructors

NomEq

ReprEq

Instances

Eq EqRel

Defined in GHC.Core.Predicate

Methods

(==) :: EqRel -> EqRel -> Bool

(/=) :: EqRel -> EqRel -> Bool

Ord EqRel

Defined in GHC.Core.Predicate

Methods

compare :: EqRel -> EqRel -> Ordering

(<) :: EqRel -> EqRel -> Bool

(<=) :: EqRel -> EqRel -> Bool

(>) :: EqRel -> EqRel -> Bool

(>=) :: EqRel -> EqRel -> Bool

max :: EqRel -> EqRel -> EqRel

min :: EqRel -> EqRel -> EqRel

Outputable EqRel

Defined in GHC.Core.Predicate

Methods

ppr :: EqRel -> SDoc

eqRelRole :: EqRel -> Role

isEqPrimPred :: PredType -> Bool

isEqPred :: PredType -> Bool

getEqPredTys :: PredType -> (Type, Type)

getEqPredTys_maybe :: PredType -> Maybe (Role, Type, Type)

getEqPredRole :: PredType -> Role

predTypeEqRel :: PredType -> EqRel

Get the equality relation relevant for a pred type.

mkPrimEqPred :: Type -> Type -> Type

Creates a primitive type equality predicate. Invariant: the types are not Coercions

mkReprPrimEqPred :: Type -> Type -> Type

mkPrimEqPredRole :: Role -> Type -> Type -> PredType

Makes a lifted equality predicate at the given role

mkHeteroPrimEqPred :: Kind -> Kind -> Type -> Type -> Type

Creates a primitive type equality predicate with explicit kinds

mkHeteroReprPrimEqPred :: Kind -> Kind -> Type -> Type -> Type

Creates a primitive representational type equality predicate with explicit kinds

data SpecialPred

SpecialPred describes all the special predicates that are currently used in GHC.

These are different from the special typeclasses (such as KnownNat, Typeable, Coercible, ...), as special predicates can't be expressed as typeclasses, as they hold evidence of a different kind.

Constructors

IsReflPrimPred Type Type

'IsRefl#'.

Instances

Outputable SpecialPred

Defined in GHC.Core.Predicate

Methods

ppr :: SpecialPred -> SDoc

mkIsReflPrimPred :: Type -> Type -> PredType

isIsReflPrimPred :: Pred -> Bool

mkClassPred :: Class -> [Type] -> PredType

isDictTy :: Type -> Bool

isClassPred :: PredType -> Bool

isEqPredClass :: Class -> Bool

isCTupleClass :: Class -> Bool

getClassPredTys :: HasDebugCallStack => PredType -> (Class, [Type])

getClassPredTys_maybe :: PredType -> Maybe (Class, [Type])

classMethodTy :: Id -> Type

classMethodInstTy :: Id -> [Type] -> Type

isIPLikePred :: Type -> Bool

hasIPSuperClasses :: Class -> [Type] -> Bool

isIPTyCon :: TyCon -> Bool

isIPClass :: Class -> Bool

isCallStackTy :: Type -> Bool

Is a type a CallStack?

isCallStackPred :: Class -> [Type] -> Maybe FastString

Is a PredType a CallStack implicit parameter?

If so, return the name of the parameter.

isCallStackPredTy :: Type -> Bool

isIPPred_maybe :: Type -> Maybe (FastString, Type)

Decomposes a predicate if it is an implicit parameter. Does not look in superclasses. See also [Local implicit parameters].

type DictId = EvId

Dictionary Identifier

isEvVar :: Var -> Bool

isDictId :: Id -> Bool