diff --git a/compiler/rustc_metadata/src/rmeta/decoder.rs b/compiler/rustc_metadata/src/rmeta/decoder.rs
index 5705831bcfaee..22c9d036e5384 100644
--- a/compiler/rustc_metadata/src/rmeta/decoder.rs
+++ b/compiler/rustc_metadata/src/rmeta/decoder.rs
@@ -438,6 +438,10 @@ impl<'a, 'tcx> rustc_middle::ty::InternerDecoder for MetadataDecodeContext<'a, '
     fn interner(&self) -> TyCtxt<'tcx> {
         self.tcx
     }
+
+    fn decode_predicate(&mut self) -> rustc_middle::ty::predicates::Predicate<Self::Interner> {
+        rustc_middle::ty::codec::decode_predicate(self)
+    }
 }
 
 impl<'a, 'tcx> Decodable<MetadataDecodeContext<'a, 'tcx>> for ExpnIndex {
diff --git a/compiler/rustc_metadata/src/rmeta/encoder.rs b/compiler/rustc_metadata/src/rmeta/encoder.rs
index f9f4c52b79d3b..c9e585b984df2 100644
--- a/compiler/rustc_metadata/src/rmeta/encoder.rs
+++ b/compiler/rustc_metadata/src/rmeta/encoder.rs
@@ -405,6 +405,15 @@ impl<'a, 'tcx> Encodable<EncodeContext<'a, 'tcx>> for [u8] {
     }
 }
 
+impl<'a, 'tcx> rustc_middle::ty::PredicateEncoder<TyCtxt<'tcx>> for EncodeContext<'a, 'tcx> {
+    fn encode_predicate(
+        &mut self,
+        predicate: rustc_middle::ty::predicates::Predicate<TyCtxt<'tcx>>,
+    ) {
+        rustc_middle::ty::codec::encode_predicate(self, predicate);
+    }
+}
+
 impl<'a, 'tcx> TyEncoder<'tcx> for EncodeContext<'a, 'tcx> {
     const CLEAR_CROSS_CRATE: bool = true;
 
diff --git a/compiler/rustc_middle/src/query/on_disk_cache.rs b/compiler/rustc_middle/src/query/on_disk_cache.rs
index 7383ad23273be..ad3eb34ef3311 100644
--- a/compiler/rustc_middle/src/query/on_disk_cache.rs
+++ b/compiler/rustc_middle/src/query/on_disk_cache.rs
@@ -531,6 +531,10 @@ impl<'a, 'tcx> rustc_type_ir::InternerDecoder for CacheDecoder<'a, 'tcx> {
     fn interner(&self) -> Self::Interner {
         self.tcx
     }
+
+    fn decode_predicate(&mut self) -> rustc_type_ir::predicates::Predicate<Self::Interner> {
+        ty::codec::decode_predicate(self)
+    }
 }
 
 impl<'a, 'tcx> Decoder for CacheDecoder<'a, 'tcx> {
@@ -916,6 +920,12 @@ impl<'tcx> SpanEncoder for CacheEncoder<'tcx> {
     }
 }
 
+impl<'tcx> rustc_type_ir::PredicateEncoder<TyCtxt<'tcx>> for CacheEncoder<'tcx> {
+    fn encode_predicate(&mut self, predicate: rustc_type_ir::predicates::Predicate<TyCtxt<'tcx>>) {
+        ty::codec::encode_predicate(self, predicate);
+    }
+}
+
 impl<'tcx> TyEncoder<'tcx> for CacheEncoder<'tcx> {
     const CLEAR_CROSS_CRATE: bool = false;
 
diff --git a/compiler/rustc_middle/src/ty/codec.rs b/compiler/rustc_middle/src/ty/codec.rs
index 81462e214b20f..2ad6b77ee37f2 100644
--- a/compiler/rustc_middle/src/ty/codec.rs
+++ b/compiler/rustc_middle/src/ty/codec.rs
@@ -27,7 +27,7 @@ mod ref_decodable;
 /// This offset is also chosen so that the first byte is never < 0x80.
 pub const SHORTHAND_OFFSET: usize = 0x80;
 
-pub trait TyEncoder<'tcx>: SpanEncoder {
+pub trait TyEncoder<'tcx>: SpanEncoder + rustc_type_ir::PredicateEncoder<TyCtxt<'tcx>> {
     const CLEAR_CROSS_CRATE: bool;
 
     fn position(&self) -> usize;
@@ -128,18 +128,11 @@ impl<'tcx, E: TyEncoder<'tcx>> Encodable<E> for Ty<'tcx> {
     }
 }
 
-impl<'tcx, E: TyEncoder<'tcx>> Encodable<E> for ty::Predicate<'tcx> {
-    fn encode(&self, e: &mut E) {
-        let kind = self.kind();
-        kind.bound_vars().encode(e);
-        encode_with_shorthand(e, &kind.skip_binder(), TyEncoder::predicate_shorthands);
-    }
-}
-
-impl<'tcx, E: TyEncoder<'tcx>> Encodable<E> for ty::Clause<'tcx> {
-    fn encode(&self, e: &mut E) {
-        self.as_predicate().encode(e);
-    }
+/// Encode a predicate using rustc's existing shorthand representation.
+pub fn encode_predicate<'tcx, E: TyEncoder<'tcx>>(e: &mut E, predicate: ty::Predicate<'tcx>) {
+    let kind = predicate.kind();
+    kind.bound_vars().encode(e);
+    encode_with_shorthand(e, &kind.skip_binder(), TyEncoder::predicate_shorthands);
 }
 
 impl<'tcx, E: TyEncoder<'tcx>> Encodable<E> for ty::Pattern<'tcx> {
@@ -203,31 +196,23 @@ impl<'tcx, D: TyDecoder<'tcx>> Decodable<D> for Ty<'tcx> {
     }
 }
 
-impl<'tcx, D: TyDecoder<'tcx>> Decodable<D> for ty::Predicate<'tcx> {
-    fn decode(decoder: &mut D) -> ty::Predicate<'tcx> {
-        let bound_vars = Decodable::decode(decoder);
-        // Handle shorthands first, if we have a usize > 0x80.
-        let predicate_kind = ty::Binder::bind_with_vars(
-            if decoder.positioned_at_shorthand() {
-                let pos = decoder.read_usize();
-                assert!(pos >= SHORTHAND_OFFSET);
-                let shorthand = pos - SHORTHAND_OFFSET;
-
-                decoder.with_position(shorthand, <ty::PredicateKind<'tcx> as Decodable<D>>::decode)
-            } else {
-                <ty::PredicateKind<'tcx> as Decodable<D>>::decode(decoder)
-            },
-            bound_vars,
-        );
-        decoder.interner().mk_predicate(predicate_kind)
-    }
-}
+/// Decode a predicate, resolving shorthand references before interning it.
+pub fn decode_predicate<'tcx, D: TyDecoder<'tcx>>(decoder: &mut D) -> ty::Predicate<'tcx> {
+    let bound_vars = Decodable::decode(decoder);
+    // Handle shorthands first, if we have a usize > 0x80.
+    let predicate_kind = ty::Binder::bind_with_vars(
+        if decoder.positioned_at_shorthand() {
+            let pos = decoder.read_usize();
+            assert!(pos >= SHORTHAND_OFFSET);
+            let shorthand = pos - SHORTHAND_OFFSET;
 
-impl<'tcx, D: TyDecoder<'tcx>> Decodable<D> for ty::Clause<'tcx> {
-    fn decode(decoder: &mut D) -> ty::Clause<'tcx> {
-        let pred: ty::Predicate<'tcx> = Decodable::decode(decoder);
-        pred.expect_clause()
-    }
+            decoder.with_position(shorthand, <ty::PredicateKind<'tcx> as Decodable<D>>::decode)
+        } else {
+            <ty::PredicateKind<'tcx> as Decodable<D>>::decode(decoder)
+        },
+        bound_vars,
+    );
+    decoder.interner().mk_predicate(predicate_kind)
 }
 
 impl<'tcx, D: TyDecoder<'tcx>> Decodable<D> for GenericArgsRef<'tcx> {
