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