prevent eta expansion in rty checking

flux-rs · Jan 13, 2025 · 52ea405 · 52ea405
1 parent 5f3c207
commit 52ea405
Show file tree

Hide file tree

Showing 5 changed files with 8 additions and 8 deletions.
diff --git a/crates/flux-infer/src/infer.rs b/crates/flux-infer/src/infer.rs
@@ -926,7 +926,7 @@ impl<'a, E: LocEnv> Sub<'a, E> {
         let vars = a
             .vars()
             .iter()
-            .map(|kind| infcx.define_vars(kind.expect_sort()))
+            .map(|kind| Expr::fvar(infcx.define_var(kind.expect_sort())))
             .collect_vec();
         let body_a = a.apply(&vars);
         let body_b = b.apply(&vars);

diff --git a/crates/flux-infer/src/refine_tree.rs b/crates/flux-infer/src/refine_tree.rs
@@ -375,7 +375,7 @@ pub struct Unpacker<'a, 'b> {
 
 impl HoisterDelegate for Unpacker<'_, '_> {
     fn hoist_exists(&mut self, ty_ctor: &TyCtor) -> Ty {
-        let ty = ty_ctor.replace_bound_refts_with(|sort, _, _| self.cursor.define_vars(sort));
+        let ty = ty_ctor.replace_bound_refts_with(|sort, _, _| Expr::fvar(self.cursor.define_var(sort)));
         if let AssumeInvariants::Yes { check_overflow } = self.assume_invariants {
             self.cursor.assume_invariants(&ty, check_overflow);
         }

diff --git a/crates/flux-refineck/src/checker.rs b/crates/flux-refineck/src/checker.rs
@@ -233,7 +233,7 @@ fn check_fn_subtyping(
     let tcx = infcx.genv.tcx();
 
     let super_sig = super_sig
-        .replace_bound_vars(|_| rty::ReErased, |sort, _| infcx.define_vars(sort))
+        .replace_bound_vars(|_| rty::ReErased, |sort, _| Expr::fvar(infcx.define_var(sort)))
         .normalize_projections(&mut infcx)?;
 
     // 1. Unpack `T_g` input types
@@ -275,7 +275,7 @@ fn check_fn_subtyping(
 
     let output = infcx
         .fully_resolve_evars(&output)
-        .replace_bound_refts_with(|sort, _, _| infcx.define_vars(sort));
+        .replace_bound_refts_with(|sort, _, _| Expr::fvar(infcx.define_var(sort)));
 
     // 4. OUTPUT subtyping (f_out <: g_out)
     infcx.ensure_resolved_evars(|infcx| {
@@ -422,7 +422,7 @@ impl<'ck, 'genv, 'tcx, M: Mode> Checker<'ck, 'genv, 'tcx, M> {
         let body = genv.mir(def_id).with_span(span)?;
 
         let fn_sig = poly_sig
-            .replace_bound_vars(|_| rty::ReErased, |sort, _| infcx.define_vars(sort))
+            .replace_bound_vars(|_| rty::ReErased, |sort, _| Expr::fvar(infcx.define_var(sort)))
             .normalize_projections(&mut infcx)
             .with_span(span)?;
 
@@ -804,7 +804,7 @@ impl<'ck, 'genv, 'tcx, M: Mode> Checker<'ck, 'genv, 'tcx, M> {
 
         let output = infcx
             .fully_resolve_evars(&fn_sig.output)
-            .replace_bound_refts_with(|sort, _, _| infcx.define_vars(sort));
+            .replace_bound_refts_with(|sort, _, _| Expr::fvar(infcx.define_var(sort)));
 
         env.assume_ensures(infcx, &output.ensures);
         fold_local_ptrs(infcx, env, span).with_span(span)?;

diff --git a/crates/flux-refineck/src/type_env.rs b/crates/flux-refineck/src/type_env.rs
@@ -775,7 +775,7 @@ impl BasicBlockEnv {
     ) -> TypeEnv<'a> {
         let data = self
             .data
-            .replace_bound_refts_with(|sort, _, _| infcx.define_vars(sort));
+            .replace_bound_refts_with(|sort, _, _| Expr::fvar(infcx.define_var(sort)));
         for constr in &data.constrs {
             infcx.assume_pred(constr);
         }

diff --git a/crates/flux-refineck/src/type_env/place_ty.rs b/crates/flux-refineck/src/type_env/place_ty.rs
@@ -828,7 +828,7 @@ fn downcast_enum(
         .variant_sig(adt.did(), variant_idx)?
         .expect("enums cannot be opaque")
         .instantiate(tcx, args, &[])
-        .replace_bound_refts_with(|sort, _, _| infcx.define_vars(sort))
+        .replace_bound_refts_with(|sort, _, _| Expr::fvar(infcx.define_var(sort)))
         .normalize_projections(infcx)?;
 
     // FIXME(nilehmann) We could assert idx1 == variant_def.idx directly, but for aggregate sorts there