EvalCtxt in rustc_next_trait_solver::solve - Rust (original) (raw)

pub struct EvalCtxt<'a, D, I = I>

where
    D: SolverDelegate<Interner = I>,
    I: Interner,

{
    delegate: &'a D,
    variables: I::CanonicalVarKinds,
    current_goal_kind: CurrentGoalKind,
    pub(super) var_values: CanonicalVarValues<I>,
    pub(super) max_input_universe: UniverseIndex,
    pub(super) initial_opaque_types_storage_num_entries: <<D as SolverDelegate>::Infcx as InferCtxtLike>::OpaqueTypeStorageEntries,
    pub(super) search_graph: &'a mut SearchGraph<SearchGraphDelegate<D>>,
    nested_goals: Vec<(GoalSource, Goal<I, I::Predicate>, Option<GoalStalledOn<I>>)>,
    pub(super) origin_span: I::Span,
    tainted: Result<(), NoSolution>,
    pub(super) inspect: ProofTreeBuilder<D>,
}

The inference context that backs (mostly) inference and placeholder terms instantiated while solving goals.

NOTE: The InferCtxt that backs the EvalCtxt is intentionally private, because the InferCtxt is much more general than EvalCtxt. Methods such as take_registered_region_obligations can mess up query responses, using At::normalize is totally wrong, calling evaluate_root_goal can cause coinductive unsoundness, etc.

Methods that are generally of use for trait solving are _intentionally_re-declared through the EvalCtxt below, often with cleaner signatures since we don’t care about things like ObligationCauses and Spans here. If some InferCtxt method is missing, please first think defensively about the method’s compatibility with this solver, or if an existing one does the job already.

The variable info for the var_values, only used to make an ambiguous response with no constraints.

What kind of goal we’re currently computing, see the enum definition for more info.

The highest universe index nameable by the caller.

When we enter a new binder inside of the query we create new universes which the caller cannot name. We have to be careful with variables from these new universes when creating the query response.

Both because these new universes can prevent us from reaching a fixpoint if we have a coinductive cycle and because that’s the only way we can return new placeholders to the caller.

The opaque types from the canonical input. We only need to return opaque types which have been added to the storage while evaluating this goal.

Source§

Source

Source§

Source

Source

Source

Source

Source

Source

Source

For some deeply nested <T>::A::B::C::D rigid associated type, we should explore the item bounds for all levels, since theassociated_type_bounds feature means that a parent associated type may carry bounds for a nested associated type.

If we have a projection, check that its self type is a rigid projection. If so, continue searching by recursively calling after normalization.

Source

Source

In coherence we have to not only care about all impls we know about, but also consider impls which may get added in a downstream or sibling crate or which an upstream impl may add in a minor release.

To do so we return a single ambiguous candidate in case such an unknown impl could apply to the current goal.

Source§

Source

Check whether we can ignore impl candidates due to specialization.

This is only necessary for feature(specialization) and seems quite ugly.

Source

Assemble and merge candidates for goals which are related to an underlying trait goal. Right now, this is normalizes-to and host effect goals.

We sadly can’t simply take all possible candidates for normalization goals and check whether they result in the same constraints. We want to make sure that trying to normalize an alias doesn’t result in constraints which aren’t otherwise required.

Most notably, when proving a trait goal by via a where-bound, we should not normalize via impls which have stricter region constraints than the where-bound:

trait Trait<'a> {
    type Assoc;
}

impl<'a, T: 'a> Trait<'a> for T {
    type Assoc = u32;
}

fn with_bound<'a, T: Trait<'a>>(_value: T::Assoc) {}

The where-bound of with_bound doesn’t specify the associated type, so we would only be able to normalize <T as Trait<'a>>::Assoc by using the impl. This impl adds a T: 'a bound however, which would result in a region error. Given that the user explicitly wrote that T: Trait<'a> holds, this is undesirable and we instead treat the alias as rigid.

See trait-system-refactor-initiative#124 for more details.

Source

Compute whether a param-env assumption is global or non-global after normalizing it.

This is necessary because, for example, given:

