1use std::mem;
2use std::ops::ControlFlow;
3
4#[cfg(feature = "nightly")]
5use rustc_macros::HashStable_NoContext;
6use rustc_type_ir::data_structures::{HashMap, HashSet};
7use rustc_type_ir::fast_reject::DeepRejectCtxt;
8use rustc_type_ir::inherent::*;
9use rustc_type_ir::relate::Relate;
10use rustc_type_ir::relate::solver_relating::RelateExt;
11use rustc_type_ir::search_graph::PathKind;
12use rustc_type_ir::{
13 self as ty, CanonicalVarValues, InferCtxtLike, Interner, TypeFoldable, TypeFolder,
14 TypeSuperFoldable, TypeSuperVisitable, TypeVisitable, TypeVisitableExt, TypeVisitor,
15 TypingMode,
16};
17use tracing::{debug, instrument, trace};
18
19use super::has_only_region_constraints;
20use crate::coherence;
21use crate::delegate::SolverDelegate;
22use crate::placeholder::BoundVarReplacer;
23use crate::solve::inspect::{self, ProofTreeBuilder};
24use crate::solve::search_graph::SearchGraph;
25use crate::solve::{
26 CanonicalInput, Certainty, FIXPOINT_STEP_LIMIT, Goal, GoalEvaluation, GoalEvaluationKind,
27 GoalSource, GoalStalledOn, HasChanged, NestedNormalizationGoals, NoSolution, QueryInput,
28 QueryResult,
29};
30
31pub(super) mod canonical;
32mod probe;
33
34#[derive(Debug, Copy, Clone)]
39enum CurrentGoalKind {
40 Misc,
41 CoinductiveTrait,
46 NormalizesTo,
54}
55
56impl CurrentGoalKind {
57 fn from_query_input<I: Interner>(cx: I, input: QueryInput<I, I::Predicate>) -> CurrentGoalKind {
58 match input.goal.predicate.kind().skip_binder() {
59 ty::PredicateKind::Clause(ty::ClauseKind::Trait(pred)) => {
60 if cx.trait_is_coinductive(pred.trait_ref.def_id) {
61 CurrentGoalKind::CoinductiveTrait
62 } else {
63 CurrentGoalKind::Misc
64 }
65 }
66 ty::PredicateKind::NormalizesTo(_) => CurrentGoalKind::NormalizesTo,
67 _ => CurrentGoalKind::Misc,
68 }
69 }
70}
71
72pub struct EvalCtxt<'a, D, I = <D as SolverDelegate>::Interner>
73where
74 D: SolverDelegate<Interner = I>,
75 I: Interner,
76{
77 delegate: &'a D,
93
94 variables: I::CanonicalVarKinds,
97
98 current_goal_kind: CurrentGoalKind,
101 pub(super) var_values: CanonicalVarValues<I>,
102
103 pub(super) max_input_universe: ty::UniverseIndex,
113 pub(super) initial_opaque_types_storage_num_entries:
116 <D::Infcx as InferCtxtLike>::OpaqueTypeStorageEntries,
117
118 pub(super) search_graph: &'a mut SearchGraph<D>,
119
120 nested_goals: Vec<(GoalSource, Goal<I, I::Predicate>, Option<GoalStalledOn<I>>)>,
121
122 pub(super) origin_span: I::Span,
123
124 tainted: Result<(), NoSolution>,
131
132 pub(super) inspect: ProofTreeBuilder<D>,
133}
134
135#[derive(PartialEq, Eq, Debug, Hash, Clone, Copy)]
136#[cfg_attr(feature = "nightly", derive(HashStable_NoContext))]
137pub enum GenerateProofTree {
138 Yes,
139 No,
140}
141
142pub trait SolverDelegateEvalExt: SolverDelegate {
143 fn evaluate_root_goal(
148 &self,
149 goal: Goal<Self::Interner, <Self::Interner as Interner>::Predicate>,
150 span: <Self::Interner as Interner>::Span,
151 stalled_on: Option<GoalStalledOn<Self::Interner>>,
152 ) -> Result<GoalEvaluation<Self::Interner>, NoSolution>;
153
154 fn root_goal_may_hold_with_depth(
162 &self,
163 root_depth: usize,
164 goal: Goal<Self::Interner, <Self::Interner as Interner>::Predicate>,
165 ) -> bool;
166
167 fn evaluate_root_goal_for_proof_tree(
170 &self,
171 goal: Goal<Self::Interner, <Self::Interner as Interner>::Predicate>,
172 span: <Self::Interner as Interner>::Span,
173 ) -> (
174 Result<
175 (NestedNormalizationGoals<Self::Interner>, GoalEvaluation<Self::Interner>),
176 NoSolution,
177 >,
178 inspect::GoalEvaluation<Self::Interner>,
179 );
180}
181
182impl<D, I> SolverDelegateEvalExt for D
183where
184 D: SolverDelegate<Interner = I>,
185 I: Interner,
186{
187 #[instrument(level = "debug", skip(self))]
188 fn evaluate_root_goal(
189 &self,
190 goal: Goal<I, I::Predicate>,
191 span: I::Span,
192 stalled_on: Option<GoalStalledOn<I>>,
193 ) -> Result<GoalEvaluation<I>, NoSolution> {
194 EvalCtxt::enter_root(
195 self,
196 self.cx().recursion_limit(),
197 GenerateProofTree::No,
198 span,
199 |ecx| ecx.evaluate_goal(GoalEvaluationKind::Root, GoalSource::Misc, goal, stalled_on),
200 )
201 .0
202 }
203
204 fn root_goal_may_hold_with_depth(
205 &self,
206 root_depth: usize,
207 goal: Goal<Self::Interner, <Self::Interner as Interner>::Predicate>,
208 ) -> bool {
209 self.probe(|| {
210 EvalCtxt::enter_root(self, root_depth, GenerateProofTree::No, I::Span::dummy(), |ecx| {
211 ecx.evaluate_goal(GoalEvaluationKind::Root, GoalSource::Misc, goal, None)
212 })
213 .0
214 })
215 .is_ok()
216 }
217
218 #[instrument(level = "debug", skip(self))]
219 fn evaluate_root_goal_for_proof_tree(
220 &self,
221 goal: Goal<I, I::Predicate>,
222 span: I::Span,
223 ) -> (
224 Result<(NestedNormalizationGoals<I>, GoalEvaluation<I>), NoSolution>,
225 inspect::GoalEvaluation<I>,
226 ) {
227 let (result, proof_tree) = EvalCtxt::enter_root(
228 self,
229 self.cx().recursion_limit(),
230 GenerateProofTree::Yes,
231 span,
232 |ecx| ecx.evaluate_goal_raw(GoalEvaluationKind::Root, GoalSource::Misc, goal, None),
233 );
234 (result, proof_tree.unwrap())
235 }
236}
237
238impl<'a, D, I> EvalCtxt<'a, D>
239where
240 D: SolverDelegate<Interner = I>,
241 I: Interner,
242{
243 pub(super) fn typing_mode(&self) -> TypingMode<I> {
244 self.delegate.typing_mode()
245 }
246
247 pub(super) fn step_kind_for_source(&self, source: GoalSource) -> PathKind {
256 match source {
257 GoalSource::Misc => PathKind::Unknown,
265 GoalSource::NormalizeGoal(path_kind) => path_kind,
266 GoalSource::ImplWhereBound => match self.current_goal_kind {
267 CurrentGoalKind::CoinductiveTrait => PathKind::Coinductive,
270 CurrentGoalKind::NormalizesTo => PathKind::Inductive,
278 CurrentGoalKind::Misc => PathKind::Unknown,
282 },
283 GoalSource::TypeRelating => PathKind::Inductive,
287 GoalSource::InstantiateHigherRanked => PathKind::Inductive,
290 GoalSource::AliasBoundConstCondition | GoalSource::AliasWellFormed => PathKind::Unknown,
294 }
295 }
296
297 pub(super) fn enter_root<R>(
301 delegate: &D,
302 root_depth: usize,
303 generate_proof_tree: GenerateProofTree,
304 origin_span: I::Span,
305 f: impl FnOnce(&mut EvalCtxt<'_, D>) -> R,
306 ) -> (R, Option<inspect::GoalEvaluation<I>>) {
307 let mut search_graph = SearchGraph::new(root_depth);
308
309 let mut ecx = EvalCtxt {
310 delegate,
311 search_graph: &mut search_graph,
312 nested_goals: Default::default(),
313 inspect: ProofTreeBuilder::new_maybe_root(generate_proof_tree),
314
315 max_input_universe: ty::UniverseIndex::ROOT,
318 initial_opaque_types_storage_num_entries: Default::default(),
319 variables: Default::default(),
320 var_values: CanonicalVarValues::dummy(),
321 current_goal_kind: CurrentGoalKind::Misc,
322 origin_span,
323 tainted: Ok(()),
324 };
325 let result = f(&mut ecx);
326
327 let proof_tree = ecx.inspect.finalize();
328 assert!(
329 ecx.nested_goals.is_empty(),
330 "root `EvalCtxt` should not have any goals added to it"
331 );
332
333 assert!(search_graph.is_empty());
334 (result, proof_tree)
335 }
336
337 pub(super) fn enter_canonical<R>(
345 cx: I,
346 search_graph: &'a mut SearchGraph<D>,
347 canonical_input: CanonicalInput<I>,
348 canonical_goal_evaluation: &mut ProofTreeBuilder<D>,
349 f: impl FnOnce(&mut EvalCtxt<'_, D>, Goal<I, I::Predicate>) -> R,
350 ) -> R {
351 let (ref delegate, input, var_values) = D::build_with_canonical(cx, &canonical_input);
352
353 for &(key, ty) in &input.predefined_opaques_in_body.opaque_types {
354 let prev = delegate.register_hidden_type_in_storage(key, ty, I::Span::dummy());
355 if let Some(prev) = prev {
367 debug!(?key, ?ty, ?prev, "ignore duplicate in `opaque_types_storage`");
368 }
369 }
370
371 let initial_opaque_types_storage_num_entries = delegate.opaque_types_storage_num_entries();
372 let mut ecx = EvalCtxt {
373 delegate,
374 variables: canonical_input.canonical.variables,
375 var_values,
376 current_goal_kind: CurrentGoalKind::from_query_input(cx, input),
377 max_input_universe: canonical_input.canonical.max_universe,
378 initial_opaque_types_storage_num_entries,
379 search_graph,
380 nested_goals: Default::default(),
381 origin_span: I::Span::dummy(),
382 tainted: Ok(()),
383 inspect: canonical_goal_evaluation.new_goal_evaluation_step(var_values),
384 };
385
386 let result = f(&mut ecx, input.goal);
387 ecx.inspect.probe_final_state(ecx.delegate, ecx.max_input_universe);
388 canonical_goal_evaluation.goal_evaluation_step(ecx.inspect);
389
390 delegate.reset_opaque_types();
396
397 result
398 }
399
400 fn evaluate_goal(
403 &mut self,
404 goal_evaluation_kind: GoalEvaluationKind,
405 source: GoalSource,
406 goal: Goal<I, I::Predicate>,
407 stalled_on: Option<GoalStalledOn<I>>,
408 ) -> Result<GoalEvaluation<I>, NoSolution> {
409 let (normalization_nested_goals, goal_evaluation) =
410 self.evaluate_goal_raw(goal_evaluation_kind, source, goal, stalled_on)?;
411 assert!(normalization_nested_goals.is_empty());
412 Ok(goal_evaluation)
413 }
414
415 pub(super) fn evaluate_goal_raw(
423 &mut self,
424 goal_evaluation_kind: GoalEvaluationKind,
425 source: GoalSource,
426 goal: Goal<I, I::Predicate>,
427 stalled_on: Option<GoalStalledOn<I>>,
428 ) -> Result<(NestedNormalizationGoals<I>, GoalEvaluation<I>), NoSolution> {
429 if let Some(stalled_on) = stalled_on {
433 if !stalled_on.stalled_vars.iter().any(|value| self.delegate.is_changed_arg(*value))
434 && !self
435 .delegate
436 .opaque_types_storage_num_entries()
437 .needs_reevaluation(stalled_on.num_opaques)
438 {
439 return Ok((
440 NestedNormalizationGoals::empty(),
441 GoalEvaluation {
442 certainty: Certainty::Maybe(stalled_on.stalled_cause),
443 has_changed: HasChanged::No,
444 stalled_on: Some(stalled_on),
445 },
446 ));
447 }
448 }
449
450 let (orig_values, canonical_goal) = self.canonicalize_goal(goal);
451 let mut goal_evaluation =
452 self.inspect.new_goal_evaluation(goal, &orig_values, goal_evaluation_kind);
453 let canonical_result = self.search_graph.evaluate_goal(
454 self.cx(),
455 canonical_goal,
456 self.step_kind_for_source(source),
457 &mut goal_evaluation,
458 );
459 goal_evaluation.query_result(canonical_result);
460 self.inspect.goal_evaluation(goal_evaluation);
461 let response = match canonical_result {
462 Err(e) => return Err(e),
463 Ok(response) => response,
464 };
465
466 let has_changed =
467 if !has_only_region_constraints(response) { HasChanged::Yes } else { HasChanged::No };
468
469 let (normalization_nested_goals, certainty) =
470 self.instantiate_and_apply_query_response(goal.param_env, &orig_values, response);
471
472 let stalled_on = match certainty {
483 Certainty::Yes => None,
484 Certainty::Maybe(stalled_cause) => match has_changed {
485 HasChanged::Yes => None,
490 HasChanged::No => {
491 let mut stalled_vars = orig_values;
492
493 stalled_vars.retain(|arg| match arg.kind() {
495 ty::GenericArgKind::Type(ty) => matches!(ty.kind(), ty::Infer(_)),
496 ty::GenericArgKind::Const(ct) => {
497 matches!(ct.kind(), ty::ConstKind::Infer(_))
498 }
499 ty::GenericArgKind::Lifetime(_) => false,
501 });
502
503 if let Some(normalizes_to) = goal.predicate.as_normalizes_to() {
505 let normalizes_to = normalizes_to.skip_binder();
506 let rhs_arg: I::GenericArg = normalizes_to.term.into();
507 let idx = stalled_vars
508 .iter()
509 .rposition(|arg| *arg == rhs_arg)
510 .expect("expected unconstrained arg");
511 stalled_vars.swap_remove(idx);
512 }
513
514 Some(GoalStalledOn {
515 num_opaques: canonical_goal
516 .canonical
517 .value
518 .predefined_opaques_in_body
519 .opaque_types
520 .len(),
521 stalled_vars,
522 stalled_cause,
523 })
524 }
525 },
526 };
527
528 Ok((normalization_nested_goals, GoalEvaluation { certainty, has_changed, stalled_on }))
529 }
530
531 pub(super) fn compute_goal(&mut self, goal: Goal<I, I::Predicate>) -> QueryResult<I> {
532 let Goal { param_env, predicate } = goal;
533 let kind = predicate.kind();
534 if let Some(kind) = kind.no_bound_vars() {
535 match kind {
536 ty::PredicateKind::Clause(ty::ClauseKind::Trait(predicate)) => {
537 self.compute_trait_goal(Goal { param_env, predicate }).map(|(r, _via)| r)
538 }
539 ty::PredicateKind::Clause(ty::ClauseKind::HostEffect(predicate)) => {
540 self.compute_host_effect_goal(Goal { param_env, predicate })
541 }
542 ty::PredicateKind::Clause(ty::ClauseKind::Projection(predicate)) => {
543 self.compute_projection_goal(Goal { param_env, predicate })
544 }
545 ty::PredicateKind::Clause(ty::ClauseKind::TypeOutlives(predicate)) => {
546 self.compute_type_outlives_goal(Goal { param_env, predicate })
547 }
548 ty::PredicateKind::Clause(ty::ClauseKind::RegionOutlives(predicate)) => {
549 self.compute_region_outlives_goal(Goal { param_env, predicate })
550 }
551 ty::PredicateKind::Clause(ty::ClauseKind::ConstArgHasType(ct, ty)) => {
552 self.compute_const_arg_has_type_goal(Goal { param_env, predicate: (ct, ty) })
553 }
554 ty::PredicateKind::Subtype(predicate) => {
555 self.compute_subtype_goal(Goal { param_env, predicate })
556 }
557 ty::PredicateKind::Coerce(predicate) => {
558 self.compute_coerce_goal(Goal { param_env, predicate })
559 }
560 ty::PredicateKind::DynCompatible(trait_def_id) => {
561 self.compute_dyn_compatible_goal(trait_def_id)
562 }
563 ty::PredicateKind::Clause(ty::ClauseKind::WellFormed(term)) => {
564 self.compute_well_formed_goal(Goal { param_env, predicate: term })
565 }
566 ty::PredicateKind::Clause(ty::ClauseKind::ConstEvaluatable(ct)) => {
567 self.compute_const_evaluatable_goal(Goal { param_env, predicate: ct })
568 }
569 ty::PredicateKind::ConstEquate(_, _) => {
570 panic!("ConstEquate should not be emitted when `-Znext-solver` is active")
571 }
572 ty::PredicateKind::NormalizesTo(predicate) => {
573 self.compute_normalizes_to_goal(Goal { param_env, predicate })
574 }
575 ty::PredicateKind::AliasRelate(lhs, rhs, direction) => self
576 .compute_alias_relate_goal(Goal {
577 param_env,
578 predicate: (lhs, rhs, direction),
579 }),
580 ty::PredicateKind::Ambiguous => {
581 self.evaluate_added_goals_and_make_canonical_response(Certainty::AMBIGUOUS)
582 }
583 }
584 } else {
585 self.enter_forall(kind, |ecx, kind| {
586 let goal = goal.with(ecx.cx(), ty::Binder::dummy(kind));
587 ecx.add_goal(GoalSource::InstantiateHigherRanked, goal);
588 ecx.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
589 })
590 }
591 }
592
593 #[instrument(level = "trace", skip(self))]
596 pub(super) fn try_evaluate_added_goals(&mut self) -> Result<Certainty, NoSolution> {
597 let mut response = Ok(Certainty::overflow(false));
598 for _ in 0..FIXPOINT_STEP_LIMIT {
599 match self.evaluate_added_goals_step() {
602 Ok(Some(cert)) => {
603 response = Ok(cert);
604 break;
605 }
606 Ok(None) => {}
607 Err(NoSolution) => {
608 response = Err(NoSolution);
609 break;
610 }
611 }
612 }
613
614 if response.is_err() {
615 self.tainted = Err(NoSolution);
616 }
617
618 response
619 }
620
621 fn evaluate_added_goals_step(&mut self) -> Result<Option<Certainty>, NoSolution> {
625 let cx = self.cx();
626 let mut unchanged_certainty = Some(Certainty::Yes);
628 for (source, goal, stalled_on) in mem::take(&mut self.nested_goals) {
629 if let Some(certainty) = self.delegate.compute_goal_fast_path(goal, self.origin_span) {
630 match certainty {
631 Certainty::Yes => {}
632 Certainty::Maybe(_) => {
633 self.nested_goals.push((source, goal, None));
634 unchanged_certainty = unchanged_certainty.map(|c| c.and(certainty));
635 }
636 }
637 continue;
638 }
639
640 if let Some(pred) = goal.predicate.as_normalizes_to() {
651 let pred = pred.no_bound_vars().unwrap();
653 let unconstrained_rhs = self.next_term_infer_of_kind(pred.term);
656 let unconstrained_goal =
657 goal.with(cx, ty::NormalizesTo { alias: pred.alias, term: unconstrained_rhs });
658
659 let (
660 NestedNormalizationGoals(nested_goals),
661 GoalEvaluation { certainty, stalled_on, has_changed: _ },
662 ) = self.evaluate_goal_raw(
663 GoalEvaluationKind::Nested,
664 source,
665 unconstrained_goal,
666 stalled_on,
667 )?;
668 trace!(?nested_goals);
670 self.nested_goals.extend(nested_goals.into_iter().map(|(s, g)| (s, g, None)));
671
672 self.eq_structurally_relating_aliases(
687 goal.param_env,
688 pred.term,
689 unconstrained_rhs,
690 )?;
691
692 let with_resolved_vars = self.resolve_vars_if_possible(goal);
699 if pred.alias != goal.predicate.as_normalizes_to().unwrap().skip_binder().alias {
700 unchanged_certainty = None;
701 }
702
703 match certainty {
704 Certainty::Yes => {}
705 Certainty::Maybe(_) => {
706 self.nested_goals.push((source, with_resolved_vars, stalled_on));
707 unchanged_certainty = unchanged_certainty.map(|c| c.and(certainty));
708 }
709 }
710 } else {
711 let GoalEvaluation { certainty, has_changed, stalled_on } =
712 self.evaluate_goal(GoalEvaluationKind::Nested, source, goal, stalled_on)?;
713 if has_changed == HasChanged::Yes {
714 unchanged_certainty = None;
715 }
716
717 match certainty {
718 Certainty::Yes => {}
719 Certainty::Maybe(_) => {
720 self.nested_goals.push((source, goal, stalled_on));
721 unchanged_certainty = unchanged_certainty.map(|c| c.and(certainty));
722 }
723 }
724 }
725 }
726
727 Ok(unchanged_certainty)
728 }
729
730 pub(crate) fn record_impl_args(&mut self, impl_args: I::GenericArgs) {
732 self.inspect.record_impl_args(self.delegate, self.max_input_universe, impl_args)
733 }
734
735 pub(super) fn cx(&self) -> I {
736 self.delegate.cx()
737 }
738
739 #[instrument(level = "debug", skip(self))]
740 pub(super) fn add_goal(&mut self, source: GoalSource, mut goal: Goal<I, I::Predicate>) {
741 goal.predicate =
742 goal.predicate.fold_with(&mut ReplaceAliasWithInfer::new(self, source, goal.param_env));
743 self.inspect.add_goal(self.delegate, self.max_input_universe, source, goal);
744 self.nested_goals.push((source, goal, None));
745 }
746
747 #[instrument(level = "trace", skip(self, goals))]
748 pub(super) fn add_goals(
749 &mut self,
750 source: GoalSource,
751 goals: impl IntoIterator<Item = Goal<I, I::Predicate>>,
752 ) {
753 for goal in goals {
754 self.add_goal(source, goal);
755 }
756 }
757
758 pub(super) fn next_region_var(&mut self) -> I::Region {
759 let region = self.delegate.next_region_infer();
760 self.inspect.add_var_value(region);
761 region
762 }
763
764 pub(super) fn next_ty_infer(&mut self) -> I::Ty {
765 let ty = self.delegate.next_ty_infer();
766 self.inspect.add_var_value(ty);
767 ty
768 }
769
770 pub(super) fn next_const_infer(&mut self) -> I::Const {
771 let ct = self.delegate.next_const_infer();
772 self.inspect.add_var_value(ct);
773 ct
774 }
775
776 pub(super) fn next_term_infer_of_kind(&mut self, term: I::Term) -> I::Term {
779 match term.kind() {
780 ty::TermKind::Ty(_) => self.next_ty_infer().into(),
781 ty::TermKind::Const(_) => self.next_const_infer().into(),
782 }
783 }
784
785 #[instrument(level = "trace", skip(self), ret)]
790 pub(super) fn term_is_fully_unconstrained(&self, goal: Goal<I, ty::NormalizesTo<I>>) -> bool {
791 let universe_of_term = match goal.predicate.term.kind() {
792 ty::TermKind::Ty(ty) => {
793 if let ty::Infer(ty::TyVar(vid)) = ty.kind() {
794 self.delegate.universe_of_ty(vid).unwrap()
795 } else {
796 return false;
797 }
798 }
799 ty::TermKind::Const(ct) => {
800 if let ty::ConstKind::Infer(ty::InferConst::Var(vid)) = ct.kind() {
801 self.delegate.universe_of_ct(vid).unwrap()
802 } else {
803 return false;
804 }
805 }
806 };
807
808 struct ContainsTermOrNotNameable<'a, D: SolverDelegate<Interner = I>, I: Interner> {
809 term: I::Term,
810 universe_of_term: ty::UniverseIndex,
811 delegate: &'a D,
812 cache: HashSet<I::Ty>,
813 }
814
815 impl<D: SolverDelegate<Interner = I>, I: Interner> ContainsTermOrNotNameable<'_, D, I> {
816 fn check_nameable(&self, universe: ty::UniverseIndex) -> ControlFlow<()> {
817 if self.universe_of_term.can_name(universe) {
818 ControlFlow::Continue(())
819 } else {
820 ControlFlow::Break(())
821 }
822 }
823 }
824
825 impl<D: SolverDelegate<Interner = I>, I: Interner> TypeVisitor<I>
826 for ContainsTermOrNotNameable<'_, D, I>
827 {
828 type Result = ControlFlow<()>;
829 fn visit_ty(&mut self, t: I::Ty) -> Self::Result {
830 if self.cache.contains(&t) {
831 return ControlFlow::Continue(());
832 }
833
834 match t.kind() {
835 ty::Infer(ty::TyVar(vid)) => {
836 if let ty::TermKind::Ty(term) = self.term.kind() {
837 if let ty::Infer(ty::TyVar(term_vid)) = term.kind() {
838 if self.delegate.root_ty_var(vid)
839 == self.delegate.root_ty_var(term_vid)
840 {
841 return ControlFlow::Break(());
842 }
843 }
844 }
845
846 self.check_nameable(self.delegate.universe_of_ty(vid).unwrap())?;
847 }
848 ty::Placeholder(p) => self.check_nameable(p.universe())?,
849 _ => {
850 if t.has_non_region_infer() || t.has_placeholders() {
851 t.super_visit_with(self)?
852 }
853 }
854 }
855
856 assert!(self.cache.insert(t));
857 ControlFlow::Continue(())
858 }
859
860 fn visit_const(&mut self, c: I::Const) -> Self::Result {
861 match c.kind() {
862 ty::ConstKind::Infer(ty::InferConst::Var(vid)) => {
863 if let ty::TermKind::Const(term) = self.term.kind() {
864 if let ty::ConstKind::Infer(ty::InferConst::Var(term_vid)) = term.kind()
865 {
866 if self.delegate.root_const_var(vid)
867 == self.delegate.root_const_var(term_vid)
868 {
869 return ControlFlow::Break(());
870 }
871 }
872 }
873
874 self.check_nameable(self.delegate.universe_of_ct(vid).unwrap())
875 }
876 ty::ConstKind::Placeholder(p) => self.check_nameable(p.universe()),
877 _ => {
878 if c.has_non_region_infer() || c.has_placeholders() {
879 c.super_visit_with(self)
880 } else {
881 ControlFlow::Continue(())
882 }
883 }
884 }
885 }
886
887 fn visit_predicate(&mut self, p: I::Predicate) -> Self::Result {
888 if p.has_non_region_infer() || p.has_placeholders() {
889 p.super_visit_with(self)
890 } else {
891 ControlFlow::Continue(())
892 }
893 }
894
895 fn visit_clauses(&mut self, c: I::Clauses) -> Self::Result {
896 if c.has_non_region_infer() || c.has_placeholders() {
897 c.super_visit_with(self)
898 } else {
899 ControlFlow::Continue(())
900 }
901 }
902 }
903
904 let mut visitor = ContainsTermOrNotNameable {
905 delegate: self.delegate,
906 universe_of_term,
907 term: goal.predicate.term,
908 cache: Default::default(),
909 };
910 goal.predicate.alias.visit_with(&mut visitor).is_continue()
911 && goal.param_env.visit_with(&mut visitor).is_continue()
912 }
913
914 #[instrument(level = "trace", skip(self, param_env), ret)]
915 pub(super) fn eq<T: Relate<I>>(
916 &mut self,
917 param_env: I::ParamEnv,
918 lhs: T,
919 rhs: T,
920 ) -> Result<(), NoSolution> {
921 self.relate(param_env, lhs, ty::Variance::Invariant, rhs)
922 }
923
924 #[instrument(level = "trace", skip(self, param_env), ret)]
930 pub(super) fn relate_rigid_alias_non_alias(
931 &mut self,
932 param_env: I::ParamEnv,
933 alias: ty::AliasTerm<I>,
934 variance: ty::Variance,
935 term: I::Term,
936 ) -> Result<(), NoSolution> {
937 if term.is_infer() {
940 let cx = self.cx();
941 let identity_args = self.fresh_args_for_item(alias.def_id);
950 let rigid_ctor = ty::AliasTerm::new_from_args(cx, alias.def_id, identity_args);
951 let ctor_term = rigid_ctor.to_term(cx);
952 let obligations = self.delegate.eq_structurally_relating_aliases(
953 param_env,
954 term,
955 ctor_term,
956 self.origin_span,
957 )?;
958 debug_assert!(obligations.is_empty());
959 self.relate(param_env, alias, variance, rigid_ctor)
960 } else {
961 Err(NoSolution)
962 }
963 }
964
965 #[instrument(level = "trace", skip(self, param_env), ret)]
969 pub(super) fn eq_structurally_relating_aliases<T: Relate<I>>(
970 &mut self,
971 param_env: I::ParamEnv,
972 lhs: T,
973 rhs: T,
974 ) -> Result<(), NoSolution> {
975 let result = self.delegate.eq_structurally_relating_aliases(
976 param_env,
977 lhs,
978 rhs,
979 self.origin_span,
980 )?;
981 assert_eq!(result, vec![]);
982 Ok(())
983 }
984
985 #[instrument(level = "trace", skip(self, param_env), ret)]
986 pub(super) fn sub<T: Relate<I>>(
987 &mut self,
988 param_env: I::ParamEnv,
989 sub: T,
990 sup: T,
991 ) -> Result<(), NoSolution> {
992 self.relate(param_env, sub, ty::Variance::Covariant, sup)
993 }
994
995 #[instrument(level = "trace", skip(self, param_env), ret)]
996 pub(super) fn relate<T: Relate<I>>(
997 &mut self,
998 param_env: I::ParamEnv,
999 lhs: T,
1000 variance: ty::Variance,
1001 rhs: T,
1002 ) -> Result<(), NoSolution> {
1003 let goals = self.delegate.relate(param_env, lhs, variance, rhs, self.origin_span)?;
1004 for &goal in goals.iter() {
1005 let source = match goal.predicate.kind().skip_binder() {
1006 ty::PredicateKind::Subtype { .. } | ty::PredicateKind::AliasRelate(..) => {
1007 GoalSource::TypeRelating
1008 }
1009 ty::PredicateKind::Clause(ty::ClauseKind::WellFormed(_)) => GoalSource::Misc,
1011 p => unreachable!("unexpected nested goal in `relate`: {p:?}"),
1012 };
1013 self.add_goal(source, goal);
1014 }
1015 Ok(())
1016 }
1017
1018 #[instrument(level = "trace", skip(self, param_env), ret)]
1024 pub(super) fn eq_and_get_goals<T: Relate<I>>(
1025 &self,
1026 param_env: I::ParamEnv,
1027 lhs: T,
1028 rhs: T,
1029 ) -> Result<Vec<Goal<I, I::Predicate>>, NoSolution> {
1030 Ok(self.delegate.relate(param_env, lhs, ty::Variance::Invariant, rhs, self.origin_span)?)
1031 }
1032
1033 pub(super) fn instantiate_binder_with_infer<T: TypeFoldable<I> + Copy>(
1034 &self,
1035 value: ty::Binder<I, T>,
1036 ) -> T {
1037 self.delegate.instantiate_binder_with_infer(value)
1038 }
1039
1040 pub(super) fn enter_forall<T: TypeFoldable<I>, U>(
1043 &mut self,
1044 value: ty::Binder<I, T>,
1045 f: impl FnOnce(&mut Self, T) -> U,
1046 ) -> U {
1047 self.delegate.enter_forall(value, |value| f(self, value))
1048 }
1049
1050 pub(super) fn resolve_vars_if_possible<T>(&self, value: T) -> T
1051 where
1052 T: TypeFoldable<I>,
1053 {
1054 self.delegate.resolve_vars_if_possible(value)
1055 }
1056
1057 pub(super) fn eager_resolve_region(&self, r: I::Region) -> I::Region {
1058 if let ty::ReVar(vid) = r.kind() {
1059 self.delegate.opportunistic_resolve_lt_var(vid)
1060 } else {
1061 r
1062 }
1063 }
1064
1065 pub(super) fn fresh_args_for_item(&mut self, def_id: I::DefId) -> I::GenericArgs {
1066 let args = self.delegate.fresh_args_for_item(def_id);
1067 for arg in args.iter() {
1068 self.inspect.add_var_value(arg);
1069 }
1070 args
1071 }
1072
1073 pub(super) fn register_ty_outlives(&self, ty: I::Ty, lt: I::Region) {
1074 self.delegate.register_ty_outlives(ty, lt, self.origin_span);
1075 }
1076
1077 pub(super) fn register_region_outlives(&self, a: I::Region, b: I::Region) {
1078 self.delegate.sub_regions(b, a, self.origin_span);
1080 }
1081
1082 pub(super) fn well_formed_goals(
1084 &self,
1085 param_env: I::ParamEnv,
1086 term: I::Term,
1087 ) -> Option<Vec<Goal<I, I::Predicate>>> {
1088 self.delegate.well_formed_goals(param_env, term)
1089 }
1090
1091 pub(super) fn trait_ref_is_knowable(
1092 &mut self,
1093 param_env: I::ParamEnv,
1094 trait_ref: ty::TraitRef<I>,
1095 ) -> Result<bool, NoSolution> {
1096 let delegate = self.delegate;
1097 let lazily_normalize_ty = |ty| self.structurally_normalize_ty(param_env, ty);
1098 coherence::trait_ref_is_knowable(&**delegate, trait_ref, lazily_normalize_ty)
1099 .map(|is_knowable| is_knowable.is_ok())
1100 }
1101
1102 pub(super) fn fetch_eligible_assoc_item(
1103 &self,
1104 goal_trait_ref: ty::TraitRef<I>,
1105 trait_assoc_def_id: I::DefId,
1106 impl_def_id: I::DefId,
1107 ) -> Result<Option<I::DefId>, I::ErrorGuaranteed> {
1108 self.delegate.fetch_eligible_assoc_item(goal_trait_ref, trait_assoc_def_id, impl_def_id)
1109 }
1110
1111 pub(super) fn register_hidden_type_in_storage(
1112 &mut self,
1113 opaque_type_key: ty::OpaqueTypeKey<I>,
1114 hidden_ty: I::Ty,
1115 ) -> Option<I::Ty> {
1116 self.delegate.register_hidden_type_in_storage(opaque_type_key, hidden_ty, self.origin_span)
1117 }
1118
1119 pub(super) fn add_item_bounds_for_hidden_type(
1120 &mut self,
1121 opaque_def_id: I::DefId,
1122 opaque_args: I::GenericArgs,
1123 param_env: I::ParamEnv,
1124 hidden_ty: I::Ty,
1125 ) {
1126 let mut goals = Vec::new();
1127 self.delegate.add_item_bounds_for_hidden_type(
1128 opaque_def_id,
1129 opaque_args,
1130 param_env,
1131 hidden_ty,
1132 &mut goals,
1133 );
1134 self.add_goals(GoalSource::AliasWellFormed, goals);
1135 }
1136
1137 pub(super) fn probe_existing_opaque_ty(
1140 &mut self,
1141 key: ty::OpaqueTypeKey<I>,
1142 ) -> Option<(ty::OpaqueTypeKey<I>, I::Ty)> {
1143 let duplicate_entries = self.delegate.clone_duplicate_opaque_types();
1146 assert!(duplicate_entries.is_empty(), "unexpected duplicates: {duplicate_entries:?}");
1147 let mut matching = self.delegate.clone_opaque_types_lookup_table().into_iter().filter(
1148 |(candidate_key, _)| {
1149 candidate_key.def_id == key.def_id
1150 && DeepRejectCtxt::relate_rigid_rigid(self.cx())
1151 .args_may_unify(candidate_key.args, key.args)
1152 },
1153 );
1154 let first = matching.next();
1155 let second = matching.next();
1156 assert_eq!(second, None);
1157 first
1158 }
1159
1160 pub(super) fn evaluate_const(
1164 &self,
1165 param_env: I::ParamEnv,
1166 uv: ty::UnevaluatedConst<I>,
1167 ) -> Option<I::Const> {
1168 self.delegate.evaluate_const(param_env, uv)
1169 }
1170
1171 pub(super) fn is_transmutable(
1172 &mut self,
1173 dst: I::Ty,
1174 src: I::Ty,
1175 assume: I::Const,
1176 ) -> Result<Certainty, NoSolution> {
1177 self.delegate.is_transmutable(dst, src, assume)
1178 }
1179
1180 pub(super) fn replace_bound_vars<T: TypeFoldable<I>>(
1181 &self,
1182 t: T,
1183 universes: &mut Vec<Option<ty::UniverseIndex>>,
1184 ) -> T {
1185 BoundVarReplacer::replace_bound_vars(&**self.delegate, universes, t).0
1186 }
1187}
1188
1189struct ReplaceAliasWithInfer<'me, 'a, D, I>
1204where
1205 D: SolverDelegate<Interner = I>,
1206 I: Interner,
1207{
1208 ecx: &'me mut EvalCtxt<'a, D>,
1209 param_env: I::ParamEnv,
1210 normalization_goal_source: GoalSource,
1211 cache: HashMap<I::Ty, I::Ty>,
1212}
1213
1214impl<'me, 'a, D, I> ReplaceAliasWithInfer<'me, 'a, D, I>
1215where
1216 D: SolverDelegate<Interner = I>,
1217 I: Interner,
1218{
1219 fn new(
1220 ecx: &'me mut EvalCtxt<'a, D>,
1221 for_goal_source: GoalSource,
1222 param_env: I::ParamEnv,
1223 ) -> Self {
1224 let step_kind = ecx.step_kind_for_source(for_goal_source);
1225 ReplaceAliasWithInfer {
1226 ecx,
1227 param_env,
1228 normalization_goal_source: GoalSource::NormalizeGoal(step_kind),
1229 cache: Default::default(),
1230 }
1231 }
1232}
1233
1234impl<D, I> TypeFolder<I> for ReplaceAliasWithInfer<'_, '_, D, I>
1235where
1236 D: SolverDelegate<Interner = I>,
1237 I: Interner,
1238{
1239 fn cx(&self) -> I {
1240 self.ecx.cx()
1241 }
1242
1243 fn fold_ty(&mut self, ty: I::Ty) -> I::Ty {
1244 match ty.kind() {
1245 ty::Alias(..) if !ty.has_escaping_bound_vars() => {
1246 let infer_ty = self.ecx.next_ty_infer();
1247 let normalizes_to = ty::PredicateKind::AliasRelate(
1248 ty.into(),
1249 infer_ty.into(),
1250 ty::AliasRelationDirection::Equate,
1251 );
1252 self.ecx.add_goal(
1253 self.normalization_goal_source,
1254 Goal::new(self.cx(), self.param_env, normalizes_to),
1255 );
1256 infer_ty
1257 }
1258 _ => {
1259 if !ty.has_aliases() {
1260 ty
1261 } else if let Some(&entry) = self.cache.get(&ty) {
1262 return entry;
1263 } else {
1264 let res = ty.super_fold_with(self);
1265 assert!(self.cache.insert(ty, res).is_none());
1266 res
1267 }
1268 }
1269 }
1270 }
1271
1272 fn fold_const(&mut self, ct: I::Const) -> I::Const {
1273 match ct.kind() {
1274 ty::ConstKind::Unevaluated(..) if !ct.has_escaping_bound_vars() => {
1275 let infer_ct = self.ecx.next_const_infer();
1276 let normalizes_to = ty::PredicateKind::AliasRelate(
1277 ct.into(),
1278 infer_ct.into(),
1279 ty::AliasRelationDirection::Equate,
1280 );
1281 self.ecx.add_goal(
1282 self.normalization_goal_source,
1283 Goal::new(self.cx(), self.param_env, normalizes_to),
1284 );
1285 infer_ct
1286 }
1287 _ => ct.super_fold_with(self),
1288 }
1289 }
1290
1291 fn fold_predicate(&mut self, predicate: I::Predicate) -> I::Predicate {
1292 if predicate.allow_normalization() { predicate.super_fold_with(self) } else { predicate }
1293 }
1294}