From d1596ee5146391e5d484d6d1fff769a6e8812a8d Mon Sep 17 00:00:00 2001
From: vrindisbacher <vrindisbacher77@gmail.com>
Date: Mon, 13 Jan 2025 12:57:31 -0800
Subject: [PATCH] prevent eta expansion in rty checking

---
 crates/flux-infer/src/infer.rs                | 2 +-
 crates/flux-infer/src/refine_tree.rs          | 3 ++-
 crates/flux-refineck/src/checker.rs           | 8 ++++----
 crates/flux-refineck/src/type_env.rs          | 2 +-
 crates/flux-refineck/src/type_env/place_ty.rs | 2 +-
 5 files changed, 9 insertions(+), 8 deletions(-)

diff --git a/crates/flux-infer/src/infer.rs b/crates/flux-infer/src/infer.rs
index 51119cca54..d310836241 100644
--- 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
index 4de91ff047..758ae2be7c 100644
--- a/crates/flux-infer/src/refine_tree.rs
+++ b/crates/flux-infer/src/refine_tree.rs
@@ -375,7 +375,8 @@ 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
index 46e33373e0..c5aa104bba 100644
--- 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
index f8d95dbd6f..f52e35a127 100644
--- 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
index 1d9133957d..8c8a2e9ad7 100644
--- 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