Delay unfolding (#928)

crates/flux-fhir-analysis/src/lib.rs

@@ -119,7 +119,8 @@ fn qualifiers(genv: GlobalEnv) -> QueryResult<Vec<rty::Qualifier>> {
         .qualifiers()
         .map(|qualifier| {
             let wfckresults = wf::check_qualifier(genv, qualifier)?;
-            normalize(genv, conv::conv_qualifier(genv, qualifier, &wfckresults)?)
+            Ok(conv::conv_qualifier(genv, qualifier, &wfckresults)?
+                .normalize(genv.spec_func_defns()?))
         })
         .try_collect()
 }
@@ -143,16 +144,7 @@ fn invariants_of(genv: GlobalEnv, item: &fhir::Item) -> QueryResult<Vec<rty::Inv
         _ => Err(query_bug!(item.owner_id.local_id(), "expected struct or enum"))?,
     };
     let wfckresults = wf::check_invariants(genv, item.owner_id, params, invariants)?;
-    conv::conv_invariants(
-        genv,
-        item.owner_id.map(|it| it.def_id),
-        params,
-        invariants,
-        &wfckresults,
-    )?
-    .into_iter()
-    .map(|invariant| normalize(genv, invariant))
-    .collect()
+    conv::conv_invariants(genv, item.owner_id.map(|it| it.def_id), params, invariants, &wfckresults)
 }
 
 fn predicates_of(
@@ -487,23 +479,16 @@ fn variants_of(
             let wfckresults = genv.check_wf(local_id)?;
             let mut cx = AfterSortck::new(genv, &wfckresults).into_conv_ctxt();
             let variants = cx.conv_enum_variants(def_id, enum_def)?;
-            let variants = struct_compat::variants(genv, &variants, def_id)?;
-            let variants = variants
-                .into_iter()
-                .map(|variant| normalize(genv, variant))
-                .try_collect()?;
+            let variants = rty::List::from_vec(struct_compat::variants(genv, &variants, def_id)?);
             rty::Opaqueness::Transparent(rty::EarlyBinder(variants))
         }
         fhir::ItemKind::Struct(struct_def) => {
             let wfckresults = genv.check_wf(local_id)?;
             let mut cx = AfterSortck::new(genv, &wfckresults).into_conv_ctxt();
             cx.conv_struct_variant(def_id, struct_def)?
-                .map(|variant| {
+                .map(|variant| -> QueryResult<_> {
                     let variants = struct_compat::variants(genv, &[variant], def_id)?;
-                    variants
-                        .into_iter()
-                        .map(|variant| normalize(genv, variant))
-                        .try_collect()
+                    Ok(rty::List::from_vec(variants))
                 })
                 .transpose()?
                 .map(rty::EarlyBinder)
@@ -528,7 +513,6 @@ fn fn_sig(genv: GlobalEnv, def_id: LocalDefId) -> QueryResult<rty::EarlyBinder<r
         .into_conv_ctxt()
         .conv_fn_sig(def_id, fhir_fn_sig)?;
     let fn_sig = struct_compat::fn_sig(genv, fhir_fn_sig.decl, &fn_sig, def_id)?;
-    let fn_sig = normalize(genv, fn_sig)?;
 
     if config::dump_rty() {
         let generics = genv.generics_of(def_id)?;
@@ -591,10 +575,6 @@ pub fn check_crate_wf(genv: GlobalEnv) -> Result<(), ErrorGuaranteed> {
     errors.into_result()
 }
 
-fn normalize<T: TypeFoldable>(genv: GlobalEnv, t: T) -> QueryResult<T> {
-    Ok(t.normalize(genv.spec_func_defns()?))
-}
-
 mod errors {
     use flux_errors::E0999;
     use flux_macros::Diagnostic;

crates/flux-infer/src/fixpoint_encoding.rs

@@ -19,6 +19,7 @@ use flux_middle::{
     global_env::GlobalEnv,
     queries::QueryResult,
     rty::{self, BoundVariableKind, ESpan, Lambda, List},
+    MaybeExternId,
 };
 use itertools::Itertools;
 use liquid_fixpoint::FixpointResult;
@@ -320,7 +321,7 @@ pub struct FixpointCtxt<'genv, 'tcx, T: Eq + Hash> {
     tags_inv: UnordMap<T, TagIdx>,
     /// [`DefId`] of the item being checked. This can be a function/method or an adt when checking
     /// invariants.
-    def_id: LocalDefId,
+    def_id: MaybeExternId,
 }
 
 pub type FixQueryCache = QueryCache<FixpointResult<TagIdx>>;
@@ -329,7 +330,7 @@ impl<'genv, 'tcx, Tag> FixpointCtxt<'genv, 'tcx, Tag>
 where
     Tag: std::hash::Hash + Eq + Copy,
 {
-    pub fn new(genv: GlobalEnv<'genv, 'tcx>, def_id: LocalDefId, kvars: KVarGen) -> Self {
+    pub fn new(genv: GlobalEnv<'genv, 'tcx>, def_id: MaybeExternId, kvars: KVarGen) -> Self {
         let def_span = genv.tcx().def_span(def_id);
         Self {
             comments: vec![],
@@ -361,7 +362,9 @@ where
 
         let constraint = self.ecx.assume_const_values(constraint);
 
-        let qualifiers = self.ecx.qualifiers_for(self.def_id, &mut self.scx)?;
+        let qualifiers = self
+            .ecx
+            .qualifiers_for(self.def_id.local_id(), &mut self.scx)?;
 
         let mut constants = self
             .ecx
@@ -397,7 +400,7 @@ where
             data_decls: self.scx.into_data_decls(),
         };
         if config::dump_constraint() {
-            dbg::dump_item_info(self.genv.tcx(), self.def_id, "smt2", &task).unwrap();
+            dbg::dump_item_info(self.genv.tcx(), self.def_id.resolved_id(), "smt2", &task).unwrap();
         }
 
         let task_key = self.genv.tcx().def_path_str(self.def_id);

crates/flux-infer/src/refine_tree.rs

@@ -14,8 +14,8 @@ use flux_middle::{
         canonicalize::{Hoister, HoisterDelegate},
         evars::EVarSol,
         fold::{TypeFoldable, TypeSuperVisitable, TypeVisitable, TypeVisitor},
-        BaseTy, EarlyBinder, EarlyReftParam, Expr, GenericArgs, Name, Sort, Ty, TyCtor, TyKind,
-        Var,
+        BaseTy, EarlyBinder, EarlyReftParam, Expr, GenericArgs, Name, Sort, SpecFuncDefns, Ty,
+        TyCtor, TyKind, Var,
     },
 };
 use itertools::Itertools;
@@ -234,8 +234,8 @@ impl RefineTree {
         Ok(RefineTree { root })
     }
 
-    pub fn simplify(&mut self) {
-        self.root.borrow_mut().simplify();
+    pub fn simplify(&mut self, defns: &SpecFuncDefns) {
+        self.root.borrow_mut().simplify(defns);
     }
 
     pub fn into_fixpoint(self, cx: &mut FixpointCtxt<Tag>) -> QueryResult<fixpoint::Constraint> {
@@ -415,14 +415,14 @@ impl std::ops::Deref for NodePtr {
 }
 
 impl Node {
-    fn simplify(&mut self) {
+    fn simplify(&mut self, defns: &SpecFuncDefns) {
         for child in &self.children {
-            child.borrow_mut().simplify();
+            child.borrow_mut().simplify(defns);
         }
 
         match &mut self.kind {
             NodeKind::Head(pred, tag) => {
-                let pred = pred.simplify();
+                let pred = pred.normalize(defns).simplify();
                 if pred.is_trivially_true() {
                     self.kind = NodeKind::True;
                 } else {
@@ -431,7 +431,7 @@ impl Node {
             }
             NodeKind::True => {}
             NodeKind::Assumption(pred) => {
-                *pred = pred.simplify();
+                *pred = pred.normalize(defns).simplify();
                 self.children
                     .extract_if(|child| {
                         matches!(child.borrow().kind, NodeKind::True)

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

@@ -1221,8 +1221,8 @@ mod pretty {
                     }
                 }
                 ExprKind::App(func, args) => {
-                    w!("({:?})({})",
-                        func,
+                    w!("{:?}({})",
+                        parens!(func, !func.is_atom()),
                         ^args
                             .iter()
                             .format_with(", ", |arg, f| f(&format_args_cx!("{:?}", arg)))

crates/flux-refineck/src/checker.rs

@@ -1950,7 +1950,7 @@ pub(crate) mod errors {
             Self { kind: CheckerErrKind::OpaqueStruct(def_id), span }
         }
 
-        pub fn emit_err(self, genv: &GlobalEnv, fn_def_id: MaybeExternId) -> ErrorGuaranteed {
+        pub fn emit(self, genv: GlobalEnv, fn_def_id: MaybeExternId) -> ErrorGuaranteed {
             let dcx = genv.sess().dcx().handle();
             match self.kind {
                 CheckerErrKind::Inference => {

crates/flux-refineck/src/invariants.rs

@@ -1,15 +1,14 @@
-use flux_common::{dbg, iter::IterExt, result::ResultExt};
-use flux_config as config;
+use flux_common::{iter::IterExt, result::ResultExt};
 use flux_errors::ErrorGuaranteed;
 use flux_infer::{
-    fixpoint_encoding::{FixQueryCache, FixpointCtxt, KVarGen},
+    fixpoint_encoding::{FixQueryCache, KVarGen},
     infer::{ConstrReason, Tag},
     refine_tree::RefineTree,
 };
 use flux_middle::{fhir, global_env::GlobalEnv, rty, MaybeExternId};
 use rustc_span::{Span, DUMMY_SP};
 
-use crate::CheckerConfig;
+use crate::{invoke_fixpoint, CheckerConfig};
 
 pub fn check_invariants(
     genv: GlobalEnv,
@@ -57,15 +56,17 @@ fn check_invariant(
         let pred = invariant.apply(&variant.idx);
         rcx.check_pred(&pred, Tag::new(ConstrReason::Other, DUMMY_SP));
     }
-    let mut fcx = FixpointCtxt::new(genv, def_id.local_id(), KVarGen::dummy());
-    if config::dump_constraint() {
-        dbg::dump_item_info(genv.tcx(), def_id.local_id(), "fluxc", &refine_tree).unwrap();
-    }
+    let errors = invoke_fixpoint(
+        genv,
+        cache,
+        def_id,
+        refine_tree,
+        KVarGen::dummy(),
+        checker_config,
+        "fluxc",
+    )
+    .emit(&genv)?;
 
-    let cstr = refine_tree.into_fixpoint(&mut fcx).emit(&genv)?;
-    let errors = fcx
-        .check(cache, cstr, checker_config.scrape_quals)
-        .emit(&genv)?;
     if errors.is_empty() {
         Ok(())
     } else {

crates/flux-refineck/src/lib.rs

@@ -80,24 +80,24 @@ fn report_fixpoint_errors(
 fn invoke_fixpoint(
     genv: GlobalEnv,
     cache: &mut FixQueryCache,
-    local_id: LocalDefId,
+    def_id: MaybeExternId,
     mut refine_tree: RefineTree,
     kvars: KVarGen,
     config: CheckerConfig,
     ext: &str,
-) -> Result<Vec<Tag>, ErrorGuaranteed> {
+) -> QueryResult<Vec<Tag>> {
     if config::dump_constraint() {
-        dbg::dump_item_info(genv.tcx(), local_id, ext, &refine_tree).unwrap();
+        dbg::dump_item_info(genv.tcx(), def_id.resolved_id(), ext, &refine_tree).unwrap();
     }
-    refine_tree.simplify();
+    refine_tree.simplify(genv.spec_func_defns()?);
     let simp_ext = format!("simp.{}", ext);
     if config::dump_constraint() {
-        dbg::dump_item_info(genv.tcx(), local_id, simp_ext, &refine_tree).unwrap();
+        dbg::dump_item_info(genv.tcx(), def_id.resolved_id(), simp_ext, &refine_tree).unwrap();
     }
 
-    let mut fcx = FixpointCtxt::new(genv, local_id, kvars);
-    let cstr = refine_tree.into_fixpoint(&mut fcx).emit(&genv)?;
-    fcx.check(cache, cstr, config.scrape_quals).emit(&genv)
+    let mut fcx = FixpointCtxt::new(genv, def_id, kvars);
+    let cstr = refine_tree.into_fixpoint(&mut fcx)?;
+    fcx.check(cache, cstr, config.scrape_quals)
 }
 
 pub fn check_fn(
@@ -147,34 +147,34 @@ pub fn check_fn(
     dbg::check_fn_span!(genv.tcx(), local_id).in_scope(|| {
         let ghost_stmts = compute_ghost_statements(genv, local_id)
             .with_span(span)
-            .map_err(|err| err.emit_err(&genv, def_id))?;
+            .map_err(|err| err.emit(genv, def_id))?;
 
         // PHASE 1: infer shape of `TypeEnv` at the entry of join points
         let shape_result = Checker::run_in_shape_mode(genv, local_id, &ghost_stmts, config)
-            // Augment the possible CheckError with the functions span so we can report
-            // helpful error messages for opaque struct field accesses
-            .map_err(|err| err.emit_err(&genv, def_id))?;
+            .map_err(|err| err.emit(genv, def_id))?;
         tracing::info!("check_fn::shape");
 
         // PHASE 2: generate refinement tree constraint
         let (refine_tree, kvars) =
             Checker::run_in_refine_mode(genv, local_id, &ghost_stmts, shape_result, config)
-                .map_err(|err| err.emit_err(&genv, def_id))?;
+                .map_err(|err| err.emit(genv, def_id))?;
         tracing::info!("check_fn::refine");
 
         // PHASE 3: invoke fixpoint on the constraint
-        let errors = invoke_fixpoint(genv, cache, local_id, refine_tree, kvars, config, "fluxc")?;
+        let errors = invoke_fixpoint(genv, cache, def_id, refine_tree, kvars, config, "fluxc")
+            .emit(&genv)?;
         tracing::info!("check_fn::fixpoint");
         report_fixpoint_errors(genv, local_id, errors)?;
 
         // PHASE 4: subtyping check for trait-method implementations
         if let Some((refine_tree, kvars)) =
             trait_impl_subtyping(genv, local_id, config.check_overflow, span)
-                .map_err(|err| err.emit_err(&genv, def_id))?
+                .map_err(|err| err.emit(genv, def_id))?
         {
             tracing::info!("check_fn::refine-subtyping");
             let errors =
-                invoke_fixpoint(genv, cache, local_id, refine_tree, kvars, config, "sub.fluxc")?;
+                invoke_fixpoint(genv, cache, def_id, refine_tree, kvars, config, "sub.fluxc")
+                    .emit(&genv)?;
             tracing::info!("check_fn::fixpoint-subtyping");
             report_fixpoint_errors(genv, local_id, errors)?;
         }

tests/tests/neg/error_messages/localize02.rs

@@ -9,7 +9,7 @@
     }
 
     fn inc1(x: int) -> int {
-        x + 1   //~ NOTE this is the condition
+        x + 1
     }
 }]
 
@@ -21,7 +21,7 @@ fn test() {
                  //~| NOTE a precondition cannot be proved
 }
 
-#[flux::sig(fn() -> i32[inc1(0)])] //~ NOTE inside this call
+#[flux::sig(fn() -> i32[inc1(0)])] //~ NOTE this is the condition
 fn moo() -> i32 {
     2 //~ ERROR refinement type
       //~| NOTE a postcondition cannot be proved