diff --git a/crates/flux-infer/src/infer.rs b/crates/flux-infer/src/infer.rs index 6ad5d9eb45..816d9f6146 100644 --- a/crates/flux-infer/src/infer.rs +++ b/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), diff --git a/crates/flux-middle/src/pretty.rs b/crates/flux-middle/src/pretty.rs index feaecb5059..950512b133 100644 --- a/crates/flux-middle/src/pretty.rs +++ 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, layers: RefCell>>, } -impl Env { +impl BoundVarEnv { fn lookup(&self, debruijn: DebruijnIndex, var: BoundVar) -> Option { 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(), } } diff --git a/crates/flux-middle/src/rty/canonicalize.rs b/crates/flux-middle/src/rty/canonicalize.rs index e88b49bd31..ba56fa4052 100644 --- a/crates/flux-middle/src/rty/canonicalize.rs +++ b/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()) diff --git a/crates/flux-middle/src/rty/expr.rs b/crates/flux-middle/src/rty/expr.rs index 7f2d464bfb..87956a6bb8 100644 --- a/crates/flux-middle/src/rty/expr.rs +++ b/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), } diff --git a/crates/flux-middle/src/rty/mod.rs b/crates/flux-middle/src/rty/mod.rs index e0184c54ad..0fedb4b8dd 100644 --- a/crates/flux-middle/src/rty/mod.rs +++ b/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 { diff --git a/crates/flux-middle/src/rty/pretty.rs b/crates/flux-middle/src/rty/pretty.rs index c2749ed773..529390cb5d 100644 --- a/crates/flux-middle/src/rty/pretty.rs +++ b/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))?; diff --git a/crates/flux-refineck/src/type_env.rs b/crates/flux-refineck/src/type_env.rs index ac65183e95..3fac7f92bc 100644 --- a/crates/flux-refineck/src/type_env.rs +++ b/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 {