GHC.Tc.Types.Constraint

This module defines types and simple operations over constraints, as used in the type-checker and constraint solver.

Documentation

data QCInst

Constructors

QCI

Fields

• qci_ev :: CtEvidence
• qci_tvs :: [TcTyVar]
• qci_pred :: TcPredType
• qci_pend_sc :: Bool

Instances

Outputable QCInst

Defined in GHC.Tc.Types.Constraint

Methods

ppr :: QCInst -> SDoc

pendingScInst_maybe :: QCInst -> Maybe QCInst

type Xi = TcType

A Xi-type is one that has been fully rewritten with respect to the inert set; that is, it has been rewritten by the algorithm in GHC.Tc.Solver.Rewrite. (Historical note: Xi, for years and years, meant that a type was type-family-free. It does *not* mean this any more.)

data Ct

Constructors

CDictCan

Fields

• cc_ev :: CtEvidence
• cc_class :: Class
• cc_tyargs :: [Xi]
• cc_pend_sc :: Bool

CIrredCan

Fields

• cc_ev :: CtEvidence
• cc_reason :: CtIrredReason

CEqCan

Fields

• cc_ev :: CtEvidence
• cc_lhs :: CanEqLHS
• cc_rhs :: Xi
• cc_eq_rel :: EqRel

CNonCanonical

Fields

• cc_ev :: CtEvidence

CQuantCan QCInst

Instances

Outputable Ct

Defined in GHC.Tc.Types.Constraint

Methods

ppr :: Ct -> SDoc

type Cts = Bag Ct

emptyCts :: Cts

andCts :: Cts -> Cts -> Cts

andManyCts :: [Cts] -> Cts

pprCts :: Cts -> SDoc

singleCt :: Ct -> Cts

listToCts :: [Ct] -> Cts

ctsElts :: Cts -> [Ct]

consCts :: Ct -> Cts -> Cts

snocCts :: Cts -> Ct -> Cts

extendCtsList :: Cts -> [Ct] -> Cts

isEmptyCts :: Cts -> Bool

isPendingScDict :: Ct -> Bool

pendingScDict_maybe :: Ct -> Maybe Ct

superClassesMightHelp :: WantedConstraints -> Bool

True if taking superclasses of givens, or of wanteds (to perhaps expose more equalities or functional dependencies) might help to solve this constraint. See Note [When superclasses help]

getPendingWantedScs :: Cts -> ([Ct], Cts)

isWantedCt :: Ct -> Bool

isGivenCt :: Ct -> Bool

isUserTypeError :: PredType -> Bool

getUserTypeErrorMsg :: PredType -> Maybe Type

A constraint is considered to be a custom type error, if it contains custom type errors anywhere in it. See Note [Custom type errors in constraints]

ctEvidence :: Ct -> CtEvidence

ctLoc :: Ct -> CtLoc

ctPred :: Ct -> PredType

ctFlavour :: Ct -> CtFlavour

Get the flavour of the given Ct

ctEqRel :: Ct -> EqRel

Get the equality relation for the given Ct

ctOrigin :: Ct -> CtOrigin

ctRewriters :: Ct -> RewriterSet

ctEvId :: HasDebugCallStack => Ct -> EvVar

wantedEvId_maybe :: Ct -> Maybe EvVar

Returns the evidence Id for the argument Ct when this Ct is a Wanted.

Returns Nothing otherwise.

mkTcEqPredLikeEv :: CtEvidence -> TcType -> TcType -> TcType

Makes a new equality predicate with the same role as the given evidence.

mkNonCanonical :: CtEvidence -> Ct

mkNonCanonicalCt :: Ct -> Ct

mkGivens :: CtLoc -> [EvId] -> [Ct]

mkIrredCt :: CtIrredReason -> CtEvidence -> Ct

ctEvPred :: CtEvidence -> TcPredType

ctEvLoc :: CtEvidence -> CtLoc

ctEvOrigin :: CtEvidence -> CtOrigin

ctEvEqRel :: CtEvidence -> EqRel

Get the equality relation relevant for a CtEvidence

ctEvExpr :: HasDebugCallStack => CtEvidence -> EvExpr

ctEvTerm :: CtEvidence -> EvTerm

ctEvCoercion :: HasDebugCallStack => CtEvidence -> TcCoercion

ctEvEvId :: CtEvidence -> EvVar

