Normalize projections before translating them

Author: Nadrieril

frontend/exporter/src/traits.rs

@@ -6,8 +6,8 @@ mod resolution;
 mod utils;
 #[cfg(feature = "rustc")]
 pub use utils::{
-    erase_and_norm, implied_predicates, predicates_defined_on, required_predicates, self_predicate,
-    Predicates, ToPolyTraitRef,
+    erase_and_norm, erase_free_regions, implied_predicates, normalize, predicates_defined_on,
+    required_predicates, self_predicate, Predicates, ToPolyTraitRef,
 };
 
 #[cfg(feature = "rustc")]

frontend/exporter/src/traits/utils.rs

@@ -169,10 +169,27 @@ pub fn implied_predicates<'tcx>(
     }
 }
 
+/// Normalize a value.
+pub fn normalize<'tcx, T>(tcx: TyCtxt<'tcx>, typing_env: TypingEnv<'tcx>, value: T) -> T
+where
+    T: TypeFoldable<TyCtxt<'tcx>> + Copy,
+{
+    use rustc_infer::infer::TyCtxtInferExt;
+    use rustc_middle::traits::ObligationCause;
+    use rustc_trait_selection::traits::query::normalize::QueryNormalizeExt;
+    let (infcx, param_env) = tcx.infer_ctxt().build_with_typing_env(typing_env);
+    infcx
+        .at(&ObligationCause::dummy(), param_env)
+        .query_normalize(value)
+        // We ignore the generated outlives relations. Unsure what we should do with them.
+        .map(|x| x.value)
+        .unwrap_or(value)
+}
+
 /// Erase free regions from the given value. Largely copied from `tcx.erase_regions`, but also
 /// erases bound regions that are bound outside `value`, so we can call this function inside a
 /// `Binder`.
-fn erase_free_regions<'tcx, T>(tcx: TyCtxt<'tcx>, value: T) -> T
+pub fn erase_free_regions<'tcx, T>(tcx: TyCtxt<'tcx>, value: T) -> T
 where
     T: TypeFoldable<TyCtxt<'tcx>>,
 {

frontend/exporter/src/types/ty.rs

@@ -804,7 +804,17 @@ impl Alias {
         alias_ty: &ty::AliasTy<'tcx>,
     ) -> TyKind {
         let tcx = s.base().tcx;
+        let typing_env = s.typing_env();
         use rustc_type_ir::AliasTyKind as RustAliasKind;
+
+        // Try to normalize the alias first.
+        let ty = ty::Ty::new_alias(tcx, *alias_kind, *alias_ty);
+        let ty = crate::traits::normalize(tcx, typing_env, ty);
+        let ty::Alias(alias_kind, alias_ty) = ty.kind() else {
+            let ty: Ty = ty.sinto(s);
+            return ty.kind().clone();
+        };
+
         let kind = match alias_kind {
             RustAliasKind::Projection => {
                 let trait_ref = alias_ty.trait_ref(tcx);
@@ -820,7 +830,7 @@ impl Alias {
                 // 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 = crate::traits::erase_and_norm(tcx, s.typing_env(), trait_ref);
+                let trait_ref = crate::traits::erase_free_regions(tcx, 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)),