diff --git a/compiler/rustc_middle/src/ty/context.rs b/compiler/rustc_middle/src/ty/context.rs
index 913f56eba36f5..fbc9e82335f08 100644
--- a/compiler/rustc_middle/src/ty/context.rs
+++ b/compiler/rustc_middle/src/ty/context.rs
@@ -250,7 +250,7 @@ impl<'tcx> CtxtInterners<'tcx> {
     /// Interns a predicate. (Use `mk_predicate` instead, where possible.)
     #[inline(never)]
     fn intern_predicate(&self, kind: Binder<'tcx, PredicateKind<'tcx>>) -> Predicate<'tcx> {
-        Predicate(Interned::new_unchecked(
+        rustc_type_ir::predicates::Predicate(Interned::new_unchecked(
             self.predicate
                 .intern(kind, |kind| {
                     let flags = ty::FlagComputation::<TyCtxt<'tcx>>::for_predicate(kind);
@@ -1747,8 +1747,6 @@ macro_rules! nop_list_lift {
 nop_lift! { type_; Ty<'a> => Ty<'tcx> }
 nop_lift! { pat; Pattern<'a> => Pattern<'tcx> }
 nop_lift! { const_allocation; ConstAllocation<'a> => ConstAllocation<'tcx> }
-nop_lift! { predicate; Predicate<'a> => Predicate<'tcx> }
-nop_lift! { predicate; Clause<'a> => Clause<'tcx> }
 nop_lift! { layout; Layout<'a> => Layout<'tcx> }
 nop_lift! { valtree; ValTree<'a> => ValTree<'tcx> }
 
@@ -1777,6 +1775,22 @@ impl<'a, 'tcx> Lift<TyCtxt<'tcx>> for Interned<'a, WithCachedTypeInfo<ConstKind<
     }
 }
 
+// Lift the interned representation used by the shared Predicate and Clause.
+impl<'a, 'tcx> Lift<TyCtxt<'tcx>>
+    for Interned<'a, WithCachedTypeInfo<ty::Binder<'a, ty::PredicateKind<'a>>>>
+{
+    type Lifted = Interned<'tcx, WithCachedTypeInfo<ty::Binder<'tcx, ty::PredicateKind<'tcx>>>>;
+
+    #[track_caller]
+    fn lift_to_interner(self, tcx: TyCtxt<'tcx>) -> Self::Lifted {
+        assert!(tcx.interners.predicate.contains_pointer_to(&InternedInSet(&*self.0)));
+
+        // SAFETY: The predicate is interned in this TyCtxt, so its storage
+        // remains valid for the lifetime of the target context.
+        unsafe { mem::transmute(self) }
+    }
+}
+
 nop_list_lift! { type_lists; Ty<'a> => Ty<'tcx> }
 nop_list_lift! { clauses: ListWithCachedTypeInfo; Clause<'a> => Clause<'tcx> }
 nop_list_lift! {
diff --git a/compiler/rustc_middle/src/ty/context/impl_interner.rs b/compiler/rustc_middle/src/ty/context/impl_interner.rs
index e849f3076a9f3..a5126a8ed977c 100644
--- a/compiler/rustc_middle/src/ty/context/impl_interner.rs
+++ b/compiler/rustc_middle/src/ty/context/impl_interner.rs
@@ -10,6 +10,7 @@ use rustc_hir::def::{CtorKind, DefKind};
 use rustc_hir::def_id::{DefId, LocalDefId};
 use rustc_span::{DUMMY_SP, Span, Symbol, bug};
 use rustc_type_ir::lang_items::{SolverAdtLangItem, SolverProjectionLangItem, SolverTraitLangItem};
+use rustc_type_ir::predicates::Predicate;
 use rustc_type_ir::solve::CanonicalInputData;
 use rustc_type_ir::{
     BoundVar, CollectAndApply, DebruijnIndex, Interner, RegionVid, TypeFoldable, Unnormalized,
@@ -24,8 +25,8 @@ use crate::traits::solve::{
     self, CanonicalInput, ExternalConstraints, ExternalConstraintsData, QueryResult, inspect,
 };
 use crate::ty::{
-    self, BoundRegion, Clause, Const, List, ParamTy, Pattern, PolyExistentialPredicate, Predicate,
-    Region, RegionKind, RequiredDepth, Ty, TyCtxt,
+    self, BoundRegion, Clause, Const, List, ParamTy, Pattern, PolyExistentialPredicate, Region,
+    RegionKind, RequiredDepth, Ty, TyCtxt,
 };
 
 #[allow(rustc::usage_of_ty_tykind)]
@@ -121,17 +122,25 @@ impl<'tcx> Interner for TyCtxt<'tcx> {
     type Scalar = Scalar;
     type InternedRegionKind = Interned<'tcx, ty::RegionKind<'tcx>>;
     type InternedConstKind = Interned<'tcx, WithCachedTypeInfo<ty::ConstKind<'tcx>>>;
+    type InternedPredicateKind =
+        Interned<'tcx, WithCachedTypeInfo<ty::Binder<'tcx, ty::PredicateKind<'tcx>>>>;
     type EarlyParamRegion = ty::EarlyParamRegion;
     type LateParamRegionKind = ty::LateParamRegionKind;
 
     type RegionAssumptions = &'tcx ty::List<ty::ArgOutlivesClause<'tcx>>;
 
     type ParamEnv = ty::ParamEnv<'tcx>;
-    type Predicate = Predicate<'tcx>;
 
     type Clause = Clause<'tcx>;
     type Clauses = ty::Clauses<'tcx>;
 
+    fn intern_predicate(
+        self,
+        predicate: ty::Binder<'tcx, ty::PredicateKind<'tcx>>,
+    ) -> Predicate<Self> {
+        self.interners.intern_predicate(predicate)
+    }
+
     type Tracked<T: fmt::Debug + Clone> = WithDepNode<T>;
     fn mk_tracked<T: fmt::Debug + Clone>(
         self,
diff --git a/compiler/rustc_middle/src/ty/elaborate_impl.rs b/compiler/rustc_middle/src/ty/elaborate_impl.rs
index cd76d49cefecb..23d281178d17a 100644
--- a/compiler/rustc_middle/src/ty/elaborate_impl.rs
+++ b/compiler/rustc_middle/src/ty/elaborate_impl.rs
@@ -23,26 +23,6 @@ impl<'tcx> Elaboratable<TyCtxt<'tcx>> for ty::Clause<'tcx> {
     }
 }
 
-impl<'tcx> Elaboratable<TyCtxt<'tcx>> for ty::Predicate<'tcx> {
-    fn predicate(&self) -> ty::Predicate<'tcx> {
-        *self
-    }
-
-    fn child(&self, clause: ty::Clause<'tcx>) -> Self {
-        clause.as_predicate()
-    }
-
-    fn child_with_derived_cause(
-        &self,
-        clause: ty::Clause<'tcx>,
-        _span: Span,
-        _parent_trait_pred: ty::PolyTraitClause<'tcx>,
-        _index: usize,
-    ) -> Self {
-        clause.as_predicate()
-    }
-}
-
 impl<'tcx> Elaboratable<TyCtxt<'tcx>> for (ty::Predicate<'tcx>, Span) {
     fn predicate(&self) -> ty::Predicate<'tcx> {
         self.0
diff --git a/compiler/rustc_middle/src/ty/predicate.rs b/compiler/rustc_middle/src/ty/predicate.rs
index 7870b20c7d304..ae00e19776570 100644
--- a/compiler/rustc_middle/src/ty/predicate.rs
+++ b/compiler/rustc_middle/src/ty/predicate.rs
@@ -1,12 +1,10 @@
 use std::cmp::Ordering;
 
-use rustc_data_structures::intern::Interned;
 use rustc_hir::def_id::DefId;
-use rustc_macros::{StableHash, extension};
-use rustc_span::bug;
+use rustc_macros::extension;
 use rustc_type_ir as ir;
 
-use crate::ty::{self, EarlyBinder, Ty, TyCtxt, TypeFlags, Upcast, UpcastFrom, WithCachedTypeInfo};
+use crate::ty::{self, Ty, TyCtxt, Upcast, UpcastFrom};
 
 pub type TraitRef<'tcx> = ir::TraitRef<TyCtxt<'tcx>>;
 pub type AliasTerm<'tcx> = ir::AliasTerm<TyCtxt<'tcx>>;
@@ -35,107 +33,11 @@ pub type PolySubtypePredicate<'tcx> = ty::Binder<'tcx, SubtypePredicate<'tcx>>;
 pub type PolyCoercePredicate<'tcx> = ty::Binder<'tcx, CoercePredicate<'tcx>>;
 pub type PolyProjectionClause<'tcx> = ty::Binder<'tcx, ProjectionClause<'tcx>>;
 
-/// A statement that can be proven by a trait solver. This includes things that may
-/// show up in where clauses, such as trait predicates and projection predicates,
-/// and also things that are emitted as part of type checking such as `DynCompatible`
-/// predicate which is emitted when a type is coerced to a trait object.
-///
-/// Use this rather than `PredicateKind`, whenever possible.
-#[derive(Clone, Copy, PartialEq, Eq, Hash, StableHash)]
-#[rustc_pass_by_value]
-pub struct Predicate<'tcx>(
-    pub(super) Interned<'tcx, WithCachedTypeInfo<ty::Binder<'tcx, PredicateKind<'tcx>>>>,
-);
+/// An interned statement the trait solver can prove.
+pub type Predicate<'tcx> = ir::predicates::Predicate<TyCtxt<'tcx>>;
 
-impl<'tcx> rustc_type_ir::inherent::Predicate<TyCtxt<'tcx>> for Predicate<'tcx> {
-    fn as_clause(self) -> Option<ty::Clause<'tcx>> {
-        self.as_clause()
-    }
-}
-
-impl<'tcx> rustc_type_ir::inherent::IntoKind for Predicate<'tcx> {
-    type Kind = ty::Binder<'tcx, ty::PredicateKind<'tcx>>;
-
-    fn kind(self) -> Self::Kind {
-        self.kind()
-    }
-}
-
-impl<'tcx> rustc_type_ir::Flags for Predicate<'tcx> {
-    fn flags(&self) -> TypeFlags {
-        self.0.flags
-    }
-
-    fn outer_exclusive_binder(&self) -> ty::DebruijnIndex {
-        self.0.outer_exclusive_binder
-    }
-}
-
-impl<'tcx> Predicate<'tcx> {
-    /// Gets the inner `ty::Binder<'tcx, PredicateKind<'tcx>>`.
-    #[inline]
-    pub fn kind(self) -> ty::Binder<'tcx, PredicateKind<'tcx>> {
-        self.0.internee
-    }
-
-    /// Flips the polarity of a Predicate.
-    ///
-    /// Given `T: Trait` predicate it returns `T: !Trait` and given `T: !Trait` returns `T: Trait`.
-    pub fn flip_polarity(self, tcx: TyCtxt<'tcx>) -> Option<Predicate<'tcx>> {
-        let kind = self
-            .kind()
-            .map_bound(|kind| match kind {
-                PredicateKind::Clause(ClauseKind::Trait(TraitClause { trait_ref, polarity })) => {
-                    Some(PredicateKind::Clause(ClauseKind::Trait(TraitClause {
-                        trait_ref,
-                        polarity: polarity.flip(),
-                    })))
-                }
-
-                _ => None,
-            })
-            .transpose()?;
-
-        Some(tcx.mk_predicate(kind))
-    }
-
-    /// Whether this projection can be soundly normalized.
-    ///
-    /// Wf predicates must not be normalized, as normalization
-    /// can remove required bounds which would cause us to
-    /// unsoundly accept some programs. See #91068.
-    #[inline]
-    pub fn allow_normalization(self) -> bool {
-        rustc_type_ir::inherent::Predicate::allow_normalization(self)
-    }
-}
-
-impl<'tcx> rustc_errors::IntoDiagArg for Predicate<'tcx> {
-    fn into_diag_arg(self, path: &mut Option<std::path::PathBuf>) -> rustc_errors::DiagArgValue {
-        ty::tls::with(|tcx| {
-            let pred = tcx.short_string(tcx.lift(self), path);
-            rustc_errors::DiagArgValue::Str(std::borrow::Cow::Owned(pred))
-        })
-    }
-}
-
-impl<'tcx> rustc_errors::IntoDiagArg for Clause<'tcx> {
-    fn into_diag_arg(self, path: &mut Option<std::path::PathBuf>) -> rustc_errors::DiagArgValue {
-        ty::tls::with(|tcx| {
-            let clause = tcx.short_string(tcx.lift(self), path);
-            rustc_errors::DiagArgValue::Str(std::borrow::Cow::Owned(clause))
-        })
-    }
-}
-
-/// A subset of predicates which can be assumed by the trait solver. They show up in
-/// an item's where clauses, hence the name `Clause`, and may either be user-written
-/// (such as traits) or may be inserted during lowering.
-#[derive(Clone, Copy, PartialEq, Eq, Hash, StableHash)]
-#[rustc_pass_by_value]
-pub struct Clause<'tcx>(
-    pub(super) Interned<'tcx, WithCachedTypeInfo<ty::Binder<'tcx, PredicateKind<'tcx>>>>,
-);
+/// An interned predicate that can be assumed by the solver.
+pub type Clause<'tcx> = ir::predicates::Clause<TyCtxt<'tcx>>;
 
 impl<'tcx> rustc_type_ir::inherent::Clause<TyCtxt<'tcx>> for Clause<'tcx> {
     fn as_predicate(self) -> Predicate<'tcx> {
@@ -147,78 +49,21 @@ impl<'tcx> rustc_type_ir::inherent::Clause<TyCtxt<'tcx>> for Clause<'tcx> {
     }
 }
 
-impl<'tcx> rustc_type_ir::inherent::IntoKind for Clause<'tcx> {
-    type Kind = ty::Binder<'tcx, ClauseKind<'tcx>>;
-
-    fn kind(self) -> Self::Kind {
-        self.kind()
-    }
-}
-
-impl<'tcx> rustc_type_ir::Flags for Clause<'tcx> {
-    fn flags(&self) -> TypeFlags {
-        self.0.flags
+// Preserve rustc's existing diagnostic formatting while the concrete
+// predicate wrappers are being migrated into rustc_type_ir.
+impl<'tcx> ir::ir_print::PredicateDiagFormatter for TyCtxt<'tcx> {
+    fn predicate_diag_string(
+        predicate: ir::predicates::Predicate<Self>,
+        path: &mut Option<std::path::PathBuf>,
+    ) -> String {
+        ty::tls::with(|tcx| tcx.short_string(tcx.lift(predicate), path))
     }
 
-    fn outer_exclusive_binder(&self) -> ty::DebruijnIndex {
-        self.0.outer_exclusive_binder
-    }
-}
-
-impl<'tcx> Clause<'tcx> {
-    pub fn as_predicate(self) -> Predicate<'tcx> {
-        Predicate(self.0)
-    }
-
-    pub fn kind(self) -> ty::Binder<'tcx, ClauseKind<'tcx>> {
-        // Outline the unreachable! call to make the happy path faster.
-        // see: https://github.com/rust-lang/rust/pull/163657#issuecomment-5956974964
-        #[cold]
-        #[inline(never)]
-        fn unreachable_inner() -> ! {
-            unreachable!()
-        }
-
-        self.0.internee.map_bound_no_validate_bound_vars(|kind| match kind {
-            PredicateKind::Clause(clause) => clause,
-            _ => unreachable_inner(),
-        })
-    }
-
-    pub fn as_trait_clause(self) -> Option<ty::Binder<'tcx, TraitClause<'tcx>>> {
-        let clause = self.kind();
-        if let ty::ClauseKind::Trait(trait_clause) = clause.skip_binder() {
-            Some(clause.rebind(trait_clause))
-        } else {
-            None
-        }
-    }
-
-    pub fn as_projection_clause(self) -> Option<ty::Binder<'tcx, ProjectionClause<'tcx>>> {
-        let clause = self.kind();
-        if let ty::ClauseKind::Projection(projection_clause) = clause.skip_binder() {
-            Some(clause.rebind(projection_clause))
-        } else {
-            None
-        }
-    }
-
-    pub fn as_type_outlives_clause(self) -> Option<ty::Binder<'tcx, TypeOutlivesClause<'tcx>>> {
-        let clause = self.kind();
-        if let ty::ClauseKind::TypeOutlives(o) = clause.skip_binder() {
-            Some(clause.rebind(o))
-        } else {
-            None
-        }
-    }
-
-    pub fn as_region_outlives_clause(self) -> Option<ty::Binder<'tcx, RegionOutlivesClause<'tcx>>> {
-        let clause = self.kind();
-        if let ty::ClauseKind::RegionOutlives(o) = clause.skip_binder() {
-            Some(clause.rebind(o))
-        } else {
-            None
-        }
+    fn clause_diag_string(
+        clause: ir::predicates::Clause<Self>,
+        path: &mut Option<std::path::PathBuf>,
+    ) -> String {
+        ty::tls::with(|tcx| tcx.short_string(tcx.lift(clause), path))
     }
 }
 
@@ -343,210 +188,6 @@ pub type PolyTraitRef<'tcx> = ty::Binder<'tcx, TraitRef<'tcx>>;
 pub type PolyExistentialTraitRef<'tcx> = ty::Binder<'tcx, ExistentialTraitRef<'tcx>>;
 pub type PolyExistentialProjection<'tcx> = ty::Binder<'tcx, ExistentialProjection<'tcx>>;
 
-impl<'tcx> Clause<'tcx> {
-    /// Performs a instantiation suitable for going from a
-    /// poly-trait-ref to supertraits that must hold if that
-    /// poly-trait-ref holds. This is slightly different from a normal
-    /// instantiation in terms of what happens with bound regions. See
-    /// lengthy comment below for details.
-    pub fn instantiate_supertrait(
-        self,
-        tcx: TyCtxt<'tcx>,
-        trait_ref: ty::PolyTraitRef<'tcx>,
-    ) -> Clause<'tcx> {
-        // The interaction between HRTB and supertraits is not entirely
-        // obvious. Let me walk you (and myself) through an example.
-        //
-        // Let's start with an easy case. Consider two traits:
-        //
-        //     trait Foo<'a>: Bar<'a,'a> { }
-        //     trait Bar<'b,'c> { }
-        //
-        // Now, if we have a trait reference `for<'x> T: Foo<'x>`, then
-        // we can deduce that `for<'x> T: Bar<'x,'x>`. Basically, if we
-        // knew that `Foo<'x>` (for any 'x) then we also know that
-        // `Bar<'x,'x>` (for any 'x). This more-or-less falls out from
-        // normal instantiation.
-        //
-        // In terms of why this is sound, the idea is that whenever there
-        // is an impl of `T:Foo<'a>`, it must show that `T:Bar<'a,'a>`
-        // holds. So if there is an impl of `T:Foo<'a>` that applies to
-        // all `'a`, then we must know that `T:Bar<'a,'a>` holds for all
-        // `'a`.
-        //
-        // Another example to be careful of is this:
-        //
-        //     trait Foo1<'a>: for<'b> Bar1<'a,'b> { }
-        //     trait Bar1<'b,'c> { }
-        //
-        // Here, if we have `for<'x> T: Foo1<'x>`, then what do we know?
-        // The answer is that we know `for<'x,'b> T: Bar1<'x,'b>`. The
-        // reason is similar to the previous example: any impl of
-        // `T:Foo1<'x>` must show that `for<'b> T: Bar1<'x, 'b>`. So
-        // basically we would want to collapse the bound lifetimes from
-        // the input (`trait_ref`) and the supertraits.
-        //
-        // To achieve this in practice is fairly straightforward. Let's
-        // consider the more complicated scenario:
-        //
-        // - We start out with `for<'x> T: Foo1<'x>`. In this case, `'x`
-        //   has a De Bruijn index of 1. We want to produce `for<'x,'b> T: Bar1<'x,'b>`,
-        //   where both `'x` and `'b` would have a DB index of 1.
-        //   The instantiation from the input trait-ref is therefore going to be
-        //   `'a => 'x` (where `'x` has a DB index of 1).
-        // - The supertrait-ref is `for<'b> Bar1<'a,'b>`, where `'a` is an
-        //   early-bound parameter and `'b` is a late-bound parameter with a
-        //   DB index of 1.
-        // - If we replace `'a` with `'x` from the input, it too will have
-        //   a DB index of 1, and thus we'll have `for<'x,'b> Bar1<'x,'b>`
-        //   just as we wanted.
-        //
-        // There is only one catch. If we just apply the instantiation `'a
-        // => 'x` to `for<'b> Bar1<'a,'b>`, the instantiation code will
-        // adjust the DB index because we instantiating into a binder (it
-        // tries to be so smart...) resulting in `for<'x> for<'b>
-        // Bar1<'x,'b>` (we have no syntax for this, so use your
-        // imagination). Basically the 'x will have DB index of 2 and 'b
-        // will have DB index of 1. Not quite what we want. So we apply
-        // the instantiation to the *contents* of the trait reference,
-        // rather than the trait reference itself (put another way, the
-        // instantiation code expects equal binding levels in the values
-        // from the instantiation and the value being instantiated into, and
-        // this trick achieves that).
-
-        // Working through the second example:
-        // trait_ref: for<'x> T: Foo1<'^0.0>; args: [T, '^0.0]
-        // predicate: for<'b> Self: Bar1<'a, '^0.0>; args: [Self, 'a, '^0.0]
-        // We want to end up with:
-        //     for<'x, 'b> T: Bar1<'^0.0, '^0.1>
-        // To do this:
-        // 1) We must shift all bound vars in predicate by the length
-        //    of trait ref's bound vars. So, we would end up with predicate like
-        //    Self: Bar1<'a, '^0.1>
-        // 2) We can then apply the trait args to this, ending up with
-        //    T: Bar1<'^0.0, '^0.1>
-        // 3) Finally, to create the final bound vars, we concatenate the bound
-        //    vars of the trait ref with those of the predicate:
-        //    ['x, 'b]
-        let bound_pred = self.kind();
-        let pred_bound_vars = bound_pred.bound_vars();
-        let trait_bound_vars = trait_ref.bound_vars();
-        // 1) Self: Bar1<'a, '^0.0> -> Self: Bar1<'a, '^0.1>
-        let shifted_pred =
-            tcx.shift_bound_var_indices(trait_bound_vars.len(), bound_pred.skip_binder());
-        // 2) Self: Bar1<'a, '^0.1> -> T: Bar1<'^0.0, '^0.1>
-        let new = EarlyBinder::bind(tcx, shifted_pred)
-            .instantiate(tcx, trait_ref.skip_binder().args)
-            .skip_norm_wip();
-        // 3) ['x] + ['b] -> ['x, 'b]
-        let bound_vars =
-            tcx.mk_bound_variable_kinds_from_iter(trait_bound_vars.iter().chain(pred_bound_vars));
-
-        // FIXME: Is it really perf sensitive to use reuse_or_mk_predicate here?
-        tcx.reuse_or_mk_predicate(
-            self.as_predicate(),
-            ty::Binder::bind_with_vars(PredicateKind::Clause(new), bound_vars),
-        )
-        .expect_clause()
-    }
-}
-
-impl<'tcx> UpcastFrom<TyCtxt<'tcx>, PredicateKind<'tcx>> for Predicate<'tcx> {
-    fn upcast_from(from: PredicateKind<'tcx>, tcx: TyCtxt<'tcx>) -> Self {
-        ty::Binder::dummy(from).upcast(tcx)
-    }
-}
-
-impl<'tcx> UpcastFrom<TyCtxt<'tcx>, ty::Binder<'tcx, PredicateKind<'tcx>>> for Predicate<'tcx> {
-    fn upcast_from(from: ty::Binder<'tcx, PredicateKind<'tcx>>, tcx: TyCtxt<'tcx>) -> Self {
-        tcx.mk_predicate(from)
-    }
-}
-
-impl<'tcx> UpcastFrom<TyCtxt<'tcx>, ClauseKind<'tcx>> for Predicate<'tcx> {
-    fn upcast_from(from: ClauseKind<'tcx>, tcx: TyCtxt<'tcx>) -> Self {
-        tcx.mk_predicate(ty::Binder::dummy(PredicateKind::Clause(from)))
-    }
-}
-
-impl<'tcx> UpcastFrom<TyCtxt<'tcx>, ty::Binder<'tcx, ClauseKind<'tcx>>> for Predicate<'tcx> {
-    fn upcast_from(from: ty::Binder<'tcx, ClauseKind<'tcx>>, tcx: TyCtxt<'tcx>) -> Self {
-        tcx.mk_predicate(from.map_bound(PredicateKind::Clause))
-    }
-}
-
-impl<'tcx> UpcastFrom<TyCtxt<'tcx>, Clause<'tcx>> for Predicate<'tcx> {
-    fn upcast_from(from: Clause<'tcx>, _tcx: TyCtxt<'tcx>) -> Self {
-        from.as_predicate()
-    }
-}
-
-impl<'tcx> UpcastFrom<TyCtxt<'tcx>, ClauseKind<'tcx>> for Clause<'tcx> {
-    fn upcast_from(from: ClauseKind<'tcx>, tcx: TyCtxt<'tcx>) -> Self {
-        tcx.mk_predicate(ty::Binder::dummy(PredicateKind::Clause(from))).expect_clause()
-    }
-}
-
-impl<'tcx> UpcastFrom<TyCtxt<'tcx>, ty::Binder<'tcx, ClauseKind<'tcx>>> for Clause<'tcx> {
-    fn upcast_from(from: ty::Binder<'tcx, ClauseKind<'tcx>>, tcx: TyCtxt<'tcx>) -> Self {
-        tcx.mk_predicate(from.map_bound(|clause| PredicateKind::Clause(clause))).expect_clause()
-    }
-}
-
-impl<'tcx> UpcastFrom<TyCtxt<'tcx>, TraitRef<'tcx>> for Predicate<'tcx> {
-    fn upcast_from(from: TraitRef<'tcx>, tcx: TyCtxt<'tcx>) -> Self {
-        ty::Binder::dummy(from).upcast(tcx)
-    }
-}
-
-impl<'tcx> UpcastFrom<TyCtxt<'tcx>, TraitRef<'tcx>> for Clause<'tcx> {
-    fn upcast_from(from: TraitRef<'tcx>, tcx: TyCtxt<'tcx>) -> Self {
-        let p: Predicate<'tcx> = from.upcast(tcx);
-        p.expect_clause()
-    }
-}
-
-impl<'tcx> UpcastFrom<TyCtxt<'tcx>, ty::Binder<'tcx, TraitRef<'tcx>>> for Predicate<'tcx> {
-    fn upcast_from(from: ty::Binder<'tcx, TraitRef<'tcx>>, tcx: TyCtxt<'tcx>) -> Self {
-        let pred: PolyTraitClause<'tcx> = from.upcast(tcx);
-        pred.upcast(tcx)
-    }
-}
-
-impl<'tcx> UpcastFrom<TyCtxt<'tcx>, ty::Binder<'tcx, TraitRef<'tcx>>> for Clause<'tcx> {
-    fn upcast_from(from: ty::Binder<'tcx, TraitRef<'tcx>>, tcx: TyCtxt<'tcx>) -> Self {
-        let pred: PolyTraitClause<'tcx> = from.upcast(tcx);
-        pred.upcast(tcx)
-    }
-}
-
-impl<'tcx> UpcastFrom<TyCtxt<'tcx>, TraitClause<'tcx>> for Predicate<'tcx> {
-    fn upcast_from(from: TraitClause<'tcx>, tcx: TyCtxt<'tcx>) -> Self {
-        PredicateKind::Clause(ClauseKind::Trait(from)).upcast(tcx)
-    }
-}
-
-impl<'tcx> UpcastFrom<TyCtxt<'tcx>, PolyTraitClause<'tcx>> for Predicate<'tcx> {
-    fn upcast_from(from: PolyTraitClause<'tcx>, tcx: TyCtxt<'tcx>) -> Self {
-        from.map_bound_no_validate_bound_vars(|p| PredicateKind::Clause(ClauseKind::Trait(p)))
-            .upcast(tcx)
-    }
-}
-
-impl<'tcx> UpcastFrom<TyCtxt<'tcx>, TraitClause<'tcx>> for Clause<'tcx> {
-    fn upcast_from(from: TraitClause<'tcx>, tcx: TyCtxt<'tcx>) -> Self {
-        let p: Predicate<'tcx> = from.upcast(tcx);
-        p.expect_clause()
-    }
-}
-
-impl<'tcx> UpcastFrom<TyCtxt<'tcx>, PolyTraitClause<'tcx>> for Clause<'tcx> {
-    fn upcast_from(from: PolyTraitClause<'tcx>, tcx: TyCtxt<'tcx>) -> Self {
-        let p: Predicate<'tcx> = from.upcast(tcx);
-        p.expect_clause()
-    }
-}
-
 impl<'tcx> UpcastFrom<TyCtxt<'tcx>, RegionOutlivesClause<'tcx>> for Predicate<'tcx> {
     fn upcast_from(from: RegionOutlivesClause<'tcx>, tcx: TyCtxt<'tcx>) -> Self {
         ty::Binder::dummy(PredicateKind::Clause(ClauseKind::RegionOutlives(from))).upcast(tcx)
@@ -565,86 +206,6 @@ impl<'tcx> UpcastFrom<TyCtxt<'tcx>, TypeOutlivesClause<'tcx>> for Predicate<'tcx
     }
 }
 