ctEvRewriters :: CtEvidence -> RewriterSet

Extract the set of rewriters from a CtEvidence See Note [Wanteds rewrite Wanteds] If the provided CtEvidence is not for a Wanted, just return an empty set.

tyCoVarsOfCt :: Ct -> TcTyCoVarSet

Returns free variables of constraints as a non-deterministic set

tyCoVarsOfCts :: Cts -> TcTyCoVarSet

Returns free variables of a bag of constraints as a non-deterministic set. See Note [Deterministic FV] in GHC.Utils.FV.

tyCoVarsOfCtList :: Ct -> [TcTyCoVar]

Returns free variables of constraints as a deterministically ordered list. See Note [Deterministic FV] in GHC.Utils.FV.

tyCoVarsOfCtsList :: Cts -> [TcTyCoVar]

Returns free variables of a bag of constraints as a deterministically ordered list. See Note [Deterministic FV] in GHC.Utils.FV.

data CtIrredReason

Used to indicate extra information about why a CIrredCan is irreducible

Constructors

IrredShapeReason

this constraint has a non-canonical shape (e.g. c Int, for a variable c)

NonCanonicalReason CheckTyEqResult

an equality where some invariant other than (TyEq:H) of CEqCan is not satisfied; the CheckTyEqResult states exactly why

ReprEqReason

an equality that cannot be decomposed because it is representational. Example: a b ~R# Int. These might still be solved later. INVARIANT: The constraint is a representational equality constraint

ShapeMismatchReason

a nominal equality that relates two wholly different types, like Int ~# Bool or a b ~# 3. INVARIANT: The constraint is a nominal equality constraint

AbstractTyConReason

an equality like T a b c ~ Q d e where either T or Q is an abstract type constructor. See Note [Skolem abstract data] in GHC.Core.TyCon. INVARIANT: The constraint is an equality constraint between two TyConApps

Instances

Outputable CtIrredReason

Defined in GHC.Tc.Types.Constraint

Methods

ppr :: CtIrredReason -> SDoc

isInsolubleReason :: CtIrredReason -> Bool

Are we sure that more solving will never solve this constraint?

data CheckTyEqResult

A set of problems in checking the validity of a type equality. See checkTypeEq.

Instances

Monoid CheckTyEqResult

Defined in GHC.Tc.Types.Constraint

Methods

mempty :: CheckTyEqResult

mappend :: CheckTyEqResult -> CheckTyEqResult -> CheckTyEqResult

mconcat :: [CheckTyEqResult] -> CheckTyEqResult

Semigroup CheckTyEqResult

Defined in GHC.Tc.Types.Constraint

Methods

(<>) :: CheckTyEqResult -> CheckTyEqResult -> CheckTyEqResult

sconcat :: NonEmpty CheckTyEqResult -> CheckTyEqResult

stimes :: Integral b => b -> CheckTyEqResult -> CheckTyEqResult

Outputable CheckTyEqResult

Defined in GHC.Tc.Types.Constraint

Methods

ppr :: CheckTyEqResult -> SDoc

data CheckTyEqProblem

An individual problem that might be logged in a CheckTyEqResult

cteProblem :: CheckTyEqProblem -> CheckTyEqResult

cterClearOccursCheck :: CheckTyEqResult -> CheckTyEqResult

cteOK :: CheckTyEqResult

No problems in checking the validity of a type equality.

cteImpredicative :: CheckTyEqProblem

cteTypeFamily :: CheckTyEqProblem

cteInsolubleOccurs :: CheckTyEqProblem

cteSolubleOccurs :: CheckTyEqProblem

cterSetOccursCheckSoluble :: CheckTyEqResult -> CheckTyEqResult

Mark a CheckTyEqResult as not having an insoluble occurs-check: any occurs check under a type family or in a representation equality is soluble.

cterHasNoProblem :: CheckTyEqResult -> Bool

Check whether a CheckTyEqResult is marked successful.

cterHasProblem :: CheckTyEqResult -> CheckTyEqProblem -> Bool

Check whether a CheckTyEqResult has a CheckTyEqProblem

cterHasOnlyProblem :: CheckTyEqResult -> CheckTyEqProblem -> Bool

Check whether a CheckTyEqResult has one CheckTyEqProblem and no other

cterRemoveProblem :: CheckTyEqResult -> CheckTyEqProblem -> CheckTyEqResult

