Prefer InferErr over CheckerErr if we can (#936)

flux-rs · Dec 11, 2024 · 35e25de · 35e25de
1 parent 2315bb0
commit 35e25de
Show file tree

Hide file tree

Showing 11 changed files with 103 additions and 130 deletions.
diff --git a/crates/flux-fhir-analysis/src/conv/mod.rs b/crates/flux-fhir-analysis/src/conv/mod.rs
@@ -1330,7 +1330,7 @@ impl<'genv, 'tcx: 'genv, P: ConvPhase<'genv, 'tcx>> ConvCtxt<P> {
         match self.owner() {
             FluxOwnerId::Rust(owner_id) => {
                 let def_id = self.genv().maybe_extern_id(owner_id.def_id);
-                Refiner::default(self.genv(), def_id.resolved_id())
+                Refiner::default_for_item(self.genv(), def_id.resolved_id())
             }
             FluxOwnerId::Flux(_) => Err(query_bug!("cannot refine types insicde flux item")),
         }

diff --git a/crates/flux-fhir-analysis/src/conv/struct_compat.rs b/crates/flux-fhir-analysis/src/conv/struct_compat.rs
@@ -30,7 +30,7 @@ pub(crate) fn type_alias(
     def_id: MaybeExternId,
 ) -> QueryResult<rty::TyCtor> {
     let rust_ty = genv.lower_type_of(def_id.resolved_id())?.skip_binder();
-    let expected = Refiner::default(genv, def_id.resolved_id())?.refine_ty(&rust_ty)?;
+    let expected = Refiner::default_for_item(genv, def_id.resolved_id())?.refine_ty(&rust_ty)?;
     let mut zipper = Zipper::new(genv, def_id);
 
     if zipper
@@ -55,7 +55,7 @@ pub(crate) fn fn_sig(
 ) -> QueryResult<rty::PolyFnSig> {
     let rust_fn_sig = genv.lower_fn_sig(def_id.resolved_id())?.skip_binder();
     let expected =
-        Refiner::default(genv, def_id.resolved_id())?.refine_poly_fn_sig(&rust_fn_sig)?;
+        Refiner::default_for_item(genv, def_id.resolved_id())?.refine_poly_fn_sig(&rust_fn_sig)?;
 
     let mut zipper = Zipper::new(genv, def_id);
     if let Err(err) = zipper.zip_poly_fn_sig(fn_sig, &expected) {
@@ -72,7 +72,7 @@ pub(crate) fn variants(
     variants: &[rty::PolyVariant],
     adt_def_id: MaybeExternId,
 ) -> QueryResult<Vec<rty::PolyVariant>> {
-    let refiner = Refiner::default(genv, adt_def_id.resolved_id())?;
+    let refiner = Refiner::default_for_item(genv, adt_def_id.resolved_id())?;
     let mut zipper = Zipper::new(genv, adt_def_id);
     // TODO check same number of variants
     for (i, variant) in variants.iter().enumerate() {

diff --git a/crates/flux-fhir-analysis/src/lib.rs b/crates/flux-fhir-analysis/src/lib.rs
@@ -432,15 +432,15 @@ fn type_of(genv: GlobalEnv, def_id: LocalDefId) -> QueryResult<rty::EarlyBinder<
                 }
                 MaybeExternId::Extern(_, extern_id) => {
                     let ty = genv.lower_type_of(extern_id)?.skip_binder();
-                    Refiner::default(genv, ty_param_owner(genv, extern_id))?
+                    Refiner::default_for_item(genv, ty_param_owner(genv, extern_id))?
                         .refine_ty_or_base(&ty)?
                         .into()
                 }
             }
         }
         DefKind::Impl { .. } | DefKind::Struct | DefKind::Enum | DefKind::AssocTy => {
             let ty = genv.lower_type_of(def_id.local_id())?.skip_binder();
-            Refiner::default(genv, def_id.resolved_id())?
+            Refiner::default_for_item(genv, def_id.resolved_id())?
                 .refine_ty_or_base(&ty)?
                 .into()
         }

diff --git a/crates/flux-middle/src/global_env.rs b/crates/flux-middle/src/global_env.rs
@@ -224,7 +224,7 @@ impl<'genv, 'tcx> GlobalEnv<'genv, 'tcx> {
         let trait_ref = trait_ref
             .lower(self.tcx())
             .map_err(|err| QueryErr::unsupported(trait_ref.def_id, err.into_err()))?;
-        let trait_ref = Refiner::default(self, impl_id)?.refine_trait_ref(&trait_ref)?;
+        let trait_ref = Refiner::default_for_item(self, impl_id)?.refine_trait_ref(&trait_ref)?;
         Ok(Some(rty::EarlyBinder(trait_ref)))
     }
 

diff --git a/crates/flux-middle/src/queries.rs b/crates/flux-middle/src/queries.rs
@@ -491,7 +491,8 @@ impl<'genv, 'tcx> Queries<'genv, 'tcx> {
                         .lower(genv.tcx())
                         .map_err(|err| QueryErr::unsupported(def_id, err))?;
 
-                    let clauses = Refiner::default(genv, def_id)?.refine_clauses(&clauses)?;
+                    let clauses =
+                        Refiner::default_for_item(genv, def_id)?.refine_clauses(&clauses)?;
 
                     Ok(rty::EarlyBinder(clauses))
                 },
@@ -512,8 +513,8 @@ impl<'genv, 'tcx> Queries<'genv, 'tcx> {
                 |def_id| genv.cstore().predicates_of(def_id),
                 |def_id| {
                     let predicates = genv.lower_predicates_of(def_id)?;
-                    let predicates =
-                        Refiner::default(genv, def_id)?.refine_generic_predicates(&predicates)?;
+                    let predicates = Refiner::default_for_item(genv, def_id)?
+                        .refine_generic_predicates(&predicates)?;
                     Ok(rty::EarlyBinder(predicates))
                 },
             )
@@ -626,7 +627,7 @@ impl<'genv, 'tcx> Queries<'genv, 'tcx> {
                     };
                     let ty = genv.lower_type_of(def_id)?.skip_binder();
                     Ok(rty::EarlyBinder(
-                        Refiner::default(genv, generics_def_id)?
+                        Refiner::default_for_item(genv, generics_def_id)?
                             .refine_ty_or_base(&ty)?
                             .into(),
                     ))
@@ -653,7 +654,8 @@ impl<'genv, 'tcx> Queries<'genv, 'tcx> {
                         .variants()
                         .indices()
                         .map(|variant_idx| {
-                            Refiner::default(genv, def_id)?.refine_variant_def(def_id, variant_idx)
+                            Refiner::default_for_item(genv, def_id)?
+                                .refine_variant_def(def_id, variant_idx)
                         })
                         .try_collect()?;
                     Ok(rty::Opaqueness::Transparent(rty::EarlyBinder(variants)))
@@ -675,7 +677,8 @@ impl<'genv, 'tcx> Queries<'genv, 'tcx> {
                 |def_id| genv.cstore().fn_sig(def_id),
                 |def_id| {
                     let fn_sig = genv.lower_fn_sig(def_id)?.skip_binder();
-                    let fn_sig = Refiner::default(genv, def_id)?.refine_poly_fn_sig(&fn_sig)?;
+                    let fn_sig =
+                        Refiner::default_for_item(genv, def_id)?.refine_poly_fn_sig(&fn_sig)?;
                     Ok(rty::EarlyBinder(fn_sig))
                 },
             )

diff --git a/crates/flux-middle/src/rty/mod.rs b/crates/flux-middle/src/rty/mod.rs
@@ -1213,7 +1213,7 @@ impl Ty {
         let def_id = genv.tcx().require_lang_item(LangItem::OwnedBox, None);
 
         let generics = genv.generics_of(def_id)?;
-        let alloc_ty = Refiner::default(genv, def_id)?.refine_ty(
+        let alloc_ty = Refiner::default_for_item(genv, def_id)?.refine_ty(
             &genv
                 .lower_type_of(generics.own_params[1].def_id)?
                 .skip_binder(),

diff --git a/crates/flux-middle/src/rty/projections.rs b/crates/flux-middle/src/rty/projections.rs
@@ -118,7 +118,7 @@ impl<'genv, 'tcx, 'cx> Normalizer<'genv, 'tcx, 'cx> {
         )
         .expect_type();
         let rustc_ty = ty.lower(self.tcx()).unwrap();
-        Ok(Refiner::default(self.genv, self.def_id)?
+        Ok(Refiner::default_for_item(self.genv, self.def_id)?
             .refine_ty_or_base(&rustc_ty)?
             .expect_base())
     }

diff --git a/crates/flux-middle/src/rty/refining.rs b/crates/flux-middle/src/rty/refining.rs
@@ -76,7 +76,7 @@ pub struct Refiner<'genv, 'tcx> {
 }
 
 impl<'genv, 'tcx> Refiner<'genv, 'tcx> {
-    pub fn new(
+    pub fn new_for_item(
         genv: GlobalEnv<'genv, 'tcx>,
         def_id: DefId,
         refine: fn(rty::BaseTy) -> rty::SubsetTyCtor,
@@ -85,12 +85,12 @@ impl<'genv, 'tcx> Refiner<'genv, 'tcx> {
         Ok(Self { genv, def_id, generics, refine })
     }
 
-    pub fn default(genv: GlobalEnv<'genv, 'tcx>, def_id: DefId) -> QueryResult<Self> {
-        Self::new(genv, def_id, refine_default)
+    pub fn default_for_item(genv: GlobalEnv<'genv, 'tcx>, def_id: DefId) -> QueryResult<Self> {
+        Self::new_for_item(genv, def_id, refine_default)
     }
 
     pub fn with_holes(genv: GlobalEnv<'genv, 'tcx>, def_id: DefId) -> QueryResult<Self> {
-        Self::new(genv, def_id, |bty| {
+        Self::new_for_item(genv, def_id, |bty| {
             let sort = bty.sort();
             let constr = rty::SubsetTy::new(
                 bty.shift_in_escaping(1),