diff --git a/Cargo.lock b/Cargo.lock
index 791f30625f..58f347b164 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -584,6 +584,7 @@ dependencies = [
  "flux-errors",
  "flux-macros",
  "flux-middle",
+ "flux-rustc-bridge",
  "itertools 0.13.0",
  "liquid-fixpoint",
  "pad-adapter",
diff --git a/crates/flux-driver/src/callbacks.rs b/crates/flux-driver/src/callbacks.rs
index e7525d4495..85e9d7d743 100644
--- a/crates/flux-driver/src/callbacks.rs
+++ b/crates/flux-driver/src/callbacks.rs
@@ -1,7 +1,6 @@
 use flux_common::{bug, cache::QueryCache, dbg, iter::IterExt, result::ResultExt};
 use flux_config as config;
 use flux_errors::FluxSession;
-use flux_fhir_analysis::compare_impl_item;
 use flux_infer::fixpoint_encoding::FixQueryCache;
 use flux_metadata::CStore;
 use flux_middle::{fhir, global_env::GlobalEnv, queries::Providers, Specs};
@@ -229,7 +228,8 @@ impl<'genv, 'tcx> CrateChecker<'genv, 'tcx> {
             }
             DefKind::Impl { of_trait } => {
                 if of_trait {
-                    compare_impl_item::check_impl_against_trait(self.genv, def_id)?;
+                    refineck::compare_impl_item::check_impl_against_trait(self.genv, def_id)
+                        .emit(&self.genv)?;
                 }
                 Ok(())
             }
diff --git a/crates/flux-fhir-analysis/locales/en-US.ftl b/crates/flux-fhir-analysis/locales/en-US.ftl
index 1fc68da899..781429944b 100644
--- a/crates/flux-fhir-analysis/locales/en-US.ftl
+++ b/crates/flux-fhir-analysis/locales/en-US.ftl
@@ -267,14 +267,5 @@ fhir_analysis_generics_on_ty_param =
 fhir_analysis_generics_on_self_ty =
     generic arguments are not allowed on self type
 
-# Check impl against trait errors
-
-fhir_analysis_incompatible_sort =
-    implemented associated refinement `{$name}` has an incompatible sort for trait
-    .label = expected `{$expected}`, found `{$found}`
-
 fhir_analysis_invalid_assoc_reft =
     associated refinement `{$name}` is not a member of trait `{$trait_}`
-
-fhir_analysis_missing_assoc_reft =
-    associated refinement `{$name}` is not defined in implementation of trait `{$trait_}`
diff --git a/crates/flux-fhir-analysis/src/conv/mod.rs b/crates/flux-fhir-analysis/src/conv/mod.rs
index e9b1516c74..8e3dca284a 100644
--- a/crates/flux-fhir-analysis/src/conv/mod.rs
+++ b/crates/flux-fhir-analysis/src/conv/mod.rs
@@ -43,8 +43,6 @@ use rustc_target::spec::abi;
 use rustc_trait_selection::traits;
 use rustc_type_ir::DebruijnIndex;
 
-use crate::compare_impl_item::errors::InvalidAssocReft;
-
 /// Wrapper over a type implementing [`ConvPhase`]. We have this to implement most functionality as
 /// inherent methods instead of defining them as default implementation in the trait definition.
 #[repr(transparent)]
@@ -1997,7 +1995,7 @@ impl<'genv, 'tcx: 'genv, P: ConvPhase<'genv, 'tcx>> ConvCtxt<P> {
             rty::AliasReft { trait_id, name: alias.name, args: List::from_vec(generic_args) };
 
         let Some(fsort) = alias_reft.fsort(self.genv())? else {
-            return Err(self.emit(InvalidAssocReft::new(
+            return Err(self.emit(errors::InvalidAssocReft::new(
                 alias.path.span,
                 alias_reft.name,
                 format!("{:?}", alias.path),
@@ -2520,4 +2518,19 @@ mod errors {
         #[primary_span]
         pub span: Span,
     }
+
+    #[derive(Diagnostic)]
+    #[diag(fhir_analysis_invalid_assoc_reft, code = E0999)]
+    pub struct InvalidAssocReft {
+        #[primary_span]
+        span: Span,
+        trait_: String,
+        name: Symbol,
+    }
+
+    impl InvalidAssocReft {
+        pub(crate) fn new(span: Span, name: Symbol, trait_: String) -> Self {
+            Self { span, trait_, name }
+        }
+    }
 }
diff --git a/crates/flux-fhir-analysis/src/lib.rs b/crates/flux-fhir-analysis/src/lib.rs
index 43ee861590..6d02d975b8 100644
--- a/crates/flux-fhir-analysis/src/lib.rs
+++ b/crates/flux-fhir-analysis/src/lib.rs
@@ -5,14 +5,12 @@ extern crate rustc_data_structures;
 extern crate rustc_errors;
 
 extern crate rustc_hir;
-extern crate rustc_infer;
 extern crate rustc_middle;
 extern crate rustc_span;
 extern crate rustc_target;
 extern crate rustc_trait_selection;
 extern crate rustc_type_ir;
 
-pub mod compare_impl_item;
 mod conv;
 mod wf;
 
diff --git a/crates/flux-infer/Cargo.toml b/crates/flux-infer/Cargo.toml
index e64b4bfefb..177a5f53ac 100644
--- a/crates/flux-infer/Cargo.toml
+++ b/crates/flux-infer/Cargo.toml
@@ -9,6 +9,7 @@ flux-config.workspace = true
 flux-errors.workspace = true
 flux-macros.workspace = true
 flux-middle.workspace = true
+flux-rustc-bridge.workspace = true
 
 itertools.workspace = true
 liquid-fixpoint.workspace = true
diff --git a/crates/flux-infer/src/infer.rs b/crates/flux-infer/src/infer.rs
index e54cc232ee..51119cca54 100644
--- a/crates/flux-infer/src/infer.rs
+++ b/crates/flux-infer/src/infer.rs
@@ -27,6 +27,7 @@ use rustc_span::Span;
 use crate::{
     evars::{EVarState, EVarStore},
     fixpoint_encoding::{FixQueryCache, FixpointCtxt, KVarEncoding, KVarGen},
+    projections::NormalizeExt as _,
     refine_tree::{AssumeInvariants, Cursor, Marker, RefineTree, Scope, Unpacker},
 };
 
@@ -101,6 +102,7 @@ impl<'genv, 'tcx> InferCtxtRootBuilder<'genv, 'tcx> {
         self
     }
 
+    /// When provided use `generic_args` to instantiate sorts
     pub fn with_generic_args(mut self, generic_args: &GenericArgs) -> Self {
         self.generic_args = Some(generic_args.clone());
         self
@@ -451,16 +453,11 @@ impl<'genv, 'tcx> InferCtxtAt<'_, '_, 'genv, 'tcx> {
             if let rty::ClauseKind::Projection(projection_pred) = clause.kind_skipping_binder() {
                 let impl_elem = BaseTy::projection(projection_pred.projection_ty)
                     .to_ty()
-                    .normalize_projections(
-                        self.infcx.genv,
-                        self.infcx.region_infcx,
-                        self.infcx.def_id,
-                    )?;
-                let term = projection_pred.term.to_ty().normalize_projections(
-                    self.infcx.genv,
-                    self.infcx.region_infcx,
-                    self.infcx.def_id,
-                )?;
+                    .normalize_projections(self.infcx)?;
+                let term = projection_pred
+                    .term
+                    .to_ty()
+                    .normalize_projections(self.infcx)?;
 
                 // TODO: does this really need to be invariant? https://github.com/flux-rs/flux/pull/478#issuecomment-1654035374
                 self.subtyping(&impl_elem, &term, reason)?;
@@ -962,7 +959,7 @@ impl<'a, E: LocEnv> Sub<'a, E> {
                     let alias_ty = pred.projection_ty.with_self_ty(bty.to_subset_ty_ctor());
                     let ty1 = BaseTy::Alias(AliasKind::Projection, alias_ty)
                         .to_ty()
-                        .normalize_projections(infcx.genv, infcx.region_infcx, infcx.def_id)?;
+                        .normalize_projections(infcx)?;
                     let ty2 = pred.term.to_ty();
                     self.tys(infcx, &ty1, &ty2)?;
                 }
diff --git a/crates/flux-infer/src/lib.rs b/crates/flux-infer/src/lib.rs
index 696d818f05..f82a489cf9 100644
--- a/crates/flux-infer/src/lib.rs
+++ b/crates/flux-infer/src/lib.rs
@@ -7,9 +7,11 @@ extern crate rustc_infer;
 extern crate rustc_macros;
 extern crate rustc_middle;
 extern crate rustc_span;
+extern crate rustc_trait_selection;
 extern crate rustc_type_ir;
 
 mod evars;
 pub mod fixpoint_encoding;
 pub mod infer;
+pub mod projections;
 pub mod refine_tree;
diff --git a/crates/flux-middle/src/rty/projections.rs b/crates/flux-infer/src/projections.rs
similarity index 90%
rename from crates/flux-middle/src/rty/projections.rs
rename to crates/flux-infer/src/projections.rs
index 6a6a486a4f..c0f552c9b2 100644
--- a/crates/flux-middle/src/rty/projections.rs
+++ b/crates/flux-infer/src/projections.rs
@@ -1,54 +1,61 @@
 use std::iter;
 
-use flux_arc_interner::List;
 use flux_common::{bug, tracked_span_bug};
+use flux_middle::{
+    global_env::GlobalEnv,
+    queries::{QueryErr, QueryResult},
+    rty::{
+        fold::{FallibleTypeFolder, TypeFoldable, TypeSuperFoldable, TypeVisitable},
+        refining::Refiner,
+        subst::{GenericsSubstDelegate, GenericsSubstFolder},
+        AliasKind, AliasReft, AliasTy, BaseTy, Binder, Clause, ClauseKind, Const, ConstKind,
+        EarlyBinder, Expr, ExprKind, GenericArg, List, ProjectionPredicate, RefineArgs, Region,
+        Sort, SubsetTy, SubsetTyCtor, Ty, TyKind,
+    },
+};
 use flux_rustc_bridge::{lowering::Lower, ToRustc};
 use rustc_hir::def_id::DefId;
-use rustc_infer::{infer::InferCtxt, traits::Obligation};
+use rustc_infer::traits::Obligation;
 use rustc_middle::{
     traits::{ImplSource, ObligationCause},
     ty::TyCtxt,
 };
 use rustc_trait_selection::traits::SelectionContext;
 
-use super::{
-    fold::{FallibleTypeFolder, TypeFoldable, TypeSuperFoldable},
-    subst::{GenericsSubstDelegate, GenericsSubstFolder},
-    AliasKind, AliasReft, AliasTy, BaseTy, Binder, Clause, ClauseKind, Const, EarlyBinder, Expr,
-    ExprKind, GenericArg, ProjectionPredicate, RefineArgs, Region, Sort, SubsetTy, SubsetTyCtor,
-    Ty, TyKind,
-};
-use crate::{
-    global_env::GlobalEnv,
-    queries::{QueryErr, QueryResult},
-    rty::{fold::TypeVisitable, refining::Refiner},
-};
+use crate::infer::InferCtxt;
+
+pub trait NormalizeExt: TypeFoldable {
+    fn normalize_projections<'tcx>(&self, infcx: &mut InferCtxt) -> QueryResult<Self>;
+}
 
-pub(crate) struct Normalizer<'genv, 'tcx, 'cx> {
-    genv: GlobalEnv<'genv, 'tcx>,
-    selcx: SelectionContext<'cx, 'tcx>,
-    def_id: DefId,
+impl<T: TypeFoldable> NormalizeExt for T {
+    fn normalize_projections<'tcx>(&self, infcx: &mut InferCtxt) -> QueryResult<Self> {
+        let mut normalizer = Normalizer::new(infcx.branch())?;
+        self.erase_regions().try_fold_with(&mut normalizer)
+    }
+}
+
+struct Normalizer<'infcx, 'genv, 'tcx> {
+    infcx: InferCtxt<'infcx, 'genv, 'tcx>,
+    selcx: SelectionContext<'infcx, 'tcx>,
     param_env: List<Clause>,
 }
 
-impl<'genv, 'tcx, 'cx> Normalizer<'genv, 'tcx, 'cx> {
-    pub(crate) fn new(
-        genv: GlobalEnv<'genv, 'tcx>,
-        infcx: &'cx InferCtxt<'tcx>,
-        callsite_def_id: DefId,
-    ) -> QueryResult<Self> {
-        let param_env = genv
-            .predicates_of(callsite_def_id)?
+impl<'infcx, 'genv, 'tcx> Normalizer<'infcx, 'genv, 'tcx> {
+    fn new(infcx: InferCtxt<'infcx, 'genv, 'tcx>) -> QueryResult<Self> {
+        let param_env = infcx
+            .genv
+            .predicates_of(infcx.def_id)?
             .instantiate_identity()
             .predicates
             .clone();
-        let selcx = SelectionContext::new(infcx);
-        Ok(Normalizer { genv, selcx, def_id: callsite_def_id, param_env })
+        let selcx = SelectionContext::new(infcx.region_infcx);
+        Ok(Normalizer { infcx, selcx, param_env })
     }
 
     fn get_impl_id_of_alias_reft(&mut self, alias_reft: &AliasReft) -> QueryResult<Option<DefId>> {
         let tcx = self.tcx();
-        let def_id = self.def_id;
+        let def_id = self.def_id();
         let selcx = &mut self.selcx;
 
         let trait_pred = Obligation::new(
@@ -71,7 +78,7 @@ impl<'genv, 'tcx, 'cx> Normalizer<'genv, 'tcx, 'cx> {
     ) -> QueryResult<Expr> {
         if let Some(impl_def_id) = self.get_impl_id_of_alias_reft(alias_reft)? {
             let impl_trait_ref = self
-                .genv
+                .genv()
                 .impl_trait_ref(impl_def_id)?
                 .unwrap()
                 .skip_binder();
@@ -86,7 +93,7 @@ impl<'genv, 'tcx, 'cx> Normalizer<'genv, 'tcx, 'cx> {
             let tcx = self.tcx();
 
             let pred = self
-                .genv
+                .genv()
                 .assoc_refinement_def(impl_def_id, alias_reft.name)?
                 .instantiate(tcx, &args, &[]);
 
@@ -106,7 +113,7 @@ impl<'genv, 'tcx, 'cx> Normalizer<'genv, 'tcx, 'cx> {
     ) -> QueryResult<SubsetTyCtor> {
         let projection_ty = obligation.to_rustc(self.tcx());
         let cause = ObligationCause::dummy();
-        let param_env = self.tcx().param_env(self.def_id);
+        let param_env = self.rustc_param_env();
 
         let ty = rustc_trait_selection::traits::normalize_projection_ty(
             &mut self.selcx,
@@ -118,7 +125,7 @@ impl<'genv, 'tcx, 'cx> Normalizer<'genv, 'tcx, 'cx> {
         )
         .expect_type();
         let rustc_ty = ty.lower(self.tcx()).unwrap();
-        Ok(Refiner::default_for_item(self.genv, self.def_id)?
+        Ok(Refiner::default_for_item(self.genv(), self.def_id())?
             .refine_ty_or_base(&rustc_ty)?
             .expect_base())
     }
@@ -139,7 +146,7 @@ impl<'genv, 'tcx, 'cx> Normalizer<'genv, 'tcx, 'cx> {
             return Ok((ty != orig_ty, ty));
         }
         if candidates.len() > 1 {
-            bug!("ambiguity when resolving `{obligation:?}` in {:?}", self.def_id);
+            bug!("ambiguity when resolving `{obligation:?}` in {:?}", self.def_id());
         }
         let ctor = self.confirm_candidate(candidates.pop().unwrap(), obligation)?;
         Ok((true, ctor))
@@ -173,7 +180,7 @@ impl<'genv, 'tcx, 'cx> Normalizer<'genv, 'tcx, 'cx> {
         impl_def_id: DefId,
     ) -> QueryResult {
         let mut projection_preds: Vec<_> = self
-            .genv
+            .genv()
             .predicates_of(impl_def_id)?
             .skip_binder()
             .predicates
@@ -222,7 +229,7 @@ impl<'genv, 'tcx, 'cx> Normalizer<'genv, 'tcx, 'cx> {
                 //            => {T -> {v. i32[v] | v > 0}, A -> Global}
 
                 let impl_trait_ref = self
-                    .genv
+                    .genv()
                     .impl_trait_ref(impl_def_id)?
                     .unwrap()
                     .skip_binder();
@@ -250,7 +257,7 @@ impl<'genv, 'tcx, 'cx> Normalizer<'genv, 'tcx, 'cx> {
 
                 let tcx = self.tcx();
                 Ok(self
-                    .genv
+                    .genv()
                     .type_of(assoc_type_id)?
                     .instantiate(tcx, &args, &[])
                     .expect_subset_ty_ctor())
@@ -280,7 +287,7 @@ impl<'genv, 'tcx, 'cx> Normalizer<'genv, 'tcx, 'cx> {
             && let BaseTy::Alias(AliasKind::Opaque, alias_ty) = ctor.as_bty_skipping_binder()
         {
             debug_assert!(!alias_ty.has_escaping_bvars());
-            let bounds = self.genv.item_bounds(alias_ty.def_id)?.instantiate(
+            let bounds = self.genv().item_bounds(alias_ty.def_id)?.instantiate(
                 self.tcx(),
                 &alias_ty.args,
                 &alias_ty.refine_args,
@@ -316,12 +323,20 @@ impl<'genv, 'tcx, 'cx> Normalizer<'genv, 'tcx, 'cx> {
         Ok(())
     }
 
+    fn def_id(&self) -> DefId {
+        self.infcx.def_id
+    }
+
+    fn genv(&self) -> GlobalEnv<'genv, 'tcx> {
+        self.infcx.genv
+    }
+
     fn tcx(&self) -> TyCtxt<'tcx> {
         self.selcx.tcx()
     }
 
     fn rustc_param_env(&self) -> rustc_middle::ty::ParamEnv<'tcx> {
-        self.selcx.tcx().param_env(self.def_id)
+        self.selcx.tcx().param_env(self.def_id())
     }
 }
 
@@ -348,7 +363,7 @@ impl FallibleTypeFolder for Normalizer<'_, '_, '_> {
     fn try_fold_sort(&mut self, sort: &Sort) -> Result<Sort, Self::Error> {
         match sort {
             Sort::Alias(AliasKind::Weak, alias_ty) => {
-                self.genv
+                self.genv()
                     .normalize_weak_alias_sort(alias_ty)?
                     .try_fold_with(self)
             }
@@ -374,9 +389,9 @@ impl FallibleTypeFolder for Normalizer<'_, '_, '_> {
         match ty.kind() {
             TyKind::Indexed(BaseTy::Alias(AliasKind::Weak, alias_ty), idx) => {
                 Ok(self
-                    .genv
+                    .genv()
                     .type_of(alias_ty.def_id)?
-                    .instantiate(self.genv.tcx(), &alias_ty.args, &alias_ty.refine_args)
+                    .instantiate(self.tcx(), &alias_ty.args, &alias_ty.refine_args)
                     .expect_ctor()
                     .replace_bound_reft(idx))
             }
@@ -427,7 +442,7 @@ impl FallibleTypeFolder for Normalizer<'_, '_, '_> {
         c.to_rustc(self.tcx())
             .normalize_internal(self.tcx(), self.rustc_param_env())
             .lower(self.tcx())
-            .map_err(|e| QueryErr::unsupported(self.def_id, e.into_err()))
+            .map_err(|e| QueryErr::unsupported(self.def_id(), e.into_err()))
     }
 }
 
@@ -595,7 +610,7 @@ impl TVarSubst {
     }
 
     fn consts(&mut self, a: &Const, b: &Const) {
-        if let super::ConstKind::Param(param_const) = a.kind {
+        if let ConstKind::Param(param_const) = a.kind {
             self.insert_generic_arg(param_const.index, GenericArg::Const(b.clone()));
         }
     }
diff --git a/crates/flux-middle/src/lib.rs b/crates/flux-middle/src/lib.rs
index 2cad2d34f8..2d9ba142a1 100644
--- a/crates/flux-middle/src/lib.rs
+++ b/crates/flux-middle/src/lib.rs
@@ -19,13 +19,11 @@ extern crate rustc_errors;
 extern crate rustc_hir;
 extern crate rustc_hir_pretty;
 extern crate rustc_index;
-extern crate rustc_infer;
 extern crate rustc_macros;
 extern crate rustc_middle;
 extern crate rustc_serialize;
 extern crate rustc_span;
 extern crate rustc_target;
-extern crate rustc_trait_selection;
 extern crate rustc_type_ir;
 
 extern crate self as flux_middle;
diff --git a/crates/flux-middle/src/rty/fold.rs b/crates/flux-middle/src/rty/fold.rs
index 8964aa4db0..ca4a6d66b0 100644
--- a/crates/flux-middle/src/rty/fold.rs
+++ b/crates/flux-middle/src/rty/fold.rs
@@ -7,20 +7,15 @@ use flux_arc_interner::{Internable, List};
 use flux_common::bug;
 use itertools::Itertools;
 use rustc_hash::FxHashSet;
-use rustc_hir::def_id::DefId;
 use rustc_type_ir::{DebruijnIndex, INNERMOST};
 
 use super::{
     normalize::{Normalizer, SpecFuncDefns},
-    projections, BaseTy, Binder, BoundVariableKinds, Const, EVid, Ensures, Expr, ExprKind,
-    GenericArg, Name, OutlivesPredicate, PolyFuncSort, PtrKind, ReBound, ReErased, Region, Sort,
-    SubsetTy, Ty, TyKind,
-};
-use crate::{
-    global_env::GlobalEnv,
-    queries::QueryResult,
-    rty::{expr::HoleKind, Var, VariantSig},
+    BaseTy, Binder, BoundVariableKinds, Const, EVid, Ensures, Expr, ExprKind, GenericArg, Name,
+    OutlivesPredicate, PolyFuncSort, PtrKind, ReBound, ReErased, Region, Sort, SubsetTy, Ty,
+    TyKind,
 };
+use crate::rty::{expr::HoleKind, Var, VariantSig};
 
 pub trait TypeVisitor: Sized {
     type BreakTy = !;
@@ -237,16 +232,6 @@ pub trait TypeFoldable: TypeVisitable {
         self.try_fold_with(folder).into_ok()
     }
 
-    fn normalize_projections<'tcx>(
-        &self,
-        genv: GlobalEnv<'_, 'tcx>,
-        infcx: &rustc_infer::infer::InferCtxt<'tcx>,
-        callsite_def_id: DefId,
-    ) -> QueryResult<Self> {
-        let mut normalizer = projections::Normalizer::new(genv, infcx, callsite_def_id)?;
-        self.erase_regions().try_fold_with(&mut normalizer)
-    }
-
     /// Normalize expressions by applying beta reductions for tuples and lambda abstractions.
     fn normalize(&self, defns: &SpecFuncDefns) -> Self {
         self.fold_with(&mut Normalizer::new(defns))
diff --git a/crates/flux-middle/src/rty/mod.rs b/crates/flux-middle/src/rty/mod.rs
index 265db6fb5f..f5b6a2d791 100644
--- a/crates/flux-middle/src/rty/mod.rs
+++ b/crates/flux-middle/src/rty/mod.rs
@@ -11,7 +11,6 @@ mod expr;
 pub mod fold;
 pub(crate) mod normalize;
 mod pretty;
-pub mod projections;
 pub mod refining;
 pub mod region_matching;
 pub mod subst;
diff --git a/crates/flux-middle/src/rty/subst.rs b/crates/flux-middle/src/rty/subst.rs
index 9c54fe7e2c..b950b85e6f 100644
--- a/crates/flux-middle/src/rty/subst.rs
+++ b/crates/flux-middle/src/rty/subst.rs
@@ -112,7 +112,7 @@ where
 /// Note that a substitution for refinement parameters (a list of expressions) must always be
 /// specified, while the behavior of other generics parameters (types, lifetimes and consts) can be
 /// configured with [`GenericsSubstDelegate`].
-pub(crate) struct GenericsSubstFolder<'a, D> {
+pub struct GenericsSubstFolder<'a, D> {
     current_index: DebruijnIndex,
     delegate: D,
     refinement_args: &'a [Expr],
@@ -243,7 +243,7 @@ where
 }
 
 impl<'a, D> GenericsSubstFolder<'a, D> {
-    pub(crate) fn new(delegate: D, refine: &'a [Expr]) -> Self {
+    pub fn new(delegate: D, refine: &'a [Expr]) -> Self {
         Self { current_index: INNERMOST, delegate, refinement_args: refine }
     }
 }
diff --git a/crates/flux-refineck/locales/en-US.ftl b/crates/flux-refineck/locales/en-US.ftl
index d0bf91ba76..dd6f5b1515 100644
--- a/crates/flux-refineck/locales/en-US.ftl
+++ b/crates/flux-refineck/locales/en-US.ftl
@@ -37,12 +37,12 @@ refineck_overflow_error =
     arithmetic operation may overflow
 
 refineck_opaque_struct_error =
-    cannot access fields of opaque struct `{$struct}`. 
+    cannot access fields of opaque struct `{$struct}`.
 
 refineck_opaque_struct_help =
     if you'd like to use fields of `{$struct}`, try annotating this method with `#[flux::trusted]`
 
-refineck_opaque_struct_note = 
+refineck_opaque_struct_note =
     fields of opaque structs can only be accessed inside trusted code (see: https://flux-rs.github.io/flux/guide/specs.html#opaque)
 
 refineck_unsupported_call =
@@ -56,3 +56,15 @@ refineck_expected_neg =
 
 refineck_invalid_invariant =
     invariant cannot be proven
+
+# Check impl against trait errors
+
+refineck_incompatible_sort =
+    implemented associated refinement `{$name}` has an incompatible sort for trait
+    .label = expected `{$expected}`, found `{$found}`
+
+refineck_invalid_assoc_reft =
+    associated refinement `{$name}` is not a member of trait `{$trait_}`
+
+refineck_missing_assoc_reft =
+    associated refinement `{$name}` is not defined in implementation of trait `{$trait_}`
diff --git a/crates/flux-refineck/src/checker.rs b/crates/flux-refineck/src/checker.rs
index 188a773e86..46e33373e0 100644
--- a/crates/flux-refineck/src/checker.rs
+++ b/crates/flux-refineck/src/checker.rs
@@ -6,6 +6,7 @@ use flux_infer::{
     infer::{
         ConstrReason, GlobalEnvExt as _, InferCtxt, InferCtxtRoot, InferResult, SubtypeReason,
     },
+    projections::NormalizeExt as _,
     refine_tree::{Marker, RefineCtxtTrace},
 };
 use flux_middle::{
@@ -161,12 +162,12 @@ impl<'ck, 'genv, 'tcx> Checker<'ck, 'genv, 'tcx, ShapeMode> {
             let inherited = Inherited::new(&mut mode, ghost_stmts)?;
 
             let body = genv.mir(local_id).with_span(span)?;
-            let infcx = root_ctxt.infcx(def_id, &body.infcx);
+            let mut infcx = root_ctxt.infcx(def_id, &body.infcx);
             let poly_sig = genv
                 .fn_sig(local_id)
                 .with_span(span)?
                 .instantiate_identity()
-                .normalize_projections(infcx.genv, infcx.region_infcx, infcx.def_id)
+                .normalize_projections(&mut infcx)
                 .with_span(span)?;
             Checker::run(infcx, local_id, inherited, poly_sig)?;
 
@@ -193,12 +194,12 @@ impl<'ck, 'genv, 'tcx> Checker<'ck, 'genv, 'tcx, RefineMode> {
             let mut mode = RefineMode { bb_envs };
             let inherited = Inherited::new(&mut mode, ghost_stmts)?;
             let body = genv.mir(local_id).with_span(span)?;
-            let infcx = root_ctxt.infcx(def_id, &body.infcx);
+            let mut infcx = root_ctxt.infcx(def_id, &body.infcx);
             let poly_sig = genv
                 .fn_sig(def_id)
                 .with_span(span)?
                 .instantiate_identity()
-                .normalize_projections(infcx.genv, infcx.region_infcx, infcx.def_id)
+                .normalize_projections(&mut infcx)
                 .with_span(span)?;
             Checker::run(infcx, local_id, inherited, poly_sig)?;
 
@@ -233,7 +234,7 @@ fn check_fn_subtyping(
 
     let super_sig = super_sig
         .replace_bound_vars(|_| rty::ReErased, |sort, _| infcx.define_vars(sort))
-        .normalize_projections(infcx.genv, infcx.region_infcx, *def_id)?;
+        .normalize_projections(&mut infcx)?;
 
     // 1. Unpack `T_g` input types
     let actuals = super_sig
@@ -252,7 +253,7 @@ fn check_fn_subtyping(
         let sub_sig = sub_sig.instantiate(tcx, sub_args, &refine_args);
         let sub_sig = sub_sig
             .replace_bound_vars(|_| rty::ReErased, |sort, mode| infcx.fresh_infer_var(sort, mode))
-            .normalize_projections(infcx.genv, infcx.region_infcx, *def_id)?;
+            .normalize_projections(infcx)?;
 
         // 3. INPUT subtyping (g-input <: f-input)
         for requires in super_sig.requires() {
@@ -306,33 +307,35 @@ pub(crate) fn trait_impl_subtyping<'genv, 'tcx>(
     let tcx = genv.tcx();
 
     // Skip the check if this is not an impl method
-    let Some((trait_ref, trait_method_id)) = find_trait_item(genv, def_id)? else {
+    let Some((impl_trait_ref, trait_method_id)) = find_trait_item(genv, def_id)? else {
         return Ok(None);
     };
+    let impl_method_id = def_id.to_def_id();
     // Skip the check if either the trait-method or the impl-method are marked as `trusted_impl`
-    if genv.has_trusted_impl(trait_method_id) || genv.has_trusted_impl(def_id.to_def_id()) {
+    if genv.has_trusted_impl(trait_method_id) || genv.has_trusted_impl(impl_method_id) {
         return Ok(None);
     }
+
+    let impl_id = tcx.impl_of_method(def_id.to_def_id()).unwrap();
+    let impl_args = GenericArg::identity_for_item(genv, def_id.to_def_id())?;
+    let trait_args = impl_args.rebase_onto(&tcx, impl_id, &impl_trait_ref.args);
+    let trait_refine_args = RefineArgs::identity_for_item(genv, trait_method_id)?;
+
     let mut root_ctxt = genv
         .infcx_root(trait_method_id, opts)
-        .with_generic_args(&trait_ref.args)
+        .with_generic_args(&impl_trait_ref.args)
         .build()?;
-
     let rustc_infcx = genv
         .tcx()
         .infer_ctxt()
         .build(TypingMode::non_body_analysis());
+    let mut infcx = root_ctxt.infcx(impl_method_id, &rustc_infcx);
 
-    let mut infcx = root_ctxt.infcx(trait_method_id, &rustc_infcx);
     let trait_fn_sig = genv.fn_sig(trait_method_id)?;
-    let impl_id = tcx.impl_of_method(def_id.to_def_id()).unwrap();
-    let impl_args = GenericArg::identity_for_item(genv, def_id.to_def_id())?;
-    let trait_args = impl_args.rebase_onto(&tcx, impl_id, &trait_ref.args);
-    let trait_refine_args = RefineArgs::identity_for_item(genv, trait_method_id)?;
-    let impl_sig = genv.fn_sig(def_id)?;
+    let impl_sig = genv.fn_sig(impl_method_id)?;
     check_fn_subtyping(
         &mut infcx,
-        &def_id.to_def_id(),
+        &impl_method_id,
         impl_sig,
         &impl_args,
         &trait_fn_sig.instantiate(tcx, &trait_args, &trait_refine_args),
@@ -420,7 +423,7 @@ impl<'ck, 'genv, 'tcx, M: Mode> Checker<'ck, 'genv, 'tcx, M> {
 
         let fn_sig = poly_sig
             .replace_bound_vars(|_| rty::ReErased, |sort, _| infcx.define_vars(sort))
-            .normalize_projections(infcx.genv, infcx.region_infcx, infcx.def_id)
+            .normalize_projections(&mut infcx)
             .with_span(span)?;
 
         let mut env = TypeEnv::new(&mut infcx, &body, &fn_sig);
@@ -780,7 +783,7 @@ impl<'ck, 'genv, 'tcx, M: Mode> Checker<'ck, 'genv, 'tcx, M> {
         let fn_sig = fn_sig
             .instantiate(tcx, &generic_args, &refine_args)
             .replace_bound_vars(|_| rty::ReErased, |sort, mode| infcx.fresh_infer_var(sort, mode))
-            .normalize_projections(genv, infcx.region_infcx, infcx.def_id)
+            .normalize_projections(infcx)
             .with_span(span)?;
 
         let mut at = infcx.at(span);
diff --git a/crates/flux-fhir-analysis/src/compare_impl_item.rs b/crates/flux-refineck/src/compare_impl_item.rs
similarity index 58%
rename from crates/flux-fhir-analysis/src/compare_impl_item.rs
rename to crates/flux-refineck/src/compare_impl_item.rs
index 7fec0372d6..1923704973 100644
--- a/crates/flux-fhir-analysis/src/compare_impl_item.rs
+++ b/crates/flux-refineck/src/compare_impl_item.rs
@@ -1,113 +1,111 @@
-use flux_common::result::ResultExt;
+use flux_common::result::ErrorEmitter;
+use flux_infer::{
+    infer::{GlobalEnvExt as _, InferCtxt},
+    projections::NormalizeExt as _,
+};
 use flux_middle::{
-    def_id_to_string, global_env::GlobalEnv, rty::fold::TypeFoldable, MaybeExternId,
+    def_id_to_string, global_env::GlobalEnv, queries::QueryResult, rty::TraitRef, MaybeExternId,
 };
 use rustc_hash::FxHashSet;
 use rustc_infer::infer::TyCtxtInferExt;
 use rustc_middle::ty::TypingMode;
-use rustc_span::{def_id::DefId, ErrorGuaranteed, Symbol};
-type Result<T = ()> = std::result::Result<T, ErrorGuaranteed>;
+use rustc_span::{def_id::DefId, Symbol};
 
-pub fn check_impl_against_trait(genv: GlobalEnv, impl_id: MaybeExternId) -> Result {
+pub fn check_impl_against_trait(genv: GlobalEnv, impl_id: MaybeExternId) -> QueryResult {
     let trait_id = genv.tcx().trait_id_of_impl(impl_id.resolved_id()).unwrap();
 
-    let impl_assoc_refts = genv.assoc_refinements_of(impl_id).emit(&genv)?;
-    let trait_assoc_refts = genv.assoc_refinements_of(trait_id).emit(&genv)?;
+    let impl_assoc_refts = genv.assoc_refinements_of(impl_id)?;
+    let trait_assoc_refts = genv.assoc_refinements_of(trait_id)?;
     let impl_names: FxHashSet<_> = impl_assoc_refts.items.iter().map(|x| x.name).collect();
 
     for trait_assoc_reft in &trait_assoc_refts.items {
         let name = trait_assoc_reft.name;
-        let has_default = genv
-            .default_assoc_refinement_def(trait_id, name)
-            .emit(&genv)?
-            .is_some();
+        let has_default = genv.default_assoc_refinement_def(trait_id, name)?.is_some();
         if !impl_names.contains(&name) && !has_default {
             let span = genv.tcx().def_span(impl_id);
-            return Err(genv.sess().emit_err(errors::MissingAssocReft::new(
-                span,
-                name,
-                def_id_to_string(trait_id),
-            )));
+            Err(genv.emit(errors::MissingAssocReft::new(span, name, def_id_to_string(trait_id))))?;
         }
     }
 
+    let impl_trait_ref = genv
+        .impl_trait_ref(impl_id.resolved_id())?
+        .unwrap()
+        .instantiate_identity();
+
+    let mut root_ctxt = genv
+        .infcx_root(trait_id, genv.infer_opts(impl_id.local_id()))
+        .with_generic_args(&impl_trait_ref.args)
+        .build()?;
+    let rustc_infcx = genv
+        .tcx()
+        .infer_ctxt()
+        .build(TypingMode::non_body_analysis());
+    let mut infcx = root_ctxt.infcx(trait_id, &rustc_infcx);
+
     for impl_assoc_reft in &impl_assoc_refts.items {
         let name = impl_assoc_reft.name;
         if trait_assoc_refts.find(name).is_none() {
             let fhir_impl_assoc_reft = genv
                 .map()
-                .expect_item(impl_id.local_id())
-                .emit(&genv)?
+                .expect_item(impl_id.local_id())?
                 .expect_impl()
                 .find_assoc_reft(name)
                 .unwrap();
-            return Err(genv.sess().emit_err(errors::InvalidAssocReft::new(
+            Err(genv.emit(errors::InvalidAssocReft::new(
                 fhir_impl_assoc_reft.span,
                 name,
                 def_id_to_string(trait_id),
-            )));
+            )))?;
         }
-        check_assoc_reft(genv, impl_id, trait_id, impl_assoc_reft.name)?;
+        check_assoc_reft(&mut infcx, impl_id, &impl_trait_ref, trait_id, impl_assoc_reft.name)?;
     }
 
     Ok(())
 }
 
 fn check_assoc_reft(
-    genv: GlobalEnv,
+    infcx: &mut InferCtxt,
     impl_id: MaybeExternId,
+    impl_trait_ref: &TraitRef,
     trait_id: DefId,
     name: Symbol,
-) -> Result {
-    let infcx = genv
-        .tcx()
-        .infer_ctxt()
-        .build(TypingMode::non_body_analysis());
-
-    let impl_span = genv
+) -> QueryResult {
+    let impl_span = infcx
+        .genv
         .map()
-        .expect_item(impl_id.local_id())
-        .emit(&genv)?
+        .expect_item(impl_id.local_id())?
         .expect_impl()
         .find_assoc_reft(name)
         .unwrap()
         .span;
 
-    let impl_trait_ref = genv
-        .impl_trait_ref(impl_id.resolved_id())
-        .emit(&genv)?
-        .unwrap()
-        .instantiate_identity();
-
-    let Some(impl_sort) = genv.sort_of_assoc_reft(impl_id, name).emit(genv.sess())? else {
-        return Err(genv.sess().emit_err(errors::InvalidAssocReft::new(
+    let Some(impl_sort) = infcx.genv.sort_of_assoc_reft(impl_id, name)? else {
+        return Err(infcx.genv.emit(errors::InvalidAssocReft::new(
             impl_span,
             name,
             def_id_to_string(trait_id),
-        )));
+        )))?;
     };
 
     let impl_sort = impl_sort
         .instantiate_identity()
-        .normalize_projections(genv, &infcx, impl_id.resolved_id())
-        .emit(&genv)?;
+        .normalize_projections(infcx)?;
 
-    let Some(trait_sort) = genv.sort_of_assoc_reft(trait_id, name).emit(genv.sess())? else {
-        return Err(genv.sess().emit_err(errors::InvalidAssocReft::new(
+    let Some(trait_sort) = infcx.genv.sort_of_assoc_reft(trait_id, name)? else {
+        return Err(infcx.genv.emit(errors::InvalidAssocReft::new(
             impl_span,
             name,
             def_id_to_string(trait_id),
-        )));
+        )))?;
     };
     let trait_sort = trait_sort
-        .instantiate(genv.tcx(), &impl_trait_ref.args, &[])
-        .normalize_projections(genv, &infcx, impl_id.resolved_id())
-        .emit(&genv)?;
+        .instantiate(infcx.tcx(), &impl_trait_ref.args, &[])
+        .normalize_projections(infcx)?;
 
     if impl_sort != trait_sort {
-        return Err(genv
-            .sess()
-            .emit_err(errors::IncompatibleSort::new(impl_span, name, trait_sort, impl_sort)));
+        return Err(infcx
+            .genv
+            .emit(errors::IncompatibleSort::new(impl_span, name, trait_sort, impl_sort)))?;
     }
 
     Ok(())
@@ -120,7 +118,7 @@ pub(crate) mod errors {
     use rustc_span::{Span, Symbol};
 
     #[derive(Diagnostic)]
-    #[diag(fhir_analysis_incompatible_sort, code = E0999)]
+    #[diag(refineck_incompatible_sort, code = E0999)]
     pub(super) struct IncompatibleSort {
         #[primary_span]
         #[label]
@@ -142,30 +140,30 @@ pub(crate) mod errors {
     }
 
     #[derive(Diagnostic)]
-    #[diag(fhir_analysis_invalid_assoc_reft, code = E0999)]
-    pub struct InvalidAssocReft {
+    #[diag(refineck_missing_assoc_reft, code = E0999)]
+    pub struct MissingAssocReft {
         #[primary_span]
         span: Span,
         trait_: String,
         name: Symbol,
     }
 
-    impl InvalidAssocReft {
+    impl MissingAssocReft {
         pub(crate) fn new(span: Span, name: Symbol, trait_: String) -> Self {
             Self { span, trait_, name }
         }
     }
 
     #[derive(Diagnostic)]
-    #[diag(fhir_analysis_missing_assoc_reft, code = E0999)]
-    pub struct MissingAssocReft {
+    #[diag(refineck_invalid_assoc_reft, code = E0999)]
+    pub struct InvalidAssocReft {
         #[primary_span]
         span: Span,
         trait_: String,
         name: Symbol,
     }
 
-    impl MissingAssocReft {
+    impl InvalidAssocReft {
         pub(crate) fn new(span: Span, name: Symbol, trait_: String) -> Self {
             Self { span, trait_, name }
         }
diff --git a/crates/flux-refineck/src/lib.rs b/crates/flux-refineck/src/lib.rs
index eef60e5856..9a8acabfac 100644
--- a/crates/flux-refineck/src/lib.rs
+++ b/crates/flux-refineck/src/lib.rs
@@ -25,6 +25,7 @@ extern crate rustc_target;
 extern crate rustc_type_ir;
 
 mod checker;
+pub mod compare_impl_item;
 mod ghost_statements;
 pub mod invariants;
 mod primops;
diff --git a/crates/flux-refineck/src/type_env/place_ty.rs b/crates/flux-refineck/src/type_env/place_ty.rs
index ed5ec417ca..1d9133957d 100644
--- a/crates/flux-refineck/src/type_env/place_ty.rs
+++ b/crates/flux-refineck/src/type_env/place_ty.rs
@@ -1,7 +1,10 @@
 use std::{clone::Clone, fmt, ops::ControlFlow};
 
 use flux_common::{iter::IterExt, tracked_span_bug};
-use flux_infer::infer::{ConstrReason, InferCtxt, InferCtxtAt, InferErr, InferResult};
+use flux_infer::{
+    infer::{ConstrReason, InferCtxt, InferCtxtAt, InferErr, InferResult},
+    projections::NormalizeExt as _,
+};
 use flux_middle::{
     global_env::GlobalEnv,
     queries::QueryResult,
@@ -778,7 +781,7 @@ fn downcast(
 ///     * `x.fld : T[A := t ..][i := e...]`
 /// i.e. by substituting the type and value indices using the types and values from `x`.
 fn downcast_struct(
-    infcx: &InferCtxt,
+    infcx: &mut InferCtxt,
     adt: &AdtDef,
     args: &[GenericArg],
     idx: &Expr,
@@ -792,7 +795,7 @@ fn downcast_struct(
     Ok(struct_variant(infcx.genv, adt.did())?
         .instantiate(tcx, args, &[])
         .replace_bound_refts(&flds)
-        .normalize_projections(infcx.genv, infcx.region_infcx, infcx.def_id)?
+        .normalize_projections(infcx)?
         .fields
         .to_vec())
 }
@@ -826,7 +829,7 @@ fn downcast_enum(
         .expect("enums cannot be opaque")
         .instantiate(tcx, args, &[])
         .replace_bound_refts_with(|sort, _, _| infcx.define_vars(sort))
-        .normalize_projections(infcx.genv, infcx.region_infcx, infcx.def_id)?;
+        .normalize_projections(infcx)?;
 
     // FIXME(nilehmann) We could assert idx1 == variant_def.idx directly, but for aggregate sorts there
     // are currently two problems.