cterHasOccursCheck :: CheckTyEqResult -> Bool

cterFromKind :: CheckTyEqResult -> CheckTyEqResult

Retain only information about occurs-check failures, because only that matters after recurring into a kind.

data CanEqLHS

A CanEqLHS is a type that can appear on the left of a canonical equality: a type variable or exactly-saturated type family application.

Constructors

TyVarLHS TcTyVar

TyFamLHS

Fields

• TyCon

  of the family

• [Xi]

  exactly saturating the family

Instances

Outputable CanEqLHS

Defined in GHC.Tc.Types.Constraint

Methods

ppr :: CanEqLHS -> SDoc

canEqLHS_maybe :: Xi -> Maybe CanEqLHS

Is a type a canonical LHS? That is, is it a tyvar or an exactly-saturated type family application? Does not look through type synonyms.

canEqLHSKind :: CanEqLHS -> TcKind

Retrieve the kind of a CanEqLHS

canEqLHSType :: CanEqLHS -> TcType

Convert a CanEqLHS back into a Type

eqCanEqLHS :: CanEqLHS -> CanEqLHS -> Bool

Are two CanEqLHSs equal?

data Hole

A hole stores the information needed to report diagnostics about holes in terms (unbound identifiers or underscores) or in types (also called wildcards, as used in partial type signatures). See Note [Holes].

Constructors

Hole

Fields

• hole_sort :: HoleSort

  What flavour of hole is this?

• hole_occ :: RdrName

  The name of this hole

• hole_ty :: TcType

  Type to be printed to the user For expression holes: type of expr For type holes: the missing type

• hole_loc :: CtLoc

  Where hole was written

Instances

Outputable Hole

Defined in GHC.Tc.Types.Constraint

Methods

ppr :: Hole -> SDoc

data HoleSort

Used to indicate which sort of hole we have.

Constructors

ExprHole HoleExprRef

Either an out-of-scope variable or a "true" hole in an expression (TypedHoles). The HoleExprRef says where to write the the erroring expression for -fdefer-type-errors.

TypeHole

A hole in a type (PartialTypeSignatures)

ConstraintHole

A hole in a constraint, like @f :: (_, Eq a) => ... Differentiated from TypeHole because a ConstraintHole is simplified differently. See Note [Do not simplify ConstraintHoles] in GHC.Tc.Solver.

Instances

Outputable HoleSort

Defined in GHC.Tc.Types.Constraint

Methods

ppr :: HoleSort -> SDoc

isOutOfScopeHole :: Hole -> Bool

Does this hole represent an "out of scope" error? See Note [Insoluble holes]

data DelayedError

A delayed error, to be reported after constraint solving, in order to benefit from deferred unifications.

Constructors

DE_Hole Hole

A hole (in a type or in a term).

See Note [Holes].

DE_NotConcrete NotConcreteError

A type could not be ensured to be concrete.

See Note [The Concrete mechanism] in GHC.Tc.Utils.Concrete.

Instances

Outputable DelayedError

Defined in GHC.Tc.Types.Constraint

Methods

ppr :: DelayedError -> SDoc

data NotConcreteError

Why did we require that a certain type be concrete?

Constructors

NCE_FRR

Concreteness was required by a representation-polymorphism check.

See Note [The Concrete mechanism] in GHC.Tc.Utils.Concrete.

Fields

• nce_loc :: CtLoc

  Where did this check take place?

• nce_frr_origin :: FixedRuntimeRepOrigin

  Which representation-polymorphism check did we perform?

• nce_reasons :: NonEmpty NotConcreteReason

  Why did the check fail?

Instances

Outputable NotConcreteError

Defined in GHC.Tc.Types.Constraint

Methods

ppr :: NotConcreteError -> SDoc

data NotConcreteReason

Why did we decide that a type was not concrete?

Constructors

NonConcreteTyCon TyCon [TcType]

The type contains a TyConApp of a non-concrete TyCon.

See Note [Concrete types] in GHC.Tc.Utils.Concrete.

NonConcretisableTyVar TyVar

The type contains a type variable that could not be made concrete (e.g. a skolem type variable).

ContainsCast TcType TcCoercionN

The type contains a cast.

ContainsForall ForAllTyBinder TcType

The type contains a forall.

ContainsCoercionTy TcCoercion

The type contains a CoercionTy.