-impl<'tcx> UpcastFrom<TyCtxt<'tcx>, ProjectionClause<'tcx>> for Predicate<'tcx> {
-    fn upcast_from(from: ProjectionClause<'tcx>, tcx: TyCtxt<'tcx>) -> Self {
-        ty::Binder::dummy(PredicateKind::Clause(ClauseKind::Projection(from))).upcast(tcx)
-    }
-}
-
-impl<'tcx> UpcastFrom<TyCtxt<'tcx>, PolyProjectionClause<'tcx>> for Predicate<'tcx> {
-    fn upcast_from(from: PolyProjectionClause<'tcx>, tcx: TyCtxt<'tcx>) -> Self {
-        from.map_bound(|p| PredicateKind::Clause(ClauseKind::Projection(p))).upcast(tcx)
-    }
-}
-
-impl<'tcx> UpcastFrom<TyCtxt<'tcx>, ProjectionClause<'tcx>> for Clause<'tcx> {
-    fn upcast_from(from: ProjectionClause<'tcx>, tcx: TyCtxt<'tcx>) -> Self {
-        let p: Predicate<'tcx> = from.upcast(tcx);
-        p.expect_clause()
-    }
-}
-
-impl<'tcx> UpcastFrom<TyCtxt<'tcx>, PolyProjectionClause<'tcx>> for Clause<'tcx> {
-    fn upcast_from(from: PolyProjectionClause<'tcx>, tcx: TyCtxt<'tcx>) -> Self {
-        let p: Predicate<'tcx> = from.upcast(tcx);
-        p.expect_clause()
-    }
-}
-
-impl<'tcx> UpcastFrom<TyCtxt<'tcx>, ty::Binder<'tcx, ty::HostEffectClause<'tcx>>>
-    for Predicate<'tcx>
-{
-    fn upcast_from(from: ty::Binder<'tcx, ty::HostEffectClause<'tcx>>, tcx: TyCtxt<'tcx>) -> Self {
-        from.map_bound(ty::ClauseKind::HostEffect).upcast(tcx)
-    }
-}
-
-impl<'tcx> UpcastFrom<TyCtxt<'tcx>, ty::Binder<'tcx, ty::HostEffectClause<'tcx>>> for Clause<'tcx> {
-    fn upcast_from(from: ty::Binder<'tcx, ty::HostEffectClause<'tcx>>, tcx: TyCtxt<'tcx>) -> Self {
-        from.map_bound(ty::ClauseKind::HostEffect).upcast(tcx)
-    }
-}
-
-impl<'tcx> UpcastFrom<TyCtxt<'tcx>, NormalizesTo<'tcx>> for Predicate<'tcx> {
-    fn upcast_from(from: NormalizesTo<'tcx>, tcx: TyCtxt<'tcx>) -> Self {
-        PredicateKind::NormalizesTo(from).upcast(tcx)
-    }
-}
-
-impl<'tcx> Predicate<'tcx> {
-    pub fn as_trait_clause(self) -> Option<PolyTraitClause<'tcx>> {
-        let predicate = self.kind();
-        match predicate.skip_binder() {
-            PredicateKind::Clause(ClauseKind::Trait(t)) => Some(predicate.rebind(t)),
-            _ => None,
-        }
-    }
-
-    pub fn as_projection_clause(self) -> Option<PolyProjectionClause<'tcx>> {
-        let predicate = self.kind();
-        match predicate.skip_binder() {
-            PredicateKind::Clause(ClauseKind::Projection(t)) => Some(predicate.rebind(t)),
-            _ => None,
-        }
-    }
-
-    /// Matches a `PredicateKind::Clause` and turns it into a `Clause`, otherwise returns `None`.
-    pub fn as_clause(self) -> Option<Clause<'tcx>> {
-        match self.kind().skip_binder() {
-            PredicateKind::Clause(..) => Some(self.expect_clause()),
-            _ => None,
-        }
-    }
-
-    /// Assert that the predicate is a clause.
-    pub fn expect_clause(self) -> Clause<'tcx> {
-        match self.kind().skip_binder() {
-            PredicateKind::Clause(..) => Clause(self.0),
-            _ => bug!("{self} is not a clause"),
-        }
-    }
-}
-
 // Some types are used a lot. Make sure they don't unintentionally get bigger.
 #[cfg(target_pointer_width = "64")]
 mod size_asserts {
@@ -653,6 +214,6 @@ mod size_asserts {
     use super::*;
     // tidy-alphabetical-start
     static_assert_size!(PredicateKind<'_>, 40);
-    static_assert_size!(WithCachedTypeInfo<PredicateKind<'_>>, 48);
+    static_assert_size!(rustc_type_ir::WithCachedTypeInfo<PredicateKind<'_>>, 48);
     // tidy-alphabetical-end
 }
diff --git a/compiler/rustc_middle/src/ty/print/pretty.rs b/compiler/rustc_middle/src/ty/print/pretty.rs
index e6e29fe7eac70..f09e7f45fff84 100644
--- a/compiler/rustc_middle/src/ty/print/pretty.rs
+++ b/compiler/rustc_middle/src/ty/print/pretty.rs
@@ -3427,14 +3427,6 @@ define_print_and_forward_display! {
       }
     }
 
-    ty::Predicate<'tcx> {
-        self.kind().print(p)?;
-    }
-
-    ty::Clause<'tcx> {
-        self.kind().print(p)?;
-    }
-
     ty::UserTypeKind<'tcx> {
         match *self {
             Self::Ty(ty) => {
@@ -3467,6 +3459,20 @@ define_print_and_forward_display! {
     }
 }
 
+// Predicate and Clause are owned by rustc_type_ir, which provides their Display impls.
+// Keep rustc's Print implementations here so its existing printer is unchanged.
+define_print! {
+    (self, p):
+
+    ty::Predicate<'tcx> {
+        self.kind().print(p)?;
+    }
+
+    ty::Clause<'tcx> {
+        self.kind().print(p)?;
+    }
+}
+
 fn for_each_def(tcx: TyCtxt<'_>, mut collect_fn: impl for<'b> FnMut(&'b Ident, Namespace, DefId)) {
     // Iterate all (non-anonymous) local crate items no matter where they are defined.
     for id in tcx.hir_free_items() {
diff --git a/compiler/rustc_middle/src/ty/structural_impls.rs b/compiler/rustc_middle/src/ty/structural_impls.rs
index 300c70e04ede6..43287c54936a6 100644
--- a/compiler/rustc_middle/src/ty/structural_impls.rs
+++ b/compiler/rustc_middle/src/ty/structural_impls.rs
@@ -9,14 +9,14 @@ use rustc_abi::TyAndLayout;
 use rustc_hir::def::Namespace;
 use rustc_hir::def_id::LocalDefId;
 use rustc_span::Spanned;
-use rustc_type_ir::{PredicateProxy, TypeFolder, Upcast, VisitorResult, try_visit};
+use rustc_type_ir::{TypeFolder, VisitorResult, try_visit};
 
 use super::{GenericArg, GenericArgKind, Pattern};
 use crate::mir::PlaceElem;
 use crate::ty::print::{FmtPrinter, Printer, with_no_trimmed_paths};
 use crate::ty::{
-    self, Binder, FallibleTypeFolder, Lift, ProjectionClause, Term, TermKind, Ty, TyCtxt,
-    TypeFoldable, TypeSuperFoldable, TypeSuperVisitable, TypeVisitable, TypeVisitor,
+    self, FallibleTypeFolder, Lift, Term, TermKind, Ty, TyCtxt, TypeFoldable, TypeSuperFoldable,
+    TypeSuperVisitable, TypeVisitable, TypeVisitor,
 };
 
 impl fmt::Debug for ty::TraitDef {
@@ -97,18 +97,6 @@ impl fmt::Debug for ty::ParamConst {
     }
 }
 
-impl<'tcx> fmt::Debug for ty::Predicate<'tcx> {
-    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
-        write!(f, "{:?}", self.kind())
-    }
-}
-
-impl<'tcx> fmt::Debug for ty::Clause<'tcx> {
-    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
-        write!(f, "{:?}", self.kind())
-    }
-}
-
 impl<'tcx> fmt::Debug for ty::consts::Expr<'tcx> {
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
         match self.kind {
@@ -467,100 +455,6 @@ impl<'tcx> TypeSuperVisitable<TyCtxt<'tcx>> for Ty<'tcx> {
     }
 }
 
-impl<'tcx> TypeFoldable<TyCtxt<'tcx>> for ty::Predicate<'tcx> {
-    fn try_fold_with<F: FallibleTypeFolder<TyCtxt<'tcx>>>(
-        self,
-        folder: &mut F,
-    ) -> Result<Self, F::Error> {
-        folder.try_fold_predicate(self)
-    }
-
-    fn fold_with<F: TypeFolder<TyCtxt<'tcx>>>(self, folder: &mut F) -> Self {
-        folder.fold_predicate(self)
-    }
-}
-
-impl<'tcx> PredicateProxy<TyCtxt<'tcx>> for ty::Predicate<'tcx> {
-    fn allow_normalization(&self) -> bool {
-        rustc_type_ir::inherent::Predicate::allow_normalization(*self)
-    }
-
-    fn map_projection(
-        self,
-        tcx: TyCtxt<'tcx>,
-        f: impl FnOnce(Binder<'tcx, ProjectionClause<'tcx>>) -> Binder<'tcx, ProjectionClause<'tcx>>,
-    ) -> Option<Self> {
-        self.as_projection_clause().map(|kind| f(kind).upcast(tcx))
-    }
-
-    fn clause_kind_unchecked(&self) -> Option<ty::Binder<'tcx, ty::ClauseKind<'tcx>>> {
-        self.as_clause().map(|clause| clause.kind())
-    }
-}
-
-// FIXME(clause): This is wonky
-impl<'tcx> TypeFoldable<TyCtxt<'tcx>> for ty::Clause<'tcx> {
-    fn try_fold_with<F: FallibleTypeFolder<TyCtxt<'tcx>>>(
-        self,
-        folder: &mut F,
-    ) -> Result<Self, F::Error> {
-        Ok(folder.try_fold_predicate(self)?)
-    }
-
-    fn fold_with<F: TypeFolder<TyCtxt<'tcx>>>(self, folder: &mut F) -> Self {
-        folder.fold_predicate(self)
-    }
-}
-
-// follow `Predicate`'s implementation (by deferring to it)
-impl<'tcx> TypeSuperFoldable<TyCtxt<'tcx>> for ty::Clause<'tcx> {
-    fn try_super_fold_with<F: FallibleTypeFolder<TyCtxt<'tcx>>>(
-        self,
-        folder: &mut F,
-    ) -> Result<Self, F::Error> {
-        <ty::Predicate<'_> as TypeSuperFoldable<TyCtxt<'tcx>>>::try_super_fold_with(
-            self.as_predicate(),
-            folder,
-        )
-        .map(|i| i.expect_clause())
-    }
-
-    fn super_fold_with<F: TypeFolder<TyCtxt<'tcx>>>(self, folder: &mut F) -> Self {
-        <ty::Predicate<'_> as TypeSuperFoldable<TyCtxt<'tcx>>>::super_fold_with(
-            self.as_predicate(),
-            folder,
-        )
-        .expect_clause()
-    }
-}
-
-impl<'tcx> TypeSuperVisitable<TyCtxt<'tcx>> for ty::Clause<'tcx> {
-    fn super_visit_with<V: TypeVisitor<TyCtxt<'tcx>>>(&self, visitor: &mut V) -> V::Result {
-        <ty::Predicate<'_> as TypeSuperVisitable<TyCtxt<'tcx>>>::super_visit_with(
-            &self.as_predicate(),
-            visitor,
-        )
-    }
-}
-
-impl<'tcx> PredicateProxy<TyCtxt<'tcx>> for ty::Clause<'tcx> {
-    fn allow_normalization(&self) -> bool {
-        self.as_predicate().allow_normalization()
-    }
-
-    fn map_projection(
-        self,
-        tcx: TyCtxt<'tcx>,
-        f: impl FnOnce(Binder<'tcx, ProjectionClause<'tcx>>) -> Binder<'tcx, ProjectionClause<'tcx>>,
-    ) -> Option<Self> {
-        self.as_projection_clause().map(|kind| f(kind).upcast(tcx))
-    }
-
-    fn clause_kind_unchecked(&self) -> Option<ty::Binder<'tcx, ty::ClauseKind<'tcx>>> {
-        Some(self.kind())
-    }
-}
-
 impl<'tcx> TypeFoldable<TyCtxt<'tcx>> for ty::Clauses<'tcx> {
     fn try_fold_with<F: FallibleTypeFolder<TyCtxt<'tcx>>>(
         self,
@@ -574,47 +468,6 @@ impl<'tcx> TypeFoldable<TyCtxt<'tcx>> for ty::Clauses<'tcx> {
     }
 }
 
-impl<'tcx> TypeVisitable<TyCtxt<'tcx>> for ty::Predicate<'tcx> {
-    fn visit_with<V: TypeVisitor<TyCtxt<'tcx>>>(&self, visitor: &mut V) -> V::Result {
-        visitor.visit_predicate(*self)
-    }
-}
-
-impl<'tcx> TypeVisitable<TyCtxt<'tcx>> for ty::Clause<'tcx> {
-    fn visit_with<V: TypeVisitor<TyCtxt<'tcx>>>(&self, visitor: &mut V) -> V::Result {
-        visitor.visit_predicate(self.as_predicate())
-    }
-}
-
-impl<'tcx> TypeSuperFoldable<TyCtxt<'tcx>> for ty::Predicate<'tcx> {
-    fn try_super_fold_with<F: FallibleTypeFolder<TyCtxt<'tcx>>>(
-        self,
-        folder: &mut F,
-    ) -> Result<Self, F::Error> {
-        // This method looks different to `Ty::try_super_fold_with` and `Const::super_fold_with`.
-        // Why is that? `PredicateKind` provides little scope for optimized folding, unlike
-        // `TyKind` and `ConstKind` (which have common variants that don't require recursive
-        // `fold_with` calls on their fields). So we just derive the `TypeFoldable` impl for
-        // `PredicateKind` and call it here because the derived code is as fast as hand-written
-        // code would be.
-        let new = self.kind().try_fold_with(folder)?;
-        Ok(folder.cx().reuse_or_mk_predicate(self, new))
-    }
-
-    fn super_fold_with<F: TypeFolder<TyCtxt<'tcx>>>(self, folder: &mut F) -> Self {
-        // See comment in `Predicate::try_super_fold_with`.
-        let new = self.kind().fold_with(folder);
-        folder.cx().reuse_or_mk_predicate(self, new)
-    }
-}
-
-impl<'tcx> TypeSuperVisitable<TyCtxt<'tcx>> for ty::Predicate<'tcx> {
-    fn super_visit_with<V: TypeVisitor<TyCtxt<'tcx>>>(&self, visitor: &mut V) -> V::Result {
-        // See comment in `Predicate::try_super_fold_with`.
-        self.kind().visit_with(visitor)
-    }
-}
-
 impl<'tcx> TypeVisitable<TyCtxt<'tcx>> for ty::Clauses<'tcx> {
     fn visit_with<V: TypeVisitor<TyCtxt<'tcx>>>(&self, visitor: &mut V) -> V::Result {
         visitor.visit_clauses(self)
diff --git a/compiler/rustc_monomorphize/src/offload/manifest.rs b/compiler/rustc_monomorphize/src/offload/manifest.rs
index a6f5d1228082e..40ccd96b40fcd 100644
--- a/compiler/rustc_monomorphize/src/offload/manifest.rs
+++ b/compiler/rustc_monomorphize/src/offload/manifest.rs
@@ -131,6 +131,12 @@ impl<'a, 'tcx> SpanEncoder for OffloadManifestEncoder<'a, 'tcx> {
     }
 }
 
+impl<'a, 'tcx> ty::PredicateEncoder<TyCtxt<'tcx>> for OffloadManifestEncoder<'a, 'tcx> {
+    fn encode_predicate(&mut self, predicate: ty::predicates::Predicate<TyCtxt<'tcx>>) {
+        ty::codec::encode_predicate(self, predicate);
+    }
+}
+
 impl<'a, 'tcx> TyEncoder<'tcx> for OffloadManifestEncoder<'a, 'tcx> {
     const CLEAR_CROSS_CRATE: bool = true;
 
@@ -370,6 +376,10 @@ impl<'a, 'tcx> rustc_middle::ty::InternerDecoder for OffloadManifestDecoder<'a,
     fn interner(&self) -> Self::Interner {
         self.tcx
     }
+
+    fn decode_predicate(&mut self) -> ty::predicates::Predicate<Self::Interner> {
+        ty::codec::decode_predicate(self)
+    }
 }
 
 /// Write a list of offload kernel instances to the manifest file.
