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