data WantedConstraints

Constructors

WC

Fields

• wc_simple :: Cts
• wc_impl :: Bag Implication
• wc_errors :: Bag DelayedError

Instances

Outputable WantedConstraints

Defined in GHC.Tc.Types.Constraint

Methods

ppr :: WantedConstraints -> SDoc

insolubleWC :: WantedConstraints -> Bool

emptyWC :: WantedConstraints

isEmptyWC :: WantedConstraints -> Bool

isSolvedWC :: WantedConstraints -> Bool

Checks whether a the given wanted constraints are solved, i.e. that there are no simple constraints left and all the implications are solved.

andWC :: WantedConstraints -> WantedConstraints -> WantedConstraints

unionsWC :: [WantedConstraints] -> WantedConstraints

mkSimpleWC :: [CtEvidence] -> WantedConstraints

mkImplicWC :: Bag Implication -> WantedConstraints

addInsols :: WantedConstraints -> Bag Ct -> WantedConstraints

dropMisleading :: WantedConstraints -> WantedConstraints

addSimples :: WantedConstraints -> Bag Ct -> WantedConstraints

addImplics :: WantedConstraints -> Bag Implication -> WantedConstraints

addHoles :: WantedConstraints -> Bag Hole -> WantedConstraints

addNotConcreteError :: WantedConstraints -> NotConcreteError -> WantedConstraints

addDelayedErrors :: WantedConstraints -> Bag DelayedError -> WantedConstraints

tyCoVarsOfWC :: WantedConstraints -> TyCoVarSet

Returns free variables of WantedConstraints as a non-deterministic set. See Note [Deterministic FV] in GHC.Utils.FV.

tyCoVarsOfWCList :: WantedConstraints -> [TyCoVar]

Returns free variables of WantedConstraints as a deterministically ordered list. See Note [Deterministic FV] in GHC.Utils.FV.

insolubleWantedCt :: Ct -> Bool

insolubleEqCt :: Ct -> Bool

insolubleCt :: Ct -> Bool

Returns True of equality constraints that are definitely insoluble, as well as TypeError constraints. Can return True for Given constraints, unlike insolubleWantedCt.

This function is critical for accurate pattern-match overlap warnings. See Note [Pattern match warnings with insoluble Givens] in GHC.Tc.Solver

Note that this does not traverse through the constraint to find nested custom type errors: it only detects TypeError msg :: Constraint, and not e.g. Eq (TypeError msg).

insolubleImplic :: Implication -> Bool

nonDefaultableTyVarsOfWC :: WantedConstraints -> TyCoVarSet

Gather all the type variables from WantedConstraints that it would be unhelpful to default. For the moment, these are only ConcreteTv metavariables participating in a nominal equality whose other side is not concrete; it's usually better to report those as errors instead of defaulting.

data Implication

Constructors

Implic

Fields

• ic_tclvl :: TcLevel
• ic_info :: SkolemInfoAnon
• ic_skols :: [TcTyVar]
• ic_given :: [EvVar]
• ic_given_eqs :: HasGivenEqs
• ic_warn_inaccessible :: Bool
• ic_env :: TcLclEnv
• ic_wanted :: WantedConstraints
• ic_binds :: EvBindsVar
• ic_need_inner :: VarSet
• ic_need_outer :: VarSet
• ic_status :: ImplicStatus

Instances

Outputable Implication

Defined in GHC.Tc.Types.Constraint

Methods

ppr :: Implication -> SDoc

implicationPrototype :: Implication

checkTelescopeSkol :: SkolemInfoAnon -> Bool

data ImplicStatus

Constructors

IC_Solved

Fields

• ics_dead :: [EvVar]

IC_Insoluble

IC_BadTelescope

IC_Unsolved

Instances

Outputable ImplicStatus

Defined in GHC.Tc.Types.Constraint

Methods

ppr :: ImplicStatus -> SDoc

isInsolubleStatus :: ImplicStatus -> Bool

isSolvedStatus :: ImplicStatus -> Bool

type UserGiven = Implication

getUserGivensFromImplics :: [Implication] -> [UserGiven]

data HasGivenEqs

Constructors

NoGivenEqs

LocalGivenEqs

MaybeGivenEqs

Instances

Monoid HasGivenEqs

Defined in GHC.Tc.Types.Constraint

Methods

mempty :: HasGivenEqs

