Struct chalk_solve::rust_ir::AssociatedTyDatum

pub struct AssociatedTyDatum<I: Interner> {
    pub trait_id: TraitId<I>,
    pub id: AssocTypeId<I>,
    pub name: I::Identifier,
    pub binders: Binders<AssociatedTyDatumBound<I>>,
}

Represents an associated type declaration found inside of a trait:

trait Foo<P1..Pn> { // P0 is Self
    type Bar<Pn..Pm>: [bounds]
    where
        [where_clauses];
}

The meaning of each of these parts:

• The parameters P0...Pm are all in scope for this associated type.
• The bounds bounds are things that the impl must prove to be true.
• The where clauses where_clauses are things that the impl can assume to be true (but which projectors must prove).

Fields

trait_id: TraitId<I>

The trait this associated type is defined in.

id: AssocTypeId<I>

The ID of this associated type

name: I::Identifier

Name of this associated type.

binders: Binders<AssociatedTyDatumBound<I>>

These binders represent the P0...Pm variables. The binders are in the order [Pn..Pm; P0..Pn]. That is, the variables from Bar come first (corresponding to the de bruijn concept that "inner" binders are lower indices, although within a given binder we do not have an ordering).

Implementations

impl<I: Interner> AssociatedTyDatum<I>

pub fn bounds_on_self(&self, interner: &I) -> Vec<QuantifiedWhereClause<I>>

Returns the associated ty's bounds applied to the projection type, e.g.:

Implemented(<?0 as Foo>::Item<?1>: Sized)

these quantified where clauses are in the scope of the binders field.

Trait Implementations

impl<I: Clone + Interner> Clone for AssociatedTyDatum<I> where
    I::Identifier: Clone, 

fn clone(&self) -> AssociatedTyDatum<I>

Returns a copy of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl<I: Debug + Interner> Debug for AssociatedTyDatum<I> where
    I::Identifier: Debug, 

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl<I: Eq + Interner> Eq for AssociatedTyDatum<I> where
    I::Identifier: Eq, 

impl<I: Hash + Interner> Hash for AssociatedTyDatum<I> where
    I::Identifier: Hash, 

fn hash<__H: Hasher>(&self, state: &mut __H)

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H) where
    H: Hasher, 

Feeds a slice of this type into the given Hasher.

impl<I: PartialEq + Interner> PartialEq<AssociatedTyDatum<I>> for AssociatedTyDatum<I> where
    I::Identifier: PartialEq, 

fn eq(&self, other: &AssociatedTyDatum<I>) -> bool

This method tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &AssociatedTyDatum<I>) -> bool

This method tests for !=.

impl<I: Interner> StructuralEq for AssociatedTyDatum<I>

impl<I: Interner> StructuralPartialEq for AssociatedTyDatum<I>

impl<I: Interner> ToProgramClauses<I> for AssociatedTyDatum<I>

fn to_program_clauses(
    &self,
    builder: &mut ClauseBuilder<'_, I>,
    _environment: &Environment<I>
)

For each associated type, we define the "projection equality" rules. There are always two; one for a successful normalization, and one for the "fallback" notion of equality.

Given: (here, 'a and T represent zero or more parameters)

trait Foo {
    type Assoc<'a, T>: Bounds where WC;
}

we generate the 'fallback' rule:

-- Rule AliasEq-Placeholder
forall<Self, 'a, T> {
    AliasEq(<Self as Foo>::Assoc<'a, T> = (Foo::Assoc<'a, T>)<Self>).
}

and

-- Rule AliasEq-Normalize
forall<Self, 'a, T, U> {
    AliasEq(<T as Foo>::Assoc<'a, T> = U) :-
        Normalize(<T as Foo>::Assoc -> U).
}

We used to generate an "elaboration" rule like this:

forall<T> {
    T: Foo :- exists<U> { AliasEq(<T as Foo>::Assoc = U) }.
}

but this caused problems with the recursive solver. In particular, whenever normalization is possible, we cannot solve that projection uniquely, since we can now elaborate AliasEq to fallback or normalize it. So instead we handle this kind of reasoning through the FromEnv predicate.

We also generate rules specific to WF requirements and implied bounds:

-- Rule WellFormed-AssocTy
forall<Self, 'a, T> {
    WellFormed((Foo::Assoc)<Self, 'a, T>) :- WellFormed(Self: Foo), WellFormed(WC).
}

-- Rule Implied-WC-From-AssocTy
forall<Self, 'a, T> {
    FromEnv(WC) :- FromEnv((Foo::Assoc)<Self, 'a, T>).
}

-- Rule Implied-Bound-From-AssocTy
forall<Self, 'a, T> {
    FromEnv(<Self as Foo>::Assoc<'a,T>: Bounds) :- FromEnv(Self: Foo), WC.
}

-- Rule Implied-Trait-From-AssocTy
forall<Self,'a, T> {
    FromEnv(Self: Foo) :- FromEnv((Foo::Assoc)<Self, 'a,T>).
}

impl<I: Interner> Visit<I> for AssociatedTyDatum<I>

fn visit_with<'i, R: VisitResult>(
    &self,
    visitor: &mut dyn Visitor<'i, I, Result = R>,
    outer_binder: DebruijnIndex
) -> R where
    I: 'i, 

Apply the given visitor visitor to self; binders is the number of binders that are in scope when beginning the visitor. Typically binders starts as 0, but is adjusted when we encounter Binders<T> in the IR or other similar constructs.