Struct chalk_solve::rust_ir::AssociatedTyDatum

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

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§

source§

impl<I: Interner> AssociatedTyDatum<I>

source

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§

source§

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

source§

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

Returns a copy of the value. Read more
1.0.0 · source§

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

Performs copy-assignment from source. Read more
source§

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

source§

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

Formats the value using the given formatter. Read more
source§

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

source§

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

Feeds this value into the given Hasher. Read more
1.3.0 · source§

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

Feeds a slice of this type into the given Hasher. Read more
source§

impl<I: PartialEq + Interner> PartialEq for AssociatedTyDatum<I>

source§

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

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

fn ne(&self, other: &Rhs) -> bool

This method tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.
source§

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

source§

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

source§

fn display<'a>( &'a self, s: &'a InternalWriterState<'a, I>, ) -> DisplayRenderAsRust<'a, I, Self>
where Self: Sized,

source§

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

source§

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.

Another set of clauses we generate for each associated type is about placeholder associated types (i.e. TyKind::AssociatedType). Given

trait Foo {
    type Assoc<'a, T>: Bar<U = Ty> where WC;
}

we generate

forall<Self, 'a, T> {
    Implemented((Foo::Assoc<'a, T>)<Self>: Bar) :- WC.
    AliasEq(<<(Foo::Assoc<'a, T>)<Self>> as Bar>::U = Ty) :- WC.
}

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>).
}
source§

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

source§

fn visit_with<B>( &self, visitor: &mut dyn TypeVisitor<I, BreakTy = B>, outer_binder: DebruijnIndex, ) -> ControlFlow<B>

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.
source§

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

source§

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

Auto Trait Implementations§

§

impl<I> Freeze for AssociatedTyDatum<I>

§

impl<I> RefUnwindSafe for AssociatedTyDatum<I>

§

impl<I> Send for AssociatedTyDatum<I>

§

impl<I> Sync for AssociatedTyDatum<I>

§

impl<I> Unpin for AssociatedTyDatum<I>

§

impl<I> UnwindSafe for AssociatedTyDatum<I>

Blanket Implementations§

source§

impl<T> Any for T
where T: 'static + ?Sized,

source§

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more
source§

impl<T> Borrow<T> for T
where T: ?Sized,

source§

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more
source§

impl<T> BorrowMut<T> for T
where T: ?Sized,

source§

fn borrow_mut(&mut self) -> &mut T

Mutably borrows from an owned value. Read more
source§

impl<T> Cast for T

source§

fn cast<U>(self, interner: <U as HasInterner>::Interner) -> U
where Self: CastTo<U>, U: HasInterner,

Cast a value to type U using CastTo.
source§

impl<T> CloneToUninit for T
where T: Clone,

source§

default unsafe fn clone_to_uninit(&self, dst: *mut T)

🔬This is a nightly-only experimental API. (clone_to_uninit)
Performs copy-assignment from self to dst. Read more
§

impl<Q, K> Equivalent<K> for Q
where Q: Eq + ?Sized, K: Borrow<Q> + ?Sized,

§

fn equivalent(&self, key: &K) -> bool

Checks if this value is equivalent to the given key. Read more
§

impl<Q, K> Equivalent<K> for Q
where Q: Eq + ?Sized, K: Borrow<Q> + ?Sized,

§

fn equivalent(&self, key: &K) -> bool

Compare self to key and return true if they are equal.
source§

impl<T> From<T> for T

source§

fn from(t: T) -> T

Returns the argument unchanged.

§

impl<T> Instrument for T

§

fn instrument(self, span: Span) -> Instrumented<Self>

Instruments this type with the provided [Span], returning an Instrumented wrapper. Read more
§

fn in_current_span(self) -> Instrumented<Self>

Instruments this type with the current Span, returning an Instrumented wrapper. Read more
source§

impl<T, U> Into<U> for T
where U: From<T>,

source§

fn into(self) -> U

Calls U::from(self).

That is, this conversion is whatever the implementation of From<T> for U chooses to do.

source§

impl<T> ToOwned for T
where T: Clone,

§

type Owned = T

The resulting type after obtaining ownership.
source§

fn to_owned(&self) -> T

Creates owned data from borrowed data, usually by cloning. Read more
source§

fn clone_into(&self, target: &mut T)

Uses borrowed data to replace owned data, usually by cloning. Read more
source§

impl<T, U> TryFrom<U> for T
where U: Into<T>,

§

type Error = Infallible

The type returned in the event of a conversion error.
source§

fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>

Performs the conversion.
source§

impl<T, U> TryInto<U> for T
where U: TryFrom<T>,

§

type Error = <U as TryFrom<T>>::Error

The type returned in the event of a conversion error.
source§

fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>

Performs the conversion.
source§

impl<T, I> VisitExt<I> for T
where I: Interner, T: TypeVisitable<I>,

source§

fn has_free_vars(&self, interner: I) -> bool

Check whether there are free (non-bound) variables.
§

impl<T> WithSubscriber for T

§

fn with_subscriber<S>(self, subscriber: S) -> WithDispatch<Self>
where S: Into<Dispatch>,

Attaches the provided Subscriber to this type, returning a [WithDispatch] wrapper. Read more
§

fn with_current_subscriber(self) -> WithDispatch<Self>

Attaches the current default Subscriber to this type, returning a [WithDispatch] wrapper. Read more