Update hax

charon/src/bin/charon-driver/translate/translate_predicates.rs

@@ -526,18 +526,6 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                 kind: TraitRefKind::BuiltinOrAuto(trait_decl_ref.clone()),
                 trait_decl_ref,
             },
-            ImplExprAtom::Todo(msg) => {
-                let error = format!("Error during trait resolution: {}", msg);
-                self.span_err(span, &error);
-                if !self.t_ctx.continue_on_failure() {
-                    panic!("{}", error)
-                } else {
-                    TraitRef {
-                        kind: TraitRefKind::Unknown(msg.clone()),
-                        trait_decl_ref,
-                    }
-                }
-            }
         };
         Ok(Some(trait_ref))
     }

charon/src/bin/charon-driver/translate/translate_traits.rs

@@ -57,7 +57,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
         for bound in bounds {
             if let rustc_middle::ty::ClauseKind::Trait(trait_pred) = bound.kind().skip_binder() {
                 let trait_ref = bound.kind().rebind(trait_pred.trait_ref);
-                let trait_ref = hax::solve_trait(&self.hax_state, param_env, trait_ref);
+                let trait_ref = hax::solve_trait(&self.hax_state, trait_ref);
                 let trait_ref = self.translate_trait_impl_expr(span, erase_regions, &trait_ref)?;
                 if let Some(trait_ref) = trait_ref {
                     trait_refs.push(trait_ref);
@@ -343,7 +343,6 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> {
             };
             let parent_trait_refs = hax::solve_item_traits(
                 &bt_ctx.hax_state,
-                tcx.param_env(rust_id),
                 rust_trait_ref.def_id,
                 rust_trait_ref.args,
                 None,

charon/tests/ui/ptr_to_promoted.out

@@ -0,0 +1,23 @@
+# Final LLBC before serialization:
+
+fn test_crate::main()
+{
+    let @0: (); // return
+    let @1: *const u8; // anonymous local
+    let @2: usize; // anonymous local
+    let x@3: &'_ (u8); // local
+    let @4: u8; // anonymous local
+    let @5: &'_ (u8); // anonymous local
+
+    @4 := const ([0])
+    @5 := &@4
+    x@3 := move (@5)
+    @1 := &raw const *(x@3)
+    @2 := cast<*const u8, usize>(copy (@1))
+    drop @2
+    @0 := ()
+    return
+}
+
+
+

charon/tests/ui/unsupported/ptr_to_promoted.rs → charon/tests/ui/ptr_to_promoted.rs

@@ -1,4 +1,3 @@
-//@ known-failure
 //@ charon-args=--mir_optimized
 
 fn main() {

charon/tests/ui/quantified-clause.out

@@ -0,0 +1,61 @@
+disabled backtrace
+warning[E9999]: Hax frontend found a projected type with escaping bound vars. Please report https://github.com/hacspec/hax/issues/495
+
+                Context:
+                 - alias_ty: AliasTy {
+                    args: [
+                        F/#0,
+                        (&'^0.Named(test_crate::foo::'a, "'a") (),),
+                    ],
+                    def_id: core::ops::function::FnOnce::Output,
+                    ..
+                }
+                 - alias_kind: Projection
+                 - trait_ref: <F as std::ops::FnOnce<(&'a (),)>>
+                 - trait_ref_and_generics: (
+                    <F as std::ops::FnOnce<(&'a (),)>>,
+                    [],
+                )
+                 - rebased_generics: [
+                    F/#0,
+                    (&'^0.Named(test_crate::foo::'a, "'a") (),),
+                    (&'^0.Named(test_crate::foo::'a, "'a") (),),
+                ]
+                 - norm_rebased_generics: Ok(
+                    <F as std::ops::FnOnce<(&'a (),)>>,
+                )
+                 - norm_generics: Ok(
+                    <F as std::ops::FnOnce<(&'a (),)>>,
+                )
+                 - early_binder_generics: Ok(
+                    <F as std::ops::FnOnce<(&'a (),)>>,
+                )
+                 - early_binder_rebased_generics: Ok(
+                    <F as std::ops::FnOnce<(&'a (),)>>,
+                )
+  |
+  = note: ⚠️ This is a bug in Hax's frontend.
+          Please report this error to https://github.com/hacspec/hax/issues with some context (e.g. the current crate)!
+
+thread 'rustc' panicked at src/bin/charon-driver/translate/translate_types.rs:78:26:
+called `Option::unwrap()` on a `None` value
+note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
+error: Thread panicked when extracting item `test_crate::foo`.
+ --> tests/ui/quantified-clause.rs:3:1
+  |
+3 | / fn foo<F>(_f: F)
+4 | | where
+5 | |     F: for<'a> FnMut(&'a ()),
+  | |_____________________________^
+
+error: Ignoring the following item due to an error: test_crate::foo
+ --> tests/ui/quantified-clause.rs:3:1
+  |
+3 | / fn foo<F>(_f: F)
+4 | | where
+5 | |     F: for<'a> FnMut(&'a ()),
+  | |_____________________________^
+
+error: aborting due to 2 previous errors; 1 warning emitted
+
+Error: Charon driver exited with code 101

charon/tests/ui/quantified-clause.rs

@@ -0,0 +1,7 @@
+//@ known-failure
+
+fn foo<F>(_f: F)
+where
+    F: for<'a> FnMut(&'a ()),
+{
+}