where
    T: Trait<Assoc = u32>,
    i32: From<T::Assoc>,

The i32: From<T::Assoc> bound is non-global before normalization, but is global after. Since the old trait solver normalized param-envs eagerly, we want to emulate this behavior lazily.

Source§

Source

Source§

Source

Canonicalizes the goal remembering the original values for each bound variable.

Source

To return the constraints of a canonical query to the caller, we canonicalize:

This takes the shallow_certainty which represents whether we’re confident that the final result of the current goal only depends on the nested goals.

In case this is Certainy::Maybe, there may still be additional nested goals or inference constraints required for this candidate to be hold. The candidate always requires all already added constraints and nested goals.

Source

Constructs a totally unconstrained, ambiguous response to a goal.

Take care when using this, since often it’s useful to respond with ambiguity but return constrained variables to guide inference.

Source

Computes the region constraints and new opaque types registered when proving a goal.

If an opaque was already constrained before proving this goal, then the external constraints do not need to record that opaque, since if it is further constrained by inference, that will be passed back in the var values.

Source

After calling a canonical query, we apply the constraints returned by the query using this function.

This happens in three steps:

Source

This returns the canonical variable values to instantiate the bound variables of the canonical response. This depends on the original_values for the bound variables.

Source

Unify the original_values with the var_values returned by the canonical query..

This assumes that this unification will always succeed. This is the case when applying a query response right away. However, calling a canonical query, doing any other kind of trait solving, and only then instantiating the result of the query can cause the instantiation to fail. This is not supported and we ICE in this case.

We always structurally instantiate aliases. Relating aliases needs to be different depending on whether the alias is rigid or not. We’re only really able to tell whether an alias is rigid by using the trait solver. When instantiating a response from the solver we assume that the solver correctly handled aliases and therefore always relate them structurally here.

Source

Source

Source§

Source

probe_kind is only called when proof tree building is enabled so it can be as expensive as necessary to output the desired information.

Source

Source

Source§

Source

Source

Computes the PathKind for the step from the current goal to the nested goal required due to source.

See #136824 for a more detailed reasoning for this behavior. We consider cycles to be coinductive if they ‘step into’ a where-clause of a coinductive trait. We will likely extend this function in the future and will need to clearly document it in the rustc-dev-guide before stabilization.

Source

Creates a root evaluation context and search graph. This should only be used from outside of any evaluation, and other methods should be preferred over using this manually (such as SolverDelegateEvalExt::evaluate_root_goal).

Source

Creates a nested evaluation context that shares the same search graph as the one passed in. This is suitable for evaluation, granted that the search graph has had the nested goal recorded on its stack (SearchGraph::with_new_goal), but it’s preferable to use other methods that call this one rather than this method directly.

This function takes care of setting up the inference context, setting the anchor, and registering opaques from the canonicalized input.

Source

Source

Recursively evaluates goal, returning whether any inference vars have been constrained and the certainty of the result.

Source

Recursively evaluates goal, returning the nested goals in case the nested goal is a NormalizesTo goal.

As all other goal kinds do not return any nested goals andNormalizesTo is only used by AliasRelate, all other callsites should use EvalCtxt::evaluate_goal which discards that empty storage.

Source

Source

Source

Iterate over all added goals: returning Ok(Some(_)) in case we can stop rerunning.

Goals for the next step get directly added to the nested goals of the EvalCtxt.

Source

Record impl args in the proof tree for later access by InspectCandidate.

Source

Source

Source

Source

Source

Source

Source

Returns a ty infer or a const infer depending on whether kind is a Ty or Const. If kind is an integer inference variable this will still return a ty infer var.

Source

Is the projection predicate is of the form exists<T> <Ty as Trait>::Assoc = T.

This is the case if the term does not occur in any other part of the predicate and is able to name all other placeholder and inference variables.

Source

Source

This should be used when relating a rigid alias with another type.

Normally we emit a nested AliasRelate when equating an inference variable and an alias. This causes us to instead constrain the inference variable to the alias without emitting a nested alias relate goals.

Source

