A subset of predicates which can be assumed by the trait solver. They show up in
an item’s where clauses, hence the name Clause
, and may either be user-written
(such as traits) or may be inserted during lowering.
Encodes that we have to coerce from the a
type to the b
type.
A ProjectionPredicate
for an ExistentialTraitRef
.
An existential reference to a trait, where Self
is erased.
For example, the trait object Trait<'a, 'b, X, Y>
is:
Used by the new solver. Unlike a ProjectionPredicate
this can only be
proven by actually normalizing alias
.
A: B
A statement that can be proven by a trait solver. This includes things that may
show up in where clauses, such as trait predicates and projection predicates,
and also things that are emitted as part of type checking such as ObjectSafe
predicate which is emitted when a type is coerced to a trait object.
This kind of predicate has no direct correspondent in the
syntax, but it roughly corresponds to the syntactic forms:
Encodes that a
must be a subtype of b
. The a_is_expected
flag indicates
whether the a
type is the type that we should label as “expected” when
presenting user diagnostics.
A complete reference to a trait. These take numerous guises in syntax,
but perhaps the most recognizable form is in a where-clause: