Delay unfolding

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/refine_tree.rs

@@ -233,8 +233,8 @@ impl RefineTree {
         Ok(RefineTree { root })
     }
 
-    pub fn simplify(&mut self) {
-        self.root.borrow_mut().simplify();
+    pub fn simplify(&mut self, genv: GlobalEnv) -> QueryResult {
+        self.root.borrow_mut().simplify(genv)
     }
 
     pub fn into_fixpoint(self, cx: &mut FixpointCtxt<Tag>) -> QueryResult<fixpoint::Constraint> {
@@ -414,14 +414,14 @@ impl std::ops::Deref for NodePtr {
 }
 
 impl Node {
-    fn simplify(&mut self) {
+    fn simplify(&mut self, genv: GlobalEnv) -> QueryResult {
         for child in &self.children {
-            child.borrow_mut().simplify();
+            child.borrow_mut().simplify(genv)?;
         }
 
         match &mut self.kind {
             NodeKind::Head(pred, tag) => {
-                let pred = pred.simplify();
+                let pred = pred.normalize(genv.spec_func_defns()?).simplify();
                 if pred.is_trivially_true() {
                     self.kind = NodeKind::True;
                 } else {
@@ -430,7 +430,7 @@ impl Node {
             }
             NodeKind::True => {}
             NodeKind::Assumption(pred) => {
-                *pred = pred.simplify();
+                *pred = pred.normalize(genv.spec_func_defns()?).simplify();
                 self.children
                     .extract_if(|child| {
                         matches!(child.borrow().kind, NodeKind::True)
@@ -447,6 +447,7 @@ impl Node {
         if !self.is_leaf() && self.children.is_empty() {
             self.kind = NodeKind::True;
         }
+        Ok(())
     }
 
     fn is_leaf(&self) -> bool {

crates/flux-refineck/src/invariants.rs

@@ -61,6 +61,7 @@ fn check_invariant(
     if config::dump_constraint() {
         dbg::dump_item_info(genv.tcx(), def_id.local_id(), "fluxc", &refine_tree).unwrap();
     }
+    refine_tree.simplify(genv).emit(&genv)?;
 
     let cstr = refine_tree.into_fixpoint(&mut fcx).emit(&genv)?;
     let errors = fcx

crates/flux-refineck/src/lib.rs

@@ -89,7 +89,7 @@ fn invoke_fixpoint(
     if config::dump_constraint() {
         dbg::dump_item_info(genv.tcx(), local_id, ext, &refine_tree).unwrap();
     }
-    refine_tree.simplify();
+    refine_tree.simplify(genv).emit(&genv)?;
     let simp_ext = format!("simp.{}", ext);
     if config::dump_constraint() {
         dbg::dump_item_info(genv.tcx(), local_id, simp_ext, &refine_tree).unwrap();