This sohuld only be used when we’re either instantiating a previously unconstrained “return value” or when we’re sure that all aliases in the types are rigid.

Source

Source

Source

Equates two values returning the nested goals without adding them to the nested goals of the EvalCtxt.

If possible, try using eq instead which automatically handles nested goals correctly.

Source

Source

enter_forall, but takes &mut self and passes it back through the callback since it can’t be aliased during the call.

Source

Source

Source

Source

Source

Source

Computes the list of goals required for arg to be well-formed

Source

Source

Source

Source

Source

Source

Source

Source

Source§

Source

Source§

Source

Source§

Source

Source§

Source

Source§

Source

Source

When normalizing an associated item, constrain the expected term to term.

We know term to always be a fully unconstrained inference variable, soeq should never fail here. However, in case term contains aliases, we emit nested AliasRelate goals to structurally normalize the alias.

Source

Unlike instantiate_normalizes_to_term this instantiates the expected term with a rigid alias. Using this is pretty much always wrong.

Source§

Source

Source§

Source

Source§

Source

Trait upcasting allows for coercions between trait objects:

trait Super {}
trait Trait: Super {}
// results in builtin impls upcasting to a super trait
impl<'a, 'b: 'a> Unsize<dyn Super + 'a> for dyn Trait + 'b {}
// and impls removing auto trait bounds.
impl<'a, 'b: 'a> Unsize<dyn Trait + 'a> for dyn Trait + Send + 'b {}

Source

Source

Source

We have the following builtin impls for arrays:

impl<T: ?Sized, const N: usize> Unsize<[T]> for [T; N] {}

While the impl itself could theoretically not be builtin, the actual unsizing behavior is builtin. Its also easier to make all impls of Unsize builtin as we’re able to use#[rustc_deny_explicit_impl] in this case.

Source

We generate a builtin Unsize impls for structs with generic parameters only mentioned by the last field.

struct Foo<T, U: ?Sized> {
    sized_field: Vec<T>,
    unsizable: Box<U>,
}
// results in the following builtin impl
impl<T: ?Sized, U: ?Sized, V: ?Sized> Unsize<Foo<T, V>> for Foo<T, U>
where
    Box<U>: Unsize<Box<V>>,
{}

Source

Source

Convenience function for traits that are structural, i.e. that only have nested subgoals that only change the self type. Unlike other evaluate-like helpers, this does a probe, so it doesn’t need to be wrapped in one.

Source§

Source

FIXME(#57893): For backwards compatability with the old trait solver implementation, we need to handle overlap between builtin and user-written impls for trait objects.

This overlap is unsound in general and something which we intend to fix separately. To avoid blocking the stabilization of the trait solver, we add this hack to avoid breakage in cases which are _mostly fine_™. Importantly, this preference is strictly weaker than the old behavior.

We only prefer builtin over user-written impls if there are no inference constraints. Importantly, we also only prefer the builtin impls for trait goals, and not during normalization. This means the only case where this special-case results in exploitable unsoundness should be lifetime dependent user-written impls.

Source

Source

Source

Source§

Source

Source

Source

Source

Source

Source

Source

Source

Source§

Source

Try to merge multiple possible ways to prove a goal, if that is not possible returns None.

In this case we tend to flounder and return ambiguity by calling [EvalCtxt::flounder].

Source

Source

If we fail to merge responses we flounder and return overflow or ambiguity.

Source

Normalize a type for when it is structurally matched on.

This function is necessary in nearly all cases before matching on a type. Not doing so is likely to be incomplete and therefore unsound during coherence.

Source

Normalize a const for when it is structurally matched on, or more likely when it needs .try_to_* called on it (e.g. to turn it into a usize).

This function is necessary in nearly all cases before matching on a const. Not doing so is likely to be incomplete and therefore unsound during coherence.

Source

Normalize a term for when it is structurally matched on.

This function is necessary in nearly all cases before matching on a ty/const. Not doing so is likely to be incomplete and therefore unsound during coherence.

Source

Note: Unable to compute type layout, possibly due to this type having generic parameters. Layout can only be computed for concrete, fully-instantiated types.