diff --git a/compiler/rustc_next_trait_solver/src/canonical/mod.rs b/compiler/rustc_next_trait_solver/src/canonical/mod.rs
index 45587d717b418..7c1fd3ca37e06 100644
--- a/compiler/rustc_next_trait_solver/src/canonical/mod.rs
+++ b/compiler/rustc_next_trait_solver/src/canonical/mod.rs
@@ -14,6 +14,7 @@ use std::iter;
 use canonicalizer::Canonicalizer;
 use rustc_index::IndexVec;
 use rustc_type_ir::inherent::*;
+use rustc_type_ir::predicates::Predicate;
 use rustc_type_ir::relate::{
     self, Relate, RelateResult, TypeRelation, VarianceDiagInfo, relate_args_invariantly,
 };
@@ -54,7 +55,7 @@ impl<I: Interner, T> ResponseT<I> for inspect::State<I, T> {
 /// This expects `goal` and `opaque_types` to be eager resolved.
 pub(super) fn canonicalize_goal<D, I>(
     delegate: &D,
-    goal: Goal<I, I::Predicate>,
+    goal: Goal<I, Predicate<I>>,
     opaque_types: &[(ty::OpaqueTypeKey<I>, I::Ty)],
     typing_mode: TypingMode<I>,
 ) -> (ThinVec<I::GenericArg>, I::CanonicalInput)
diff --git a/compiler/rustc_next_trait_solver/src/delegate.rs b/compiler/rustc_next_trait_solver/src/delegate.rs
index 630e1dd68e041..f06299c48350d 100644
--- a/compiler/rustc_next_trait_solver/src/delegate.rs
+++ b/compiler/rustc_next_trait_solver/src/delegate.rs
@@ -1,6 +1,7 @@
 use std::fmt::Debug;
 use std::ops::Deref;
 
+use rustc_type_ir::predicates::Predicate;
 use rustc_type_ir::solve::{
     ComputeGoalFastPathOutcome, FetchEligibleAssocItemResponse, Goal, NoSolution,
     VisibleForLeakCheck,
@@ -42,7 +43,7 @@ pub trait SolverDelegate: Deref<Target = Self::Infcx> + Sized {
 
     fn compute_goal_fast_path(
         &self,
-        goal: Goal<Self::Interner, <Self::Interner as Interner>::Predicate>,
+        goal: Goal<Self::Interner, Predicate<Self::Interner>>,
         span: <Self::Interner as Interner>::Span,
     ) -> ComputeGoalFastPathOutcome<Self::Interner>;
 
@@ -73,7 +74,7 @@ pub trait SolverDelegate: Deref<Target = Self::Infcx> + Sized {
         &self,
         param_env: <Self::Interner as Interner>::ParamEnv,
         term: <Self::Interner as Interner>::Term,
-    ) -> Option<Vec<Goal<Self::Interner, <Self::Interner as Interner>::Predicate>>>;
+    ) -> Option<Vec<Goal<Self::Interner, Predicate<Self::Interner>>>>;
 
     fn make_deduplicated_region_constraints(
         &self,
@@ -101,7 +102,7 @@ pub trait SolverDelegate: Deref<Target = Self::Infcx> + Sized {
         args: <Self::Interner as Interner>::GenericArgs,
         param_env: <Self::Interner as Interner>::ParamEnv,
         hidden_ty: <Self::Interner as Interner>::Ty,
-        goals: &mut Vec<Goal<Self::Interner, <Self::Interner as Interner>::Predicate>>,
+        goals: &mut Vec<Goal<Self::Interner, Predicate<Self::Interner>>>,
     );
 
     fn fetch_eligible_assoc_item(
@@ -130,7 +131,7 @@ pub trait SolverDelegate: Deref<Target = Self::Infcx> + Sized {
 
     fn emit_next_solver_overflow_fcw(
         &self,
-        goal: Goal<Self::Interner, <Self::Interner as Interner>::Predicate>,
+        goal: Goal<Self::Interner, Predicate<Self::Interner>>,
         span: <Self::Interner as Interner>::Span,
     );
 }
diff --git a/compiler/rustc_next_trait_solver/src/solve/assembly/mod.rs b/compiler/rustc_next_trait_solver/src/solve/assembly/mod.rs
index aaa2d723460d5..10998840573cc 100644
--- a/compiler/rustc_next_trait_solver/src/solve/assembly/mod.rs
+++ b/compiler/rustc_next_trait_solver/src/solve/assembly/mod.rs
@@ -8,6 +8,7 @@ use std::ops::ControlFlow;
 use derive_where::derive_where;
 use rustc_type_ir::inherent::*;
 use rustc_type_ir::lang_items::SolverTraitLangItem;
+use rustc_type_ir::predicates::Predicate;
 use rustc_type_ir::search_graph::CandidateHeadUsages;
 use rustc_type_ir::solve::{
     AliasBoundKind, MaybeInfo, NoSolutionOrRerunNonErased, QueryResultOrRerunNonErased,
@@ -65,7 +66,7 @@ where
         parent_source: CandidateSource<I>,
         goal: Goal<I, Self>,
         assumption: I::Clause,
-        requirements: impl IntoIterator<Item = (GoalSource, Goal<I, I::Predicate>)>,
+        requirements: impl IntoIterator<Item = (GoalSource, Goal<I, Predicate<I>>)>,
     ) -> Result<Candidate<I>, NoSolutionOrRerunNonErased> {
         Self::probe_and_match_goal_against_assumption(ecx, parent_source, goal, assumption, |ecx| {
             for (nested_source, goal) in requirements {
@@ -1039,7 +1040,7 @@ where
                 // prove the super trait bounds of the current goal.
                 //
                 // We skip the goal itself as that one would cycle.
-                let predicate: I::Predicate = trait_ref.upcast(cx);
+                let predicate: Predicate<I> = trait_ref.upcast(cx);
                 ecx.add_goals(
                     GoalSource::Misc,
                     elaborate::elaborate(cx, [predicate])
diff --git a/compiler/rustc_next_trait_solver/src/solve/assembly/structural_traits.rs b/compiler/rustc_next_trait_solver/src/solve/assembly/structural_traits.rs
index a7e02f07661c6..27a89ad2c6a64 100644
--- a/compiler/rustc_next_trait_solver/src/solve/assembly/structural_traits.rs
+++ b/compiler/rustc_next_trait_solver/src/solve/assembly/structural_traits.rs
@@ -5,6 +5,7 @@ use derive_where::derive_where;
 use rustc_type_ir::data_structures::HashMap;
 use rustc_type_ir::inherent::*;
 use rustc_type_ir::lang_items::{SolverProjectionLangItem, SolverTraitLangItem};
+use rustc_type_ir::predicates::Predicate;
 use rustc_type_ir::solve::SizedTraitKind;
 use rustc_type_ir::solve::inspect::ProbeKind;
 use rustc_type_ir::{
@@ -437,7 +438,7 @@ pub(in crate::solve) fn extract_tupled_inputs_and_output_from_async_callable<I:
     self_ty: I::Ty,
     goal_kind: ty::ClosureKind,
     env_region: Region<I>,
-) -> Result<(ty::Binder<I, AsyncCallableRelevantTypes<I>>, Vec<I::Predicate>), NoSolution> {
+) -> Result<(ty::Binder<I, AsyncCallableRelevantTypes<I>>, Vec<Predicate<I>>), NoSolution> {
     match self_ty.kind() {
         ty::CoroutineClosure(def_id, args) => {
             if !cx.coroutine_is_async(cx.coroutine_for_closure(def_id)) {
@@ -596,7 +597,7 @@ pub(in crate::solve) fn extract_tupled_inputs_and_output_from_async_callable<I:
 fn fn_item_to_async_callable<I: Interner>(
     cx: I,
     bound_sig: ty::Binder<I, ty::FnSig<I>>,
-) -> Result<(ty::Binder<I, AsyncCallableRelevantTypes<I>>, Vec<I::Predicate>), NoSolution> {
+) -> Result<(ty::Binder<I, AsyncCallableRelevantTypes<I>>, Vec<Predicate<I>>), NoSolution> {
     let sig = bound_sig.skip_binder();
     let future_trait_def_id = cx.require_trait_lang_item(SolverTraitLangItem::Future);
     // `FnDef` and `FnPtr` only implement `AsyncFn*` when their
@@ -889,7 +890,7 @@ pub(in crate::solve) fn predicates_for_object_candidate<D, I>(
     param_env: I::ParamEnv,
     trait_ref: ty::TraitRef<I>,
     object_bounds: I::BoundExistentialPredicates,
-) -> Result<Vec<Goal<I, I::Predicate>>, AmbiguousOrRerunNonErased>
+) -> Result<Vec<Goal<I, Predicate<I>>>, AmbiguousOrRerunNonErased>
 where
     D: SolverDelegate<Interner = I>,
     I: Interner,
@@ -951,7 +952,9 @@ where
     Ok(folder
         .nested
         .into_iter()
-        .chain(requirements.into_iter().map(|clause| Goal::new(cx, param_env, clause)))
+        .chain(
+            requirements.into_iter().map(|clause| Goal::new(cx, param_env, clause.as_predicate())),
+        )
         .collect())
 }
 
@@ -960,7 +963,7 @@ struct ReplaceProjectionWith<'a, 'b, I: Interner, D: SolverDelegate<Interner = I
     param_env: I::ParamEnv,
     self_ty: I::Ty,
     mapping: &'a HashMap<I::TraitAssocTermId, Vec<ty::Binder<I, ty::ProjectionClause<I>>>>,
-    nested: Vec<Goal<I, I::Predicate>>,
+    nested: Vec<Goal<I, Predicate<I>>>,
 }
 
 impl<D, I> ReplaceProjectionWith<'_, '_, I, D>
diff --git a/compiler/rustc_next_trait_solver/src/solve/effect_goals.rs b/compiler/rustc_next_trait_solver/src/solve/effect_goals.rs
index bb6fce7691222..a6e65ba3f82fd 100644
--- a/compiler/rustc_next_trait_solver/src/solve/effect_goals.rs
+++ b/compiler/rustc_next_trait_solver/src/solve/effect_goals.rs
@@ -121,7 +121,8 @@ where
                                     cx,
                                     trait_ref
                                         .to_host_effect_clause(cx, goal.predicate.constness)
-                                        .skip_norm_wip(),
+                                        .skip_norm_wip()
+                                        .as_predicate(),
                                 )
                             },
                         ),
@@ -176,7 +177,7 @@ where
                 .clauses_of(impl_def_id.into())
                 .iter_instantiated(cx, impl_args)
                 .map(Unnormalized::skip_norm_wip)
-                .map(|clause| goal.with(cx, clause));
+                .map(|clause| goal.with(cx, clause.as_predicate()));
             ecx.add_goals(GoalSource::ImplWhereBound, where_clause_bounds)?;
 
             // For this impl to be `const`, we need to check its `[const]` bounds too.
@@ -188,7 +189,8 @@ where
                         cx,
                         bound_trait_ref
                             .to_host_effect_clause(cx, goal.predicate.constness)
-                            .skip_norm_wip(),
+                            .skip_norm_wip()
+                            .as_predicate(),
                     )
                 });
             ecx.add_goals(GoalSource::ImplWhereBound, const_conditions)?;
@@ -225,7 +227,7 @@ where
                 .clauses_of(goal.predicate.def_id().into())
                 .iter_instantiated(cx, goal.predicate.trait_ref.args)
                 .map(Unnormalized::skip_norm_wip)
-                .map(|c| goal.with(cx, c));
+                .map(|c| goal.with(cx, c.as_predicate()));
 
             let const_conditions = cx
                 .const_conditions(goal.predicate.def_id().into())
@@ -235,7 +237,8 @@ where
                         cx,
                         bound_trait_ref
                             .to_host_effect_clause(cx, goal.predicate.constness)
-                            .skip_norm_wip(),
+                            .skip_norm_wip()
+                            .as_predicate(),
                     )
                 });
             // While you could think of trait aliases to have a single builtin impl
@@ -320,7 +323,8 @@ where
                         cx,
                         trait_ref
                             .to_host_effect_clause(cx, goal.predicate.constness)
-                            .skip_norm_wip(),
+                            .skip_norm_wip()
+                            .as_predicate(),
                     ),
                 )
             })
@@ -430,7 +434,8 @@ where
                     goal.with(
                         cx,
                         ty::Binder::dummy(trait_ref)
-                            .to_host_effect_clause(cx, goal.predicate.constness),
+                            .to_host_effect_clause(cx, goal.predicate.constness)
+                            .as_predicate(),
                     )
                 }),
             )?;
diff --git a/compiler/rustc_next_trait_solver/src/solve/eval_ctxt/fast_path.rs b/compiler/rustc_next_trait_solver/src/solve/eval_ctxt/fast_path.rs
index 988850bc64c5b..a65c7c6eaa410 100644
--- a/compiler/rustc_next_trait_solver/src/solve/eval_ctxt/fast_path.rs
+++ b/compiler/rustc_next_trait_solver/src/solve/eval_ctxt/fast_path.rs
@@ -6,6 +6,7 @@
 //! For debugging, fast paths can be disabled using `-Zdisable-fast-paths`.
 
 use rustc_type_ir::inherent::*;