mappend :: HasGivenEqs -> HasGivenEqs -> HasGivenEqs

mconcat :: [HasGivenEqs] -> HasGivenEqs

Semigroup HasGivenEqs

Defined in GHC.Tc.Types.Constraint

Methods

(<>) :: HasGivenEqs -> HasGivenEqs -> HasGivenEqs

sconcat :: NonEmpty HasGivenEqs -> HasGivenEqs

stimes :: Integral b => b -> HasGivenEqs -> HasGivenEqs

Outputable HasGivenEqs

Defined in GHC.Tc.Types.Constraint

Methods

ppr :: HasGivenEqs -> SDoc

Eq HasGivenEqs

Defined in GHC.Tc.Types.Constraint

Methods

(==) :: HasGivenEqs -> HasGivenEqs -> Bool

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

checkImplicationInvariants :: (HasCallStack, Applicative m) => Implication -> m ()

data SubGoalDepth

See Note [SubGoalDepth]

Instances

Outputable SubGoalDepth

Defined in GHC.Tc.Types.Constraint

Methods

ppr :: SubGoalDepth -> SDoc

Eq SubGoalDepth

Defined in GHC.Tc.Types.Constraint

Methods

(==) :: SubGoalDepth -> SubGoalDepth -> Bool

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

Ord SubGoalDepth

Defined in GHC.Tc.Types.Constraint

Methods

compare :: SubGoalDepth -> SubGoalDepth -> Ordering

(<) :: SubGoalDepth -> SubGoalDepth -> Bool

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

(>) :: SubGoalDepth -> SubGoalDepth -> Bool

(>=) :: SubGoalDepth -> SubGoalDepth -> Bool

max :: SubGoalDepth -> SubGoalDepth -> SubGoalDepth

min :: SubGoalDepth -> SubGoalDepth -> SubGoalDepth

initialSubGoalDepth :: SubGoalDepth

maxSubGoalDepth :: SubGoalDepth -> SubGoalDepth -> SubGoalDepth

bumpSubGoalDepth :: SubGoalDepth -> SubGoalDepth

subGoalDepthExceeded :: DynFlags -> SubGoalDepth -> Bool

data CtLoc

Constructors

CtLoc

Fields

• ctl_origin :: CtOrigin
• ctl_env :: TcLclEnv
• ctl_t_or_k :: Maybe TypeOrKind
• ctl_depth :: !SubGoalDepth

ctLocSpan :: CtLoc -> RealSrcSpan

ctLocEnv :: CtLoc -> TcLclEnv

ctLocLevel :: CtLoc -> TcLevel

ctLocOrigin :: CtLoc -> CtOrigin

ctLocTypeOrKind_maybe :: CtLoc -> Maybe TypeOrKind

ctLocDepth :: CtLoc -> SubGoalDepth

bumpCtLocDepth :: CtLoc -> CtLoc

isGivenLoc :: CtLoc -> Bool

setCtLocOrigin :: CtLoc -> CtOrigin -> CtLoc

updateCtLocOrigin :: CtLoc -> (CtOrigin -> CtOrigin) -> CtLoc

setCtLocEnv :: CtLoc -> TcLclEnv -> CtLoc

setCtLocSpan :: CtLoc -> RealSrcSpan -> CtLoc

pprCtLoc :: CtLoc -> SDoc

data CtEvidence

Constructors

CtGiven

Fields

• ctev_pred :: TcPredType
• ctev_evar :: EvVar
• ctev_loc :: CtLoc

CtWanted

Fields

• ctev_pred :: TcPredType
• ctev_dest :: TcEvDest
• ctev_loc :: CtLoc
• ctev_rewriters :: RewriterSet

Instances

Outputable CtEvidence

Defined in GHC.Tc.Types.Constraint

Methods

ppr :: CtEvidence -> SDoc

data TcEvDest

A place for type-checking evidence to go after it is generated.

• Wanted equalities use HoleDest,
• other Wanteds use EvVarDest.

Constructors

EvVarDest EvVar

bind this var to the evidence EvVarDest is always used for non-type-equalities e.g. class constraints

HoleDest CoercionHole

fill in this hole with the evidence HoleDest is always used for type-equalities See Note [Coercion holes] in GHC.Core.TyCo.Rep

Instances

Outputable TcEvDest

Defined in GHC.Tc.Types.Constraint

