Frontend: silence an error about escaping bounded variables

frontend/exporter/src/traits.rs

@@ -127,12 +127,13 @@ pub(crate) mod search_clause {
         s: &S,
     ) -> bool {
         let tcx = s.base().tcx;
-        let x = tcx.try_normalize_erasing_regions(param_env, x).unwrap_or(x);
-        let y = tcx.try_normalize_erasing_regions(param_env, y).unwrap_or(y);
-        // Below: "~const " may appear in the string, and comes from the way the
-        // trait ref is internalized by rustc. We remove such occurrences (yes, this is sad).
-        let sx = format!("{:?}", x).replace("~const ", "");
-        let sy = format!("{:?}", y).replace("~const ", "");
+        let erase_and_norm =
+            |x| tcx.erase_regions(tcx.try_normalize_erasing_regions(param_env, x).unwrap_or(x));
+        // Lifetime and constantness are irrelevant when resolving instances
+        let x = erase_and_norm(x).without_const(tcx);
+        let y = erase_and_norm(y).without_const(tcx);
+        let sx = format!("{:?}", x.kind().skip_binder());
+        let sy = format!("{:?}", y.kind().skip_binder());
         let result = sx == sy;
         const DEBUG: bool = false;
         if DEBUG && result {
@@ -298,15 +299,6 @@ pub trait IntoImplExpr<'tcx> {
     ) -> ImplExpr;
 }
 
-impl<'tcx> IntoImplExpr<'tcx> for rustc_middle::ty::TraitRef<'tcx> {
-    fn impl_expr<S: UnderOwnerState<'tcx>>(
-        &self,
-        s: &S,
-        param_env: rustc_middle::ty::ParamEnv<'tcx>,
-    ) -> ImplExpr {
-        rustc_middle::ty::Binder::dummy(self.clone()).impl_expr(s, param_env)
-    }
-}
 impl<'tcx> IntoImplExpr<'tcx> for rustc_middle::ty::PolyTraitPredicate<'tcx> {
     fn impl_expr<S: UnderOwnerState<'tcx>>(
         &self,

frontend/exporter/src/types/copied.rs

