rustc_next_trait_solver/solve/
search_graph.rs

1use std::convert::Infallible;
2use std::marker::PhantomData;
3
4use rustc_type_ir::data_structures::ensure_sufficient_stack;
5use rustc_type_ir::search_graph::{self, PathKind};
6use rustc_type_ir::solve::{CanonicalInput, Certainty, NoSolution, QueryResult};
7use rustc_type_ir::{Interner, TypingMode};
8
9use crate::delegate::SolverDelegate;
10use crate::solve::inspect::ProofTreeBuilder;
11use crate::solve::{EvalCtxt, FIXPOINT_STEP_LIMIT, has_no_inference_or_external_constraints};
12
13/// This type is never constructed. We only use it to implement `search_graph::Delegate`
14/// for all types which impl `SolverDelegate` and doing it directly fails in coherence.
15pub(super) struct SearchGraphDelegate<D: SolverDelegate> {
16    _marker: PhantomData<D>,
17}
18pub(super) type SearchGraph<D> = search_graph::SearchGraph<SearchGraphDelegate<D>>;
19impl<D, I> search_graph::Delegate for SearchGraphDelegate<D>
20where
21    D: SolverDelegate<Interner = I>,
22    I: Interner,
23{
24    type Cx = D::Interner;
25
26    const ENABLE_PROVISIONAL_CACHE: bool = true;
27    type ValidationScope = Infallible;
28    fn enter_validation_scope(
29        _cx: Self::Cx,
30        _input: CanonicalInput<I>,
31    ) -> Option<Self::ValidationScope> {
32        None
33    }
34
35    const FIXPOINT_STEP_LIMIT: usize = FIXPOINT_STEP_LIMIT;
36
37    type ProofTreeBuilder = ProofTreeBuilder<D>;
38    fn inspect_is_noop(inspect: &mut Self::ProofTreeBuilder) -> bool {
39        inspect.is_noop()
40    }
41
42    const DIVIDE_AVAILABLE_DEPTH_ON_OVERFLOW: usize = 4;
43
44    fn initial_provisional_result(
45        cx: I,
46        kind: PathKind,
47        input: CanonicalInput<I>,
48    ) -> QueryResult<I> {
49        match kind {
50            PathKind::Coinductive => response_no_constraints(cx, input, Certainty::Yes),
51            PathKind::Unknown => response_no_constraints(cx, input, Certainty::overflow(false)),
52            // Even though we know these cycles to be unproductive, we still return
53            // overflow during coherence. This is both as we are not 100% confident in
54            // the implementation yet and any incorrect errors would be unsound there.
55            // The affected cases are also fairly artificial and not necessarily desirable
56            // so keeping this as ambiguity is fine for now.
57            //
58            // See `tests/ui/traits/next-solver/cycles/unproductive-in-coherence.rs` for an
59            // example where this would matter. We likely should change these cycles to `NoSolution`
60            // even in coherence once this is a bit more settled.
61            PathKind::Inductive => match input.typing_mode {
62                TypingMode::Coherence => {
63                    response_no_constraints(cx, input, Certainty::overflow(false))
64                }
65                TypingMode::Analysis { .. }
66                | TypingMode::Borrowck { .. }
67                | TypingMode::PostBorrowckAnalysis { .. }
68                | TypingMode::PostAnalysis => Err(NoSolution),
69            },
70        }
71    }
72
73    fn is_initial_provisional_result(
74        cx: Self::Cx,
75        kind: PathKind,
76        input: CanonicalInput<I>,
77        result: QueryResult<I>,
78    ) -> bool {
79        Self::initial_provisional_result(cx, kind, input) == result
80    }
81
82    fn on_stack_overflow(
83        cx: I,
84        input: CanonicalInput<I>,
85        inspect: &mut ProofTreeBuilder<D>,
86    ) -> QueryResult<I> {
87        inspect.canonical_goal_evaluation_overflow();
88        response_no_constraints(cx, input, Certainty::overflow(true))
89    }
90
91    fn on_fixpoint_overflow(cx: I, input: CanonicalInput<I>) -> QueryResult<I> {
92        response_no_constraints(cx, input, Certainty::overflow(false))
93    }
94
95    fn is_ambiguous_result(result: QueryResult<I>) -> bool {
96        result.is_ok_and(|response| {
97            has_no_inference_or_external_constraints(response)
98                && matches!(response.value.certainty, Certainty::Maybe(_))
99        })
100    }
101
102    fn propagate_ambiguity(
103        cx: I,
104        for_input: CanonicalInput<I>,
105        from_result: QueryResult<I>,
106    ) -> QueryResult<I> {
107        let certainty = from_result.unwrap().value.certainty;
108        response_no_constraints(cx, for_input, certainty)
109    }
110
111    fn compute_goal(
112        search_graph: &mut SearchGraph<D>,
113        cx: I,
114        input: CanonicalInput<I>,
115        inspect: &mut Self::ProofTreeBuilder,
116    ) -> QueryResult<I> {
117        ensure_sufficient_stack(|| {
118            EvalCtxt::enter_canonical(cx, search_graph, input, inspect, |ecx, goal| {
119                let result = ecx.compute_goal(goal);
120                ecx.inspect.query_result(result);
121                result
122            })
123        })
124    }
125}
126
127fn response_no_constraints<I: Interner>(
128    cx: I,
129    input: CanonicalInput<I>,
130    certainty: Certainty,
131) -> QueryResult<I> {
132    Ok(super::response_no_constraints_raw(
133        cx,
134        input.canonical.max_universe,
135        input.canonical.variables,
136        certainty,
137    ))
138}