Merge pull request #990 from Nadrieril/ty-alias

Remove workaround in trait resolution for associated items
cryspen · Oct 14, 2024 · 1ba7ce3 · 1ba7ce3
2 parents 19fe681 + 7307809
commit 1ba7ce3
Show file tree

Hide file tree

Showing 2 changed files with 19 additions and 17 deletions.
diff --git a/frontend/exporter/src/traits.rs b/frontend/exporter/src/traits.rs
@@ -257,7 +257,7 @@ pub mod rustc {
         }
 
         // Lifetimes are irrelevant when resolving instances.
-        pub(super) fn erase_and_norm<'tcx, T>(
+        pub(crate) fn erase_and_norm<'tcx, T>(
             tcx: TyCtxt<'tcx>,
             param_env: ParamEnv<'tcx>,
             x: T,

diff --git a/frontend/exporter/src/types/copied.rs b/frontend/exporter/src/types/copied.rs
@@ -1775,31 +1775,33 @@ pub enum AliasKind {
 #[cfg(feature = "rustc")]
 impl Alias {
     #[tracing::instrument(level = "trace", skip(s))]
-    fn from<'tcx, S: BaseState<'tcx> + HasOwnerId>(
+    fn from<'tcx, S: UnderOwnerState<'tcx>>(
         s: &S,
         alias_kind: &rustc_type_ir::AliasTyKind,
         alias_ty: &rustc_middle::ty::AliasTy<'tcx>,
     ) -> Self {
         use rustc_type_ir::AliasTyKind as RustAliasKind;
         let kind = match alias_kind {
             RustAliasKind::Projection => {
-                use rustc_middle::ty::{Binder, TypeVisitableExt};
                 let tcx = s.base().tcx;
                 let trait_ref = alias_ty.trait_ref(tcx);
-                // We don't have a clear handling of binders here; this is causing a number of
-                // problems in Charon. In the meantime we return something well-formed when we
-                // can't trait-solve. See also https://github.com/hacspec/hax/issues/495.
-                if trait_ref.has_escaping_bound_vars() {
-                    warning!(
-                        s,
-                        "Hax frontend found a projected type with escaping bound vars. Please report https://github.com/hacspec/hax/issues/495"
-                    );
-                    AliasKind::Opaque
-                } else {
-                    AliasKind::Projection {
-                        assoc_item: tcx.associated_item(alias_ty.def_id).sinto(s),
-                        impl_expr: solve_trait(s, Binder::dummy(trait_ref)),
-                    }
+                // In a case like:
+                // ```
+                // impl<T, U> Trait for Result<T, U>
+                // where
+                //     for<'a> &'a Result<T, U>: IntoIterator,
+                //     for<'a> <&'a Result<T, U> as IntoIterator>::Item: Copy,
+                // {}
+                // ```
+                // the `&'a Result<T, U> as IntoIterator` trait ref has escaping bound variables
+                // yet we dont have a binder around (could even be several). Binding this correctly
+                // is therefore difficult. Since our trait resolution ignores lifetimes anyway, we
+                // just erase them. See also https://github.com/hacspec/hax/issues/747.
+                let trait_ref =
+                    traits::rustc::search_clause::erase_and_norm(tcx, s.param_env(), trait_ref);
+                AliasKind::Projection {
+                    assoc_item: tcx.associated_item(alias_ty.def_id).sinto(s),
+                    impl_expr: solve_trait(s, ty::Binder::dummy(trait_ref)),
                 }
             }
             RustAliasKind::Inherent => AliasKind::Inherent,