@@ -1592,10 +1592,51 @@ impl Alias {
         use rustc_type_ir::sty::AliasKind as RustAliasKind;
         let kind = match alias_kind {
             RustAliasKind::Projection => {
+                use rustc_middle::ty::{Binder, EarlyBinder, TypeVisitableExt};
                 let tcx = s.base().tcx;
+                let trait_ref = alias_ty.trait_ref(tcx);
+                // Sometimes (see
+                // https://github.com/hacspec/hax/issues/495), we get
+                // trait refs with escaping bound vars. Empirically,
+                // this seems fine. If we detect such a situation, we
+                // emit a warning with a lot of debugging information.
+                let poly_trait_ref = if trait_ref.has_escaping_bound_vars() {
+                    let trait_ref_and_substs = alias_ty.trait_ref_and_own_substs(tcx);
+                    let rebased_substs = alias_ty.rebase_substs_onto_impl(alias_ty.substs, tcx);
+                    let norm_rebased_substs = tcx.try_subst_and_normalize_erasing_regions(
+                        rebased_substs,
+                        get_param_env(s),
+                        EarlyBinder::bind(trait_ref),
+                    );
+                    let norm_substs = tcx.try_subst_and_normalize_erasing_regions(
+                        alias_ty.substs,
+                        get_param_env(s),
+                        EarlyBinder::bind(trait_ref),
+                    );
+                    let early_binder_substs =
+                        std::panic::catch_unwind(std::panic::AssertUnwindSafe(|| {
+                            EarlyBinder::bind(trait_ref).subst(tcx, alias_ty.substs)
+                        }));
+                    let early_binder_rebased_substs =
+                        std::panic::catch_unwind(std::panic::AssertUnwindSafe(|| {
+                            EarlyBinder::bind(trait_ref).subst(tcx, alias_ty.substs)
+                        }));
+                    warning!(
+                        s,
+                        "Hax frontend found a projected type with escaping bound vars. Please report https://github.com/hacspec/hax/issues/495";
+                        {alias_ty, alias_kind, trait_ref, trait_ref_and_substs, rebased_substs,
+                         norm_rebased_substs, norm_substs,
+                         early_binder_substs, early_binder_rebased_substs}
+                    );
+                    // we cannot use `Binder::dummy`: it asserts that
+                    // there is no any escaping bound vars
+                    Binder::bind_with_vars(trait_ref, rustc_middle::ty::List::empty())
+                } else {
+                    Binder::dummy(trait_ref)
+                };
                 AliasKind::Projection {
                     assoc_item: tcx.associated_item(alias_ty.def_id).sinto(s),
-                    impl_expr: alias_ty.trait_ref(tcx).impl_expr(s, get_param_env(s)),
+                    impl_expr: poly_trait_ref.impl_expr(s, get_param_env(s)),
                 }
             }
             RustAliasKind::Inherent => AliasKind::Inherent,

test-harness/src/snapshots/toolchain__traits into-fstar.snap

@@ -15,20 +15,103 @@ info:
     issue_id: ~
     positive: true
     snapshot:
-      stderr: true
+      stderr: false
       stdout: true
     include_flag: ~
     backend_options: ~
 ---
 exit = 0
-stderr = '''
-Compiling traits v0.1.0 (WORKSPACE_ROOT/traits)
-    Finished dev [unoptimized + debuginfo] target(s) in XXs'''
 
 [stdout]
 diagnostics = []
 
 [stdout.files]
+"Traits.For_clauses.Issue_495_.Minimized_3_.fst" = '''
+module Traits.For_clauses.Issue_495_.Minimized_3_
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open Core
+open FStar.Mul
+
+class t_Trait (v_Self: Type0) = { __marker_trait_t_Trait:Prims.unit }
+
+[@@ FStar.Tactics.Typeclasses.tcinstance]
+let impl
+      (#v_P: Type0)
+      (#[FStar.Tactics.Typeclasses.tcresolve ()] i0: Core.Ops.Function.t_FnMut v_P u8)
+    : t_Trait v_P = { __marker_trait = () }
+'''
+"Traits.For_clauses.Issue_495_.fst" = '''
+module Traits.For_clauses.Issue_495_
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open Core
+open FStar.Mul
+
+let minimized_1_ (list: Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
+    : Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
+  Core.Iter.Traits.Iterator.f_collect (Core.Iter.Traits.Iterator.f_filter ({
+            Core.Ops.Range.f_start = 0uy;
+            Core.Ops.Range.f_end = 5uy
+          }
+          <:
+          Core.Ops.Range.t_Range u8)
+        (fun temp_0_ ->
+            let _:u8 = temp_0_ in
+            true)
+      <:
+      Core.Iter.Adapters.Filter.t_Filter (Core.Ops.Range.t_Range u8) (u8 -> bool))
+
+let minimized_2_ (it: Core.Iter.Adapters.Filter.t_Filter (Core.Ops.Range.t_Range u8) (u8 -> bool))
+    : Prims.unit =
+  let (v__indices: Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global):Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global
+  =
+    Core.Iter.Traits.Iterator.f_collect it
+  in
+  ()
+
+let original_function_from_495_ (list: Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) : Prims.unit =
+  let (v__indices: Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global):Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global
+  =
+    Core.Iter.Traits.Iterator.f_collect (Core.Iter.Traits.Iterator.f_filter ({
+              Core.Ops.Range.f_start = 0uy;
+              Core.Ops.Range.f_end = 5uy
+            }
+            <:
+            Core.Ops.Range.t_Range u8)
+          (fun i ->
+              let i:u8 = i in
+              let _, out:(Core.Slice.Iter.t_Iter u8 & bool) =
+                Core.Iter.Traits.Iterator.f_any (Core.Slice.impl__iter (Core.Ops.Deref.f_deref list
+                        <:
+                        t_Slice u8)
+                    <:
+                    Core.Slice.Iter.t_Iter u8)
+                  (fun n ->
+                      let n:u8 = n in
+                      n =. i <: bool)
+              in
+              out)
+        <:
+        Core.Iter.Adapters.Filter.t_Filter (Core.Ops.Range.t_Range u8) (u8 -> bool))
+  in
+  ()
+'''
+"Traits.For_clauses.fst" = '''
+module Traits.For_clauses
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open Core
+open FStar.Mul
+
+class t_Foo (v_Self: Type0) (v_T: Type0) = {
+  f_to_t_pre:v_Self -> bool;
+  f_to_t_post:v_Self -> v_T -> bool;
+  f_to_t:x0: v_Self -> Prims.Pure v_T (f_to_t_pre x0) (fun result -> f_to_t_post x0 result)
+}
+
+let v__f (#v_X: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Foo v_X u8) (x: v_X)
+    : Prims.unit =
+  let _:u8 = f_to_t x in
+  ()
+'''
 "Traits.fst" = '''
 module Traits
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"

tests/traits/Cargo.toml

@@ -6,5 +6,5 @@ edition = "2021"
 [dependencies]
 
 [package.metadata.hax-tests]
-into."fstar" = { }
+into."fstar" = { snapshot = "stdout" }
 

tests/traits/src/lib.rs

@@ -77,3 +77,34 @@ impl Error {
         || Self::Fail
     }
 }
+
+mod for_clauses {
+    trait Foo<T> {
+        fn to_t(&self) -> T;
+    }
+
+    fn _f<X: for<'a> Foo<&'a u8>>(x: X) {
+        x.to_t();
+    }
+
+    // From issue #495
+    mod issue_495 {
+        use core::iter::Filter;
+        use core::ops::Range;
+
+        fn original_function_from_495(list: Vec<u8>) {
+            let _indices: Vec<_> = (0..5).filter(|i| list.iter().any(|n| n == i)).collect();
+        }
+
+        fn minimized_1(list: Vec<u8>) -> Vec<u8> {
+            (0..5).filter(|_| true).collect()
+        }
+        fn minimized_2(it: Filter<Range<u8>, for<'a> fn(&'a u8) -> bool>) {
+            let _indices: Vec<_> = it.collect();
+        }
+        mod minimized_3 {
+            pub trait Trait {}
+            impl<P: FnMut(&u8) -> bool> Trait for P {}
+        }
+    }
+}