+use rustc_type_ir::predicates::Predicate;
 use rustc_type_ir::solve::{
     Certainty, ComputeGoalFastPathOutcome, Goal, GoalStalledOn, GoalStalledOnOpaques, MaybeInfo,
     SucceededInErased,
@@ -132,7 +133,7 @@ where
 #[inline(never)]
 pub(super) fn compute_goal_fast_path_cold<D, I>(
     delegate: &D,
-    goal: Goal<I, I::Predicate>,
+    goal: Goal<I, Predicate<I>>,
     origin_span: I::Span,
 ) -> Option<GoalEvaluation<I>>
 where
@@ -146,7 +147,7 @@ where
 /// See the docs on [`ComputeGoalFastPathOutcome`]
 pub fn compute_goal_fast_path<D, I>(
     delegate: &D,
-    goal: Goal<I, I::Predicate>,
+    goal: Goal<I, Predicate<I>>,
     origin_span: I::Span,
 ) -> Option<GoalEvaluation<I>>
 where
diff --git a/compiler/rustc_next_trait_solver/src/solve/eval_ctxt/mod.rs b/compiler/rustc_next_trait_solver/src/solve/eval_ctxt/mod.rs
index 3b372876f574b..56ff4af0b9829 100644
--- a/compiler/rustc_next_trait_solver/src/solve/eval_ctxt/mod.rs
+++ b/compiler/rustc_next_trait_solver/src/solve/eval_ctxt/mod.rs
@@ -5,6 +5,7 @@ use std::ops::ControlFlow;
 use rustc_macros::StableHash;
 use rustc_type_ir::data_structures::HashSet;
 use rustc_type_ir::inherent::*;
+use rustc_type_ir::predicates::Predicate;
 use rustc_type_ir::region_constraint::RegionConstraint;
 use rustc_type_ir::relate::Relate;
 use rustc_type_ir::relate::solver_relating::RelateExt;
@@ -83,7 +84,7 @@ enum CurrentGoalKind {
 }
 
 impl CurrentGoalKind {
-    fn from_query_input<I: Interner>(cx: I, input: QueryInput<I, I::Predicate>) -> CurrentGoalKind {
+    fn from_query_input<I: Interner>(cx: I, input: QueryInput<I, Predicate<I>>) -> CurrentGoalKind {
         match input.goal.predicate.kind().skip_binder() {
             ty::PredicateKind::Clause(ty::ClauseKind::Trait(pred)) => {
                 if cx.trait_is_coinductive(pred.trait_ref.def_id) {
@@ -149,7 +150,7 @@ where
 
     pub(super) search_graph: &'a mut SearchGraph<D>,
 
-    nested_goals: Vec<(GoalSource, Goal<I, I::Predicate>, Option<GoalStalledOn<I>>)>,
+    nested_goals: Vec<(GoalSource, Goal<I, Predicate<I>>, Option<GoalStalledOn<I>>)>,
 
     pub(super) origin_span: I::Span,
 
@@ -181,7 +182,7 @@ pub trait SolverDelegateEvalExt: SolverDelegate {
     /// search graph which would break cycle detection.
     fn evaluate_root_goal(
         &self,
-        goal: Goal<Self::Interner, <Self::Interner as Interner>::Predicate>,
+        goal: Goal<Self::Interner, Predicate<Self::Interner>>,
         span: <Self::Interner as Interner>::Span,
         stalled_on: Option<GoalStalledOn<Self::Interner>>,
     ) -> Result<GoalEvaluation<Self::Interner>, NoSolution>;
@@ -196,7 +197,7 @@ pub trait SolverDelegateEvalExt: SolverDelegate {
     /// See the comment on [OpaqueTypesJank] for more details.
     fn root_goal_may_hold_opaque_types_jank(
         &self,
-        goal: Goal<Self::Interner, <Self::Interner as Interner>::Predicate>,
+        goal: Goal<Self::Interner, Predicate<Self::Interner>>,
     ) -> bool;
 
     /// Check whether evaluating `goal` with a depth of `root_depth` may
@@ -209,14 +210,14 @@ pub trait SolverDelegateEvalExt: SolverDelegate {
     fn root_goal_may_hold_with_depth(
         &self,
         root_depth: usize,
-        goal: Goal<Self::Interner, <Self::Interner as Interner>::Predicate>,
+        goal: Goal<Self::Interner, Predicate<Self::Interner>>,
     ) -> bool;
 
     // FIXME: This is only exposed because we need to use it in `analyse.rs`
     // which is not yet uplifted. Once that's done, we should remove this.
     fn evaluate_root_goal_for_proof_tree(
         &self,
-        goal: Goal<Self::Interner, <Self::Interner as Interner>::Predicate>,
+        goal: Goal<Self::Interner, Predicate<Self::Interner>>,
         span: <Self::Interner as Interner>::Span,
     ) -> (
         Result<NestedNormalizationGoals<Self::Interner>, NoSolution>,
@@ -232,7 +233,7 @@ where
     #[instrument(level = "debug", skip(self), ret)]
     fn evaluate_root_goal(
         &self,
-        goal: Goal<I, I::Predicate>,
+        goal: Goal<I, Predicate<I>>,
         span: I::Span,
         stalled_on: Option<GoalStalledOn<I>>,
     ) -> Result<GoalEvaluation<I>, NoSolution> {
@@ -283,7 +284,7 @@ where
     #[instrument(level = "debug", skip(self), ret)]
     fn root_goal_may_hold_opaque_types_jank(
         &self,
-        goal: Goal<Self::Interner, <Self::Interner as Interner>::Predicate>,
+        goal: Goal<Self::Interner, Predicate<Self::Interner>>,
     ) -> bool {
         self.probe(|| {
             self.evaluate_root_goal(goal, I::Span::dummy(), None).is_ok_and(|r| match r.certainty {
@@ -303,7 +304,7 @@ where
     fn root_goal_may_hold_with_depth(
         &self,
         root_depth: usize,
-        goal: Goal<Self::Interner, <Self::Interner as Interner>::Predicate>,
+        goal: Goal<Self::Interner, Predicate<Self::Interner>>,
     ) -> bool {
         self.probe(|| {
             EvalCtxt::enter_root(self, root_depth, I::Span::dummy(), |ecx| {
@@ -316,7 +317,7 @@ where
     #[instrument(level = "debug", skip(self))]
     fn evaluate_root_goal_for_proof_tree(
         &self,
-        goal: Goal<I, I::Predicate>,
+        goal: Goal<I, Predicate<I>>,
         span: I::Span,
     ) -> (Result<NestedNormalizationGoals<I>, NoSolution>, inspect::GoalEvaluation<I>) {
         let mut result =
@@ -338,7 +339,7 @@ where
 /// See the doc comment on `RECURSION_DEPTH_EXCEEDING_LIMIT` and #159228 for more details.
 fn maybe_evaluate_root_goal_with_higher_recursion_limit<D, I>(
     delegate: &D,
-    goal: Goal<I, I::Predicate>,
+    goal: Goal<I, Predicate<I>>,
     span: I::Span,
     initial_result: &mut Result<GoalEvaluation<I>, NoSolutionOrRerunNonErased>,
 ) where
@@ -380,7 +381,7 @@ fn maybe_evaluate_root_goal_with_higher_recursion_limit<D, I>(
 /// See the doc comment on `RECURSION_DEPTH_EXCEEDING_LIMIT` and #159228 for more details.
 fn maybe_evaluate_root_goal_for_proof_tree_with_higher_recursion_limit<D, I>(
     delegate: &D,
-    goal: Goal<I, I::Predicate>,
+    goal: Goal<I, Predicate<I>>,
     span: I::Span,
     initial_result: &mut (
         Result<NestedNormalizationGoals<I>, NoSolution>,
@@ -416,7 +417,7 @@ fn maybe_evaluate_root_goal_for_proof_tree_with_higher_recursion_limit<D, I>(
         }
     });
     if let Ok(rerun_result) = rerun_result {
-        let predicate: I::Predicate = goal_evaluation.uncanonicalized_goal.predicate;
+        let predicate: Predicate<I> = goal_evaluation.uncanonicalized_goal.predicate;
         delegate.emit_next_solver_overflow_fcw(goal.with(delegate.cx(), predicate), span);
         *initial_result = rerun_result;
     }
@@ -510,7 +511,7 @@ where
         proof_tree_builder: &mut inspect::ProofTreeBuilder<D>,
         f: impl FnOnce(
             &mut EvalCtxt<'_, D>,
-            Goal<I, I::Predicate>,
+            Goal<I, Predicate<I>>,
         ) -> Result<T, NoSolutionOrRerunNonErased>,
     ) -> (Result<T, NoSolution>, AccessedOpaques<I>) {
         let (ref delegate, input, var_values) = D::build_with_canonical(cx, &canonical_input);
@@ -592,7 +593,7 @@ where
     fn evaluate_goal(
         &mut self,
         source: GoalSource,
-        goal: Goal<I, I::Predicate>,
+        goal: Goal<I, Predicate<I>>,
         stalled_on: Option<GoalStalledOn<I>>,
     ) -> Result<GoalEvaluation<I>, NoSolutionOrRerunNonErased> {
         if let RerunStalled::WontMakeProgress(stalled_maybe_info) =
@@ -624,7 +625,7 @@ where
     fn evaluate_goal_no_fast_paths(
         &mut self,
         source: GoalSource,
-        goal: Goal<I, I::Predicate>,
+        goal: Goal<I, Predicate<I>>,
     ) -> Result<GoalEvaluation<I>, NoSolutionOrRerunNonErased> {
         let (normalization_nested_goals, goal_evaluation) = self.evaluate_goal_raw(source, goal)?;
         assert!(normalization_nested_goals.is_empty());
@@ -749,7 +750,7 @@ where
     pub(super) fn evaluate_goal_raw(
         &mut self,
         source: GoalSource,
-        goal: Goal<I, I::Predicate>,
+        goal: Goal<I, Predicate<I>>,
     ) -> Result<(NestedNormalizationGoals<I>, GoalEvaluation<I>), NoSolutionOrRerunNonErased> {
         // We only care about one entry per `OpaqueTypeKey` here,
         // so we only canonicalize the lookup table and ignore
@@ -970,7 +971,7 @@ where
 
     pub(super) fn compute_goal(
         &mut self,
-        goal: Goal<I, I::Predicate>,
+        goal: Goal<I, Predicate<I>>,
     ) -> QueryResultOrRerunNonErased<I> {
         let Goal { param_env, predicate } = goal;
         let kind = predicate.kind();
@@ -1095,7 +1096,7 @@ where
     pub(super) fn add_goal(
         &mut self,
         source: GoalSource,
-        mut goal: Goal<I, I::Predicate>,
+        mut goal: Goal<I, Predicate<I>>,
     ) -> Result<(), NoSolutionOrRerunNonErased> {
         goal.predicate =
             self.normalize(goal.param_env, ty::Unnormalized::new_wip(goal.predicate))?;
@@ -1121,7 +1122,7 @@ where
     pub(super) fn add_goals(
         &mut self,
         source: GoalSource,
-        goals: impl IntoIterator<Item = Goal<I, I::Predicate>>,
+        goals: impl IntoIterator<Item = Goal<I, Predicate<I>>>,
     ) -> Result<(), NoSolutionOrRerunNonErased> {
         for goal in goals {
             self.add_goal(source, goal)?;
@@ -1350,7 +1351,7 @@ where
         param_env: I::ParamEnv,
         lhs: T,
         rhs: T,
-    ) -> Result<Vec<Goal<I, I::Predicate>>, NoSolution> {
+    ) -> Result<Vec<Goal<I, Predicate<I>>>, NoSolution> {
         Ok(self.delegate.relate(param_env, lhs, ty::Variance::Invariant, rhs, self.origin_span)?)
     }
 
@@ -1442,7 +1443,7 @@ where
         &self,
         param_env: I::ParamEnv,
         term: I::Term,
-    ) -> Option<Vec<Goal<I, I::Predicate>>> {
+    ) -> Option<Vec<Goal<I, Predicate<I>>>> {
         self.delegate.well_formed_goals(param_env, term)
     }
 
@@ -2031,7 +2032,7 @@ pub fn evaluate_root_goal_for_proof_tree_raw_provider<
 /// [EvalCtxt] and uses a separate cache.
 pub(super) fn evaluate_root_goal_for_proof_tree<D: SolverDelegate<Interner = I>, I: Interner>(
     delegate: &D,
-    goal: Goal<I, I::Predicate>,
+    goal: Goal<I, Predicate<I>>,
     origin_span: I::Span,
     root_depth: usize,
 ) -> (Result<NestedNormalizationGoals<I>, NoSolution>, inspect::GoalEvaluation<I>) {
diff --git a/compiler/rustc_next_trait_solver/src/solve/eval_ctxt/probe.rs b/compiler/rustc_next_trait_solver/src/solve/eval_ctxt/probe.rs
index d9d18bdeea7e7..e2b788a9b90be 100644
--- a/compiler/rustc_next_trait_solver/src/solve/eval_ctxt/probe.rs
+++ b/compiler/rustc_next_trait_solver/src/solve/eval_ctxt/probe.rs
@@ -1,5 +1,6 @@
 use std::marker::PhantomData;
 
+use rustc_type_ir::predicates::Predicate;
 use rustc_type_ir::search_graph::CandidateHeadUsages;
 use rustc_type_ir::solve::{
     AccessedOpaques, CanonicalResponse, NoSolutionOrRerunNonErased, RerunResultExt,
@@ -67,7 +68,7 @@ where
     pub(in crate::solve) fn enter_inner(
         self,
         f: impl FnOnce(&mut EvalCtxt<'_, D>) -> Result<T, NoSolutionOrRerunNonErased>,
-        propagated_nested_goals: Vec<(GoalSource, Goal<I, I::Predicate>, Option<GoalStalledOn<I>>)>,
+        propagated_nested_goals: Vec<(GoalSource, Goal<I, Predicate<I>>, Option<GoalStalledOn<I>>)>,
     ) -> Result<T, NoSolutionOrRerunNonErased> {
         let ProbeCtxt { ecx: outer, probe_kind, _result } = self;
 
diff --git a/compiler/rustc_next_trait_solver/src/solve/eval_ctxt/solver_region_constraints.rs b/compiler/rustc_next_trait_solver/src/solve/eval_ctxt/solver_region_constraints.rs
index 8a4d3fba99a39..92b8ce9c7ec06 100644
--- a/compiler/rustc_next_trait_solver/src/solve/eval_ctxt/solver_region_constraints.rs
+++ b/compiler/rustc_next_trait_solver/src/solve/eval_ctxt/solver_region_constraints.rs
@@ -4,6 +4,7 @@
 use rustc_data_structures::transitive_relation::TransitiveRelationBuilder;
 use rustc_type_ir::inherent::*;
 use rustc_type_ir::outlives::{Component, push_outlives_components};
+use rustc_type_ir::predicates::Predicate;
 #[cfg(not(feature = "nightly"))]
 use rustc_type_ir::region_constraint::TransitiveRelationBuilder;
 use rustc_type_ir::region_constraint::{
@@ -11,7 +12,7 @@ use rustc_type_ir::region_constraint::{
 };
 use rustc_type_ir::{
     AliasTy, Binder, ClauseKind, Const, InferCtxtLike, Interner, Region, TypeVisitable,
-    TypeVisitableExt, TypeVisitor, UniverseIndex,
+    TypeVisitableExt, TypeVisitor, UniverseIndex, Upcast as _,
 };
 use tracing::{debug, instrument};
 
@@ -39,7 +40,7 @@ where
         struct RawAssumptions<'a, 'b, D: SolverDelegate<Interner = I>, I: Interner> {
             ecx: &'a mut EvalCtxt<'b, D, I>,
             param_env: I::ParamEnv,
-            out: Vec<Goal<I, I::Predicate>>,
+            out: Vec<Goal<I, Predicate<I>>>,
         }
 
         impl<D, I> TypeVisitor<I> for RawAssumptions<'_, '_, D, I>
@@ -100,7 +101,10 @@ where
         //
         // `Assumptions::new` elaborates, restricts the clauses to `u` and picks out the
         // outlives ones for us, so we just hand over everything the requirements gave us.
-        let clauses = reqs.into_iter().filter_map(|goal| goal.predicate.as_clause());
+        let cx = self.cx();
+        let clauses = reqs
+            .into_iter()
+            .filter_map(|goal| goal.predicate.as_clause().map(|clause| clause.kind().upcast(cx)));
 
         Some(Assumptions::new(
             &**self.delegate,
diff --git a/compiler/rustc_next_trait_solver/src/solve/inspect/build.rs b/compiler/rustc_next_trait_solver/src/solve/inspect/build.rs
index 9584e16d68725..aa4cd250bf9d7 100644
--- a/compiler/rustc_next_trait_solver/src/solve/inspect/build.rs
+++ b/compiler/rustc_next_trait_solver/src/solve/inspect/build.rs
@@ -8,6 +8,7 @@ use std::marker::PhantomData;
 
 use derive_where::derive_where;
 use rustc_type_ir::inherent::*;
+use rustc_type_ir::predicates::Predicate;
 use rustc_type_ir::{self as ty, Interner};
 
 use crate::canonical;
@@ -146,7 +147,7 @@ impl<I: Interner> WipProbe<I> {
 
 #[derive_where(PartialEq, Debug; I: Interner)]
 enum WipProbeStep<I: Interner> {
-    AddGoal(GoalSource, inspect::CanonicalState<I, Goal<I, I::Predicate>>),
+    AddGoal(GoalSource, inspect::CanonicalState<I, Goal<I, Predicate<I>>>),
     NestedProbe(WipProbe<I>),
     MakeCanonicalResponse { shallow_certainty: Certainty },
     RecordImplArgs { impl_args: inspect::CanonicalState<I, I::GenericArgs> },
@@ -232,7 +233,7 @@ impl<D: SolverDelegate<Interner = I>, I: Interner> EvaluationStepBuilder<D> {
         delegate: &D,
         max_input_universe: ty::UniverseIndex,
         source: GoalSource,
-        goal: Goal<I, I::Predicate>,
+        goal: Goal<I, Predicate<I>>,
     ) {
         if let Some(this) = self.as_mut() {
             let goal = canonical::make_canonical_state(
diff --git a/compiler/rustc_next_trait_solver/src/solve/mod.rs b/compiler/rustc_next_trait_solver/src/solve/mod.rs
index c9da77eced6d3..b452ef0f05cc2 100644
--- a/compiler/rustc_next_trait_solver/src/solve/mod.rs
+++ b/compiler/rustc_next_trait_solver/src/solve/mod.rs
@@ -23,6 +23,7 @@ mod trait_goals;
 use derive_where::derive_where;
 use rustc_type_ir::inherent::*;
 use rustc_type_ir::lang_items::SolverTraitLangItem;
+use rustc_type_ir::predicates::Predicate;
 pub use rustc_type_ir::solve::*;
 use rustc_type_ir::transmute::Condition;
 use rustc_type_ir::{self as ty, Const, Interner, Region, TraitClause, TypeVisitableExt, Upcast};
@@ -487,7 +488,7 @@ pub struct GoalEvaluation<I: Interner> {
     /// `Vec<?y>: Trait`. If this goal is still ambiguous and we later resolve `?y` to `u32`,
     /// then reevaluating this goal now only needs to resolve `?y` while it would otherwise
     /// have to resolve both `?x` and `?y`,
-    pub goal: Goal<I, I::Predicate>,
+    pub goal: Goal<I, Predicate<I>>,
     pub certainty: Certainty,
     pub has_changed: HasChanged,
     /// If the [`Certainty`] was `Maybe`, then keep track of whether the goal has changed
@@ -501,7 +502,7 @@ pub fn flatten_answer_tree<I: Interner>(
     interner: I,
     predicate: TraitClause<I>,
     cond: Condition<Region<I>, I::Ty>,
-) -> ThinVec<I::Predicate> {
+) -> ThinVec<Predicate<I>> {
     match cond {
         // FIXME(bryangarza): Add separate `IfAny` case, instead of treating as `IfAll`
         // Not possible until the trait solver supports disjunctions of obligations
@@ -519,7 +520,7 @@ pub fn flatten_answer_tree<I: Interner>(
         }
         Condition::Outlives { long, short } => {
             let outlives = ty::OutlivesClause(long, short);
-            thin_vec![outlives.upcast(interner)]
+            thin_vec![ty::ClauseKind::RegionOutlives(outlives).upcast(interner)]
         }
         Condition::Transmutable { src, dst } => {
             let transmute_trait = predicate.def_id();
diff --git a/compiler/rustc_next_trait_solver/src/solve/normalizes_to.rs b/compiler/rustc_next_trait_solver/src/solve/normalizes_to.rs
index f8c4597dce654..1128d8c2d5e64 100644
--- a/compiler/rustc_next_trait_solver/src/solve/normalizes_to.rs
+++ b/compiler/rustc_next_trait_solver/src/solve/normalizes_to.rs
@@ -224,7 +224,7 @@ where
             cx.own_clauses_of(goal.predicate.alias.expect_projection_def_id().into())
                 .iter_instantiated(cx, goal.predicate.alias.args)
                 .map(Unnormalized::skip_norm_wip)
-                .map(|clause| goal.with(cx, clause)),
+                .map(|clause| goal.with(cx, clause.as_predicate())),
         )?;
 
         then(ecx)
@@ -293,7 +293,7 @@ where
                 .clauses_of(impl_def_id.into())
                 .iter_instantiated(cx, impl_args)
                 .map(Unnormalized::skip_norm_wip)
-                .map(|clause| goal.with(cx, clause));
+                .map(|clause| goal.with(cx, clause.as_predicate()));
             ecx.add_goals(GoalSource::ImplWhereBound, where_clause_bounds)?;
 
             // Bail if the nested goals don't hold here. This is to avoid unnecessarily
@@ -310,7 +310,7 @@ where
                 cx.own_clauses_of(alias_def_id.into())
                     .iter_instantiated(cx, goal.predicate.alias.args)
                     .map(Unnormalized::skip_norm_wip)
-                    .map(|clause| goal.with(cx, clause)),
+                    .map(|clause| goal.with(cx, clause.as_predicate())),
             )?;
 
             let error_response = |ecx: &mut EvalCtxt<'_, D>, guar| {
@@ -1126,7 +1126,7 @@ where
                 cx.clauses_of(target_container_def_id)
                     .iter_instantiated(cx, target_args)
                     .map(Unnormalized::skip_norm_wip)
-                    .map(|clause| goal.with(cx, clause)),
+                    .map(|clause| goal.with(cx, clause.as_predicate())),
             )?;
             goal.predicate.alias.args.rebase_onto(cx, impl_trait_ref.def_id.into(), target_args)
         })
diff --git a/compiler/rustc_next_trait_solver/src/solve/project_goals/free_alias.rs b/compiler/rustc_next_trait_solver/src/solve/project_goals/free_alias.rs
index dfcc89b91a4f2..9010c1e7f29be 100644
--- a/compiler/rustc_next_trait_solver/src/solve/project_goals/free_alias.rs
+++ b/compiler/rustc_next_trait_solver/src/solve/project_goals/free_alias.rs
@@ -4,6 +4,7 @@
 //! Since a free alias is never ambiguous, this just computes the `type_of` of
 //! the alias and registers the where-clauses of the type alias.
 
+use rustc_type_ir::inherent::*;
 use rustc_type_ir::solve::QueryResultOrRerunNonErased;
 use rustc_type_ir::{self as ty, Interner, Unnormalized};
 
@@ -28,7 +29,7 @@ where
             cx.clauses_of(free_alias.expect_free_def_id().into())
                 .iter_instantiated(cx, free_alias.args)
                 .map(Unnormalized::skip_norm_wip)
-                .map(|clause| goal.with(cx, clause)),
+                .map(|clause| goal.with(cx, clause.as_predicate())),
         )?;
 
         let actual = match free_alias.kind {
diff --git a/compiler/rustc_next_trait_solver/src/solve/project_goals/inherent.rs b/compiler/rustc_next_trait_solver/src/solve/project_goals/inherent.rs
index 45ece5a0589fb..df40c7678ed4e 100644
--- a/compiler/rustc_next_trait_solver/src/solve/project_goals/inherent.rs
+++ b/compiler/rustc_next_trait_solver/src/solve/project_goals/inherent.rs
@@ -5,6 +5,7 @@
 //! 2. equate the self type, and
 //! 3. instantiate and register where clauses.
 
+use rustc_type_ir::inherent::*;
 use rustc_type_ir::solve::{NoSolutionOrRerunNonErased, QueryResultOrRerunNonErased};
 use rustc_type_ir::{self as ty, Interner, Unnormalized};
 
@@ -39,7 +40,7 @@ where
             cx.clauses_of(def_id.into())
                 .iter_instantiated(cx, inherent_args)
                 .map(Unnormalized::skip_norm_wip)
-                .map(|clause| goal.with(cx, clause)),
+                .map(|clause| goal.with(cx, clause.as_predicate())),
         )?;
 
         let normalized: I::Term = match inherent_kind {
diff --git a/compiler/rustc_next_trait_solver/src/solve/trait_goals.rs b/compiler/rustc_next_trait_solver/src/solve/trait_goals.rs
index 1d3008da399dc..0034b74cf084a 100644
--- a/compiler/rustc_next_trait_solver/src/solve/trait_goals.rs
+++ b/compiler/rustc_next_trait_solver/src/solve/trait_goals.rs
@@ -106,7 +106,7 @@ where
                 .clauses_of(impl_def_id.into())
                 .iter_instantiated(cx, impl_args)
                 .map(Unnormalized::skip_norm_wip)
-                .map(|clause| goal.with(cx, clause));
+                .map(|clause| goal.with(cx, clause.as_predicate()));
             ecx.add_goals(GoalSource::ImplWhereBound, where_clause_bounds)?;
 
             // We currently elaborate all supertrait outlives obligations from impls.
@@ -117,7 +117,7 @@ where
                 cx.impl_super_outlives(impl_def_id)
                     .iter_instantiated(cx, impl_args)
                     .map(Unnormalized::skip_norm_wip)
-                    .map(|pred| goal.with(cx, pred)),
+                    .map(|pred| goal.with(cx, pred.as_predicate())),
             )?;
 
             then(ecx)
@@ -273,7 +273,7 @@ where
                 .clauses_of(goal.predicate.def_id().into())
                 .iter_instantiated(cx, goal.predicate.trait_ref.args)
                 .map(Unnormalized::skip_norm_wip)
-                .map(|c| goal.with(cx, c));
+                .map(|c| goal.with(cx, c.as_predicate()));
             // While you could think of trait aliases to have a single builtin impl
             // which uses its implied trait bounds as where-clauses, using
             // `GoalSource::ImplWhereClause` here would be incorrect, as we also
@@ -901,7 +901,13 @@ where
                     }
                     ecx.add_goal(
                         GoalSource::Misc,
-                        goal.with(cx, ty::OutlivesClause(ty_lifetime, lifetime)),
+                        goal.with(
+                            cx,
+                            ty::ClauseKind::RegionOutlives(ty::OutlivesClause(
+                                ty_lifetime,
+                                lifetime,
+                            )),
+                        ),
                     )?;
                     ecx.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
                 }
@@ -1072,7 +1078,7 @@ where
             // (i.e. the principal, all of the associated types match, and any auto traits)
             ecx.add_goals(
                 GoalSource::ImplWhereBound,
-                b_data.iter().map(|pred| goal.with(cx, pred.with_self_ty(cx, a_ty))),
+                b_data.iter().map(|pred| goal.with(cx, pred.with_self_ty(cx, a_ty).as_predicate())),
             )?;
 
             // The type must be `Sized` to be unsized.
@@ -1089,7 +1095,10 @@ where
             )?;
 
             // The type must outlive the lifetime of the `dyn` we're unsizing into.
-            ecx.add_goal(GoalSource::Misc, goal.with(cx, ty::OutlivesClause(a_ty, b_region)))?;
+            ecx.add_goal(
+                GoalSource::Misc,
+                goal.with(cx, ty::ClauseKind::TypeOutlives(ty::OutlivesClause(a_ty, b_region))),
+            )?;
             ecx.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
         })
     }
@@ -1219,7 +1228,11 @@ where
             // Also require that a_ty's lifetime outlives b_ty's lifetime.
             ecx.add_goal(
                 GoalSource::ImplWhereBound,
-                Goal::new(ecx.cx(), param_env, ty::OutlivesClause(a_region, b_region)),
+                Goal::new(
+                    ecx.cx(),
+                    param_env,
+                    ty::ClauseKind::RegionOutlives(ty::OutlivesClause(a_region, b_region)),
+                ),
             )?;
 
             ecx.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
diff --git a/compiler/rustc_type_ir/src/elaborate.rs b/compiler/rustc_type_ir/src/elaborate.rs
index 2110521eae764..f562c6348b6fe 100644
--- a/compiler/rustc_type_ir/src/elaborate.rs
+++ b/compiler/rustc_type_ir/src/elaborate.rs
@@ -6,6 +6,7 @@ use crate::data_structures::HashSet;
 use crate::inherent::*;
 use crate::lang_items::SolverTraitLangItem;
 use crate::outlives::{Component, push_outlives_components};
+use crate::predicates::Predicate;
 use crate::{self as ty, Interner, Region, Unnormalized, Upcast as _};
 
 /// "Elaboration" is the process of identifying all the predicates that
@@ -35,7 +36,7 @@ enum ElaborateSized {
 
 /// Describes how to elaborate an obligation into a sub-obligation.
 pub trait Elaboratable<I: Interner> {
-    fn predicate(&self) -> I::Predicate;
+    fn predicate(&self) -> Predicate<I>;
 
     // Makes a new `Self` but with a different clause that comes from elaboration.
     fn child(&self, clause: I::Clause) -> Self;
@@ -51,6 +52,26 @@ pub trait Elaboratable<I: Interner> {
     ) -> Self;
 }
 
+impl<I: Interner> Elaboratable<I> for Predicate<I> {
+    fn predicate(&self) -> Self {
+        *self
+    }
+
+    fn child(&self, clause: I::Clause) -> Self {
+        clause.as_predicate()
+    }
+
+    fn child_with_derived_cause(
+        &self,
+        clause: I::Clause,
+        _span: I::Span,
+        _parent_trait_pred: ty::Binder<I, ty::TraitClause<I>>,
+        _index: usize,
+    ) -> Self {
+        clause.as_predicate()
+    }
+}
+
 pub struct ClauseWithSupertraitSpan<I: Interner> {
     pub clause: I::Clause,
     // Span of the supertrait predicate that lead to this clause.
@@ -64,7 +85,7 @@ impl<I: Interner> ClauseWithSupertraitSpan<I> {
 }
 
 impl<I: Interner> Elaboratable<I> for ClauseWithSupertraitSpan<I> {
-    fn predicate(&self) -> <I as Interner>::Predicate {
+    fn predicate(&self) -> Predicate<I> {
         self.clause.as_predicate()
     }
 
diff --git a/compiler/rustc_type_ir/src/inherent.rs b/compiler/rustc_type_ir/src/inherent.rs
index 4fd92194c5d81..15fdcac548e8f 100644
--- a/compiler/rustc_type_ir/src/inherent.rs
+++ b/compiler/rustc_type_ir/src/inherent.rs
@@ -11,13 +11,11 @@ use rustc_ast_ir::Mutability;
 
 use crate::elaborate::Elaboratable;
 use crate::fold::{TypeFoldable, TypeSuperFoldable};
+use crate::predicates::Predicate;
 use crate::relate::Relate;
 use crate::solve::{AdtDestructorKind, SizedTraitKind};
 use crate::visit::{Flags, TypeSuperVisitable, TypeVisitable};
-use crate::{
-    self as ty, ClauseKind, CollectAndApply, Const, FieldInfo, Interner, PredicateKind, Region,
-    UpcastFrom,
-};
+use crate::{self as ty, CollectAndApply, Const, FieldInfo, Interner, Region, UpcastFrom};
 
 #[rust_analyzer::prefer_underscore_import]
 pub trait Ty<I: Interner<Ty = Self>>:
@@ -412,53 +410,6 @@ pub trait GenericArgs<I: Interner<GenericArgs = Self>>:
     }
 }
 
-#[rust_analyzer::prefer_underscore_import]
-pub trait Predicate<I: Interner<Predicate = Self>>:
-    Copy
-    + Debug
-    + Hash
-    + Eq
-    + TypeSuperVisitable<I>
-    + TypeSuperFoldable<I>
-    + Flags
-    + UpcastFrom<I, ty::PredicateKind<I>>
-    + UpcastFrom<I, ty::Binder<I, ty::PredicateKind<I>>>
-    + UpcastFrom<I, ty::ClauseKind<I>>
-    + UpcastFrom<I, ty::Binder<I, ty::ClauseKind<I>>>
-    + UpcastFrom<I, I::Clause>
-    + UpcastFrom<I, ty::NormalizesTo<I>>
-    + UpcastFrom<I, ty::TraitRef<I>>
-    + UpcastFrom<I, ty::Binder<I, ty::TraitRef<I>>>
-    + UpcastFrom<I, ty::TraitClause<I>>
-    + UpcastFrom<I, ty::ProjectionClause<I>>
-    + UpcastFrom<I, ty::OutlivesClause<I, I::Ty>>
-    + UpcastFrom<I, ty::OutlivesClause<I, Region<I>>>
-    + IntoKind<Kind = ty::Binder<I, ty::PredicateKind<I>>>
-    + Elaboratable<I>
-{
-    fn as_clause(self) -> Option<I::Clause>;
-
-    fn allow_normalization(self) -> bool {
-        match self.kind().skip_binder() {
-            PredicateKind::Clause(ClauseKind::WellFormed(_)) => false,
-            PredicateKind::Clause(ClauseKind::Trait(_))
-            | PredicateKind::Clause(ClauseKind::HostEffect(..))
-            | PredicateKind::Clause(ClauseKind::RegionOutlives(_))
-            | PredicateKind::Clause(ClauseKind::TypeOutlives(_))
-            | PredicateKind::Clause(ClauseKind::Projection(_))
-            | PredicateKind::Clause(ClauseKind::ConstArgHasType(..))
-            | PredicateKind::Clause(ClauseKind::UnstableFeature(_))
-            | PredicateKind::DynCompatible(_)
-            | PredicateKind::Subtype(_)
-            | PredicateKind::Coerce(_)
-            | PredicateKind::Clause(ClauseKind::ConstEvaluatable(_))
-            | PredicateKind::ConstEquate(_, _)
-            | PredicateKind::NormalizesTo(..)
-            | PredicateKind::Ambiguous => true,
-        }
-    }
-}
-
 #[rust_analyzer::prefer_underscore_import]
 pub trait Clause<I: Interner<Clause = Self>>:
     Copy
@@ -477,7 +428,7 @@ pub trait Clause<I: Interner<Clause = Self>>:
     + IntoKind<Kind = ty::Binder<I, ty::ClauseKind<I>>>
     + Elaboratable<I>
 {
-    fn as_predicate(self) -> I::Predicate;
+    fn as_predicate(self) -> Predicate<I>;
 
     fn as_type_outlives_clause(self) -> Option<ty::Binder<I, ty::OutlivesClause<I, I::Ty>>> {
         self.kind()
diff --git a/compiler/rustc_type_ir/src/interner.rs b/compiler/rustc_type_ir/src/interner.rs
index 159c2939875b0..08966aed8798e 100644
--- a/compiler/rustc_type_ir/src/interner.rs
+++ b/compiler/rustc_type_ir/src/interner.rs
@@ -19,6 +19,7 @@ use crate::search_graph::RequiredDepth;
 use crate::solve::{
     AccessedOpaques, CanonicalInputData, Certainty, ExternalConstraintsData, QueryResult, inspect,
 };
+use crate::sty::predicates::Predicate as InternedPredicate;
 use crate::visit::{Flags, TypeVisitable};
 use crate::{
     self as ty, AliasTermKind, BoundRegion, BoundVar, CanonicalParamEnvCache, Const, ConstKind,
@@ -245,6 +246,7 @@ pub trait Interner:
 
     type InternedRegionKind: Interned<Self, Value = RegionKind<Self>>;
     type InternedConstKind: Interned<Self, Value = WithCachedTypeInfo<ConstKind<Self>>>;
+    type InternedPredicateKind: Interned<Self, Value = WithCachedTypeInfo<ty::Binder<Self, ty::PredicateKind<Self>>>>;
 
     type RegionAssumptions: Copy
         + Debug
@@ -255,10 +257,14 @@ pub trait Interner:
 
     // Predicates
     type ParamEnv: ParamEnv<Self>;
-    type Predicate: Predicate<Self>;
     type Clause: Clause<Self>;
     type Clauses: Clauses<Self>;
 
+    fn intern_predicate(
+        self,
+        predicate: ty::Binder<Self, ty::PredicateKind<Self>>,
+    ) -> InternedPredicate<Self>;
+
     fn with_global_cache<R>(self, f: impl FnOnce(&mut search_graph::GlobalCache<Self>) -> R) -> R;
 
     fn with_canonical_param_env_cache<R>(
@@ -591,6 +597,7 @@ declare_lift_into! {
     InherentAssocConstId,
     InherentAssocTyId,
     InternedConstKind,
+    InternedPredicateKind,
     InternedRegionKind,
     OpaqueTyId,
     ParamEnv,
diff --git a/compiler/rustc_type_ir/src/ir_print.rs b/compiler/rustc_type_ir/src/ir_print.rs
index 1f588a64bd80d..7595bc3cf244b 100644
--- a/compiler/rustc_type_ir/src/ir_print.rs
+++ b/compiler/rustc_type_ir/src/ir_print.rs
@@ -1,5 +1,6 @@
 use std::fmt;
 
+use crate::predicates::{Clause, Predicate};
 #[cfg(feature = "nightly")]
 use crate::{AliasConst, ClosureKind};
 use crate::{
@@ -64,6 +65,20 @@ where
     }
 }
 
+// Display is implemented where the representation is defined. Each frontend
+// provides the actual formatting through IrPrint.
+impl<I: Interner + IrPrint<Predicate<I>>> fmt::Display for Predicate<I> {
+    fn fmt(&self, fmt: &mut fmt::Formatter<'_>) -> fmt::Result {
+        <I as IrPrint<Self>>::print(self, fmt)
+    }
+}
+
+impl<I: Interner + IrPrint<Clause<I>>> fmt::Display for Clause<I> {
+    fn fmt(&self, fmt: &mut fmt::Formatter<'_>) -> fmt::Result {
+        <I as IrPrint<Self>>::print(self, fmt)
+    }
+}
+
 impl<I: Interner> fmt::Display for Const<I>
 where
     I: IrPrint<Const<I>>,
@@ -100,12 +115,37 @@ where
     }
 }
 
+/// Provides frontend-specific diagnostic formatting for predicates.
+///
+/// The frontend owns the type-printing context and long-type path handling.
+#[cfg(feature = "nightly")]
+pub trait PredicateDiagFormatter: Interner {
+    fn predicate_diag_string(
+        predicate: Predicate<Self>,
+        path: &mut Option<std::path::PathBuf>,
+    ) -> String;
+
+    fn clause_diag_string(clause: Clause<Self>, path: &mut Option<std::path::PathBuf>) -> String;
+}
+
 #[cfg(feature = "nightly")]
 mod into_diag_arg_impls {
     use rustc_error_messages::{DiagArgValue, IntoDiagArg};
 
     use super::*;
 
+    impl<I: PredicateDiagFormatter> IntoDiagArg for Predicate<I> {
+        fn into_diag_arg(self, path: &mut Option<std::path::PathBuf>) -> DiagArgValue {
+            DiagArgValue::Str(I::predicate_diag_string(self, path).into())
+        }
+    }
+
+    impl<I: PredicateDiagFormatter> IntoDiagArg for Clause<I> {
+        fn into_diag_arg(self, path: &mut Option<std::path::PathBuf>) -> DiagArgValue {
+            DiagArgValue::Str(I::clause_diag_string(self, path).into())
+        }
+    }
+
     impl<I: Interner> IntoDiagArg for TraitRef<I> {
         fn into_diag_arg(self, path: &mut Option<std::path::PathBuf>) -> DiagArgValue {
             self.to_string().into_diag_arg(path)
diff --git a/compiler/rustc_type_ir/src/relate/combine.rs b/compiler/rustc_type_ir/src/relate/combine.rs
index 054dff869e650..25dd9d6845138 100644
--- a/compiler/rustc_type_ir/src/relate/combine.rs
+++ b/compiler/rustc_type_ir/src/relate/combine.rs
@@ -7,6 +7,7 @@ use super::{
 };
 use crate::error::TypeError;
 use crate::inherent::*;
+use crate::predicates::Predicate;
 use crate::relate::VarianceDiagInfo;
 use crate::solve::Goal;
 use crate::visit::TypeVisitableExt as _;
@@ -23,13 +24,13 @@ where
     fn param_env(&self) -> I::ParamEnv;
 
     /// Register obligations that must hold in order for this relation to hold
-    fn register_goals(&mut self, obligations: impl IntoIterator<Item = Goal<I, I::Predicate>>);
+    fn register_goals(&mut self, obligations: impl IntoIterator<Item = Goal<I, Predicate<I>>>);
 
     /// Register predicates that must hold in order for this relation to hold.
     /// This uses the default `param_env` of the obligation.
     fn register_predicates(
         &mut self,
-        obligations: impl IntoIterator<Item: Upcast<I, I::Predicate>>,
+        obligations: impl IntoIterator<Item: Upcast<I, Predicate<I>>>,
     );
 }
 
diff --git a/compiler/rustc_type_ir/src/relate/solver_relating.rs b/compiler/rustc_type_ir/src/relate/solver_relating.rs
index 3a7056234553b..018f0ab3d947e 100644
--- a/compiler/rustc_type_ir/src/relate/solver_relating.rs
+++ b/compiler/rustc_type_ir/src/relate/solver_relating.rs
@@ -2,6 +2,7 @@ use tracing::{debug, instrument};
 
 use self::combine::{PredicateEmittingRelation, super_combine_consts, super_combine_tys};
 use crate::data_structures::DelayedSet;
+use crate::predicates::Predicate;
 use crate::relate::combine::combine_ty_args;
 pub use crate::relate::*;
 use crate::solve::{Goal, VisibleForLeakCheck};
@@ -15,10 +16,7 @@ pub trait RelateExt: InferCtxtLike {
         variance: ty::Variance,
         rhs: T,
         span: <Self::Interner as Interner>::Span,
-    ) -> Result<
-        Vec<Goal<Self::Interner, <Self::Interner as Interner>::Predicate>>,
-        TypeError<Self::Interner>,
-    >;
+    ) -> Result<Vec<Goal<Self::Interner, Predicate<Self::Interner>>>, TypeError<Self::Interner>>;
 }
 
 impl<Infcx: InferCtxtLike> RelateExt for Infcx {
@@ -29,10 +27,8 @@ impl<Infcx: InferCtxtLike> RelateExt for Infcx {
         variance: ty::Variance,
         rhs: T,
         span: <Self::Interner as Interner>::Span,
-    ) -> Result<
-        Vec<Goal<Self::Interner, <Self::Interner as Interner>::Predicate>>,
-        TypeError<Self::Interner>,
-    > {
+    ) -> Result<Vec<Goal<Self::Interner, Predicate<Self::Interner>>>, TypeError<Self::Interner>>
+    {
         let mut relate = SolverRelating::new(self, variance, param_env, span);
         relate.relate(lhs, rhs)?;
         Ok(relate.goals)
@@ -47,7 +43,7 @@ pub struct SolverRelating<'infcx, Infcx, I: Interner> {
     span: I::Span,
     // Mutable fields.
     ambient_variance: ty::Variance,
-    goals: Vec<Goal<I, I::Predicate>>,
+    goals: Vec<Goal<I, Predicate<I>>>,
     /// The cache only tracks the `ambient_variance` as it's the
     /// only field which is mutable and which meaningfully changes
     /// the result when relating types.
@@ -353,14 +349,14 @@ where
 
     fn register_predicates(
         &mut self,
-        obligations: impl IntoIterator<Item: ty::Upcast<I, I::Predicate>>,
+        obligations: impl IntoIterator<Item: ty::Upcast<I, Predicate<I>>>,
     ) {
         self.goals.extend(
             obligations.into_iter().map(|pred| Goal::new(self.infcx.cx(), self.param_env, pred)),
         );
     }
 
-    fn register_goals(&mut self, obligations: impl IntoIterator<Item = Goal<I, I::Predicate>>) {
+    fn register_goals(&mut self, obligations: impl IntoIterator<Item = Goal<I, Predicate<I>>>) {
         self.goals.extend(obligations);
     }
 }
diff --git a/compiler/rustc_type_ir/src/serialize.rs b/compiler/rustc_type_ir/src/serialize.rs
index eae1d05b7e8e7..ef4840b273bed 100644
--- a/compiler/rustc_type_ir/src/serialize.rs
+++ b/compiler/rustc_type_ir/src/serialize.rs
@@ -1,6 +1,7 @@
 use rustc_serialize::{Decodable, Decoder, Encodable, Encoder};
 
 use crate::inherent::*;
+use crate::predicates::{Clause, Predicate};
 use crate::visit::TypeVisitable;
 use crate::{self as ty, Const, ConstKind, Interner, Region, RegionKind, UnsafeBinderInner};
 
@@ -15,6 +16,8 @@ pub trait InternerDecoder: Decoder {
     type Interner: Interner;
 
     fn interner(&self) -> Self::Interner;
+
+    fn decode_predicate(&mut self) -> Predicate<Self::Interner>;
 }
 
 macro_rules! impl_binder_encode_decode {
@@ -135,3 +138,34 @@ where
         Const::new(decoder.interner(), Decodable::decode(decoder))
     }
 }
+
+/// Encodes a shared predicate using the frontend's existing representation.
+///
+/// Rustc uses predicate shorthands for metadata and incremental caches.
+pub trait PredicateEncoder<I: Interner>: Encoder {
+    fn encode_predicate(&mut self, predicate: Predicate<I>);
+}
+
+impl<I: Interner, E: PredicateEncoder<I>> Encodable<E> for Predicate<I> {
+    fn encode(&self, encoder: &mut E) {
+        encoder.encode_predicate(*self);
+    }
+}
+
+impl<I: Interner, D: InternerDecoder<Interner = I>> Decodable<D> for Predicate<I> {
+    fn decode(decoder: &mut D) -> Self {
+        decoder.decode_predicate()
+    }
+}
+
+impl<I: Interner, E: PredicateEncoder<I>> Encodable<E> for Clause<I> {
+    fn encode(&self, encoder: &mut E) {
+        self.as_predicate().encode(encoder);
+    }
+}
+
+impl<I: Interner, D: InternerDecoder<Interner = I>> Decodable<D> for Clause<I> {
+    fn decode(decoder: &mut D) -> Self {
+        Predicate::decode(decoder).expect_clause()
+    }
+}
diff --git a/compiler/rustc_type_ir/src/solve/inspect.rs b/compiler/rustc_type_ir/src/solve/inspect.rs
index 610bb2389ddf4..9c56498656e75 100644
--- a/compiler/rustc_type_ir/src/solve/inspect.rs
+++ b/compiler/rustc_type_ir/src/solve/inspect.rs
@@ -21,6 +21,7 @@ use derive_where::derive_where;
 use rustc_type_ir_macros::{GenericTypeVisitable, TypeFoldable_Generic, TypeVisitable_Generic};
 use thin_vec::ThinVec;
 
+use crate::predicates::Predicate;
 use crate::search_graph::RequiredDepth;
 use crate::solve::{CandidateSource, Certainty, Goal, GoalSource, QueryResult};
 use crate::{Canonical, Interner};
@@ -49,7 +50,7 @@ pub type CanonicalState<I, T> = Canonical<I, State<I, T>>;
 /// of the solver query to the `InferCtxt` of the caller.
 #[derive_where(PartialEq, Eq, Hash; I: Interner)]
 pub struct GoalEvaluation<I: Interner> {
-    pub uncanonicalized_goal: Goal<I, I::Predicate>,
+    pub uncanonicalized_goal: Goal<I, Predicate<I>>,
     pub orig_values: ThinVec<I::GenericArg>,
     pub final_revision: I::Probe,
     pub result: QueryResult<I>,
@@ -71,7 +72,7 @@ pub struct Probe<I: Interner> {
 pub enum ProbeStep<I: Interner> {
     /// We added a goal to the `EvalCtxt` which will get proven
     /// the next time `EvalCtxt::try_evaluate_added_goals` is called.
-    AddGoal(GoalSource, CanonicalState<I, Goal<I, I::Predicate>>),
+    AddGoal(GoalSource, CanonicalState<I, Goal<I, Predicate<I>>>),
     /// A call to `probe` while proving the current goal. This is
     /// used whenever there are multiple candidates to prove the
     /// current goal.
diff --git a/compiler/rustc_type_ir/src/solve/mod.rs b/compiler/rustc_type_ir/src/solve/mod.rs
index 55fb628e1ee3e..8434392a9f20e 100644
--- a/compiler/rustc_type_ir/src/solve/mod.rs
+++ b/compiler/rustc_type_ir/src/solve/mod.rs
@@ -15,14 +15,14 @@ use tracing::debug;
 
 use crate::inherent::*;
 use crate::lang_items::SolverTraitLangItem;
+use crate::predicates::Predicate;
 use crate::region_constraint::RegionConstraint;
 use crate::{
     self as ty, Canonical, CantBeErased, Const, ConstVid, FloatVid, GenericArgKind, InferConst,
     IntVid, Interner, TermKind, TyVid, TypingMode, Upcast,
 };
 
-pub type CanonicalInputData<I> =
-    ty::CanonicalQueryInput<I, QueryInput<I, <I as Interner>::Predicate>>;
+pub type CanonicalInputData<I> = ty::CanonicalQueryInput<I, QueryInput<I, Predicate<I>>>;
 pub type CanonicalResponse<I> = Canonical<I, Response<I>>;
 /// The result of evaluating a canonical query.
 ///
@@ -746,7 +746,7 @@ impl VisibleForLeakCheck {
 #[derive_where(Clone, Hash, PartialEq, Debug, Default; I: Interner)]
 #[derive(TypeVisitable_Generic, GenericTypeVisitable, TypeFoldable_Generic)]
 #[cfg_attr(feature = "nightly", derive(StableHash_NoContext))]
-pub struct NestedNormalizationGoals<I: Interner>(pub Vec<(GoalSource, Goal<I, I::Predicate>)>);
+pub struct NestedNormalizationGoals<I: Interner>(pub Vec<(GoalSource, Goal<I, Predicate<I>>)>);
 
 impl<I: Interner> Eq for NestedNormalizationGoals<I> {}
 
diff --git a/compiler/rustc_type_ir/src/sty/mod.rs b/compiler/rustc_type_ir/src/sty/mod.rs
index d513dd88faae6..1553d013972b7 100644
--- a/compiler/rustc_type_ir/src/sty/mod.rs
+++ b/compiler/rustc_type_ir/src/sty/mod.rs
@@ -1,5 +1,6 @@
 pub use consts::*;
 mod consts;
+pub mod predicates;
 
 use std::fmt;
 
diff --git a/compiler/rustc_type_ir/src/sty/predicates.rs b/compiler/rustc_type_ir/src/sty/predicates.rs
new file mode 100644
index 0000000000000..26458c66b314c
--- /dev/null
+++ b/compiler/rustc_type_ir/src/sty/predicates.rs
@@ -0,0 +1,537 @@
+use std::fmt;
+
+use derive_where::derive_where;
+#[cfg(feature = "nightly")]
+use rustc_macros::StableHash_NoContext;
+use rustc_type_ir_macros::{GenericTypeVisitable, Lift_Generic};
+
+use crate::inherent::*;
+use crate::intern::Interned as _;
+use crate::{
+    Binder, ClauseKind, DebruijnIndex, EarlyBinder, FallibleTypeFolder, Flags, HostEffectClause,
+    Interner, NormalizesTo, OutlivesClause, PredicateKind, PredicateProxy, ProjectionClause,
+    Region, TraitClause, TraitRef, TypeFlags, TypeFoldable, TypeFolder, TypeSuperFoldable,
+    TypeSuperVisitable, TypeVisitable, TypeVisitor, Upcast, UpcastFrom, shift_bound_var_indices,
+};
+
+/// A statement that can be proven by a trait solver.
+///
+/// This is the interner-generic representation of a predicate. The interned
+/// representation also stores cached type flags and binder information.
+#[derive_where(Clone, Copy, PartialEq, Eq, Hash; I: Interner)]
+#[cfg_attr(feature = "nightly", derive(StableHash_NoContext))]
+#[cfg_attr(feature = "nightly", rustc_pass_by_value)]
+#[derive(GenericTypeVisitable, Lift_Generic)]
+pub struct Predicate<I: Interner>(pub I::InternedPredicateKind);
+
+impl<I: Interner> Predicate<I> {
+    #[inline]
+    pub fn new(interner: I, kind: Binder<I, PredicateKind<I>>) -> Self {
+        interner.intern_predicate(kind)
+    }
+
+    #[inline]
+    pub fn kind(self) -> Binder<I, PredicateKind<I>> {
+        self.0.get().internee
+    }
+
+    /// Matches a `PredicateKind::Clause` and turns it into a `Clause`.
+    #[inline]
+    pub fn as_clause(self) -> Option<Clause<I>> {
+        match self.kind().skip_binder() {
+            PredicateKind::Clause(_) => Some(Clause(self)),
+            _ => None,
+        }
+    }
+
+    /// Assert that this predicate is a clause.
+    #[inline]
+    pub fn expect_clause(self) -> Clause<I> {
+        match self.as_clause() {
+            Some(clause) => clause,
+            None => panic!("{self:?} is not a clause"),
+        }
+    }
+
+    /// Flips the polarity of a trait predicate.
+    ///
+    /// Given `T: Trait`, returns `T: !Trait`, and vice versa.
+    pub fn flip_polarity(self, interner: I) -> Option<Self> {
+        let kind = self
+            .kind()
+            .map_bound(|kind| match kind {
+                PredicateKind::Clause(ClauseKind::Trait(TraitClause { trait_ref, polarity })) => {
+                    Some(PredicateKind::Clause(ClauseKind::Trait(TraitClause {
+                        trait_ref,
+                        polarity: polarity.flip(),
+                    })))
+                }
+
+                _ => None,
+            })
+            .transpose()?;
+
+        Some(Self::new(interner, kind))
+    }
+
+    pub fn as_trait_clause(self) -> Option<Binder<I, TraitClause<I>>> {
+        let predicate = self.kind();
+        match predicate.skip_binder() {
+            PredicateKind::Clause(ClauseKind::Trait(trait_clause)) => {
+                Some(predicate.rebind(trait_clause))
+            }
+            _ => None,
+        }
+    }
+
+    pub fn as_projection_clause(self) -> Option<Binder<I, ProjectionClause<I>>> {
+        let predicate = self.kind();
+        match predicate.skip_binder() {
+            PredicateKind::Clause(ClauseKind::Projection(projection_clause)) => {
+                Some(predicate.rebind(projection_clause))
+            }
+            _ => None,
+        }
+    }
+
+    /// Whether this predicate can be soundly normalized.
+    #[inline]
+    pub fn allow_normalization(self) -> bool {
+        match self.kind().skip_binder() {
+            PredicateKind::Clause(ClauseKind::WellFormed(_)) => false,
+
+            PredicateKind::Clause(ClauseKind::Trait(_))
+            | PredicateKind::Clause(ClauseKind::HostEffect(..))
+            | PredicateKind::Clause(ClauseKind::RegionOutlives(_))
+            | PredicateKind::Clause(ClauseKind::TypeOutlives(_))
+            | PredicateKind::Clause(ClauseKind::Projection(_))
+            | PredicateKind::Clause(ClauseKind::ConstArgHasType(..))
+            | PredicateKind::Clause(ClauseKind::UnstableFeature(_))
+            | PredicateKind::DynCompatible(_)
+            | PredicateKind::Subtype(_)
+            | PredicateKind::Coerce(_)
+            | PredicateKind::Clause(ClauseKind::ConstEvaluatable(_))
+            | PredicateKind::ConstEquate(_, _)
+            | PredicateKind::NormalizesTo(..)
+            | PredicateKind::Ambiguous => true,
+        }
+    }
+}
+
+impl<I: Interner> fmt::Debug for Predicate<I> {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        self.kind().fmt(f)
+    }
+}
+
+impl<I: Interner> Flags for Predicate<I> {
+    #[inline]
+    fn flags(&self) -> TypeFlags {
+        self.0.get().flags
+    }
+
+    #[inline]
+    fn outer_exclusive_binder(&self) -> DebruijnIndex {
+        self.0.get().outer_exclusive_binder
+    }
+}
+
+impl<I: Interner> IntoKind for Predicate<I> {
+    type Kind = Binder<I, PredicateKind<I>>;
+
+    #[inline]
+    fn kind(self) -> Self::Kind {
+        self.kind()
+    }
+}
+
+/// A predicate which can be assumed by the trait solver.
+///
+/// `Clause` deliberately shares the same interned representation as
+/// `Predicate`; construction is restricted to predicates whose kind is
+/// `PredicateKind::Clause`.
+#[derive_where(Clone, Copy, PartialEq, Eq, Hash; I: Interner)]
+#[cfg_attr(feature = "nightly", derive(StableHash_NoContext))]
+#[cfg_attr(feature = "nightly", rustc_pass_by_value)]
+#[derive(GenericTypeVisitable, Lift_Generic)]
+pub struct Clause<I: Interner>(Predicate<I>);
+
+impl<I: Interner> Clause<I> {
+    #[inline]
+    pub fn as_predicate(self) -> Predicate<I> {
+        self.0
+    }
+
+    #[inline]
+    pub fn kind(self) -> Binder<I, ClauseKind<I>> {
+        #[cold]
+        #[inline(never)]
+        fn unreachable_inner() -> ! {
+            unreachable!()
+        }
+
+        self.0.kind().map_bound_no_validate_bound_vars(|kind| match kind {
+            PredicateKind::Clause(clause) => clause,
+            _ => unreachable_inner(),
+        })
+    }
+
+    pub fn as_trait_clause(self) -> Option<Binder<I, TraitClause<I>>> {
+        let clause = self.kind();
+        if let ClauseKind::Trait(trait_clause) = clause.skip_binder() {
+            Some(clause.rebind(trait_clause))
+        } else {
+            None
+        }
+    }
+
+    pub fn as_projection_clause(self) -> Option<Binder<I, ProjectionClause<I>>> {
+        let clause = self.kind();
+        if let ClauseKind::Projection(projection_clause) = clause.skip_binder() {
+            Some(clause.rebind(projection_clause))
+        } else {
+            None
+        }
+    }
+
+    pub fn as_type_outlives_clause(self) -> Option<Binder<I, OutlivesClause<I, I::Ty>>> {
+        let clause = self.kind();
+        if let ClauseKind::TypeOutlives(outlives) = clause.skip_binder() {
+            Some(clause.rebind(outlives))
+        } else {
+            None
+        }
+    }
+
+    pub fn as_region_outlives_clause(self) -> Option<Binder<I, OutlivesClause<I, Region<I>>>> {
+        let clause = self.kind();
+        if let ClauseKind::RegionOutlives(outlives) = clause.skip_binder() {
+            Some(clause.rebind(outlives))
+        } else {
+            None
+        }
+    }
+
+    pub fn as_host_effect_clause(self) -> Option<Binder<I, HostEffectClause<I>>> {
+        let clause = self.kind();
+        if let ClauseKind::HostEffect(host_effect) = clause.skip_binder() {
+            Some(clause.rebind(host_effect))
+        } else {
+            None
+        }
+    }
+}
+
+impl<I: Interner> fmt::Debug for Clause<I> {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        self.kind().fmt(f)
+    }
+}
+
+impl<I: Interner> Flags for Clause<I> {
+    #[inline]
+    fn flags(&self) -> TypeFlags {
+        self.0.flags()
+    }
+
+    #[inline]
+    fn outer_exclusive_binder(&self) -> DebruijnIndex {
+        self.0.outer_exclusive_binder()
+    }
+}
+
+impl<I: Interner> IntoKind for Clause<I> {
+    type Kind = Binder<I, ClauseKind<I>>;
+
+    #[inline]
+    fn kind(self) -> Self::Kind {
+        self.kind()
+    }
+}
+
+impl<I: Interner> UpcastFrom<I, PredicateKind<I>> for Predicate<I> {
+    fn upcast_from(from: PredicateKind<I>, interner: I) -> Self {
+        Self::new(interner, Binder::dummy(from))
+    }
+}
+
+impl<I: Interner> UpcastFrom<I, Binder<I, PredicateKind<I>>> for Predicate<I> {
+    fn upcast_from(from: Binder<I, PredicateKind<I>>, interner: I) -> Self {
+        Self::new(interner, from)
+    }
+}
+
+impl<I: Interner> UpcastFrom<I, ClauseKind<I>> for Predicate<I> {
+    fn upcast_from(from: ClauseKind<I>, interner: I) -> Self {
+        Self::new(interner, Binder::dummy(PredicateKind::Clause(from)))
+    }
+}
+
+impl<I: Interner> UpcastFrom<I, Binder<I, ClauseKind<I>>> for Predicate<I> {
+    fn upcast_from(from: Binder<I, ClauseKind<I>>, interner: I) -> Self {
+        Self::new(interner, from.map_bound(PredicateKind::Clause))
+    }
+}
+
+impl<I: Interner> UpcastFrom<I, Clause<I>> for Predicate<I> {
+    fn upcast_from(from: Clause<I>, _interner: I) -> Self {
+        from.as_predicate()
+    }
+}
+
+impl<I: Interner> UpcastFrom<I, ClauseKind<I>> for Clause<I> {
+    fn upcast_from(from: ClauseKind<I>, interner: I) -> Self {
+        Predicate::new(interner, Binder::dummy(PredicateKind::Clause(from))).expect_clause()
+    }
+}
+
+impl<I: Interner> UpcastFrom<I, Binder<I, ClauseKind<I>>> for Clause<I> {
+    fn upcast_from(from: Binder<I, ClauseKind<I>>, interner: I) -> Self {
+        Predicate::new(interner, from.map_bound(PredicateKind::Clause)).expect_clause()
+    }
+}
+
+impl<I: Interner> UpcastFrom<I, TraitRef<I>> for Predicate<I> {
+    fn upcast_from(from: TraitRef<I>, interner: I) -> Self {
+        let trait_clause: TraitClause<I> = from.upcast(interner);
+        PredicateKind::Clause(ClauseKind::Trait(trait_clause)).upcast(interner)
+    }
+}
+
+impl<I: Interner> UpcastFrom<I, TraitRef<I>> for Clause<I> {
+    fn upcast_from(from: TraitRef<I>, interner: I) -> Self {
+        let predicate: Predicate<I> = from.upcast(interner);
+        predicate.expect_clause()
+    }
+}
+
+impl<I: Interner> UpcastFrom<I, Binder<I, TraitRef<I>>> for Predicate<I> {
+    fn upcast_from(from: Binder<I, TraitRef<I>>, interner: I) -> Self {
+        let trait_clause: Binder<I, TraitClause<I>> = from.upcast(interner);
+        trait_clause.upcast(interner)
+    }
+}
+
+impl<I: Interner> UpcastFrom<I, Binder<I, TraitRef<I>>> for Clause<I> {
+    fn upcast_from(from: Binder<I, TraitRef<I>>, interner: I) -> Self {
+        let predicate: Predicate<I> = from.upcast(interner);
+        predicate.expect_clause()
+    }
+}
+
+impl<I: Interner> UpcastFrom<I, TraitClause<I>> for Predicate<I> {
+    fn upcast_from(from: TraitClause<I>, interner: I) -> Self {
+        PredicateKind::Clause(ClauseKind::Trait(from)).upcast(interner)
+    }
+}
+
+impl<I: Interner> UpcastFrom<I, Binder<I, TraitClause<I>>> for Predicate<I> {
+    fn upcast_from(from: Binder<I, TraitClause<I>>, interner: I) -> Self {
+        from.map_bound_no_validate_bound_vars(|trait_clause| {
+            PredicateKind::Clause(ClauseKind::Trait(trait_clause))
+        })
+        .upcast(interner)
+    }
+}
+
+impl<I: Interner> UpcastFrom<I, TraitClause<I>> for Clause<I> {
+    fn upcast_from(from: TraitClause<I>, interner: I) -> Self {
+        let predicate: Predicate<I> = from.upcast(interner);
+        predicate.expect_clause()
+    }
+}
+
+impl<I: Interner> UpcastFrom<I, Binder<I, TraitClause<I>>> for Clause<I> {
+    fn upcast_from(from: Binder<I, TraitClause<I>>, interner: I) -> Self {
+        let predicate: Predicate<I> = from.upcast(interner);
+        predicate.expect_clause()
+    }
+}
+
+impl<I: Interner> UpcastFrom<I, ProjectionClause<I>> for Predicate<I> {
+    fn upcast_from(from: ProjectionClause<I>, interner: I) -> Self {
+        PredicateKind::Clause(ClauseKind::Projection(from)).upcast(interner)
+    }
+}
+
+impl<I: Interner> UpcastFrom<I, Binder<I, ProjectionClause<I>>> for Predicate<I> {
+    fn upcast_from(from: Binder<I, ProjectionClause<I>>, interner: I) -> Self {
+        from.map_bound(|projection| PredicateKind::Clause(ClauseKind::Projection(projection)))
+            .upcast(interner)
+    }
+}
+
+impl<I: Interner> UpcastFrom<I, ProjectionClause<I>> for Clause<I> {
+    fn upcast_from(from: ProjectionClause<I>, interner: I) -> Self {
+        let predicate: Predicate<I> = from.upcast(interner);
+        predicate.expect_clause()
+    }
+}
+
+impl<I: Interner> UpcastFrom<I, Binder<I, ProjectionClause<I>>> for Clause<I> {
+    fn upcast_from(from: Binder<I, ProjectionClause<I>>, interner: I) -> Self {
+        let predicate: Predicate<I> = from.upcast(interner);
+        predicate.expect_clause()
+    }
+}
+
+impl<I: Interner> UpcastFrom<I, Binder<I, HostEffectClause<I>>> for Predicate<I> {
+    fn upcast_from(from: Binder<I, HostEffectClause<I>>, interner: I) -> Self {
+        from.map_bound(ClauseKind::HostEffect).upcast(interner)
+    }
+}
+
+impl<I: Interner> UpcastFrom<I, Binder<I, HostEffectClause<I>>> for Clause<I> {
+    fn upcast_from(from: Binder<I, HostEffectClause<I>>, interner: I) -> Self {
+        let predicate: Predicate<I> = from.map_bound(ClauseKind::HostEffect).upcast(interner);
+        predicate.expect_clause()
+    }
+}
+
+impl<I: Interner> UpcastFrom<I, NormalizesTo<I>> for Predicate<I> {
+    fn upcast_from(from: NormalizesTo<I>, interner: I) -> Self {
+        PredicateKind::NormalizesTo(from).upcast(interner)
+    }
+}
+
+impl<I: Interner> TypeFoldable<I> for Predicate<I> {
+    fn try_fold_with<F: FallibleTypeFolder<I>>(self, folder: &mut F) -> Result<Self, F::Error> {
+        folder.try_fold_predicate(self)
+    }
+
+    fn fold_with<F: TypeFolder<I>>(self, folder: &mut F) -> Self {
+        folder.fold_predicate(self)
+    }
+}
+
+impl<I: Interner> TypeVisitable<I> for Predicate<I> {
+    fn visit_with<V: TypeVisitor<I>>(&self, visitor: &mut V) -> V::Result {
+        visitor.visit_predicate(*self)
+    }
+}
+
+impl<I: Interner> TypeSuperFoldable<I> for Predicate<I> {
+    fn try_super_fold_with<F: FallibleTypeFolder<I>>(
+        self,
+        folder: &mut F,
+    ) -> Result<Self, F::Error> {
+        let new = self.kind().try_fold_with(folder)?;
+
+        if new == self.kind() { Ok(self) } else { Ok(Self::new(folder.cx(), new)) }
+    }
+
+    fn super_fold_with<F: TypeFolder<I>>(self, folder: &mut F) -> Self {
+        let new = self.kind().fold_with(folder);
+
+        if new == self.kind() { self } else { Self::new(folder.cx(), new) }
+    }
+}
+
+impl<I: Interner> TypeSuperVisitable<I> for Predicate<I> {
+    fn super_visit_with<V: TypeVisitor<I>>(&self, visitor: &mut V) -> V::Result {
+        self.kind().visit_with(visitor)
+    }
+}
+
+impl<I: Interner> PredicateProxy<I> for Predicate<I> {
+    fn allow_normalization(&self) -> bool {
+        (*self).allow_normalization()
+    }
+
+    fn clause_kind_unchecked(&self) -> Option<Binder<I, ClauseKind<I>>> {
+        self.as_clause().map(Clause::kind)
+    }
+
+    fn map_projection(
+        self,
+        cx: I,
+        f: impl FnOnce(Binder<I, ProjectionClause<I>>) -> Binder<I, ProjectionClause<I>>,
+    ) -> Option<Self> {
+        self.as_projection_clause().map(|projection| f(projection).upcast(cx))
+    }
+}
+
+impl<I: Interner> TypeFoldable<I> for Clause<I> {
+    fn try_fold_with<F: FallibleTypeFolder<I>>(self, folder: &mut F) -> Result<Self, F::Error> {
+        folder.try_fold_predicate(self)
+    }
+
+    fn fold_with<F: TypeFolder<I>>(self, folder: &mut F) -> Self {
+        folder.fold_predicate(self)
+    }
+}
+
+impl<I: Interner> TypeVisitable<I> for Clause<I> {
+    fn visit_with<V: TypeVisitor<I>>(&self, visitor: &mut V) -> V::Result {
+        visitor.visit_predicate(*self)
+    }
+}
+
+impl<I: Interner> TypeSuperFoldable<I> for Clause<I> {
+    fn try_super_fold_with<F: FallibleTypeFolder<I>>(
+        self,
+        folder: &mut F,
+    ) -> Result<Self, F::Error> {
+        self.as_predicate().try_super_fold_with(folder).map(Predicate::expect_clause)
+    }
+
+    fn super_fold_with<F: TypeFolder<I>>(self, folder: &mut F) -> Self {
+        self.as_predicate().super_fold_with(folder).expect_clause()
+    }
+}
+
+impl<I: Interner> TypeSuperVisitable<I> for Clause<I> {
+    fn super_visit_with<V: TypeVisitor<I>>(&self, visitor: &mut V) -> V::Result {
+        self.as_predicate().super_visit_with(visitor)
+    }
+}
+
+impl<I: Interner> PredicateProxy<I> for Clause<I> {
+    fn allow_normalization(&self) -> bool {
+        self.as_predicate().allow_normalization()
+    }
+
+    fn clause_kind_unchecked(&self) -> Option<Binder<I, ClauseKind<I>>> {
+        Some(self.kind())
+    }
+
+    fn map_projection(
+        self,
+        cx: I,
+        f: impl FnOnce(Binder<I, ProjectionClause<I>>) -> Binder<I, ProjectionClause<I>>,
+    ) -> Option<Self> {
+        self.as_projection_clause().map(|projection| f(projection).upcast(cx))
+    }
+}
+
+impl<I: Interner> Clause<I> {
+    /// Instantiate a supertrait clause using the arguments of `trait_ref`.
+    ///
+    /// Both binders' variables become bound by the resulting binder.
+    /// Shift the supertrait's bound-variable indices before substituting
+    /// the trait arguments, so the two sets of variables do not overlap.
+    pub fn instantiate_supertrait(self, cx: I, trait_ref: Binder<I, TraitRef<I>>) -> Self {
+        let bound_pred = self.kind();
+        let pred_bound_vars = bound_pred.bound_vars();
+        let trait_bound_vars = trait_ref.bound_vars();
+
+        let shifted_pred =
+            shift_bound_var_indices(cx, trait_bound_vars.len(), bound_pred.skip_binder());
+
+        let new = EarlyBinder::bind(cx, shifted_pred)
+            .instantiate(cx, trait_ref.skip_binder().args)
+            .skip_norm_wip();
+
+        let bound_vars =
+            I::BoundVarKinds::from_vars(cx, trait_bound_vars.iter().chain(pred_bound_vars.iter()));
+
+        let new_kind = Binder::bind_with_vars(PredicateKind::Clause(new), bound_vars);
+        let old_predicate = self.as_predicate();
+
+        if old_predicate.kind() == new_kind {
+            self
+        } else {
+            Predicate::new(cx, new_kind).expect_clause()
+        }
+    }
+}
diff --git a/tests/ui-fulldeps/internal-lints/import-of-type-ir-inherent.rs b/tests/ui-fulldeps/internal-lints/import-of-type-ir-inherent.rs
index a26d00b77ac44..27f455c2394fd 100644
--- a/tests/ui-fulldeps/internal-lints/import-of-type-ir-inherent.rs
+++ b/tests/ui-fulldeps/internal-lints/import-of-type-ir-inherent.rs
@@ -9,7 +9,7 @@ use rustc_type_ir::inherent::*;
 //~^ ERROR do not use `rustc_type_ir::inherent` unless you're inside of the trait solver
 use rustc_type_ir::inherent;
 //~^ ERROR do not use `rustc_type_ir::inherent` unless you're inside of the trait solver
-use rustc_type_ir::inherent::Predicate;
+use rustc_type_ir::inherent::Clause;
 //~^ ERROR do not use `rustc_type_ir::inherent` unless you're inside of the trait solver
 
 fn main() {}
diff --git a/tests/ui-fulldeps/internal-lints/import-of-type-ir-inherent.stderr b/tests/ui-fulldeps/internal-lints/import-of-type-ir-inherent.stderr
index 3326b1047ac8a..cf78823cf2dc1 100644
--- a/tests/ui-fulldeps/internal-lints/import-of-type-ir-inherent.stderr
+++ b/tests/ui-fulldeps/internal-lints/import-of-type-ir-inherent.stderr
@@ -22,7 +22,7 @@ LL | use rustc_type_ir::inherent;
 error: do not use `rustc_type_ir::inherent` unless you're inside of the trait solver
   --> $DIR/import-of-type-ir-inherent.rs:12:20
    |
-LL | use rustc_type_ir::inherent::Predicate;
+LL | use rustc_type_ir::inherent::Clause;
    |                    ^^^^^^^^
    |
    = note: the method or struct you're looking for is likely defined somewhere else downstream in the compiler
diff --git a/tests/ui-fulldeps/internal-lints/non_glob_import_of_type_ir_inherent.rs b/tests/ui-fulldeps/internal-lints/non_glob_import_of_type_ir_inherent.rs
index c761b8e94bd7b..f801359942692 100644
--- a/tests/ui-fulldeps/internal-lints/non_glob_import_of_type_ir_inherent.rs
+++ b/tests/ui-fulldeps/internal-lints/non_glob_import_of_type_ir_inherent.rs
@@ -13,7 +13,7 @@ mod ok {
 }
 
 mod direct {
-    use rustc_type_ir::inherent::Predicate; //~ ERROR non-glob import of `rustc_type_ir::inherent`
+    use rustc_type_ir::inherent::Clause; //~ ERROR non-glob import of `rustc_type_ir::inherent`
     use rustc_type_ir::inherent::{AdtDef, Ty};
     //~^ ERROR non-glob import of `rustc_type_ir::inherent`
     //~| ERROR non-glob import of `rustc_type_ir::inherent`
diff --git a/tests/ui-fulldeps/internal-lints/non_glob_import_of_type_ir_inherent.stderr b/tests/ui-fulldeps/internal-lints/non_glob_import_of_type_ir_inherent.stderr
index c5c10bb070a31..344a4079fe6d6 100644
--- a/tests/ui-fulldeps/internal-lints/non_glob_import_of_type_ir_inherent.stderr
+++ b/tests/ui-fulldeps/internal-lints/non_glob_import_of_type_ir_inherent.stderr
@@ -1,8 +1,8 @@
 error: non-glob import of `rustc_type_ir::inherent`
   --> $DIR/non_glob_import_of_type_ir_inherent.rs:16:9
    |
-LL |     use rustc_type_ir::inherent::Predicate;
-   |         ^^^^^^^^^^^^^^^^^^^^^^^^^---------
+LL |     use rustc_type_ir::inherent::Clause;
+   |         ^^^^^^^^^^^^^^^^^^^^^^^^^------
    |                                  |
    |                                  help: try using a glob import instead: `*`
    |