Misc improvements (#931)

crates/flux-infer/src/infer.rs

@@ -11,7 +11,7 @@ use flux_middle::{
         fold::TypeFoldable,
         AliasKind, AliasTy, BaseTy, Binder, BoundVariableKinds, CoroutineObligPredicate, ESpan,
         EVar, EVarGen, EarlyBinder, Expr, ExprKind, GenericArg, GenericArgs, HoleKind, InferMode,
-        Lambda, List, Loc, Mutability, Path, PolyVariant, PtrKind, Ref, RefineArgs, RefineArgsExt,
+        Lambda, List, Loc, Mutability, Path, PolyVariant, PtrKind, RefineArgs, RefineArgsExt,
         Region, Sort, Ty, TyKind, Var,
     },
 };
@@ -184,7 +184,7 @@ impl<'infcx, 'genv, 'tcx> InferCtxt<'infcx, 'genv, 'tcx> {
                 let kvar = self.fresh_kvar(&[vars], KVarEncoding::Single);
                 Expr::abs(Lambda::bind_with_fsort(kvar, fsort))
             }
-            InferMode::EVar => self.fresh_evars(sort),
+            InferMode::EVar => self.fresh_evar(),
         }
     }
 
@@ -195,11 +195,11 @@ impl<'infcx, 'genv, 'tcx> InferCtxt<'infcx, 'genv, 'tcx> {
     ) -> Expr {
         match kind {
             HoleKind::Pred => self.fresh_kvar(binders, KVarEncoding::Conj),
-            HoleKind::Expr(sort) => {
+            HoleKind::Expr(_) => {
                 // We only use expression holes to infer early param arguments for opaque types
                 // at function calls. These should be well-scoped in the current scope, so we ignore
                 // the extra `binders` around the hole.
-                self.fresh_evars(&sort)
+                self.fresh_evar()
             }
         }
     }
@@ -212,9 +212,9 @@ impl<'infcx, 'genv, 'tcx> InferCtxt<'infcx, 'genv, 'tcx> {
             .fresh(binders, inner.evars.current_data().iter(), encoding)
     }
 
-    fn fresh_evars(&self, sort: &Sort) -> Expr {
+    fn fresh_evar(&self) -> Expr {
         let evars = &mut self.inner.borrow_mut().evars;
-        Expr::fold_sort(sort, |_| Expr::evar(evars.fresh_in_current()))
+        Expr::evar(evars.fresh_in_current())
     }
 
     pub fn unify_exprs(&self, e1: &Expr, e2: &Expr) {
@@ -521,9 +521,16 @@ impl Sub {
                 infcx.unify_exprs(&path1.to_expr(), &path2.to_expr());
                 self.tys(infcx, &ty1, ty2)
             }
-            (TyKind::Ptr(PtrKind::Mut(re), path), Ref!(_, bound, Mutability::Mut)) => {
+            (
+                TyKind::Ptr(PtrKind::Mut(re), path),
+                TyKind::Indexed(BaseTy::Ref(_, bound, Mutability::Mut), idx),
+            ) => {
+                // We sometimes generate evars for the index of references so we need to make sure
+                // we solve them.
+                self.idxs_eq(infcx, &Expr::unit(), idx);
+
                 let mut at = infcx.at(self.span);
-                env.ptr_to_ref(&mut at, ConstrReason::Call, *re, path, bound.clone())?;
+                env.ptr_to_ref(&mut at, self.reason, *re, path, bound.clone())?;
                 Ok(())
             }
             _ => self.tys(infcx, a, b),

crates/flux-middle/src/pretty.rs

@@ -183,7 +183,7 @@ pub struct PrettyCx<'genv, 'tcx> {
     pub hide_refinements: bool,
     pub hide_regions: bool,
     pub hide_sorts: bool,
-    env: Env,
+    env: BoundVarEnv,
 }
 
 newtype_index! {
@@ -193,12 +193,12 @@ newtype_index! {
 }
 
 #[derive(Default)]
-struct Env {
+struct BoundVarEnv {
     name_gen: IndexGen<BoundVarName>,
     layers: RefCell<Vec<FxHashMap<BoundVar, BoundVarName>>>,
 }
 
-impl Env {
+impl BoundVarEnv {
     fn lookup(&self, debruijn: DebruijnIndex, var: BoundVar) -> Option<BoundVarName> {
         let layers = self.layers.borrow();
         layers
@@ -283,7 +283,7 @@ impl<'genv, 'tcx> PrettyCx<'genv, 'tcx> {
             hide_refinements: false,
             hide_regions: false,
             hide_sorts: true,
-            env: Env::default(),
+            env: BoundVarEnv::default(),
         }
     }
 

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

@@ -317,7 +317,7 @@ impl CanonicalTy {
                 {
                     let ctor = poly_constr_ty
                         .as_ref()
-                        .map(|constr| SubsetTy::new(bty.clone(), Expr::nu(), &constr.pred));
+                        .map(|constr| SubsetTy::new(bty.clone(), idx, &constr.pred));
                     TyOrBase::Base(ctor)
                 } else {
                     TyOrBase::Ty(self.to_ty())

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

@@ -244,6 +244,10 @@ pub enum HoleKind {
     Pred,
     /// A hole used as a refinement argument or index. It will be inferred by generating an evar.
     /// The expression filling the hole must have the provided sort.
+    ///
+    /// NOTE(nilehmann) we used to require the `Sort` for generating the evar because we needed it
+    /// to eta-expand aggregate sorts. We've since removed this behavior but I'm keeping it here
+    /// just in case. We could remove in case it becomes too problematic.
     Expr(Sort),
 }
 

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

@@ -1614,6 +1614,30 @@ impl BaseTy {
             tracked_span_bug!("expected adt `{self:?}`")
         }
     }
+
+    /// A type is an *atom* if it is "self-delimiting", i.e., it has a clear boundary
+    /// when printed. This is used to avoid unnecessary parenthesis when pretty printing.
+    pub fn is_atom(&self) -> bool {
+        // (nilehmann) I'm not sure about this list, please adjust if you get any odd behavior
+        matches!(
+            self,
+            BaseTy::Int(_)
+                | BaseTy::Uint(_)
+                | BaseTy::Slice(_)
+                | BaseTy::Bool
+                | BaseTy::Char
+                | BaseTy::Str
+                | BaseTy::Adt(..)
+                | BaseTy::Tuple(..)
+                // opaque alias are atoms the way we print them now, but they won't
+                // be if we print them as `impl Trait`
+                | BaseTy::Alias(..)
+                | BaseTy::Array(..)
+                | BaseTy::Never
+                | BaseTy::Closure(..)
+                | BaseTy::Coroutine(..)
+        )
+    }
 }
 
 impl<'tcx> ToRustc<'tcx> for BaseTy {

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

@@ -263,7 +263,7 @@ impl Pretty for Ty {
         define_scoped!(cx, f);
         match self.kind() {
             TyKind::Indexed(bty, idx) => {
-                w!("{:?}", bty)?;
+                w!("{:?}", parens!(bty, !bty.is_atom()))?;
                 if cx.hide_refinements {
                     return Ok(());
                 }
@@ -300,15 +300,14 @@ impl Pretty for Ty {
             }
             TyKind::Param(param_ty) => w!("{}", ^param_ty),
             TyKind::Downcast(adt, .., variant_idx, fields) => {
-                let is_struct = adt.is_struct();
                 // base-name
                 w!("{:?}", adt.did())?;
                 // variant-name: if it is not a struct
-                if !is_struct {
+                if !adt.is_struct() {
                     w!("::{}", ^adt.variant(*variant_idx).name)?;
                 }
                 // fields: use curly-braces + names for structs, otherwise use parens
-                if is_struct {
+                if adt.is_struct() {
                     let field_binds = iter::zip(&adt.variant(*variant_idx).fields, fields)
                         .map(|(field_def, value)| FieldBind { name: field_def.name, value });
                     w!(" {{ {:?} }}", join!(", ", field_binds))?;

crates/flux-refineck/src/type_env.rs

@@ -202,10 +202,6 @@ impl<'a> TypeEnv<'a> {
         // t1 <: t2
         let t2 = match bound {
             PtrToRefBound::Ty(t2) => {
-                // FIXME(nilehmann) we could match regions against `t1` instead of mapping the path
-                // to a place which requires annoying bookkeping.
-                // let place = self.bindings.path_to_place(path);
-                // let rust_ty = place.ty(infcx.genv, self.local_decls)?.ty;
                 let t2 = rty_match_regions(&t2, &t1);
                 infcx.subtyping(&t1, &t2, reason)?;
                 t2
@@ -715,7 +711,8 @@ impl BasicBlockEnvShape {
             (GenericArg::Base(ctor1), GenericArg::Base(ctor2)) => {
                 let sty1 = ctor1.as_ref().skip_binder();
                 let sty2 = ctor2.as_ref().skip_binder();
-                debug_assert_eq3!(&sty1.idx, &sty2.idx, &Expr::nu());
+                debug_assert!(sty1.idx.is_nu());
+                debug_assert!(sty2.idx.is_nu());
 
                 let bty = self.join_bty(&sty1.bty, &sty2.bty);
                 let pred = if self.scope.has_free_vars(&sty2.pred) || sty1.pred != sty2.pred {