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 | PathKind::ForcedAmbiguity => {
52                response_no_constraints(cx, input, Certainty::overflow(false))
53            }
54            // Even though we know these cycles to be unproductive, we still return
55            // overflow during coherence. This is both as we are not 100% confident in
56            // the implementation yet and any incorrect errors would be unsound there.
57            // The affected cases are also fairly artificial and not necessarily desirable
58            // so keeping this as ambiguity is fine for now.
59            //
60            // See `tests/ui/traits/next-solver/cycles/unproductive-in-coherence.rs` for an
61            // example where this would matter. We likely should change these cycles to `NoSolution`
62            // even in coherence once this is a bit more settled.
63            PathKind::Inductive => match input.typing_mode {
64                TypingMode::Coherence => {
65                    response_no_constraints(cx, input, Certainty::overflow(false))
66                }
67                TypingMode::Analysis { .. }
68                | TypingMode::Borrowck { .. }
69                | TypingMode::PostBorrowckAnalysis { .. }
70                | TypingMode::PostAnalysis => Err(NoSolution),
71            },
72        }
73    }
74
75    fn is_initial_provisional_result(
76        cx: Self::Cx,
77        kind: PathKind,
78        input: CanonicalInput<I>,
79        result: QueryResult<I>,
80    ) -> bool {
81        Self::initial_provisional_result(cx, kind, input) == result
82    }
83
84    fn on_stack_overflow(
85        cx: I,
86        input: CanonicalInput<I>,
87        inspect: &mut ProofTreeBuilder<D>,
88    ) -> QueryResult<I> {
89        inspect.canonical_goal_evaluation_overflow();
90        response_no_constraints(cx, input, Certainty::overflow(true))
91    }
92
93    fn on_fixpoint_overflow(cx: I, input: CanonicalInput<I>) -> QueryResult<I> {
94        response_no_constraints(cx, input, Certainty::overflow(false))
95    }
96
97    fn is_ambiguous_result(result: QueryResult<I>) -> bool {
98        result.is_ok_and(|response| {
99            has_no_inference_or_external_constraints(response)
100                && matches!(response.value.certainty, Certainty::Maybe(_))
101        })
102    }
103
104    fn propagate_ambiguity(
105        cx: I,
106        for_input: CanonicalInput<I>,
107        from_result: QueryResult<I>,
108    ) -> QueryResult<I> {
109        let certainty = from_result.unwrap().value.certainty;
110        response_no_constraints(cx, for_input, certainty)
111    }
112
113    fn compute_goal(
114        search_graph: &mut SearchGraph<D>,
115        cx: I,
116        input: CanonicalInput<I>,
117        inspect: &mut Self::ProofTreeBuilder,
118    ) -> QueryResult<I> {
119        ensure_sufficient_stack(|| {
120            EvalCtxt::enter_canonical(cx, search_graph, input, inspect, |ecx, goal| {
121                let result = ecx.compute_goal(goal);
122                ecx.inspect.query_result(result);
123                result
124            })
125        })
126    }
127}
128
129fn response_no_constraints<I: Interner>(
130    cx: I,
131    input: CanonicalInput<I>,
132    certainty: Certainty,
133) -> QueryResult<I> {
134    Ok(super::response_no_constraints_raw(
135        cx,
136        input.canonical.max_universe,
137        input.canonical.variables,
138        certainty,
139    ))
140}