hax_frontend_exporter/traits/
resolution.rs

1//! Trait resolution: given a trait reference, we track which local clause caused it to be true.
2//! This module is independent from the rest of hax, in particular it doesn't use its
3//! state-tracking machinery.
4
5use hax_frontend_exporter_options::BoundsOptions;
6use itertools::{Either, Itertools};
7use std::collections::{HashMap, hash_map::Entry};
8
9use rustc_hir::def::DefKind;
10use rustc_hir::def_id::DefId;
11use rustc_middle::traits::CodegenObligationError;
12use rustc_middle::ty::{self, *};
13use rustc_trait_selection::traits::ImplSource;
14
15use super::utils::{
16    self, ToPolyTraitRef, erase_and_norm, implied_predicates, normalize_bound_val,
17    required_predicates, self_predicate, type_alias_implied_predicates,
18};
19
20#[derive(Debug, Clone)]
21pub enum PathChunk<'tcx> {
22    AssocItem {
23        item: AssocItem,
24        /// The arguments provided to the item (for GATs). Includes trait args.
25        generic_args: GenericArgsRef<'tcx>,
26        /// The implemented predicate.
27        predicate: PolyTraitPredicate<'tcx>,
28        /// The index of this predicate in the list returned by `implied_predicates`.
29        index: usize,
30    },
31    Parent {
32        /// The implemented predicate.
33        predicate: PolyTraitPredicate<'tcx>,
34        /// The index of this predicate in the list returned by `implied_predicates`.
35        index: usize,
36    },
37}
38pub type Path<'tcx> = Vec<PathChunk<'tcx>>;
39
40#[derive(Debug, Clone)]
41pub enum ImplExprAtom<'tcx> {
42    /// A concrete `impl Trait for Type {}` item.
43    Concrete {
44        def_id: DefId,
45        generics: GenericArgsRef<'tcx>,
46    },
47    /// A context-bound clause like `where T: Trait`.
48    LocalBound {
49        predicate: Predicate<'tcx>,
50        /// The nth (non-self) predicate found for this item. We use predicates from
51        /// `required_predicates` starting from the parentmost item.
52        index: usize,
53        r#trait: PolyTraitRef<'tcx>,
54        path: Path<'tcx>,
55    },
56    /// The automatic clause `Self: Trait` present inside a `impl Trait for Type {}` item.
57    SelfImpl {
58        r#trait: PolyTraitRef<'tcx>,
59        path: Path<'tcx>,
60    },
61    /// `dyn Trait` is a wrapped value with a virtual table for trait
62    /// `Trait`.  In other words, a value `dyn Trait` is a dependent
63    /// triple that gathers a type τ, a value of type τ and an
64    /// instance of type `Trait`.
65    /// `dyn Trait` implements `Trait` using a built-in implementation; this refers to that
66    /// built-in implementation.
67    Dyn,
68    /// A built-in trait whose implementation is computed by the compiler, such as `FnMut`. This
69    /// morally points to an invisible `impl` block; as such it contains the information we may
70    /// need from one.
71    Builtin {
72        /// Extra data for the given trait.
73        trait_data: BuiltinTraitData<'tcx>,
74        /// The `ImplExpr`s required to satisfy the implied predicates on the trait declaration.
75        /// E.g. since `FnMut: FnOnce`, a built-in `T: FnMut` impl would have an `ImplExpr` for `T:
76        /// FnOnce`.
77        impl_exprs: Vec<ImplExpr<'tcx>>,
78        /// The values of the associated types for this trait.
79        types: Vec<(DefId, Ty<'tcx>, Vec<ImplExpr<'tcx>>)>,
80    },
81    /// An error happened while resolving traits.
82    Error(String),
83}
84
85#[derive(Debug, Clone)]
86pub enum BuiltinTraitData<'tcx> {
87    /// A virtual `Destruct` implementation.
88    /// `Destruct` is implemented automatically for all types. For our purposes, we chose to attach
89    /// the information about `drop_in_place` to that trait. This data tells us what kind of
90    /// `drop_in_place` the target type has.
91    Destruct(DestructData<'tcx>),
92    /// Some other builtin trait.
93    Other,
94}
95
96#[derive(Debug, Clone)]
97pub enum DestructData<'tcx> {
98    /// A drop that does nothing, e.g. for scalars and pointers.
99    Noop,
100    /// An implicit `Destruct` local clause, if the `resolve_destruct_bounds` option is `false`. If
101    /// that option is `true`, we'll add `Destruct` bounds to every type param, and use that to
102    /// resolve `Destruct` impls of generics. If it's `false`, we use this variant to indicate that
103    /// the clause comes from a generic or associated type.
104    Implicit,
105    /// The `drop_in_place` is known and non-trivial.
106    Glue {
107        /// The type we're generating glue for.
108        ty: Ty<'tcx>,
109    },
110}
111
112#[derive(Clone, Debug)]
113pub struct ImplExpr<'tcx> {
114    /// The trait this is an impl for.
115    pub r#trait: PolyTraitRef<'tcx>,
116    /// The kind of implemention of the root of the tree.
117    pub r#impl: ImplExprAtom<'tcx>,
118}
119
120/// Items have various predicates in scope. `path_to` uses them as a starting point for trait
121/// resolution. This tracks where each of them comes from.
122#[derive(Clone, Copy, Debug, Eq, PartialEq, Hash)]
123pub enum BoundPredicateOrigin {
124    /// The `Self: Trait` predicate implicitly present within trait declarations (note: we
125    /// don't add it for trait implementations, should we?).
126    SelfPred,
127    /// The nth (non-self) predicate found for this item. We use predicates from
128    /// `required_predicates` starting from the parentmost item.
129    Item(usize),
130}
131
132#[derive(Clone, Copy, Debug, Eq, PartialEq, Hash)]
133pub struct AnnotatedTraitPred<'tcx> {
134    pub origin: BoundPredicateOrigin,
135    pub clause: PolyTraitPredicate<'tcx>,
136}
137
138/// Returns the predicate to resolve as `Self`, if that makes sense in the current item.
139/// Currently this predicate is only used inside trait declarations and their asosciated types.
140fn initial_self_pred<'tcx>(
141    tcx: TyCtxt<'tcx>,
142    def_id: rustc_span::def_id::DefId,
143) -> Option<PolyTraitPredicate<'tcx>> {
144    use DefKind::*;
145    let trait_def_id = match tcx.def_kind(def_id) {
146        Trait | TraitAlias => def_id,
147        // Associated types can refer to the implicit `Self` clause. For methods and associated
148        // consts we pass an explicit `Self: Trait` clause to make the corresponding item
149        // reuseable.
150        AssocTy => tcx.parent(def_id),
151        _ => return None,
152    };
153    let self_pred = self_predicate(tcx, trait_def_id).upcast(tcx);
154    Some(self_pred)
155}
156
157/// The predicates to use as a starting point for resolving trait references within this item. This
158/// includes the `required_predicates` of this item and all its parents.
159fn local_bound_predicates<'tcx>(
160    tcx: TyCtxt<'tcx>,
161    def_id: rustc_span::def_id::DefId,
162    options: BoundsOptions,
163) -> Vec<PolyTraitPredicate<'tcx>> {
164    fn acc_predicates<'tcx>(
165        tcx: TyCtxt<'tcx>,
166        def_id: rustc_span::def_id::DefId,
167        options: BoundsOptions,
168        predicates: &mut Vec<PolyTraitPredicate<'tcx>>,
169    ) {
170        use DefKind::*;
171        match tcx.def_kind(def_id) {
172            // These inherit predicates from their parent.
173            AssocTy | AssocFn | AssocConst | Closure | Ctor(..) | Variant => {
174                let parent = tcx.parent(def_id);
175                acc_predicates(tcx, parent, options, predicates);
176            }
177            _ => {}
178        }
179        predicates.extend(
180            required_predicates(tcx, def_id, options)
181                .iter()
182                .map(|(clause, _span)| *clause)
183                .filter_map(|clause| clause.as_trait_clause()),
184        );
185    }
186
187    let mut predicates = vec![];
188    acc_predicates(tcx, def_id, options, &mut predicates);
189    predicates
190}
191
192#[tracing::instrument(level = "trace", skip(tcx))]
193fn parents_trait_predicates<'tcx>(
194    tcx: TyCtxt<'tcx>,
195    pred: PolyTraitPredicate<'tcx>,
196    options: BoundsOptions,
197) -> Vec<PolyTraitPredicate<'tcx>> {
198    let self_trait_ref = pred.to_poly_trait_ref();
199    implied_predicates(tcx, pred.def_id(), options)
200        .iter()
201        .map(|(clause, _span)| *clause)
202        // Substitute with the `self` args so that the clause makes sense in the
203        // outside context.
204        .map(|clause| clause.instantiate_supertrait(tcx, self_trait_ref))
205        .filter_map(|pred| pred.as_trait_clause())
206        .collect()
207}
208
209/// A candidate projects `self` along a path reaching some predicate. A candidate is
210/// selected when its predicate is the one expected, aka `target`.
211#[derive(Debug, Clone)]
212struct Candidate<'tcx> {
213    path: Path<'tcx>,
214    pred: PolyTraitPredicate<'tcx>,
215    origin: AnnotatedTraitPred<'tcx>,
216}
217
218impl<'tcx> Candidate<'tcx> {
219    fn into_impl_expr(self, tcx: TyCtxt<'tcx>) -> ImplExprAtom<'tcx> {
220        let path = self.path;
221        let r#trait = self.origin.clause.to_poly_trait_ref();
222        match self.origin.origin {
223            BoundPredicateOrigin::SelfPred => ImplExprAtom::SelfImpl { r#trait, path },
224            BoundPredicateOrigin::Item(index) => ImplExprAtom::LocalBound {
225                predicate: self.origin.clause.upcast(tcx),
226                index,
227                r#trait,
228                path,
229            },
230        }
231    }
232}
233
234/// Stores a set of predicates along with where they came from.
235#[derive(Clone)]
236pub struct PredicateSearcher<'tcx> {
237    tcx: TyCtxt<'tcx>,
238    typing_env: rustc_middle::ty::TypingEnv<'tcx>,
239    /// Local clauses available in the current context.
240    candidates: HashMap<PolyTraitPredicate<'tcx>, Candidate<'tcx>>,
241    /// Resolution options.
242    options: BoundsOptions,
243    /// Count the number of bound clauses in scope; used to identify clauses uniquely.
244    bound_clause_count: usize,
245}
246
247impl<'tcx> PredicateSearcher<'tcx> {
248    /// Initialize the elaborator with the predicates accessible within this item.
249    pub fn new_for_owner(tcx: TyCtxt<'tcx>, owner_id: DefId, options: BoundsOptions) -> Self {
250        let mut param_env = tcx.param_env(owner_id);
251        // A type alias's body can rely on bounds the alias doesn't declare; make them available to
252        // resolution too, not just in the alias's predicate list.
253        let extra_clauses = type_alias_implied_predicates(tcx, owner_id);
254        if !extra_clauses.is_empty() {
255            let clauses = tcx.mk_clauses_from_iter(
256                param_env
257                    .caller_bounds()
258                    .iter()
259                    .chain(extra_clauses.into_iter().map(|(clause, _)| clause)),
260            );
261            param_env = ParamEnv::new(clauses);
262        }
263        let mut out = Self {
264            tcx,
265            typing_env: TypingEnv {
266                param_env,
267                typing_mode: TypingMode::PostAnalysis,
268            },
269            candidates: Default::default(),
270            options,
271            bound_clause_count: 0,
272        };
273        out.insert_predicates(
274            initial_self_pred(tcx, owner_id).map(|clause| AnnotatedTraitPred {
275                origin: BoundPredicateOrigin::SelfPred,
276                clause,
277            }),
278        );
279        out.insert_bound_predicates(local_bound_predicates(tcx, owner_id, options));
280        out
281    }
282
283    /// Insert the bound clauses in the search context. Prefer inserting them all at once as this
284    /// will give priority to shorter resolution paths. Bound clauses are numbered from `0` in
285    /// insertion order.
286    pub fn insert_bound_predicates(
287        &mut self,
288        clauses: impl IntoIterator<Item = PolyTraitPredicate<'tcx>>,
289    ) {
290        let mut count = usize::MAX;
291        // Swap to avoid borrow conflicts.
292        std::mem::swap(&mut count, &mut self.bound_clause_count);
293        self.insert_predicates(clauses.into_iter().map(|clause| {
294            let i = count;
295            count += 1;
296            AnnotatedTraitPred {
297                origin: BoundPredicateOrigin::Item(i),
298                clause,
299            }
300        }));
301        std::mem::swap(&mut count, &mut self.bound_clause_count);
302    }
303
304    /// Override the param env; we use this when resolving `dyn` predicates to add more clauses to
305    /// the scope.
306    pub fn set_param_env(&mut self, param_env: ParamEnv<'tcx>) {
307        self.typing_env.param_env = param_env;
308    }
309
310    /// Insert annotated predicates in the search context. Prefer inserting them all at once as
311    /// this will give priority to shorter resolution paths.
312    fn insert_predicates(&mut self, preds: impl IntoIterator<Item = AnnotatedTraitPred<'tcx>>) {
313        self.insert_candidates(preds.into_iter().map(|clause| Candidate {
314            path: vec![],
315            pred: clause.clause,
316            origin: clause,
317        }))
318    }
319
320    /// Insert new candidates and all their parent predicates. This deduplicates predicates
321    /// to avoid divergence.
322    fn insert_candidates(&mut self, candidates: impl IntoIterator<Item = Candidate<'tcx>>) {
323        let tcx = self.tcx;
324        // Filter out duplicated candidates.
325        let mut new_candidates = Vec::new();
326        for mut candidate in candidates {
327            // Normalize and erase all lifetimes.
328            candidate.pred = normalize_bound_val(tcx, self.typing_env, candidate.pred);
329            if let Entry::Vacant(entry) = self.candidates.entry(candidate.pred) {
330                entry.insert(candidate.clone());
331                new_candidates.push(candidate);
332            }
333        }
334        if !new_candidates.is_empty() {
335            // Insert the parents all at once.
336            self.insert_candidate_parents(new_candidates);
337        }
338    }
339
340    /// Add the parents of these candidates. This is a separate function to avoid
341    /// polymorphic recursion due to the closures capturing the type parameters of this
342    /// function.
343    fn insert_candidate_parents(&mut self, new_candidates: Vec<Candidate<'tcx>>) {
344        let tcx = self.tcx;
345        // Then recursively add their parents. This way ensures a breadth-first order,
346        // which means we select the shortest path when looking up predicates.
347        let options = self.options;
348        self.insert_candidates(new_candidates.into_iter().flat_map(|candidate| {
349            parents_trait_predicates(tcx, candidate.pred, options)
350                .into_iter()
351                .enumerate()
352                .map(move |(index, parent_pred)| {
353                    let mut parent_candidate = Candidate {
354                        pred: parent_pred,
355                        path: candidate.path.clone(),
356                        origin: candidate.origin,
357                    };
358                    parent_candidate.path.push(PathChunk::Parent {
359                        predicate: parent_pred,
360                        index,
361                    });
362                    parent_candidate
363                })
364        }));
365    }
366
367    /// If the type is a trait associated type, we add any relevant bounds to our context.
368    fn add_associated_type_refs(
369        &mut self,
370        ty: Binder<'tcx, Ty<'tcx>>,
371        // Call back into hax-related code to display a nice warning.
372        warn: &impl Fn(&str),
373    ) -> Result<(), String> {
374        let tcx = self.tcx;
375        // Note: We skip a binder but rebind it just after.
376        let TyKind::Alias(AliasTyKind::Projection, alias_ty) = ty.skip_binder().kind() else {
377            return Ok(());
378        };
379        let trait_ref = ty.rebind(alias_ty.trait_ref(tcx)).upcast(tcx);
380
381        // The predicate we're looking for is is `<T as Trait>::Type: OtherTrait`. We look up `T as
382        // Trait` in the current context and add all the bounds on `Trait::Type` to our context.
383        let Some(trait_candidate) = self.resolve_local(trait_ref, warn)? else {
384            return Ok(());
385        };
386
387        // The bounds that hold on the associated type.
388        let item_bounds = implied_predicates(tcx, alias_ty.def_id, self.options);
389        let item_bounds = item_bounds
390            .iter()
391            .map(|(clause, _span)| *clause)
392            .filter_map(|pred| pred.as_trait_clause())
393            // Substitute the item generics
394            .map(|pred| EarlyBinder::bind(pred).instantiate(tcx, alias_ty.args))
395            .enumerate();
396
397        // Add all the bounds on the corresponding associated item.
398        self.insert_candidates(item_bounds.map(|(index, pred)| {
399            let mut candidate = Candidate {
400                path: trait_candidate.path.clone(),
401                pred,
402                origin: trait_candidate.origin,
403            };
404            candidate.path.push(PathChunk::AssocItem {
405                item: tcx.associated_item(alias_ty.def_id),
406                generic_args: alias_ty.args,
407                predicate: pred,
408                index,
409            });
410            candidate
411        }));
412
413        Ok(())
414    }
415
416    /// Resolve a local clause by looking it up in this set. If the predicate applies to an
417    /// associated type, we add the relevant implied associated type bounds to the set as well.
418    fn resolve_local(
419        &mut self,
420        target: PolyTraitPredicate<'tcx>,
421        // Call back into hax-related code to display a nice warning.
422        warn: &impl Fn(&str),
423    ) -> Result<Option<Candidate<'tcx>>, String> {
424        tracing::trace!("Looking for {target:?}");
425
426        // Look up the predicate
427        let ret = self.candidates.get(&target).cloned();
428        if ret.is_some() {
429            return Ok(ret);
430        }
431
432        // Add clauses related to associated type in the `Self` type of the predicate.
433        self.add_associated_type_refs(target.self_ty(), warn)?;
434
435        let ret = self.candidates.get(&target).cloned();
436        if ret.is_none() {
437            tracing::trace!(
438                "Couldn't find {target:?} in: [\n{}]",
439                self.candidates
440                    .iter()
441                    .map(|(_, c)| format!("  - {:?}\n", c.pred))
442                    .join("")
443            );
444        }
445        Ok(ret)
446    }
447
448    /// Resolve the given trait reference in the local context.
449    #[tracing::instrument(level = "trace", skip(self, warn))]
450    pub fn resolve(
451        &mut self,
452        tref: &PolyTraitRef<'tcx>,
453        // Call back into hax-related code to display a nice warning.
454        warn: &impl Fn(&str),
455    ) -> Result<ImplExpr<'tcx>, String> {
456        use rustc_trait_selection::traits::{
457            BuiltinImplSource, ImplSource, ImplSourceUserDefinedData,
458        };
459        let tcx = self.tcx;
460        let destruct_trait = tcx.lang_items().destruct_trait().unwrap();
461
462        let erased_tref = normalize_bound_val(self.tcx, self.typing_env, *tref);
463        let trait_def_id = erased_tref.skip_binder().def_id;
464
465        let error = |msg: String| {
466            warn(&msg);
467            Ok(ImplExpr {
468                r#impl: ImplExprAtom::Error(msg),
469                r#trait: *tref,
470            })
471        };
472
473        let impl_source = shallow_resolve_trait_ref(tcx, self.typing_env.param_env, erased_tref);
474        let atom = match impl_source {
475            Ok(ImplSource::UserDefined(ImplSourceUserDefinedData {
476                impl_def_id,
477                args: generics,
478                ..
479            })) => ImplExprAtom::Concrete {
480                def_id: impl_def_id,
481                generics,
482            },
483            Ok(ImplSource::Param(_)) => {
484                match self.resolve_local(erased_tref.upcast(self.tcx), warn)? {
485                    Some(candidate) => candidate.into_impl_expr(tcx),
486                    None => {
487                        let msg = format!(
488                            "Could not find a clause for `{tref:?}` in the item parameters"
489                        );
490                        return error(msg);
491                    }
492                }
493            }
494            Ok(ImplSource::Builtin(BuiltinImplSource::Object { .. }, _)) => ImplExprAtom::Dyn,
495            Ok(ImplSource::Builtin(_, _)) => {
496                // Resolve the predicates implied by the trait.
497                // If we wanted to not skip this binder, we'd have to instantiate the bound
498                // regions, solve, then wrap the result in a binder. And track higher-kinded
499                // clauses better all over.
500                let impl_exprs = self.resolve_item_implied_predicates(
501                    trait_def_id,
502                    erased_tref.skip_binder().args,
503                    warn,
504                )?;
505                let types = tcx
506                    .associated_items(trait_def_id)
507                    .in_definition_order()
508                    .filter(|assoc| matches!(assoc.kind, AssocKind::Type { .. }))
509                    .filter_map(|assoc| {
510                        let ty =
511                            Ty::new_projection(tcx, assoc.def_id, erased_tref.skip_binder().args);
512                        let ty = erase_and_norm(tcx, self.typing_env, ty);
513                        if let TyKind::Alias(_, alias_ty) = ty.kind() {
514                            if alias_ty.def_id == assoc.def_id {
515                                // Couldn't normalize the type to anything different than itself;
516                                // this must be a built-in associated type such as
517                                // `DiscriminantKind::Discriminant`.
518                                // We can't return the unnormalized associated type as that would
519                                // make the trait ref contain itself, which would make hax's
520                                // `sinto` infrastructure loop. That's ok because we can't provide
521                                // a value for this type other than the associate type alias
522                                // itself.
523                                return None;
524                            }
525                        }
526                        let impl_exprs = self
527                            .resolve_item_implied_predicates(
528                                assoc.def_id,
529                                erased_tref.skip_binder().args,
530                                warn,
531                            )
532                            .ok()?;
533                        Some((assoc.def_id, ty, impl_exprs))
534                    })
535                    .collect();
536
537                let trait_data = if erased_tref.skip_binder().def_id == destruct_trait {
538                    let ty = erased_tref.skip_binder().args[0].as_type().unwrap();
539                    // Source of truth are `ty::needs_drop_components` and `tcx.needs_drop_raw`.
540                    let destruct_data = match ty.kind() {
541                        // TODO: Does `UnsafeBinder` drop its contents?
542                        ty::Bool
543                        | ty::Char
544                        | ty::Int(..)
545                        | ty::Uint(..)
546                        | ty::Float(..)
547                        | ty::Foreign(..)
548                        | ty::Str
549                        | ty::RawPtr(..)
550                        | ty::Ref(..)
551                        | ty::FnDef(..)
552                        | ty::FnPtr(..)
553                        | ty::UnsafeBinder(..)
554                        | ty::Never => Either::Left(DestructData::Noop),
555                        ty::Tuple(tys) if tys.is_empty() => Either::Left(DestructData::Noop),
556                        ty::Array(..)
557                        | ty::Pat(..)
558                        | ty::Slice(..)
559                        | ty::Tuple(..)
560                        | ty::Adt(..)
561                        | ty::Closure(..)
562                        | ty::Coroutine(..)
563                        | ty::CoroutineClosure(..)
564                        | ty::CoroutineWitness(..) => Either::Left(DestructData::Glue { ty }),
565                        // Every `dyn` has a `drop_in_place` in its vtable, ergo we pretend that every
566                        // `dyn` has `Destruct` in its list of traits.
567                        ty::Dynamic(..) => Either::Right(ImplExprAtom::Dyn),
568                        ty::Param(..) | ty::Alias(..) | ty::Bound(..) => {
569                            if self.options.resolve_destruct {
570                                // We've added `Destruct` impls on everything, we should be able to resolve
571                                // it.
572                                match self.resolve_local(erased_tref.upcast(self.tcx), warn)? {
573                                    Some(candidate) => Either::Right(candidate.into_impl_expr(tcx)),
574                                    None => {
575                                        let msg = format!(
576                                            "Cannot find virtual `Destruct` clause: `{tref:?}`"
577                                        );
578                                        return error(msg);
579                                    }
580                                }
581                            } else {
582                                Either::Left(DestructData::Implicit)
583                            }
584                        }
585
586                        ty::Placeholder(..) | ty::Infer(..) | ty::Error(..) => {
587                            let msg = format!(
588                                "Cannot resolve clause `{tref:?}` \
589                                because of a type error"
590                            );
591                            return error(msg);
592                        }
593                    };
594                    destruct_data.map_left(BuiltinTraitData::Destruct)
595                } else {
596                    Either::Left(BuiltinTraitData::Other)
597                };
598                match trait_data {
599                    Either::Left(trait_data) => ImplExprAtom::Builtin {
600                        trait_data,
601                        impl_exprs,
602                        types,
603                    },
604                    Either::Right(atom) => atom,
605                }
606            }
607            Err(e) => {
608                let msg = format!(
609                    "Could not find a clause for `{tref:?}` \
610                    in the current context: `{e:?}`"
611                );
612                return error(msg);
613            }
614        };
615
616        Ok(ImplExpr {
617            r#impl: atom,
618            r#trait: *tref,
619        })
620    }
621
622    /// Resolve the predicates required by the given item.
623    pub fn resolve_item_required_predicates(
624        &mut self,
625        def_id: DefId,
626        generics: GenericArgsRef<'tcx>,
627        // Call back into hax-related code to display a nice warning.
628        warn: &impl Fn(&str),
629    ) -> Result<Vec<ImplExpr<'tcx>>, String> {
630        let tcx = self.tcx;
631        self.resolve_predicates(
632            generics,
633            required_predicates(tcx, def_id, self.options),
634            warn,
635        )
636    }
637
638    /// Resolve the predicates implied by the given item.
639    pub fn resolve_item_implied_predicates(
640        &mut self,
641        def_id: DefId,
642        generics: GenericArgsRef<'tcx>,
643        // Call back into hax-related code to display a nice warning.
644        warn: &impl Fn(&str),
645    ) -> Result<Vec<ImplExpr<'tcx>>, String> {
646        let tcx = self.tcx;
647        self.resolve_predicates(
648            generics,
649            implied_predicates(tcx, def_id, self.options),
650            warn,
651        )
652    }
653
654    /// Apply the given generics to the provided clauses and resolve the trait references in the
655    /// current context.
656    pub fn resolve_predicates(
657        &mut self,
658        generics: GenericArgsRef<'tcx>,
659        predicates: utils::Predicates<'tcx>,
660        // Call back into hax-related code to display a nice warning.
661        warn: &impl Fn(&str),
662    ) -> Result<Vec<ImplExpr<'tcx>>, String> {
663        let tcx = self.tcx;
664        predicates
665            .iter()
666            .map(|(clause, _span)| *clause)
667            .filter_map(|clause| clause.as_trait_clause())
668            .map(|trait_pred| trait_pred.map_bound(|p| p.trait_ref))
669            // Substitute the item generics
670            .map(|trait_ref| EarlyBinder::bind(trait_ref).instantiate(tcx, generics))
671            // Resolve
672            .map(|trait_ref| self.resolve(&trait_ref, warn))
673            .collect()
674    }
675}
676
677/// Attempts to resolve an obligation to an `ImplSource`. The result is a shallow `ImplSource`
678/// resolution, meaning that we do not resolve all nested obligations on the impl. Note that type
679/// check should guarantee to us that all nested obligations *could be* resolved if we wanted to.
680///
681/// This expects that `trait_ref` is fully normalized.
682///
683/// This is based on `rustc_traits::codegen::codegen_select_candidate` in rustc.
684pub fn shallow_resolve_trait_ref<'tcx>(
685    tcx: TyCtxt<'tcx>,
686    param_env: ParamEnv<'tcx>,
687    trait_ref: PolyTraitRef<'tcx>,
688) -> Result<ImplSource<'tcx, ()>, CodegenObligationError> {
689    use rustc_infer::infer::TyCtxtInferExt;
690    use rustc_middle::traits::CodegenObligationError;
691    use rustc_middle::ty::TypeVisitableExt;
692    use rustc_trait_selection::traits::{
693        Obligation, ObligationCause, ObligationCtxt, SelectionContext, SelectionError,
694    };
695    // Do the initial selection for the obligation. This yields the
696    // shallow result we are looking for -- that is, what specific impl.
697    let infcx = tcx
698        .infer_ctxt()
699        .ignoring_regions()
700        .build(TypingMode::PostAnalysis);
701    let mut selcx = SelectionContext::new(&infcx);
702
703    let obligation_cause = ObligationCause::dummy();
704    let obligation = Obligation::new(tcx, obligation_cause, param_env, trait_ref);
705
706    let selection = match selcx.poly_select(&obligation) {
707        Ok(Some(selection)) => selection,
708        Ok(None) => return Err(CodegenObligationError::Ambiguity),
709        Err(SelectionError::Unimplemented) => return Err(CodegenObligationError::Unimplemented),
710        Err(_) => return Err(CodegenObligationError::Ambiguity),
711    };
712
713    // Currently, we use a fulfillment context to completely resolve
714    // all nested obligations. This is because they can inform the
715    // inference of the impl's type parameters.
716    // FIXME(-Znext-solver): Doesn't need diagnostics if new solver.
717    let ocx = ObligationCtxt::new(&infcx);
718    let impl_source = selection.map(|obligation| {
719        ocx.register_obligation(obligation.clone());
720        ()
721    });
722
723    let errors = ocx.evaluate_obligations_error_on_ambiguity();
724    if !errors.is_empty() {
725        return Err(CodegenObligationError::Ambiguity);
726    }
727
728    let impl_source = infcx.resolve_vars_if_possible(impl_source);
729    let impl_source = tcx.erase_and_anonymize_regions(impl_source);
730
731    if impl_source.has_infer() {
732        // Unused lifetimes on an impl get replaced with inference vars, but never resolved.
733        return Err(CodegenObligationError::Ambiguity);
734    }
735
736    Ok(impl_source)
737}
hax_frontend_exporter/traits/resolution.rs

hax_frontend_exporter/traits/
resolution.rs