Methods

ppr :: TcEvDest -> SDoc

mkKindLoc :: TcType -> TcType -> CtLoc -> CtLoc

toKindLoc :: CtLoc -> CtLoc

Take a CtLoc and moves it to the kind level

mkGivenLoc :: TcLevel -> SkolemInfoAnon -> TcLclEnv -> CtLoc

isWanted :: CtEvidence -> Bool

isGiven :: CtEvidence -> Bool

ctEvRole :: CtEvidence -> Role

Get the role relevant for a CtEvidence

setCtEvPredType :: HasDebugCallStack => CtEvidence -> Type -> CtEvidence

Set the type of CtEvidence.

This function ensures that the invariants on CtEvidence hold, by updating the evidence and the ctev_pred in sync with each other. See Note [CtEvidence invariants].

setCtEvLoc :: CtEvidence -> CtLoc -> CtEvidence

arisesFromGivens :: Ct -> Bool

tyCoVarsOfCtEvList :: CtEvidence -> [TcTyCoVar]

Returns free variables of constraints as a deterministically ordered list. See Note [Deterministic FV] in GHC.Utils.FV.

tyCoVarsOfCtEv :: CtEvidence -> TcTyCoVarSet

Returns free variables of constraints as a non-deterministic set

tyCoVarsOfCtEvsList :: [CtEvidence] -> [TcTyCoVar]

Returns free variables of a bag of constraints as a deterministically ordered list. See Note [Deterministic FV] in GHC.Utils.FV.

ctEvUnique :: CtEvidence -> Unique

tcEvDestUnique :: TcEvDest -> Unique

newtype RewriterSet

Stores a set of CoercionHoles that have been used to rewrite a constraint. See Note [Wanteds rewrite Wanteds].

Constructors

RewriterSet (UniqSet CoercionHole)

Instances

Monoid RewriterSet

Defined in GHC.Tc.Types.Constraint

Methods

mempty :: RewriterSet

mappend :: RewriterSet -> RewriterSet -> RewriterSet

mconcat :: [RewriterSet] -> RewriterSet

Semigroup RewriterSet

Defined in GHC.Tc.Types.Constraint

Methods

(<>) :: RewriterSet -> RewriterSet -> RewriterSet

sconcat :: NonEmpty RewriterSet -> RewriterSet

stimes :: Integral b => b -> RewriterSet -> RewriterSet

Outputable RewriterSet

Defined in GHC.Tc.Types.Constraint

Methods

ppr :: RewriterSet -> SDoc

emptyRewriterSet :: RewriterSet

isEmptyRewriterSet :: RewriterSet -> Bool

rewriterSetFromType :: Type -> RewriterSet

Makes a RewriterSet from all the coercion holes that occur in the given type.

rewriterSetFromTypes :: [Type] -> RewriterSet

Makes a RewriterSet from all the coercion holes that occur in the given types.

rewriterSetFromCo :: Coercion -> RewriterSet

Makes a RewriterSet from all the coercion holes that occur in the given coercion.

addRewriterSet :: RewriterSet -> CoercionHole -> RewriterSet

wrapType :: Type -> [TyVar] -> [PredType] -> Type

data CtFlavour

Constructors

Given

Wanted

Instances

Outputable CtFlavour

Defined in GHC.Tc.Types.Constraint

Methods

ppr :: CtFlavour -> SDoc

Eq CtFlavour

Defined in GHC.Tc.Types.Constraint

Methods

(==) :: CtFlavour -> CtFlavour -> Bool

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

ctEvFlavour :: CtEvidence -> CtFlavour

type CtFlavourRole = (CtFlavour, EqRel)

Whether or not one Ct can rewrite another is determined by its flavour and its equality relation. See also Note [Flavours with roles] in GHC.Tc.Solver.InertSet

ctEvFlavourRole :: CtEvidence -> CtFlavourRole

Extract the flavour, role, and boxity from a CtEvidence

ctFlavourRole :: Ct -> CtFlavourRole

Extract the flavour and role from a Ct

eqCanRewrite :: EqRel -> EqRel -> Bool

eqCanRewriteFR :: CtFlavourRole -> CtFlavourRole -> Bool

pprEvVarTheta :: [EvVar] -> SDoc

pprEvVars :: [EvVar] -> SDoc

pprEvVarWithType :: EvVar -> SDoc