Remove all references to define_var

crates/flux-infer/src/infer.rs

@@ -381,10 +381,6 @@ impl<'infcx, 'genv, 'tcx> InferCtxt<'infcx, 'genv, 'tcx> {
         InferCtxt { cursor: self.cursor.branch(), ..*self }
     }
 
-    pub fn define_vars(&mut self, sort: &Sort) -> Expr {
-        self.cursor.define_vars(sort)
-    }
-
     pub fn define_var(&mut self, sort: &Sort) -> Name {
         self.cursor.define_var(sort)
     }

crates/flux-infer/src/refine_tree.rs

@@ -130,21 +130,6 @@ impl<'a> Cursor<'a> {
         fresh
     }
 
-    /// Given a [`sort`] that may contain aggregate sorts ([tuple] or [adt]), it destructs the sort
-    /// recursively, generating multiple fresh variables and returning an "eta-expanded" expression
-    /// of fresh variables. This is in contrast to generating a single fresh variable of aggregate
-    /// sort.
-    ///
-    /// For example, given the sort `(int, (bool, int))` it returns `(a0, (a1, a2))` for fresh variables
-    /// `a0: int`, `a1: bool`, and `a2: int`.
-    ///
-    /// [`sort`]: Sort
-    /// [tuple]: Sort::Tuple
-    /// [adt]: flux_middle::rty::SortCtor::Adt
-    pub(crate) fn define_vars(&mut self, sort: &Sort) -> Expr {
-        Expr::fold_sort(sort, |sort| Expr::fvar(self.define_var(sort)))
-    }
-
     /// Pushes an [assumption] and moves the cursor into the new node.
     ///
     /// [assumption]: NodeKind::Assumption

crates/flux-middle/src/rty/expr.rs

@@ -35,7 +35,7 @@ use crate::{
             TypeFoldable, TypeFolder, TypeSuperFoldable, TypeSuperVisitable, TypeVisitable as _,
             TypeVisitor,
         },
-        BoundVariableKind, SortCtor,
+        BoundVariableKind,
     },
 };
 
@@ -537,20 +537,6 @@ impl Expr {
         Lambda::bind_with_vars(body, inputs.clone(), output)
     }
 
-    pub fn fold_sort(sort: &Sort, mut f: impl FnMut(&Sort) -> Expr) -> Expr {
-        fn go(sort: &Sort, f: &mut impl FnMut(&Sort) -> Expr) -> Expr {
-            match sort {
-                Sort::Tuple(sorts) => Expr::tuple(sorts.iter().map(|sort| go(sort, f)).collect()),
-                Sort::App(SortCtor::Adt(adt_sort_def), args) => {
-                    let flds = adt_sort_def.field_sorts(args);
-                    Expr::adt(adt_sort_def.did(), flds.iter().map(|sort| go(sort, f)).collect())
-                }
-                _ => f(sort),
-            }
-        }
-        go(sort, &mut f)
-    }
-
     /// Applies a field projection to an expression and optimistically try to beta reduce it
     pub fn proj_and_reduce(&self, proj: FieldProj) -> Expr {
         match self.kind() {

crates/flux-refineck/src/invariants.rs

@@ -55,18 +55,18 @@ fn check_invariant(
     for variant_idx in adt_def.variants().indices() {
         let mut rcx = infcx_root.infcx(resolved_id, &region_infercx);
 
-        let variant = genv
+        let variant_sig = genv
             .variant_sig(adt_def.did(), variant_idx)
             .emit(&genv)?
             .expect("cannot check opaque structs")
             .instantiate_identity()
-            .replace_bound_refts_with(|sort, _, _| rcx.define_vars(sort));
+            .replace_bound_refts_with(|sort, _, _| rty::Expr::fvar(rcx.define_var(sort)));
 
-        for ty in variant.fields() {
+        for ty in variant_sig.fields() {
             let ty = rcx.unpack(ty);
             rcx.assume_invariants(&ty);
         }
-        let pred = invariant.apply(&variant.idx);
+        let pred = invariant.apply(&variant_sig.idx);
         rcx.check_pred(&pred, Tag::new(ConstrReason::Other, DUMMY_SP));
     }
     let errors = infcx_root

crates/flux-refineck/src/type_env/place_ty.rs

@@ -809,12 +809,12 @@ fn struct_variant(genv: GlobalEnv, def_id: DefId) -> InferResult<EarlyBinder<Bin
 
 /// In contrast (w.r.t. `struct`) downcast on `enum` works as follows.
 /// Given
-///     * a "place" `x : T[i..]`
-///     * a "variant" of type `forall z..,(y:t...) => E[j...]`
+///     * a "place" `x : T[i]`
+///     * a "variant" of type `forall z..,(y:t...) => E[j]`
 /// We want `downcast` to return a vector of types _and an assertion_ by
-///     1. *Instantiate* the type to fresh names `z'...` to get `(y:t'...) => T[j'...]`
+///     1. *Instantiate* the type to fresh names `z'...` to get `(y:t'...) => T[j']`
 ///     2. *Unpack* the fields using `y:t'...`
-///     3. *Assert* the constraint `i == j'...`
+///     3. *Assume* the constraint `i == j'`
 fn downcast_enum(
     infcx: &mut InferCtxt,
     adt: &AdtDef,
@@ -823,28 +823,17 @@ fn downcast_enum(
     idx1: &Expr,
 ) -> InferResult<Vec<Ty>> {
     let tcx = infcx.genv.tcx();
-    let variant_def = infcx
+    let variant_sig = infcx
         .genv
         .variant_sig(adt.did(), variant_idx)?
         .expect("enums cannot be opaque")
         .instantiate(tcx, args, &[])
         .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
-    // are currently two problems.
-    // 1. The encoded fixpoint constraint won't parse if it has nested expressions inside data constructors.
-    // 2. We could expand the equality during encoding, but that would require annotating the sort
-    // of the equality operator, which will be cumbersome because we create equalities in some places where
-    // the sort is not readily available.
-    let constr = Expr::and_from_iter(adt.sort_def().projections().map(|proj| {
-        let e1 = idx1.proj_and_reduce(proj);
-        let e2 = variant_def.idx.proj_and_reduce(proj);
-        Expr::eq(e1, e2)
-    }));
-    infcx.assume_pred(&constr);
-
-    Ok(variant_def.fields.to_vec())
+    infcx.assume_pred(Expr::eq(idx1, variant_sig.idx));
+
+    Ok(variant_sig.fields.to_vec())
 }
 
 fn fold(