From 81b77688fc69788a3372d85c56497829405fbe53 Mon Sep 17 00:00:00 2001
From: Alexa VanHattum <av111@wellesley.edu>
Date: Wed, 28 Oct 2026 16:15:27 -0400
Subject: [PATCH] Cranelift: ISLE: Clif type terms should be controlling type

Per discussion with cfallin, when a Clif ISLE term has a type (e.g. `(icmp ty x y)`, the type should be the controlling type from the Clif definition (here, the width of `x`/`y`), not the result type (here, `i8`) when they differ. Make this change and update the affected rules.

Note this actually improves GVN due to it previously failing to deduplicate across the version of the instruction that correctly used the controlling type (before the egraph) and the one using the result type (in the egraph).
---
 cranelift/codegen/meta/src/gen_isle.rs        |   7 +
 cranelift/codegen/src/egraph/mod.rs           |  21 +-
 cranelift/codegen/src/opts.rs                 |  11 +-
 cranelift/codegen/src/opts/arithmetic.isle    |  59 +--
 cranelift/codegen/src/opts/bitops.isle        | 102 +++---
 cranelift/codegen/src/opts/cprop.isle         |   9 +-
 cranelift/codegen/src/opts/extends.isle       |  60 +--
 cranelift/codegen/src/opts/icmp.isle          | 346 +++++++++---------
 cranelift/codegen/src/opts/selects.isle       |  80 ++--
 cranelift/codegen/src/opts/spaceship.isle     |   8 +-
 cranelift/codegen/src/opts/vector.isle        |   8 +-
 cranelift/codegen/src/prelude_opt.isle        |  15 +-
 cranelift/codegen/src/spec/inst_specs.isle    |   6 +
 cranelift/codegen/src/spec/opt.isle           |  20 +-
 .../filetests/egraph/arithmetic-precise.clif  |  36 +-
 .../filetests/filetests/egraph/cprop.clif     | 100 ++---
 .../filetests/egraph/icmp-parameterized.clif  | 192 +++++-----
 .../filetests/filetests/egraph/icmp.clif      |   4 +-
 .../filetests/filetests/egraph/spaceship.clif | 164 ++++-----
 19 files changed, 653 insertions(+), 595 deletions(-)

diff --git a/cranelift/codegen/meta/src/gen_isle.rs b/cranelift/codegen/meta/src/gen_isle.rs
index 6518356a719e..b776418181c4 100644
--- a/cranelift/codegen/meta/src/gen_isle.rs
+++ b/cranelift/codegen/meta/src/gen_isle.rs
@@ -240,6 +240,13 @@ fn gen_common_isle(
                 (IsleTarget::Lower, _, _, _) => ("Inst", false, "make_inst", "inst_data_value"),
             };
 
+        if ty_in_decl && isle_target == IsleTarget::Opt {
+            fmt.line(";; The `Type` argument is the instruction's *controlling* type, both");
+            fmt.line(";; when matching and when constructing. For most instructions this is");
+            fmt.line(";; the result type, but not for e.g. comparisons (`icmp`'s controlling");
+            fmt.line(";; type is the operand type; its result is `i8` or a lane-wise mask).");
+            fmt.line(";; Use `(has_type ty ...)` to bind the result type instead.");
+        }
         fmtln!(
             fmt,
             "(decl {} ({}{}) {})",
diff --git a/cranelift/codegen/src/egraph/mod.rs b/cranelift/codegen/src/egraph/mod.rs
index c0e44f21e936..82c9856b8dfa 100644
--- a/cranelift/codegen/src/egraph/mod.rs
+++ b/cranelift/codegen/src/egraph/mod.rs
@@ -175,12 +175,27 @@ pub(crate) enum NewOrExistingInst {
     Existing(Inst),
 }
 
+/// The type paired with an instruction's `InstructionData` throughout the
+/// e-graph: its controlling type variable, or, for a non-polymorphic
+/// instruction that has no controlling type (e.g. `f32const`), the type of its
+/// first result.
+pub(crate) fn inst_ctrl_type(dfg: &DataFlowGraph, inst: Inst) -> Type {
+    let ty = dfg.ctrl_typevar(inst);
+    if ty != crate::ir::types::INVALID {
+        ty
+    } else if let Some(result) = dfg.inst_results(inst).first() {
+        dfg.value_type(*result)
+    } else {
+        ty
+    }
+}
+
 impl NewOrExistingInst {
     fn get_inst_key<'a>(&'a self, dfg: &'a DataFlowGraph) -> (Type, InstructionData) {
         match self {
             NewOrExistingInst::New(data, ty) => (*ty, *data),
             NewOrExistingInst::Existing(inst) => {
-                let ty = dfg.ctrl_typevar(*inst);
+                let ty = inst_ctrl_type(dfg, *inst);
                 (ty, dfg.insts[*inst])
             }
         }
@@ -250,7 +265,7 @@ where
                 NewOrExistingInst::Existing(inst) => {
                     self.stats.pure_inst_insert_orig += 1;
                     let result = self.func.dfg.first_result(inst);
-                    let ty = self.func.dfg.ctrl_typevar(inst);
+                    let ty = inst_ctrl_type(&self.func.dfg, inst);
                     (inst, result, ty)
                 }
             };
@@ -514,7 +529,7 @@ where
             // skeleton (`Layout`), we need to be mindful of whether
             // our current position is dominated by an instance of the
             // instruction. (See #5796 for details.)
-            let ty = self.func.dfg.ctrl_typevar(inst);
+            let ty = inst_ctrl_type(&self.func.dfg, inst);
             match self
                 .gvn_map
                 .entry(&NullCtx, (ty, self.func.dfg.insts[inst]))
diff --git a/cranelift/codegen/src/opts.rs b/cranelift/codegen/src/opts.rs
index 69d3cc19fbf2..0fbd1f09d63c 100644
--- a/cranelift/codegen/src/opts.rs
+++ b/cranelift/codegen/src/opts.rs
@@ -2,7 +2,7 @@
 
 mod div_const;
 
-use crate::egraph::{NewOrExistingInst, OptimizeCtx};
+use crate::egraph::{NewOrExistingInst, OptimizeCtx, inst_ctrl_type};
 pub use crate::ir::condcodes::{FloatCC, IntCC};
 use crate::ir::dfg::ValueDef;
 pub use crate::ir::immediates::{Ieee16, Ieee32, Ieee64, Ieee128, Imm64, Offset32, Uimm8, V128Imm};
@@ -114,8 +114,13 @@ where
                         return None;
                     }
                     ctx.ctx.extractor_fuel -= 1;
-                    let ty = ctx.ctx.func.dfg.value_type(value);
-                    trace!(" -> value of type {}", ty);
+                    // The type we yield is the instruction's controlling
+                    // type, matching what `make_inst` takes when a rule
+                    // constructs an instruction. For most opcodes this is
+                    // the result type, but e.g. `icmp`'s controlling type
+                    // is the operand type while its result is `i8`.
+                    let ty = inst_ctrl_type(&ctx.ctx.func.dfg, inst);
+                    trace!(" -> controlling type {}", ty);
                     return Some((ty, ctx.ctx.func.dfg.insts[inst]));
                 }
                 _ => {}
diff --git a/cranelift/codegen/src/opts/arithmetic.isle b/cranelift/codegen/src/opts/arithmetic.isle
index afa325f9c34d..22207658d574 100644
--- a/cranelift/codegen/src/opts/arithmetic.isle
+++ b/cranelift/codegen/src/opts/arithmetic.isle
@@ -413,10 +413,10 @@
 (rule 1 (cmp_true (ty_vec128 ty)) (iconst_s ty -1))
 
 ;; (x + y) == (y + x) --> true
-(rule (simplify (eq ty (iadd cty x y) (iadd cty y x))) (cmp_true ty))
-(rule (simplify (eq ty (iadd cty y x) (iadd cty x y))) (cmp_true ty))
-(rule (simplify (eq ty (iadd cty x y) (iadd cty x y))) (cmp_true ty))
-(rule (simplify (eq ty (iadd cty y x) (iadd cty y x))) (cmp_true ty))
+(rule (simplify (has_type ty (eq _ (iadd cty x y) (iadd cty y x)))) (cmp_true ty))
+(rule (simplify (has_type ty (eq _ (iadd cty y x) (iadd cty x y)))) (cmp_true ty))
+(rule (simplify (has_type ty (eq _ (iadd cty x y) (iadd cty x y)))) (cmp_true ty))
+(rule (simplify (has_type ty (eq _ (iadd cty y x) (iadd cty y x)))) (cmp_true ty))
 
 ;; (x - y) != x --> y != 0
 (rule (simplify (ne cty (isub ty x y) x)) (ne cty y (all_zero ty)))
@@ -440,24 +440,24 @@
 (rule (simplify (ineg ty (imul ty x (ineg ty y)))) (imul ty x y))
 
 ;; max(x, y) >= x
-(rule (simplify (sge ty (smax ty x y) x)) (cmp_true ty))
-(rule (simplify (sge ty (smax ty y x) x)) (cmp_true ty))
-(rule (simplify (sle ty x (smax ty x y))) (cmp_true ty))
-(rule (simplify (sle ty x (smax ty y x))) (cmp_true ty))
-(rule (simplify (uge ty (umax ty x y) x)) (cmp_true ty))
-(rule (simplify (uge ty (umax ty y x) x)) (cmp_true ty))
-(rule (simplify (ule ty x (umax ty x y))) (cmp_true ty))
-(rule (simplify (ule ty x (umax ty y x))) (cmp_true ty))
+(rule (simplify (has_type bty (sge ty (smax ty x y) x))) (cmp_true bty))
+(rule (simplify (has_type bty (sge ty (smax ty y x) x))) (cmp_true bty))
+(rule (simplify (has_type bty (sle ty x (smax ty x y)))) (cmp_true bty))
+(rule (simplify (has_type bty (sle ty x (smax ty y x)))) (cmp_true bty))
+(rule (simplify (has_type bty (uge ty (umax ty x y) x))) (cmp_true bty))
+(rule (simplify (has_type bty (uge ty (umax ty y x) x))) (cmp_true bty))
+(rule (simplify (has_type bty (ule ty x (umax ty x y)))) (cmp_true bty))
+(rule (simplify (has_type bty (ule ty x (umax ty y x)))) (cmp_true bty))
 
 ;; x >= min(x, y)
-(rule (simplify (sge ty x (smin ty x y))) (cmp_true ty))
-(rule (simplify (sge ty x (smin ty y x))) (cmp_true ty))
-(rule (simplify (sle ty (smin ty x y) x)) (cmp_true ty))
-(rule (simplify (sle ty (smin ty y x) x)) (cmp_true ty))
-(rule (simplify (uge ty x (umin ty x y))) (cmp_true ty))
-(rule (simplify (uge ty x (umin ty y x))) (cmp_true ty))
-(rule (simplify (ule ty (umin ty x y) x)) (cmp_true ty))
-(rule (simplify (ule ty (umin ty y x) x)) (cmp_true ty))
+(rule (simplify (has_type bty (sge ty x (smin ty x y)))) (cmp_true bty))
+(rule (simplify (has_type bty (sge ty x (smin ty y x)))) (cmp_true bty))
+(rule (simplify (has_type bty (sle ty (smin ty x y) x))) (cmp_true bty))
+(rule (simplify (has_type bty (sle ty (smin ty y x) x))) (cmp_true bty))
+(rule (simplify (has_type bty (uge ty x (umin ty x y)))) (cmp_true bty))
+(rule (simplify (has_type bty (uge ty x (umin ty y x)))) (cmp_true bty))
+(rule (simplify (has_type bty (ule ty (umin ty x y) x))) (cmp_true bty))
+(rule (simplify (has_type bty (ule ty (umin ty y x) x))) (cmp_true bty))
 
 ;; min/max(x,x) --> x
 (rule (simplify (umin ty x x)) x)
@@ -586,14 +586,17 @@
 (rule (simplify (umax ty (umin ty x y) (umax ty y x))) (umax ty x y))
 
 ;; x > max(x, y) --> 0
-(rule (simplify (sgt ty x (smax ty x y))) (all_zero ty))
-(rule (simplify (sgt ty x (smax ty y x))) (all_zero ty))
-(rule (simplify (slt ty (smax ty x y) x)) (all_zero ty))
-(rule (simplify (slt ty (smax ty y x) x)) (all_zero ty))
-(rule (simplify (ugt ty x (umax ty x y))) (all_zero ty))
-(rule (simplify (ugt ty x (umax ty y x))) (all_zero ty))
-(rule (simplify (ult ty (umax ty x y) x)) (all_zero ty))
-(rule (simplify (ult ty (umax ty y x) x)) (all_zero ty))
+;;
+;; Note: result type `rty` is an i8 for scalars, which may not be the
+;; same as the controlling type ty.
+(rule (simplify (has_type rty (sgt ty x (smax ty x y)))) (all_zero rty))
+(rule (simplify (has_type rty (sgt ty x (smax ty y x)))) (all_zero rty))
+(rule (simplify (has_type rty (slt ty (smax ty x y) x))) (all_zero rty))
+(rule (simplify (has_type rty (slt ty (smax ty y x) x))) (all_zero rty))
+(rule (simplify (has_type rty (ugt ty x (umax ty x y)))) (all_zero rty))
+(rule (simplify (has_type rty (ugt ty x (umax ty y x)))) (all_zero rty))
+(rule (simplify (has_type rty (ult ty (umax ty x y) x))) (all_zero rty))
+(rule (simplify (has_type rty (ult ty (umax ty y x) x))) (all_zero rty))
 
 ;; (-X) * C = X * (-C)
 (rule imul_ineg_const (simplify (imul (fits_in_64 ty) (ineg ty x) (iconst ty y))) (imul ty x (iconst ty (imm64_neg ty y))))
diff --git a/cranelift/codegen/src/opts/bitops.isle b/cranelift/codegen/src/opts/bitops.isle
index fb54ceec37ec..5230997aa616 100644
--- a/cranelift/codegen/src/opts/bitops.isle
+++ b/cranelift/codegen/src/opts/bitops.isle
@@ -101,7 +101,7 @@
 
 ;; Since icmp is always 0 or 1, bmask is just a negation.
 ;; TODO: Explore whether this makes sense for things needing extension too.
-(rule (simplify (bmask $I8 cmp@(icmp $I8 _ _ _)))
+(rule (simplify (bmask $I8 cmp@(icmp _ _ _ _)))
       (ineg $I8 cmp))
 
 ;; Matches any expressions that preserve "truthiness".
@@ -126,10 +126,10 @@
 (rule (simplify (bmask ty v)) (if-let x (truthy v)) (bmask ty x))
 (rule (simplify (select ty v t f)) (if-let c (truthy v)) (select ty c t f))
 ;; (ne ty (iconst 0) v) is also canonicalized into this form via another rule
-(rule (simplify (ne cty v (all_zero _)))
+(rule (simplify (ne _ v (all_zero _)))
       (if-let c (truthy v))
       (if-let (value_type (ty_int_ref_scalar_64_extract ty)) c)
-      (ne cty c (all_zero ty)))
+      (ne ty c (all_zero ty)))
 
 
 
@@ -343,24 +343,24 @@
 (rule (simplify (bxor ty (bor ty y x) (bnot ty x))) (bor ty x (bnot ty y)))
 
 ; (x < y) | (x > y) --> x != y
-(rule (simplify (bor ty (slt ty x y) (sgt ty x y))) (ne ty x y))
-(rule (simplify (bor ty (sgt ty x y) (slt ty x y))) (ne ty x y))
-(rule (simplify (bor ty (slt ty x y) (slt ty y x))) (ne ty x y))
-(rule (simplify (bor ty (slt ty y x) (slt ty x y))) (ne ty x y))
-(rule (simplify (bor ty (sgt ty y x) (sgt ty x y))) (ne ty x y))
-(rule (simplify (bor ty (sgt ty x y) (sgt ty y x))) (ne ty x y))
-(rule (simplify (bor ty (sgt ty y x) (slt ty y x))) (ne ty x y))
-(rule (simplify (bor ty (slt ty y x) (sgt ty y x))) (ne ty x y))
+(rule (simplify (bor _ (slt ty x y) (sgt ty x y))) (ne ty x y))
+(rule (simplify (bor _ (sgt ty x y) (slt ty x y))) (ne ty x y))
+(rule (simplify (bor _ (slt ty x y) (slt ty y x))) (ne ty x y))
+(rule (simplify (bor _ (slt ty y x) (slt ty x y))) (ne ty x y))
+(rule (simplify (bor _ (sgt ty y x) (sgt ty x y))) (ne ty x y))
+(rule (simplify (bor _ (sgt ty x y) (sgt ty y x))) (ne ty x y))
+(rule (simplify (bor _ (sgt ty y x) (slt ty y x))) (ne ty x y))
+(rule (simplify (bor _ (slt ty y x) (sgt ty y x))) (ne ty x y))
 
 ; (x <_u y) | (x >_u y) --> x != y
-(rule (simplify (bor ty (ult ty x y) (ugt ty x y))) (ne ty x y))
-(rule (simplify (bor ty (ugt ty x y) (ult ty x y))) (ne ty x y))
-(rule (simplify (bor ty (ult ty x y) (ult ty y x))) (ne ty x y))
-(rule (simplify (bor ty (ult ty y x) (ult ty x y))) (ne ty x y))
-(rule (simplify (bor ty (ugt ty y x) (ugt ty x y))) (ne ty x y))
-(rule (simplify (bor ty (ugt ty x y) (ugt ty y x))) (ne ty x y))
-(rule (simplify (bor ty (ugt ty y x) (ult ty y x))) (ne ty x y))
-(rule (simplify (bor ty (ult ty y x) (ugt ty y x))) (ne ty x y))
+(rule (simplify (bor _ (ult ty x y) (ugt ty x y))) (ne ty x y))
+(rule (simplify (bor _ (ugt ty x y) (ult ty x y))) (ne ty x y))
+(rule (simplify (bor _ (ult ty x y) (ult ty y x))) (ne ty x y))
+(rule (simplify (bor _ (ult ty y x) (ult ty x y))) (ne ty x y))
+(rule (simplify (bor _ (ugt ty y x) (ugt ty x y))) (ne ty x y))
+(rule (simplify (bor _ (ugt ty x y) (ugt ty y x))) (ne ty x y))
+(rule (simplify (bor _ (ugt ty y x) (ult ty y x))) (ne ty x y))
+(rule (simplify (bor _ (ult ty y x) (ugt ty y x))) (ne ty x y))
 
 ; ~((~x) & y) --> x | ~y
 (rule (simplify (bnot ty (band ty (bnot ty x) y))) (bor ty x (bnot ty y)))
@@ -371,28 +371,28 @@
 (rule (simplify (bnot ty (bor ty y (bnot ty x)))) (band ty x (bnot ty y)))
 
 ; (x <_u y) | (x == y) --> (x <=_u y)
-(rule (simplify (bor ty (ult ty x y) (eq ty x y))) (ule ty x y))
-(rule (simplify (bor ty (eq ty x y) (ult ty x y))) (ule ty x y))
-(rule (simplify (bor ty (ult ty x y) (eq ty y x))) (ule ty x y))
-(rule (simplify (bor ty (eq ty y x) (ult ty x y))) (ule ty x y))
+(rule (simplify (bor _ (ult ty x y) (eq ty x y))) (ule ty x y))
+(rule (simplify (bor _ (eq ty x y) (ult ty x y))) (ule ty x y))
+(rule (simplify (bor _ (ult ty x y) (eq ty y x))) (ule ty x y))
+(rule (simplify (bor _ (eq ty y x) (ult ty x y))) (ule ty x y))
 
 ; (y >_u x) | (x == y) --> (x <=_u y)
-(rule (simplify (bor ty (ugt ty y x) (eq ty x y))) (ule ty x y))
-(rule (simplify (bor ty (eq ty x y) (ugt ty y x))) (ule ty x y))
-(rule (simplify (bor ty (ugt ty y x) (eq ty y x))) (ule ty x y))
-(rule (simplify (bor ty (eq ty y x) (ugt ty y x))) (ule ty x y))
+(rule (simplify (bor _ (ugt ty y x) (eq ty x y))) (ule ty x y))
+(rule (simplify (bor _ (eq ty x y) (ugt ty y x))) (ule ty x y))
+(rule (simplify (bor _ (ugt ty y x) (eq ty y x))) (ule ty x y))
+(rule (simplify (bor _ (eq ty y x) (ugt ty y x))) (ule ty x y))
 
 ; (x < y) | (x == y) --> (x <= y)
-(rule (simplify (bor ty (slt ty x y) (eq ty x y))) (sle ty x y))
-(rule (simplify (bor ty (eq ty x y) (slt ty x y))) (sle ty x y))
-(rule (simplify (bor ty (slt ty x y) (eq ty y x))) (sle ty x y))
-(rule (simplify (bor ty (eq ty y x) (slt ty x y))) (sle ty x y))
+(rule (simplify (bor _ (slt ty x y) (eq ty x y))) (sle ty x y))
+(rule (simplify (bor _ (eq ty x y) (slt ty x y))) (sle ty x y))
+(rule (simplify (bor _ (slt ty x y) (eq ty y x))) (sle ty x y))
+(rule (simplify (bor _ (eq ty y x) (slt ty x y))) (sle ty x y))
 
 ; (y > x) | (x == y) --> (x <= y)
-(rule (simplify (bor ty (sgt ty y x) (eq ty x y))) (sle ty x y))
-(rule (simplify (bor ty (eq ty x y) (sgt ty y x))) (sle ty x y))
-(rule (simplify (bor ty (sgt ty y x) (eq ty y x))) (sle ty x y))
-(rule (simplify (bor ty (eq ty y x) (sgt ty y x))) (sle ty x y))
+(rule (simplify (bor _ (sgt ty y x) (eq ty x y))) (sle ty x y))
+(rule (simplify (bor _ (eq ty x y) (sgt ty y x))) (sle ty x y))
+(rule (simplify (bor _ (sgt ty y x) (eq ty y x))) (sle ty x y))
+(rule (simplify (bor _ (eq ty y x) (sgt ty y x))) (sle ty x y))
 
 ; (x ^ z) | (((x ^ z) ^ y)) --> (x ^ z) | y
 (rule (simplify (bor ty (bxor ty x z) (bxor ty (bxor ty x z) y))) (bor ty (bxor ty x z) y))
@@ -760,24 +760,24 @@
       (subsume (all_zero ty)))
 
 ;; x >=u (x & y) --> true
-(rule (simplify (uge rty x (band ty x y))) (cmp_true rty))
-(rule (simplify (uge rty x (band ty y x))) (cmp_true rty))
-(rule (simplify (ule rty (band ty x y) x)) (cmp_true rty))
-(rule (simplify (ule rty (band ty y x) x)) (cmp_true rty))
-(rule (simplify (ugt rty (band ty x y) x)) (subsume (all_zero rty)))
-(rule (simplify (ugt rty (band ty y x) x)) (subsume (all_zero rty)))
-(rule (simplify (ult rty x (band ty x y))) (subsume (all_zero rty)))
-(rule (simplify (ult rty x (band ty y x))) (subsume (all_zero rty)))
+(rule (simplify (has_type rty (uge _ x (band ty x y)))) (cmp_true rty))
+(rule (simplify (has_type rty (uge _ x (band ty y x)))) (cmp_true rty))
+(rule (simplify (has_type rty (ule _ (band ty x y) x))) (cmp_true rty))
+(rule (simplify (has_type rty (ule _ (band ty y x) x))) (cmp_true rty))
+(rule (simplify (has_type rty (ugt _ (band ty x y) x))) (subsume (all_zero rty)))
+(rule (simplify (has_type rty (ugt _ (band ty y x) x))) (subsume (all_zero rty)))
+(rule (simplify (has_type rty (ult _ x (band ty x y)))) (subsume (all_zero rty)))
+(rule (simplify (has_type rty (ult _ x (band ty y x)))) (subsume (all_zero rty)))
 
 ;; (x | y) >=u x --> true
-(rule (simplify (uge rty (bor ty x y) x)) (cmp_true rty))
-(rule (simplify (uge rty (bor ty y x) x)) (cmp_true rty))
-(rule (simplify (ule rty x (bor ty x y))) (cmp_true rty))
-(rule (simplify (ule rty x (bor ty y x))) (cmp_true rty))
-(rule (simplify (ult rty (bor ty x y) x)) (subsume (all_zero rty)))
-(rule (simplify (ult rty (bor ty y x) x)) (subsume (all_zero rty)))
-(rule (simplify (ugt rty x (bor ty x y))) (subsume (all_zero rty)))
-(rule (simplify (ugt rty x (bor ty y x))) (subsume (all_zero rty)))
+(rule (simplify (has_type rty (uge _ (bor ty x y) x))) (cmp_true rty))
+(rule (simplify (has_type rty (uge _ (bor ty y x) x))) (cmp_true rty))
+(rule (simplify (has_type rty (ule _ x (bor ty x y)))) (cmp_true rty))
+(rule (simplify (has_type rty (ule _ x (bor ty y x)))) (cmp_true rty))
+(rule (simplify (has_type rty (ult _ (bor ty x y) x))) (subsume (all_zero rty)))
+(rule (simplify (has_type rty (ult _ (bor ty y x) x))) (subsume (all_zero rty)))
+(rule (simplify (has_type rty (ugt _ x (bor ty x y)))) (subsume (all_zero rty)))
+(rule (simplify (has_type rty (ugt _ x (bor ty y x)))) (subsume (all_zero rty)))
 
 ;; (x & y) & (x & z) --> (x & y) & z
 (rule (simplify (band ty (band ty x y) (band ty x z))) (band ty (band ty x y) z))
diff --git a/cranelift/codegen/src/opts/cprop.isle b/cranelift/codegen/src/opts/cprop.isle
index d4861f20f3d5..ea0587550c6b 100644
--- a/cranelift/codegen/src/opts/cprop.isle
+++ b/cranelift/codegen/src/opts/cprop.isle
@@ -133,10 +133,11 @@
       (subsume (iconst_s wide k)))
 
 (rule (simplify
-       (icmp result_ty
-            cc
-            (iconst ty k1)
-            (iconst ty k2)))
+       (has_type result_ty
+         (icmp ty
+              cc
+              (iconst ty k1)
+              (iconst ty k2))))
       (subsume (iconst result_ty (imm64_icmp ty cc k1 k2))))
 
 
diff --git a/cranelift/codegen/src/opts/extends.isle b/cranelift/codegen/src/opts/extends.isle
index b86ae1c60285..0e7cb007919d 100644
--- a/cranelift/codegen/src/opts/extends.isle
+++ b/cranelift/codegen/src/opts/extends.isle
@@ -26,14 +26,16 @@
 
 ;; 32-bit integers zero-extended to 64-bit integers are never negative
 (rule (simplify
-       (slt ty
-             (uextend $I64 x @ (value_type $I32))
-             (all_zero _)))
+       (has_type ty
+         (slt _
+               (uextend $I64 x @ (value_type $I32))
+               (all_zero _))))
       (subsume (all_zero ty)))
 (rule (simplify
-       (sge ty
-             (uextend $I64 x @ (value_type $I32))
-             (all_zero _)))
+       (has_type ty
+         (sge _
+               (uextend $I64 x @ (value_type $I32))
+               (all_zero _))))
       (subsume (iconst_u ty 1)))
 
 ;; Sign-extending can't change whether a number is zero nor how it signed-compares to zero
@@ -91,49 +93,49 @@
 (rule (simplify (ireduce ty (band _ x y))) (band ty (ireduce ty x) (ireduce ty y)))
 
 ;; Try to transform an `iconcat` into an i128 into either an sextend or uextend
-(rule (simplify (iconcat $I128 x (all_zero _))) (uextend $I128 x))
-(rule (simplify (iconcat $I128 x (sshr _ x (iconst_u _ 63)))) (sextend $I128 x))
+(rule (simplify (iconcat $I64 x (all_zero _))) (uextend $I128 x))
+(rule (simplify (iconcat $I64 x (sshr _ x (iconst_u _ 63)))) (sextend $I128 x))
 
 ;; ireduce(ireduce(x)) --> ireduce(x)
 (rule (simplify (ireduce ty (ireduce cty x))) (ireduce ty x))
 
 ;; uextend(x) <u uextend(y) --> x <u y
-(rule (simplify (ult ty (uextend cty x @ (value_type ty1)) (uextend cty y @ (value_type ty1)))) (ult ty x y))
+(rule (simplify (ult _ (uextend cty x @ (value_type ty1)) (uextend cty y @ (value_type ty1)))) (ult ty1 x y))
 
 ;; uextend(x) == 0 --> x == 0
-(rule (simplify (eq ty
+(rule (simplify (eq _
                     (uextend ty1 x @ (value_type cty))
                     (iconst_u ty1 0)))
-      (eq ty x (iconst_u cty 0)))
+      (eq cty x (iconst_u cty 0)))
 
 ;; uextend(x) == uextend(y) --> x == y
-(rule (simplify (eq ty
+(rule (simplify (eq _
                     (uextend cty x @ (value_type ty1))
                     (uextend cty y @ (value_type ty1))))
-      (eq ty x y))
+      (eq ty1 x y))
 
 ;; sextend(x) OP sextend(y) --> x OP y (OP = {==, <s})
-(rule (simplify (eq ty (sextend cty x @ (value_type ty1)) (sextend cty y @ (value_type ty1)))) (eq ty x y))
-(rule (simplify (slt ty (sextend cty x @ (value_type ty1)) (sextend cty y @ (value_type ty1)))) (slt ty x y))
+(rule (simplify (eq _ (sextend cty x @ (value_type ty1)) (sextend cty y @ (value_type ty1)))) (eq ty1 x y))
+(rule (simplify (slt _ (sextend cty x @ (value_type ty1)) (sextend cty y @ (value_type ty1)))) (slt ty1 x y))
 
 ;; extend(x) != extend(y) --> x != y
-(rule (simplify (ne ty (sextend cty x @ (value_type ty1)) (sextend cty y @ (value_type ty1)))) (ne ty x y))
-(rule (simplify (ne ty (uextend cty x @ (value_type ty1)) (uextend cty y @ (value_type ty1)))) (ne ty x y))
+(rule (simplify (ne _ (sextend cty x @ (value_type ty1)) (sextend cty y @ (value_type ty1)))) (ne ty1 x y))
+(rule (simplify (ne _ (uextend cty x @ (value_type ty1)) (uextend cty y @ (value_type ty1)))) (ne ty1 x y))
 
 ;; sextend(x) OPs sextend(y) --> x OPs y
-(rule (simplify (sge ty (sextend cty x @ (value_type ty1)) (sextend cty y @ (value_type ty1)))) (sge ty x y))
-(rule (simplify (sle ty (sextend cty x @ (value_type ty1)) (sextend cty y @ (value_type ty1)))) (sge ty y x))
+(rule (simplify (sge _ (sextend cty x @ (value_type ty1)) (sextend cty y @ (value_type ty1)))) (sge ty1 x y))
+(rule (simplify (sle _ (sextend cty x @ (value_type ty1)) (sextend cty y @ (value_type ty1)))) (sge ty1 y x))
 
 ;; uextend(x) OPs uextend(y) --> x OPu y
-(rule (simplify (sge ty (uextend cty x @ (value_type ty1)) (uextend cty y @ (value_type ty1)))) (uge ty x y))
-(rule (simplify (sgt ty (uextend cty x @ (value_type ty1)) (uextend cty y @ (value_type ty1)))) (ugt ty x y))
-(rule (simplify (sle ty (uextend cty x @ (value_type ty1)) (uextend cty y @ (value_type ty1)))) (ule ty x y))
-(rule (simplify (slt ty (uextend cty x @ (value_type ty1)) (uextend cty y @ (value_type ty1)))) (ult ty x y))
+(rule (simplify (sge _ (uextend cty x @ (value_type ty1)) (uextend cty y @ (value_type ty1)))) (uge ty1 x y))
+(rule (simplify (sgt _ (uextend cty x @ (value_type ty1)) (uextend cty y @ (value_type ty1)))) (ugt ty1 x y))
+(rule (simplify (sle _ (uextend cty x @ (value_type ty1)) (uextend cty y @ (value_type ty1)))) (ule ty1 x y))
+(rule (simplify (slt _ (uextend cty x @ (value_type ty1)) (uextend cty y @ (value_type ty1)))) (ult ty1 x y))
 
 ;; extend(x) OPu extend(y) --> x OPu y
-(rule (simplify (uge ty (sextend cty x @ (value_type ty1)) (sextend cty y @ (value_type ty1)))) (uge ty x y))
-(rule (simplify (ugt ty (sextend cty x @ (value_type ty1)) (sextend cty y @ (value_type ty1)))) (ugt ty x y))
-(rule (simplify (ule ty (sextend cty x @ (value_type ty1)) (sextend cty y @ (value_type ty1)))) (ule ty x y))
-(rule (simplify (ult ty (sextend cty x @ (value_type ty1)) (sextend cty y @ (value_type ty1)))) (ult ty x y))
-(rule (simplify (uge ty (uextend cty x @ (value_type ty1)) (uextend cty y @ (value_type ty1)))) (uge ty x y))
-(rule (simplify (ule ty (uextend cty x @ (value_type ty1)) (uextend cty y @ (value_type ty1)))) (ule ty x y))
+(rule (simplify (uge _ (sextend cty x @ (value_type ty1)) (sextend cty y @ (value_type ty1)))) (uge ty1 x y))
+(rule (simplify (ugt _ (sextend cty x @ (value_type ty1)) (sextend cty y @ (value_type ty1)))) (ugt ty1 x y))
+(rule (simplify (ule _ (sextend cty x @ (value_type ty1)) (sextend cty y @ (value_type ty1)))) (ule ty1 x y))
+(rule (simplify (ult _ (sextend cty x @ (value_type ty1)) (sextend cty y @ (value_type ty1)))) (ult ty1 x y))
+(rule (simplify (uge _ (uextend cty x @ (value_type ty1)) (uextend cty y @ (value_type ty1)))) (uge ty1 x y))
+(rule (simplify (ule _ (uextend cty x @ (value_type ty1)) (uextend cty y @ (value_type ty1)))) (ule ty1 x y))
diff --git a/cranelift/codegen/src/opts/icmp.isle b/cranelift/codegen/src/opts/icmp.isle
index ce85807e246c..b28120a7aae8 100644
--- a/cranelift/codegen/src/opts/icmp.isle
+++ b/cranelift/codegen/src/opts/icmp.isle
@@ -2,16 +2,16 @@
 
 ;; `x == x` is always true for integers; `x != x` is false. Strict
 ;; inequalities are false, and loose inequalities are true.
-(rule (simplify (eq ty x x)) (subsume (cmp_true ty)))
-(rule (simplify (ne ty x x)) (subsume (all_zero ty)))
-(rule (simplify (ugt ty x x)) (subsume (all_zero ty)))
-(rule (simplify (uge ty x x)) (subsume (cmp_true ty)))
-(rule (simplify (sgt ty x x)) (subsume (all_zero ty)))
-(rule (simplify (sge ty x x)) (subsume (cmp_true ty)))
-(rule (simplify (ult ty x x)) (subsume (all_zero ty)))
-(rule (simplify (ule ty x x)) (subsume (cmp_true ty)))
-(rule (simplify (slt ty x x)) (subsume (all_zero ty)))
-(rule (simplify (sle ty x x)) (subsume (cmp_true ty)))
+(rule (simplify (has_type ty (eq _ x x))) (subsume (cmp_true ty)))
+(rule (simplify (has_type ty (ne _ x x))) (subsume (all_zero ty)))
+(rule (simplify (has_type ty (ugt _ x x))) (subsume (all_zero ty)))
+(rule (simplify (has_type ty (uge _ x x))) (subsume (cmp_true ty)))
+(rule (simplify (has_type ty (sgt _ x x))) (subsume (all_zero ty)))
+(rule (simplify (has_type ty (sge _ x x))) (subsume (cmp_true ty)))
+(rule (simplify (has_type ty (ult _ x x))) (subsume (all_zero ty)))
+(rule (simplify (has_type ty (ule _ x x))) (subsume (cmp_true ty)))
+(rule (simplify (has_type ty (slt _ x x))) (subsume (all_zero ty)))
+(rule (simplify (has_type ty (sle _ x x))) (subsume (cmp_true ty)))
 
 ;; For integers, adding the same thing on both sides of an equality check
 ;; (or an inequality check) doesn't change the result.
@@ -46,28 +46,28 @@
 ;; Optimize icmp-of-icmp.
 ;; ne(icmp(ty, cc, x, y), 0) == icmp(ty, cc, x, y)
 ;; e.g. neq(ugt(x, y), 0) == ugt(x, y)
-(rule (simplify (ne ty
-                      (uextend_maybe _ inner @ (icmp ty _ _ _))
+(rule (simplify (ne _
+                      (uextend_maybe _ inner @ (icmp _ _ _ _))
                       (all_zero _)))
       (subsume inner))
 
 ;; Likewise for icmp-of-fcmp.
 ;; ne(fcmp(ty, cc, x, y), 0) == fcmp(ty, cc, x, y)
-(rule (simplify (ne ty
-                      (uextend_maybe _ inner @ (fcmp ty _ _ _))
+(rule (simplify (ne _
+                      (uextend_maybe _ inner @ (fcmp _ _ _ _))
                       (all_zero _)))
       (subsume inner))
 
 ;; eq(icmp(ty, cc, x, y), 0) == icmp(ty, cc_complement, x, y)
 ;; e.g. eq(ugt(x, y), 0) == ule(x, y)
-(rule (simplify (eq ty
+(rule (simplify (eq _
                       (uextend_maybe _ (icmp ty cc x y))
                       (all_zero _)))
       (subsume (icmp ty (intcc_complement cc) x y)))
 
 ;; ne(icmp(ty, cc, x, y), 1) == icmp(ty, cc_complement, x, y)
 ;; e.g. ne(ugt(x, y), 1) == ule(x, y)
-(rule (simplify (ne ty
+(rule (simplify (ne _
                       (uextend_maybe _ (icmp ty cc x y))
                       (iconst_u _ 1)))
       (subsume (icmp ty (intcc_complement cc) x y)))
@@ -101,89 +101,89 @@
 
 ;; Comparisons against largest/smallest signed/unsigned values:
 ;; ult(x, 0) == false.
-(rule (simplify (ult bty x zero @ (all_zero _)))
+(rule (simplify (has_type bty (ult _ x zero @ (all_zero _))))
       (subsume (all_zero bty)))
 
 ;; ule(x, 0) == eq(x, 0)
-(rule (simplify (ule (fits_in_64 (ty_int bty)) x zero @ (all_zero _)))
-      (eq bty x zero))
+(rule (simplify (ule (fits_in_64 (ty_int cty)) x zero @ (all_zero _)))
+      (eq cty x zero))
 
 ;; ugt(x, 0) == ne(x, 0).
-(rule (simplify (ugt (fits_in_64 (ty_int bty)) x zero @ (all_zero _)))
-      (ne bty x zero))
+(rule (simplify (ugt (fits_in_64 (ty_int cty)) x zero @ (all_zero _)))
+      (ne cty x zero))
 
 ;; uge(x, 0) == true.
-(rule (simplify (uge bty x zero @ (all_zero _)))
+(rule (simplify (has_type bty (uge _ x zero @ (all_zero _))))
       (subsume (cmp_true bty)))
 
 ;; ult(x, UMAX) == ne(x, UMAX).
-(rule (simplify (ult (fits_in_64 (ty_int bty)) x umax @ (iconst_u cty y)))
+(rule (simplify (ult (fits_in_64 (ty_int cty)) x umax @ (iconst_u cty y)))
        (if-let true (u64_eq y (ty_umax cty)))
-       (ne bty x umax))
+       (ne cty x umax))
 
 ;; ule(x, UMAX) == true.
-(rule (simplify (ule (fits_in_64 (ty_int bty)) x umax @ (iconst_u cty y)))
+(rule (simplify (has_type bty (ule (fits_in_64 (ty_int cty)) x umax @ (iconst_u cty y))))
        (if-let true (u64_eq y (ty_umax cty)))
        (subsume (iconst_u bty 1)))
 
 ;; ugt(x, UMAX) == false.
-(rule (simplify (ugt (fits_in_64 (ty_int bty)) x umax @ (iconst_u cty y)))
+(rule (simplify (has_type bty (ugt (fits_in_64 (ty_int cty)) x umax @ (iconst_u cty y))))
        (if-let true (u64_eq y (ty_umax cty)))
        (subsume (all_zero bty)))
 
 ;; uge(x, UMAX) == eq(x, UMAX).
-(rule (simplify (uge (fits_in_64 (ty_int bty)) x umax @ (iconst_u cty y)))
+(rule (simplify (uge (fits_in_64 (ty_int cty)) x umax @ (iconst_u cty y)))
        (if-let true (u64_eq y (ty_umax cty)))
-       (eq bty x umax))
+       (eq cty x umax))
 
 ;; slt(x, SMIN) == false.
-(rule (simplify (slt (fits_in_64 (ty_int bty)) x smin @ (iconst_u cty y)))
+(rule (simplify (has_type bty (slt (fits_in_64 (ty_int cty)) x smin @ (iconst_u cty y))))
        (if-let true (u64_eq y (ty_smin cty)))
        (subsume (all_zero bty)))
 
 ;; sle(x, SMIN) == eq(x, SMIN).
-(rule (simplify (sle (fits_in_64 (ty_int bty)) x smin @ (iconst_u cty y)))
+(rule (simplify (sle (fits_in_64 (ty_int cty)) x smin @ (iconst_u cty y)))
        (if-let true (u64_eq y (ty_smin cty)))
-       (eq bty x smin))
+       (eq cty x smin))
 
 ;; sgt(x, SMIN) == ne(x, SMIN).
-(rule (simplify (sgt (fits_in_64 (ty_int bty)) x smin @ (iconst_u cty y)))
+(rule (simplify (sgt (fits_in_64 (ty_int cty)) x smin @ (iconst_u cty y)))
        (if-let true (u64_eq y (ty_smin cty)))
-       (ne bty x smin))
+       (ne cty x smin))
 
 ;; sge(x, SMIN) == true.
-(rule (simplify (sge (fits_in_64 (ty_int bty)) x smin @ (iconst_u cty y)))
+(rule (simplify (has_type bty (sge (fits_in_64 (ty_int cty)) x smin @ (iconst_u cty y))))
        (if-let true (u64_eq y (ty_smin cty)))
        (subsume (iconst_u bty 1)))
 
 ;; slt(x, SMAX) == ne(x, SMAX).
-(rule (simplify (slt (fits_in_64 (ty_int bty)) x smax @ (iconst_u cty y)))
+(rule (simplify (slt (fits_in_64 (ty_int cty)) x smax @ (iconst_u cty y)))
        (if-let true (u64_eq y (ty_smax cty)))
-       (ne bty x smax))
+       (ne cty x smax))
 
 ;; sle(x, SMAX) == true.
-(rule (simplify (sle (fits_in_64 (ty_int bty)) x smax @ (iconst_u cty y)))
+(rule (simplify (has_type bty (sle (fits_in_64 (ty_int cty)) x smax @ (iconst_u cty y))))
        (if-let true (u64_eq y (ty_smax cty)))
        (subsume (iconst_u bty 1)))
 
 ;; sgt(x, SMAX) == false.
-(rule (simplify (sgt (fits_in_64 (ty_int bty)) x smax @ (iconst_u cty y)))
+(rule (simplify (has_type bty (sgt (fits_in_64 (ty_int cty)) x smax @ (iconst_u cty y))))
        (if-let true (u64_eq y (ty_smax cty)))
        (subsume (all_zero bty)))
 
 ;; sge(x, SMAX) == eq(x, SMAX).
-(rule (simplify (sge (fits_in_64 (ty_int bty)) x smax @ (iconst_u cty y)))
+(rule (simplify (sge (fits_in_64 (ty_int cty)) x smax @ (iconst_u cty y)))
        (if-let true (u64_eq y (ty_smax cty)))
-       (eq bty x smax))
+       (eq cty x smax))
 
 ;; `band`/`bor` of 2 comparisons:
-(rule (simplify (band (fits_in_64 ty) (icmp ty cc1 x y) (icmp ty cc2 x y)))
+(rule (simplify (band (fits_in_64 bty) (icmp ty cc1 x y) (icmp ty cc2 x y)))
   (if-let signed (intcc_comparable cc1 cc2))
-  (compose_icmp ty (u64_and (decompose_intcc cc1) (decompose_intcc cc2)) signed x y))
+  (compose_icmp bty ty (u64_and (decompose_intcc cc1) (decompose_intcc cc2)) signed x y))
 
-(rule (simplify (bor (fits_in_64 ty) (icmp ty cc1 x y) (icmp ty cc2 x y)))
+(rule (simplify (bor (fits_in_64 bty) (icmp ty cc1 x y) (icmp ty cc2 x y)))
   (if-let signed (intcc_comparable cc1 cc2))
-  (compose_icmp ty (u64_or (decompose_intcc cc1) (decompose_intcc cc2)) signed x y))
+  (compose_icmp bty ty (u64_or (decompose_intcc cc1) (decompose_intcc cc2)) signed x y))
 
 ;; Prefer comparing against zero
 ;; uge(x, 1) == ne(x, 0)
@@ -222,19 +222,21 @@
 (rule (decompose_intcc (IntCC.SignedGreaterThanOrEqual)) 5)
 (rule (decompose_intcc (IntCC.NotEqual)) 6)
 
-(decl compose_icmp (Type u64 bool Value Value) Value)
-(rule (compose_icmp ty 0 _ _ _) (subsume (all_zero ty)))
-(rule (compose_icmp ty 1 _ x y) (icmp ty (IntCC.Equal) x y))
-(rule (compose_icmp ty 2 false x y) (icmp ty (IntCC.UnsignedLessThan) x y))
-(rule (compose_icmp ty 2 true x y) (icmp ty (IntCC.SignedLessThan) x y))
-(rule (compose_icmp ty 3 false x y) (icmp ty (IntCC.UnsignedLessThanOrEqual) x y))
-(rule (compose_icmp ty 3 true x y) (icmp ty (IntCC.SignedLessThanOrEqual) x y))
-(rule (compose_icmp ty 4 false x y) (icmp ty (IntCC.UnsignedGreaterThan) x y))
-(rule (compose_icmp ty 4 true x y) (icmp ty (IntCC.SignedGreaterThan) x y))
-(rule (compose_icmp ty 5 false x y) (icmp ty (IntCC.UnsignedGreaterThanOrEqual) x y))
-(rule (compose_icmp ty 5 true x y) (icmp ty (IntCC.SignedGreaterThanOrEqual) x y))
-(rule (compose_icmp ty 6 _ x y) (icmp ty (IntCC.NotEqual) x y))
-(rule (compose_icmp ty 7 _ _ _) (subsume (iconst_u ty 1)))
+;; Compose a comparison from its decomposed condition code. The first type
+;; is the comparison's result type, the second its operand (controlling) type.
+(decl compose_icmp (Type Type u64 bool Value Value) Value)
+(rule (compose_icmp bty _ 0 _ _ _) (subsume (all_zero bty)))
+(rule (compose_icmp _ ty 1 _ x y) (icmp ty (IntCC.Equal) x y))
+(rule (compose_icmp _ ty 2 false x y) (icmp ty (IntCC.UnsignedLessThan) x y))
+(rule (compose_icmp _ ty 2 true x y) (icmp ty (IntCC.SignedLessThan) x y))
+(rule (compose_icmp _ ty 3 false x y) (icmp ty (IntCC.UnsignedLessThanOrEqual) x y))
+(rule (compose_icmp _ ty 3 true x y) (icmp ty (IntCC.SignedLessThanOrEqual) x y))
+(rule (compose_icmp _ ty 4 false x y) (icmp ty (IntCC.UnsignedGreaterThan) x y))
+(rule (compose_icmp _ ty 4 true x y) (icmp ty (IntCC.SignedGreaterThan) x y))
+(rule (compose_icmp _ ty 5 false x y) (icmp ty (IntCC.UnsignedGreaterThanOrEqual) x y))
+(rule (compose_icmp _ ty 5 true x y) (icmp ty (IntCC.SignedGreaterThanOrEqual) x y))
+(rule (compose_icmp _ ty 6 _ x y) (icmp ty (IntCC.NotEqual) x y))
+(rule (compose_icmp bty _ 7 _ _ _) (subsume (iconst_u bty 1)))
 
 (decl pure intcc_class (IntCC) u64)
 (rule (intcc_class (IntCC.UnsignedLessThan)) 1)
@@ -251,45 +253,45 @@
 ;; Pattern-match what LLVM emits today for 128-bit comparisons into actual
 ;; 128-bit comparisons. Platforms like x64 and aarch64 have more optimal
 ;; lowerings for 128-bit arithmetic than the default structure.
-(rule (simplify (select ty (eq _   a_hi @ (value_type $I64) b_hi @ (value_type $I64))
-                           (uge ty a_lo @ (value_type $I64) b_lo @ (value_type $I64))
-                           (uge ty a_hi b_hi)))
-      (uge ty (iconcat $I64 a_lo a_hi) (iconcat $I64 b_lo b_hi)))
-
-(rule (simplify (select ty (eq _   a_hi @ (value_type $I64) b_hi @ (value_type $I64))
-                           (uge ty a_lo @ (value_type $I64) b_lo @ (value_type $I64))
-                           (sge ty a_hi b_hi)))
-      (sge ty (iconcat $I64 a_lo a_hi) (iconcat $I64 b_lo b_hi)))
-
-(rule (simplify (select ty (eq _   a_hi @ (value_type $I64) b_hi @ (value_type $I64))
-                           (ugt ty a_lo @ (value_type $I64) b_lo @ (value_type $I64))
-                           (ugt ty a_hi b_hi)))
-      (ugt ty (iconcat $I64 a_lo a_hi) (iconcat $I64 b_lo b_hi)))
-
-(rule (simplify (select ty (eq _   a_hi @ (value_type $I64) b_hi @ (value_type $I64))
-                           (ugt ty a_lo @ (value_type $I64) b_lo @ (value_type $I64))
-                           (sgt ty a_hi b_hi)))
-      (sgt ty (iconcat $I64 a_lo a_hi) (iconcat $I64 b_lo b_hi)))
-
-(rule (simplify (select ty (eq _   a_hi @ (value_type $I64) b_hi @ (value_type $I64))
-                           (ule ty a_lo @ (value_type $I64) b_lo @ (value_type $I64))
-                           (ule ty a_hi b_hi)))
-      (ule ty (iconcat $I64 a_lo a_hi) (iconcat $I64 b_lo b_hi)))
-
-(rule (simplify (select ty (eq _   a_hi @ (value_type $I64) b_hi @ (value_type $I64))
-                           (ule ty a_lo @ (value_type $I64) b_lo @ (value_type $I64))
-                           (sle ty a_hi b_hi)))
-      (sle ty (iconcat $I64 a_lo a_hi) (iconcat $I64 b_lo b_hi)))
-
-(rule (simplify (select ty (eq _   a_hi @ (value_type $I64) b_hi @ (value_type $I64))
-                           (ult ty a_lo @ (value_type $I64) b_lo @ (value_type $I64))
-                           (ult ty a_hi b_hi)))
-      (ult ty (iconcat $I64 a_lo a_hi) (iconcat $I64 b_lo b_hi)))
-
-(rule (simplify (select ty (eq _   a_hi @ (value_type $I64) b_hi @ (value_type $I64))
-                           (ult ty a_lo @ (value_type $I64) b_lo @ (value_type $I64))
-                           (slt ty a_hi b_hi)))
-      (slt ty (iconcat $I64 a_lo a_hi) (iconcat $I64 b_lo b_hi)))
+(rule (simplify (select _ (eq _   a_hi @ (value_type $I64) b_hi @ (value_type $I64))
+                           (uge _ a_lo @ (value_type $I64) b_lo @ (value_type $I64))
+                           (uge _ a_hi b_hi)))
+      (uge $I128 (iconcat $I64 a_lo a_hi) (iconcat $I64 b_lo b_hi)))
+
+(rule (simplify (select _ (eq _   a_hi @ (value_type $I64) b_hi @ (value_type $I64))
+                           (uge _ a_lo @ (value_type $I64) b_lo @ (value_type $I64))
+                           (sge _ a_hi b_hi)))
+      (sge $I128 (iconcat $I64 a_lo a_hi) (iconcat $I64 b_lo b_hi)))
+
+(rule (simplify (select _ (eq _   a_hi @ (value_type $I64) b_hi @ (value_type $I64))
+                           (ugt _ a_lo @ (value_type $I64) b_lo @ (value_type $I64))
+                           (ugt _ a_hi b_hi)))
+      (ugt $I128 (iconcat $I64 a_lo a_hi) (iconcat $I64 b_lo b_hi)))
+
+(rule (simplify (select _ (eq _   a_hi @ (value_type $I64) b_hi @ (value_type $I64))
+                           (ugt _ a_lo @ (value_type $I64) b_lo @ (value_type $I64))
+                           (sgt _ a_hi b_hi)))
+      (sgt $I128 (iconcat $I64 a_lo a_hi) (iconcat $I64 b_lo b_hi)))
+
+(rule (simplify (select _ (eq _   a_hi @ (value_type $I64) b_hi @ (value_type $I64))
+                           (ule _ a_lo @ (value_type $I64) b_lo @ (value_type $I64))
+                           (ule _ a_hi b_hi)))
+      (ule $I128 (iconcat $I64 a_lo a_hi) (iconcat $I64 b_lo b_hi)))
+
+(rule (simplify (select _ (eq _   a_hi @ (value_type $I64) b_hi @ (value_type $I64))
+                           (ule _ a_lo @ (value_type $I64) b_lo @ (value_type $I64))
+                           (sle _ a_hi b_hi)))
+      (sle $I128 (iconcat $I64 a_lo a_hi) (iconcat $I64 b_lo b_hi)))
+
+(rule (simplify (select _ (eq _   a_hi @ (value_type $I64) b_hi @ (value_type $I64))
+                           (ult _ a_lo @ (value_type $I64) b_lo @ (value_type $I64))
+                           (ult _ a_hi b_hi)))
+      (ult $I128 (iconcat $I64 a_lo a_hi) (iconcat $I64 b_lo b_hi)))
+
+(rule (simplify (select _ (eq _   a_hi @ (value_type $I64) b_hi @ (value_type $I64))
+                           (ult _ a_lo @ (value_type $I64) b_lo @ (value_type $I64))
+                           (slt _ a_hi b_hi)))
+      (slt $I128 (iconcat $I64 a_lo a_hi) (iconcat $I64 b_lo b_hi)))
 
 
 (rule (simplify (eq cty x (bxor (ty_int bty) x y))) (subsume (eq cty y (all_zero bty))))
@@ -300,120 +302,120 @@
 (rule (simplify (ule cty (isub ty x y) x)) (ule cty y x))
 
 ;; (x < y) ? x : y != x == x > y, for both signed and unsigned.
-(rule (simplify (ne cty (select ty (slt cty x y) x y) x)) (sgt cty x y))
-(rule (simplify (ne cty (select ty (ult cty x y) x y) x)) (ugt cty x y))
+(rule (simplify (ne ty (select ty (slt ty x y) x y) x)) (sgt ty x y))
+(rule (simplify (ne ty (select ty (ult ty x y) x y) x)) (ugt ty x y))
 
 (rule (simplify (ult cty (bnot ty x) (bnot ty y))) (ugt cty x y))
 (rule (simplify (slt cty (bnot ty x) (bnot ty y))) (sgt cty x y))
 
 ;; a < b ^^ a > b => (a ≠ b)
-(rule (simplify (bxor ty (sgt ty x y) (sgt ty y x))) (ne ty x y))
-(rule (simplify (bxor ty (sgt ty x y) (slt ty x y))) (ne ty x y))
-(rule (simplify (bxor ty (slt ty x y) (sgt ty x y))) (ne ty x y))
-(rule (simplify (bxor ty (slt ty x y) (slt ty y x))) (ne ty x y))
-(rule (simplify (bxor ty (ugt ty x y) (ugt ty y x))) (ne ty x y))
-(rule (simplify (bxor ty (ugt ty x y) (ult ty x y))) (ne ty x y))
-(rule (simplify (bxor ty (ult ty x y) (ugt ty x y))) (ne ty x y))
-(rule (simplify (bxor ty (ult ty x y) (ult ty y x))) (ne ty x y))
+(rule (simplify (bxor _ (sgt ty x y) (sgt ty y x))) (ne ty x y))
+(rule (simplify (bxor _ (sgt ty x y) (slt ty x y))) (ne ty x y))
+(rule (simplify (bxor _ (slt ty x y) (sgt ty x y))) (ne ty x y))
+(rule (simplify (bxor _ (slt ty x y) (slt ty y x))) (ne ty x y))
+(rule (simplify (bxor _ (ugt ty x y) (ugt ty y x))) (ne ty x y))
+(rule (simplify (bxor _ (ugt ty x y) (ult ty x y))) (ne ty x y))
+(rule (simplify (bxor _ (ult ty x y) (ugt ty x y))) (ne ty x y))
+(rule (simplify (bxor _ (ult ty x y) (ult ty y x))) (ne ty x y))
 
 ;; a < b && a > b = false
-(rule (simplify (band (ty_int_vec128 ty) (sgt ty x y) (slt ty x y))) (all_zero ty))
-(rule (simplify (band (ty_int_vec128 ty) (slt ty x y) (sgt ty x y))) (all_zero ty))
-(rule (simplify (band (ty_int_vec128 ty) (ugt ty x y) (ult ty x y))) (all_zero ty))
-(rule (simplify (band (ty_int_vec128 ty) (ult ty x y) (ugt ty x y))) (all_zero ty))
+(rule (simplify (band (ty_int_vec128 bty) (sgt ty x y) (slt ty x y))) (all_zero bty))
+(rule (simplify (band (ty_int_vec128 bty) (slt ty x y) (sgt ty x y))) (all_zero bty))
+(rule (simplify (band (ty_int_vec128 bty) (ugt ty x y) (ult ty x y))) (all_zero bty))
+(rule (simplify (band (ty_int_vec128 bty) (ult ty x y) (ugt ty x y))) (all_zero bty))
 (rule
-  (simplify (band ty (sgt ty x (iconst_s _ y)) (ult ty x (iconst_s _ y))))
+  (simplify (band bty (sgt _ x (iconst_s _ y)) (ult _ x (iconst_s _ y))))
   (if-let true (i64_gt_eq y 0))
-  (all_zero ty))
+  (all_zero bty))
 (rule
-  (simplify (band ty (sgt ty (iconst_s _ x) y) (ult ty (iconst_s _ x) y)))
+  (simplify (band bty (sgt _ (iconst_s _ x) y) (ult _ (iconst_s _ x) y)))
   (if-let true (i64_lt x 0))
-  (all_zero ty))
+  (all_zero bty))
 (rule
-  (simplify (band ty (slt ty x (iconst_s _ y)) (ugt ty x (iconst_s _ y))))
+  (simplify (band bty (slt _ x (iconst_s _ y)) (ugt _ x (iconst_s _ y))))
   (if-let true (i64_lt y 0))
-  (all_zero ty))
+  (all_zero bty))
 (rule
-  (simplify (band ty (slt ty (iconst_s _ x) y) (ugt ty (iconst_s _ x) y)))
+  (simplify (band bty (slt _ (iconst_s _ x) y) (ugt _ (iconst_s _ x) y)))
   (if-let true (i64_gt_eq x 0))
-  (all_zero ty))
+  (all_zero bty))
 (rule
-  (simplify (band ty (ugt ty x (iconst_s _ y)) (slt ty x (iconst_s _ y))))
+  (simplify (band bty (ugt _ x (iconst_s _ y)) (slt _ x (iconst_s _ y))))
   (if-let true (i64_lt y 0))
-  (all_zero ty))
+  (all_zero bty))
 (rule
-  (simplify (band ty (ugt ty (iconst_s _ x) y) (slt ty (iconst_s _ x) y)))
+  (simplify (band bty (ugt _ (iconst_s _ x) y) (slt _ (iconst_s _ x) y)))
   (if-let true (i64_gt_eq x 0))
-  (all_zero ty))
+  (all_zero bty))
 (rule
-  (simplify (band ty (ult ty x (iconst_s _ y)) (sgt ty x (iconst_s _ y))))
+  (simplify (band bty (ult _ x (iconst_s _ y)) (sgt _ x (iconst_s _ y))))
   (if-let true (i64_gt_eq y 0))
-  (all_zero ty))
+  (all_zero bty))
 (rule
-  (simplify (band ty (ult ty (iconst_s _ x) y) (sgt ty (iconst_s _ x) y)))
+  (simplify (band bty (ult _ (iconst_s _ x) y) (sgt _ (iconst_s _ x) y)))
   (if-let true (i64_lt x 0))
-  (all_zero ty))
+  (all_zero bty))
 
 ;; (x < y) & (x ≠ -1) = (x < y)
 (rule
-  (simplify (band ty (ne ty x (iconst_s _ -1)) (ugt ty y x)))
+  (simplify (band _ (ne ty x (iconst_s _ -1)) (ugt ty y x)))
    (ult ty x y))
 (rule
-  (simplify (band ty (ne ty x (iconst_s _ -1)) (ult ty x z)))
+  (simplify (band _ (ne ty x (iconst_s _ -1)) (ult ty x z)))
    (ult ty x z))
 (rule
-  (simplify (band ty (ne ty (iconst_s _ -1) x) (ugt ty y x)))
+  (simplify (band _ (ne ty (iconst_s _ -1) x) (ugt ty y x)))
    (ult ty x y))
 (rule
-  (simplify (band ty (ne ty (iconst_s _ -1) x) (ult ty x z)))
+  (simplify (band _ (ne ty (iconst_s _ -1) x) (ult ty x z)))
    (ult ty x z))
 (rule
-  (simplify (band ty (ugt ty x y) (ne ty y (iconst_s _ -1))))
+  (simplify (band _ (ugt ty x y) (ne ty y (iconst_s _ -1))))
    (ult ty y x))
 (rule
-  (simplify (band ty (ugt ty x y) (ne ty (iconst_s _ -1) y)))
+  (simplify (band _ (ugt ty x y) (ne ty (iconst_s _ -1) y)))
    (ult ty y x))
 (rule
-  (simplify (band ty (ult ty x y) (ne ty x (iconst_s _ -1))))
+  (simplify (band _ (ult ty x y) (ne ty x (iconst_s _ -1))))
    (ult ty x y))
 (rule
-  (simplify (band ty (ult ty x y) (ne ty (iconst_s _ -1) x)))
+  (simplify (band _ (ult ty x y) (ne ty (iconst_s _ -1) x)))
    (ult ty x y))
 
 ;; icmp on select with two constant inputs compared with one of the two
 ;; constants can directly use the inner select condition.
 ;; See: https://github.com/bytecodealliance/wasmtime/issues/11578
 (rule (simplify (eq _
-  (select select_ty inner_cond @ (value_type inner_ty)
+  (select _ inner_cond @ (value_type inner_ty)
     (iconst_u _ k1)
     (iconst_u _ k2))
   (iconst_u _ k1)))
   (if-let false (u64_eq k1 k2))
-  (ne select_ty inner_cond (all_zero inner_ty)))
+  (ne inner_ty inner_cond (all_zero inner_ty)))
 
 (rule (simplify (eq _
-  (select select_ty inner_cond @ (value_type inner_ty)
+  (select _ inner_cond @ (value_type inner_ty)
     (iconst_u _ k1)
     (iconst_u _ k2))
   (iconst_u _ k2)))
   (if-let false (u64_eq k1 k2))
-  (eq select_ty inner_cond (all_zero inner_ty)))
+  (eq inner_ty inner_cond (all_zero inner_ty)))
 
 (rule (simplify (ne _
-  (select select_ty inner_cond @ (value_type inner_ty)
+  (select _ inner_cond @ (value_type inner_ty)
     (iconst_u _ k1)
     (iconst_u _ k2))
   (iconst_u _ k1)))
   (if-let false (u64_eq k1 k2))
-  (eq select_ty inner_cond (all_zero inner_ty)))
+  (eq inner_ty inner_cond (all_zero inner_ty)))
 
 (rule (simplify (ne _
-  (select select_ty inner_cond @ (value_type inner_ty)
+  (select _ inner_cond @ (value_type inner_ty)
     (iconst_u _ k1)
     (iconst_u _ k2))
   (iconst_u _ k2)))
   (if-let false (u64_eq k1 k2))
-  (ne select_ty inner_cond (all_zero inner_ty)))
+  (ne inner_ty inner_cond (all_zero inner_ty)))
 
 ;;;;; Boolean-context simplifications for `ctz` and `clz` ;;;;;;;;;;;;;;;;;;;;;;
 ;;
@@ -460,50 +462,50 @@
 ;; `brif (ctz X) bt be` branches when `ctz(X) != 0`, i.e. LSB(X) == 0.
 (rule (simplify_skeleton (brif (ctz x_ty X) _ _))
       (replace_branch_cond
-        (eq $I8 (band x_ty X (iconst_u x_ty 1)) (all_zero x_ty))))
+        (eq x_ty (band x_ty X (iconst_u x_ty 1)) (all_zero x_ty))))
 
 ;; `brif (clz X) bt be` branches when `clz(X) != 0`, i.e. MSB(X) == 0.
 (rule (simplify_skeleton (brif (clz x_ty X) _ _))
-      (replace_branch_cond (sge $I8 X (all_zero x_ty))))
+      (replace_branch_cond (sge x_ty X (all_zero x_ty))))
 
 ;; Same when an `ireduce` (truncation) sits between the count and the
 ;; brif. The count is in [0, bitwidth] so the truncation is lossless.
 (rule (simplify_skeleton (brif (ireduce _ (ctz x_ty x)) _ _))
       (replace_branch_cond
-        (eq $I8 (band x_ty x (iconst_u x_ty 1)) (all_zero x_ty))))
+        (eq x_ty (band x_ty x (iconst_u x_ty 1)) (all_zero x_ty))))
 
 (rule (simplify_skeleton (brif (ireduce _ (clz x_ty x)) _ _))
-      (replace_branch_cond (sge $I8 x (all_zero x_ty))))
+      (replace_branch_cond (sge x_ty x (all_zero x_ty))))
 
 ;; ~x == x --> 0
-(rule (simplify (eq ty (bnot cty x) x)) (subsume (all_zero ty)))
+(rule (simplify (has_type ty (eq _ (bnot cty x) x))) (subsume (all_zero ty)))
 
 ;; ~x != x --> 1
-(rule (simplify (ne ty (bnot cty x) x)) (subsume (cmp_true ty)))
+(rule (simplify (has_type ty (ne _ (bnot cty x) x))) (subsume (cmp_true ty)))
 
 ;; x >=u (x - y) --> x >=u y
 (rule (simplify (uge rty x (isub ty x y))) (uge rty x y))
 (rule (simplify (ult rty x (isub ty x y))) (ult rty x y))
 
 ;; x >=u (x >>u y) --> true
-(rule (simplify (uge rty x (ushr ty x y))) (cmp_true rty))
-(rule (simplify (ule rty (ushr ty x y) x)) (cmp_true rty))
-(rule (simplify (ugt rty (ushr ty x y) x)) (subsume (all_zero rty)))
-(rule (simplify (ult rty x (ushr ty x y))) (subsume (all_zero rty)))
+(rule (simplify (has_type rty (uge _ x (ushr ty x y)))) (cmp_true rty))
+(rule (simplify (has_type rty (ule _ (ushr ty x y) x))) (cmp_true rty))
+(rule (simplify (has_type rty (ugt _ (ushr ty x y) x))) (subsume (all_zero rty)))
+(rule (simplify (has_type rty (ult _ x (ushr ty x y)))) (subsume (all_zero rty)))
 
 ;; smin(x, y) > smax(x, y) --> false
-(rule (simplify (sgt ty (smin cty x y) (smax cty x y))) (all_zero ty))
+(rule (simplify (has_type ty (sgt _ (smin cty x y) (smax cty x y)))) (all_zero ty))
 
 ;; umin(x, y) > umax(x, y) --> false
-(rule (simplify (ugt ty (umin cty x y) (umax cty x y))) (all_zero ty))
+(rule (simplify (has_type ty (ugt _ (umin cty x y) (umax cty x y)))) (all_zero ty))
 
 ;; smin(x, y) <= smax(x, y) --> true
-(rule (simplify (sle ty (smin cty x y) (smax cty x y))) (cmp_true ty))
-(rule (simplify (sle ty (smin cty x y) (smax cty y x))) (cmp_true ty))
+(rule (simplify (has_type ty (sle _ (smin cty x y) (smax cty x y)))) (cmp_true ty))
+(rule (simplify (has_type ty (sle _ (smin cty x y) (smax cty y x)))) (cmp_true ty))
 
 ;; umin(x, y) <= umax(x, y) --> true
-(rule (simplify (ule ty (umin cty x y) (umax cty x y))) (cmp_true ty))
-(rule (simplify (ule ty (umin cty x y) (umax cty y x))) (cmp_true ty))
+(rule (simplify (has_type ty (ule _ (umin cty x y) (umax cty x y)))) (cmp_true ty))
+(rule (simplify (has_type ty (ule _ (umin cty x y) (umax cty y x)))) (cmp_true ty))
 
 ;; smin(x, y) == smax(x, y) --> x == y
 (rule (simplify (eq ty (smin cty x y) (smax cty x y))) (eq ty x y))
@@ -547,16 +549,16 @@
       (subsume (eq ty x y)))
 
 ;; (x >=s 0) & (x <s N) --> x <u N, 0 < N < 2^(B - 1)
-(rule (simplify (band rty
-                     (sge rty x (all_zero ty))
-                     (slt rty x n @ (iconst_s (ty_int ty) limit))))
+(rule (simplify (band _
+                     (sge ty x (all_zero ty))
+                     (slt ty x n @ (iconst_s (ty_int ty) limit))))
       (if-let true (i64_gt limit 0))
-      (ult rty x n))
-(rule (simplify (band rty
-                     (slt rty x n @ (iconst_s (ty_int ty) limit))
-                     (sge rty x (all_zero ty))))
+      (ult ty x n))
+(rule (simplify (band _
+                     (slt ty x n @ (iconst_s (ty_int ty) limit))
+                     (sge ty x (all_zero ty))))
       (if-let true (i64_gt limit 0))
-      (ult rty x n))
+      (ult ty x n))
 
 ;; x == ((x + (y >>u (B - k))) & -2^k) --> (x & (2^k - 1)) == 0
 (rule (simplify (eq rty x
@@ -607,10 +609,10 @@
                       (all_zero ty))))
 
 ;; (x == y) ^ 1 --> x != y
-(rule (simplify (bxor ty
-                      (eq ty x @ (value_type cty) y @ (value_type cty))
-                      (iconst_u ty 1)))
-      (ne ty x y))
+(rule (simplify (bxor bty
+                      (eq cty x y)
+                      (iconst_u bty 1)))
+      (ne cty x y))
 
 ;; x >u (x - 1) --> x != 0
 (rule (simplify (ugt ty x (isub cty x (iconst_u cty 1))))
@@ -623,6 +625,6 @@
       (subsume (eq ty x y)))
 
 ;; (x != 0) | (y != 0) --> (x | y) != 0
-(rule (simplify (bor ty (ne ty x (iconst_u cty 0)) (ne ty y (iconst_u cty 0)))) (ne ty (bor cty x y) (all_zero cty)))
+(rule (simplify (bor _ (ne cty x (iconst_u cty 0)) (ne cty y (iconst_u cty 0)))) (ne cty (bor cty x y) (all_zero cty)))
 ;; (x == 0) & (y == 0) --> (x | y) == 0
-(rule (simplify (band ty (eq ty x (iconst_u cty 0)) (eq ty y (iconst_u cty 0)))) (eq ty (bor cty x y) (all_zero cty)))
+(rule (simplify (band _ (eq cty x (iconst_u cty 0)) (eq cty y (iconst_u cty 0)))) (eq cty (bor cty x y) (all_zero cty)))
diff --git a/cranelift/codegen/src/opts/selects.isle b/cranelift/codegen/src/opts/selects.isle
index c61df8a22ef8..6a6a9129f382 100644
--- a/cranelift/codegen/src/opts/selects.isle
+++ b/cranelift/codegen/src/opts/selects.isle
@@ -110,14 +110,14 @@
 (rule (simplify (select ty d (select ty d x _) a)) (select ty d x a))
 
 ;; min x y < x => false and its commutative versions
-(rule (simplify (sgt (fits_in_64 ty) (smin _ x y) x)) (all_zero ty))
-(rule (simplify (sgt (fits_in_64 ty) (smin _ x y) y)) (all_zero ty))
-(rule (simplify (slt (fits_in_64 ty) x (smin _ x z))) (all_zero ty))
-(rule (simplify (slt (fits_in_64 ty) x (smin _ y x))) (all_zero ty))
-(rule (simplify (ugt (fits_in_64 ty) (umin _ x y) x)) (all_zero ty))
-(rule (simplify (ugt (fits_in_64 ty) (umin _ x y) y)) (all_zero ty))
-(rule (simplify (ult (fits_in_64 ty) x (umin _ x z))) (all_zero ty))
-(rule (simplify (ult (fits_in_64 ty) x (umin _ y x))) (all_zero ty))
+(rule (simplify (has_type ty (sgt (fits_in_64 _) (smin _ x y) x))) (all_zero ty))
+(rule (simplify (has_type ty (sgt (fits_in_64 _) (smin _ x y) y))) (all_zero ty))
+(rule (simplify (has_type ty (slt (fits_in_64 _) x (smin _ x z)))) (all_zero ty))
+(rule (simplify (has_type ty (slt (fits_in_64 _) x (smin _ y x)))) (all_zero ty))
+(rule (simplify (has_type ty (ugt (fits_in_64 _) (umin _ x y) x))) (all_zero ty))
+(rule (simplify (has_type ty (ugt (fits_in_64 _) (umin _ x y) y))) (all_zero ty))
+(rule (simplify (has_type ty (ult (fits_in_64 _) x (umin _ x z)))) (all_zero ty))
+(rule (simplify (has_type ty (ult (fits_in_64 _) x (umin _ y x)))) (all_zero ty))
 
 ;; (x == y) ? x : y => y
 ;; select(eq/ne) patterns that always collapse to y.
@@ -127,10 +127,10 @@
 (rule (simplify (select ty (ne cty y x) y x)) (subsume y))
 
 ;; (x | (y != z)) ? y : z  ==> y
-(rule (simplify (select ty (bor cty x (ne cty y z)) y z)) (subsume y))
-(rule (simplify (select ty (bor cty (ne cty y z) x) y z)) (subsume y))
-(rule (simplify (select ty (bor cty x (ne cty z y)) y z)) (subsume y))
-(rule (simplify (select ty (bor cty (ne cty z y) x) y z)) (subsume y))
+(rule (simplify (select ty (bor _ x (ne _ y z)) y z)) (subsume y))
+(rule (simplify (select ty (bor _ (ne _ y z) x) y z)) (subsume y))
+(rule (simplify (select ty (bor _ x (ne _ z y)) y z)) (subsume y))
+(rule (simplify (select ty (bor _ (ne _ z y) x) y z)) (subsume y))
 
 ;; (x == y) ? x : (x | y)  ==> (x | y)
 ;; and equivalent operand-order variants.
@@ -156,33 +156,33 @@
 
 ;; (x <_u y) ? 1 : (x == y)  ==> (x <=_u y)
 ;; and equivalent operand-order variants.
-(rule (simplify (select ty (ult cty x y) (iconst_u ty 1) (eq ty x y))) (ule ty x y))
-(rule (simplify (select ty (uge cty x y) (eq ty x y) (iconst_u ty 1))) (ule ty x y))
-(rule (simplify (select ty (ugt cty y x) (iconst_u ty 1) (eq ty x y))) (ule ty x y))
-(rule (simplify (select ty (ule cty y x) (eq ty x y) (iconst_u ty 1))) (ule ty x y))
-(rule (simplify (select ty (ult cty x y) (iconst_u ty 1) (eq ty y x))) (ule ty x y))
-(rule (simplify (select ty (uge cty x y) (eq ty y x) (iconst_u ty 1))) (ule ty x y))
-(rule (simplify (select ty (ugt cty y x) (iconst_u ty 1) (eq ty y x))) (ule ty x y))
-(rule (simplify (select ty (ule cty y x) (eq ty y x) (iconst_u ty 1))) (ule ty x y))
+(rule (simplify (select ty (ult cty x y) (iconst_u ty 1) (eq cty x y))) (ule cty x y))
+(rule (simplify (select ty (uge cty x y) (eq cty x y) (iconst_u ty 1))) (ule cty x y))
+(rule (simplify (select ty (ugt cty y x) (iconst_u ty 1) (eq cty x y))) (ule cty x y))
+(rule (simplify (select ty (ule cty y x) (eq cty x y) (iconst_u ty 1))) (ule cty x y))
+(rule (simplify (select ty (ult cty x y) (iconst_u ty 1) (eq cty y x))) (ule cty x y))
+(rule (simplify (select ty (uge cty x y) (eq cty y x) (iconst_u ty 1))) (ule cty x y))
+(rule (simplify (select ty (ugt cty y x) (iconst_u ty 1) (eq cty y x))) (ule cty x y))
+(rule (simplify (select ty (ule cty y x) (eq cty y x) (iconst_u ty 1))) (ule cty x y))
 
 ;; (x < y) ? 1 : (x > y)  ==> (x != y)
 ;; and equivalent operand-order variants.
-(rule (simplify (select ty (slt cty x y) (iconst_u ty 1) (sgt ty x y))) (ne ty x y))
-(rule (simplify (select ty (sge cty x y) (sgt ty x y) (iconst_u ty 1))) (ne ty x y))
-(rule (simplify (select ty (sgt cty y x) (iconst_u ty 1) (sgt ty x y))) (ne ty x y))
-(rule (simplify (select ty (sle cty y x) (sgt ty x y) (iconst_u ty 1))) (ne ty x y))
-(rule (simplify (select ty (slt cty x y) (iconst_u ty 1) (slt ty y x))) (ne ty x y))
-(rule (simplify (select ty (sge cty x y) (slt ty y x) (iconst_u ty 1))) (ne ty x y))
-(rule (simplify (select ty (sgt cty y x) (iconst_u ty 1) (slt ty y x))) (ne ty x y))
-(rule (simplify (select ty (sle cty y x) (slt ty y x) (iconst_u ty 1))) (ne ty x y))
-(rule (simplify (select ty (ult cty x y) (iconst_u ty 1) (ugt ty x y))) (ne ty x y))
-(rule (simplify (select ty (uge cty x y) (ugt ty x y) (iconst_u ty 1))) (ne ty x y))
-(rule (simplify (select ty (ugt cty y x) (iconst_u ty 1) (ugt ty x y))) (ne ty x y))
-(rule (simplify (select ty (ule cty y x) (ugt ty x y) (iconst_u ty 1))) (ne ty x y))
-(rule (simplify (select ty (ult cty x y) (iconst_u ty 1) (ult ty y x))) (ne ty x y))
-(rule (simplify (select ty (uge cty x y) (ult ty y x) (iconst_u ty 1))) (ne ty x y))
-(rule (simplify (select ty (ugt cty y x) (iconst_u ty 1) (ult ty y x))) (ne ty x y))
-(rule (simplify (select ty (ule cty y x) (ult ty y x) (iconst_u ty 1))) (ne ty x y))
+(rule (simplify (select ty (slt cty x y) (iconst_u ty 1) (sgt cty x y))) (ne cty x y))
+(rule (simplify (select ty (sge cty x y) (sgt cty x y) (iconst_u ty 1))) (ne cty x y))
+(rule (simplify (select ty (sgt cty y x) (iconst_u ty 1) (sgt cty x y))) (ne cty x y))
+(rule (simplify (select ty (sle cty y x) (sgt cty x y) (iconst_u ty 1))) (ne cty x y))
+(rule (simplify (select ty (slt cty x y) (iconst_u ty 1) (slt cty y x))) (ne cty x y))
+(rule (simplify (select ty (sge cty x y) (slt cty y x) (iconst_u ty 1))) (ne cty x y))
+(rule (simplify (select ty (sgt cty y x) (iconst_u ty 1) (slt cty y x))) (ne cty x y))
+(rule (simplify (select ty (sle cty y x) (slt cty y x) (iconst_u ty 1))) (ne cty x y))
+(rule (simplify (select ty (ult cty x y) (iconst_u ty 1) (ugt cty x y))) (ne cty x y))
+(rule (simplify (select ty (uge cty x y) (ugt cty x y) (iconst_u ty 1))) (ne cty x y))
+(rule (simplify (select ty (ugt cty y x) (iconst_u ty 1) (ugt cty x y))) (ne cty x y))
+(rule (simplify (select ty (ule cty y x) (ugt cty x y) (iconst_u ty 1))) (ne cty x y))
+(rule (simplify (select ty (ult cty x y) (iconst_u ty 1) (ult cty y x))) (ne cty x y))
+(rule (simplify (select ty (uge cty x y) (ult cty y x) (iconst_u ty 1))) (ne cty x y))
+(rule (simplify (select ty (ugt cty y x) (iconst_u ty 1) (ult cty y x))) (ne cty x y))
+(rule (simplify (select ty (ule cty y x) (ult cty y x) (iconst_u ty 1))) (ne cty x y))
 
 ;; (x ? 1 : (x | y))  ==>  (x ? 1 : y)
 (rule (simplify (select ty x (iconst_u ty 1) (bor ty x y))) (select ty x (iconst_u ty 1) y))
@@ -196,10 +196,10 @@
 (rule (simplify (select ty (ne cty (iconst_u ty n) x) (isub ty y x) (isub ty y (iconst_u ty n)))) (isub ty y x))
 
 ;; select(cond, eq(z, y), eq(p, y))  ==>  eq(y, select(cond, z, p))
-(rule (simplify (select ty x (eq ty z y) (eq ty (iconst_u cty p) y))) (eq ty y (select cty x z (iconst_u cty p))))
-(rule (simplify (select ty x (eq ty z y) (eq ty y (iconst_u cty p)))) (eq ty y (select cty x z (iconst_u cty p))))
-(rule (simplify (select ty x (eq ty y z) (eq ty (iconst_u cty p) y))) (eq ty y (select cty x z (iconst_u cty p))))
-(rule (simplify (select ty x (eq ty y z) (eq ty y (iconst_u cty p)))) (eq ty y (select cty x z (iconst_u cty p))))
+(rule (simplify (select _ x (eq cty z y) (eq cty (iconst_u cty p) y))) (eq cty y (select cty x z (iconst_u cty p))))
+(rule (simplify (select _ x (eq cty z y) (eq cty y (iconst_u cty p)))) (eq cty y (select cty x z (iconst_u cty p))))
+(rule (simplify (select _ x (eq cty y z) (eq cty (iconst_u cty p) y))) (eq cty y (select cty x z (iconst_u cty p))))
+(rule (simplify (select _ x (eq cty y z) (eq cty y (iconst_u cty p)))) (eq cty y (select cty x z (iconst_u cty p))))
 
 ;; (x == y) ? 0 : (x - y) --> x - y
 (rule (simplify (select ty (eq cty x y) (all_zero ty) (isub ty x y)))
diff --git a/cranelift/codegen/src/opts/spaceship.isle b/cranelift/codegen/src/opts/spaceship.isle
index a834aa49e4cf..840721fd8430 100644
--- a/cranelift/codegen/src/opts/spaceship.isle
+++ b/cranelift/codegen/src/opts/spaceship.isle
@@ -54,7 +54,7 @@
 ;; x > y ? 1 : x >= y ? 0 : -1
 (rule (simplify (select ty (ugt rty x y)
                            (iconst_s ty 1)
-                           (ineg rty (ult rty x y))))
+                           (ineg ty (ult rty x y))))
       (sextend_maybe ty (spaceship_u rty x y)))
 (rule (simplify (select ty (ugt rty x y)
                            (iconst_s ty 1)
@@ -64,7 +64,7 @@
 ;; x > y ? 1 : x == y ? 0 : -1
 (rule (simplify (select ty (ugt rty x y)
                            (iconst_s ty 1)
-                           (ineg rty (ne rty x y))))
+                           (ineg ty (ne rty x y))))
       (sextend_maybe ty (spaceship_u rty x y)))
 (rule (simplify (select ty (ugt rty x y)
                            (iconst_s ty 1)
@@ -119,7 +119,7 @@
 ;; x > y ? 1 : x >= y ? 0 : -1
 (rule (simplify (select ty (sgt rty x y)
                            (iconst_s ty 1)
-                           (ineg rty (slt rty x y))))
+                           (ineg ty (slt rty x y))))
       (sextend_maybe ty (spaceship_s rty x y)))
 (rule (simplify (select ty (sgt rty x y)
                            (iconst_s ty 1)
@@ -129,7 +129,7 @@
 ;; x > y ? 1 : x == y ? 0 : -1
 (rule (simplify (select ty (sgt rty x y)
                            (iconst_s ty 1)
-                           (ineg rty (ne rty x y))))
+                           (ineg ty (ne rty x y))))
       (sextend_maybe ty (spaceship_s rty x y)))
 (rule (simplify (select ty (sgt rty x y)
                            (iconst_s ty 1)
diff --git a/cranelift/codegen/src/opts/vector.isle b/cranelift/codegen/src/opts/vector.isle
index 5ad57d8dc604..0072a64725bb 100644
--- a/cranelift/codegen/src/opts/vector.isle
+++ b/cranelift/codegen/src/opts/vector.isle
@@ -82,8 +82,8 @@
       (splat ty (sshr (lane_type ty) x y)))
 
 ;; {u,s}widen_{low,high}+splat is the same as splat+{u,s}extend
-(rule (simplify (swiden_high wide (splat _ x))) (splat wide (sextend (lane_type wide) x)))
-(rule (simplify (swiden_low wide (splat _ x))) (splat wide (sextend (lane_type wide) x)))
+(rule (simplify (has_type wide (swiden_high _ (splat _ x)))) (splat wide (sextend (lane_type wide) x)))
+(rule (simplify (has_type wide (swiden_low _ (splat _ x)))) (splat wide (sextend (lane_type wide) x)))
 
-(rule (simplify (uwiden_high wide (splat _ x))) (splat wide (uextend (lane_type wide) x)))
-(rule (simplify (uwiden_low wide (splat _ x))) (splat wide (uextend (lane_type wide) x)))
+(rule (simplify (has_type wide (uwiden_high _ (splat _ x)))) (splat wide (uextend (lane_type wide) x)))
+(rule (simplify (has_type wide (uwiden_low _ (splat _ x)))) (splat wide (uextend (lane_type wide) x)))
diff --git a/cranelift/codegen/src/prelude_opt.isle b/cranelift/codegen/src/prelude_opt.isle
index e76d27f36854..d8eb08cf4057 100644
--- a/cranelift/codegen/src/prelude_opt.isle
+++ b/cranelift/codegen/src/prelude_opt.isle
@@ -11,9 +11,21 @@
 ;;;;; eclass and enode access ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
 ;; Extract any node(s) for the given eclass ID.
+;;
+;; The `Type` is the instruction's *controlling* type (not necessarily its
+;; result type).
 (decl multi inst_data_value (Type InstructionData) Value)
 (extern extractor inst_data_value inst_data_value_etor)
 
+;; Bind the type of a `Value` while also matching it against a sub-pattern,
+;; mirroring `has_type` in the lowering prelude. Use this when a rule needs
+;; the *result* type of an instruction differs from its controlling type.
+(spec (has_type ty arg)
+      (provide (= result arg)
+               (= (:bits ty) (widthof arg)) (= (:lanes ty) (lanesof arg))))
+(decl has_type (Type Value) Value)
+(extractor (has_type ty val) (and (value_type ty) val))
+
 ;; An extractor from an `Inst` to its `InstructionData`.
 (decl inst_data (InstructionData) Inst)
 (extern extractor inst_data inst_data_etor)
@@ -27,7 +39,8 @@
 (extern extractor inst_data_value_tupled inst_data_value_tupled_etor)
 
 ;; Construct a pure node, returning a new (or deduplicated
-;; already-existing) eclass ID.
+;; already-existing) eclass ID. The `Type` is the instruction's controlling
+;; type; see `inst_data_value`.
 (decl make_inst (Type InstructionData) Value)
 (extern constructor make_inst make_inst_ctor)
 
diff --git a/cranelift/codegen/src/spec/inst_specs.isle b/cranelift/codegen/src/spec/inst_specs.isle
index 4867cbf3c961..68c44141b8aa 100644
--- a/cranelift/codegen/src/spec/inst_specs.isle
+++ b/cranelift/codegen/src/spec/inst_specs.isle
@@ -598,6 +598,9 @@
 
 (spec (icmp ty cc x y)
     (provide
+        ;; `ty` is the controlling type: the operand type, not the result type.
+        (= (:bits ty) (widthof x))
+        (= (:lanes ty) (lanesof x))
         (= result
             (if
                 (match cc
@@ -879,6 +882,9 @@
 ; fcmp: floating-point compare.
 (spec (fcmp ty c x y)
     (provide
+        ;; `ty` is the controlling type: the operand type, not the result type.
+        (= (:bits ty) (widthof x))
+        (= (:lanes ty) (lanesof x))
         ;; Restrict to operations used from Wasm for now
         (or (= c (FloatCC.Equal))
             (= c (FloatCC.NotEqual))
diff --git a/cranelift/codegen/src/spec/opt.isle b/cranelift/codegen/src/spec/opt.isle
index 78f75b131890..bd50df5599ea 100644
--- a/cranelift/codegen/src/spec/opt.isle
+++ b/cranelift/codegen/src/spec/opt.isle
@@ -133,7 +133,10 @@
 (spec (u64_lt x y) (provide (= result (bvult x y))))
 (spec (imm64 x) (provide (= result x)))
 
-(spec (cmp_true ty) (provide (= result (zero_ext (widthof result) #b1))))
+(spec (cmp_true ty)
+    (provide (= result (zero_ext (widthof result) #b1))
+             (= (:bits ty) (widthof result))
+             (= (:lanes ty) (lanesof result))))
 (instantiate cmp_true
     ((args (named Type)) (ret (bv  8)))
     ((args (named Type)) (ret (bv 16)))
@@ -654,7 +657,13 @@
             ((SignedGreaterThanOrEqual) (int2bv 64 5))
             ((NotEqual) (int2bv 64 6))))))
 (macro (icmp_bit c) (if c #x01 #x00))
-(spec (compose_icmp ty v signed x y)
+(spec (compose_icmp rty ty v signed x y)
+    ;; `compose_icmp` is verified as a root term, so the operand type tie is a
+    ;; requirement (assumed here, discharged at the `band`/`bor` call sites).
+    ;; `rty` only selects the constant's type; the result width comes from the
+    ;; instantiation.
+    (require (= (:bits ty) (widthof x))
+             (= (:lanes ty) (lanesof x)))
     (provide (= result
         (if (= v (int2bv 64 0)) #x00
         (if (= v (int2bv 64 1)) (icmp_bit! (= x y))
@@ -665,9 +674,12 @@
         (if (= v (int2bv 64 6)) (icmp_bit! (not (= x y)))
         #x01))))))))))
 
-;; Reached only at `ty = I8` (icmp results are `(bv 8)`), so all operands/result bv8.
+;; `rty` is the comparison's result type (`i8`), `ty` its operand type.
 (instantiate compose_icmp
-    ((args (named Type) (bv 64) Bool (bv 8) (bv 8)) (ret (bv 8))))
+    ((args (named Type) (named Type) (bv 64) Bool (bv  8) (bv  8)) (ret (bv 8)))
+    ((args (named Type) (named Type) (bv 64) Bool (bv 16) (bv 16)) (ret (bv 8)))
+    ((args (named Type) (named Type) (bv 64) Bool (bv 32) (bv 32)) (ret (bv 8)))
+    ((args (named Type) (named Type) (bv 64) Bool (bv 64) (bv 64)) (ret (bv 8))))
 
 ;;;; Bit-manipulation instructions ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; `bitrev` = `rev`. `bmask` broadcasts truthiness to an all-ones/all-zeros mask of
diff --git a/cranelift/filetests/filetests/egraph/arithmetic-precise.clif b/cranelift/filetests/filetests/egraph/arithmetic-precise.clif
index d8538950aa90..95028dce7b18 100644
--- a/cranelift/filetests/filetests/egraph/arithmetic-precise.clif
+++ b/cranelift/filetests/filetests/egraph/arithmetic-precise.clif
@@ -307,10 +307,8 @@ block0(v0: i32, v1: i32):
 
 ; function %test_eq_ineg_ineg(i32, i32) -> i8 fast {
 ; block0(v0: i32, v1: i32):
-;     v2 = ineg v0
-;     v3 = ineg v1
-;     v4 = icmp eq v2, v3
-;     return v4
+;     v5 = icmp eq v0, v1
+;     return v5
 ; }
 
 ;; -((-y) * x) --> x * y
@@ -352,9 +350,8 @@ block0(v0: i32, v1: i32):
 
 ; function %test_sge_smax_x(i32, i32) -> i8 fast {
 ; block0(v0: i32, v1: i32):
-;     v2 = smax v0, v1
-;     v3 = icmp sge v2, v0
-;     return v3
+;     v4 = iconst.i8 1
+;     return v4  ; v4 = 1
 ; }
 
 ;; x <=_u umax(x, y) --> true
@@ -367,9 +364,8 @@ block0(v0: i32, v1: i32):
 
 ; function %test_ule_x_umax(i32, i32) -> i8 fast {
 ; block0(v0: i32, v1: i32):
-;     v2 = umax v0, v1
-;     v3 = icmp ule v0, v2
-;     return v3
+;     v4 = iconst.i8 1
+;     return v4  ; v4 = 1
 ; }
 
 ;; x >= smin(x, y) --> true
@@ -382,9 +378,8 @@ block0(v0: i32, v1: i32):
 
 ; function %test_sge_x_smin(i32, i32) -> i8 fast {
 ; block0(v0: i32, v1: i32):
-;     v2 = smin v0, v1
-;     v3 = icmp sge v0, v2
-;     return v3
+;     v4 = iconst.i8 1
+;     return v4  ; v4 = 1
 ; }
 
 ;; umin(x, y) <=_u x --> true
@@ -397,9 +392,8 @@ block0(v0: i32, v1: i32):
 
 ; function %test_ule_umin_x(i32, i32) -> i8 fast {
 ; block0(v0: i32, v1: i32):
-;     v2 = umin v0, v1
-;     v3 = icmp ule v2, v0
-;     return v3
+;     v4 = iconst.i8 1
+;     return v4  ; v4 = 1
 ; }
 
 ;; umin(x, x) --> x
@@ -542,9 +536,8 @@ block0(v0: i32, v1: i32):
 
 ; function %test_sgt_x_smax(i32, i32) -> i8 fast {
 ; block0(v0: i32, v1: i32):
-;     v2 = smax v0, v1
-;     v3 = icmp sgt v0, v2
-;     return v3
+;     v4 = iconst.i8 0
+;     return v4  ; v4 = 0
 ; }
 
 ;; x >_u umax(x, y) --> false
@@ -557,9 +550,8 @@ block0(v0: i32, v1: i32):
 
 ; function %test_ugt_x_umax(i32, i32) -> i8 fast {
 ; block0(v0: i32, v1: i32):
-;     v2 = umax v0, v1
-;     v3 = icmp ugt v0, v2
-;     return v3
+;     v4 = iconst.i8 0
+;     return v4  ; v4 = 0
 ; }
 
 function %udiv_shift_i32(i32, i32) -> i32 {
diff --git a/cranelift/filetests/filetests/egraph/cprop.clif b/cranelift/filetests/filetests/egraph/cprop.clif
index 904dc90ad37c..7ed2c4275c1c 100644
--- a/cranelift/filetests/filetests/egraph/cprop.clif
+++ b/cranelift/filetests/filetests/egraph/cprop.clif
@@ -507,8 +507,8 @@ block0:
     return v3
 }
 
-; check: v4 = f16const -0x1.500p7
-; check: return v4  ; v4 = -0x1.500p7
+; check: v2 = f16const -0x1.500p7
+; check: return v2  ; v2 = -0x1.500p7
 
 function %f16_fmin_zero_1() -> f16 {
 block0:
@@ -518,8 +518,8 @@ block0:
     return v3
 }
 
-; check: v4 = f16const -0.0
-; check: return v4  ; v4 = -0.0
+; check: v2 = f16const -0.0
+; check: return v2  ; v2 = -0.0
 
 function %f16_fmin_zero_2() -> f16 {
 block0:
@@ -529,8 +529,8 @@ block0:
     return v3
 }
 
-; check: v4 = f16const -0.0
-; check: return v4  ; v4 = -0.0
+; check: v1 = f16const -0.0
+; check: return v1  ; v1 = -0.0
 
 function %f16_fmin_promotes_correctly() -> f64 {
 block0:
@@ -541,8 +541,8 @@ block0:
     return v4
 }
 
-; check: v5 = f16const 0x1.000p0
-; check: v4 = fpromote.f64 v5  ; v5 = 0x1.000p0
+; check: v1 = f16const 0x1.000p0
+; check: v4 = fpromote.f64 v1  ; v1 = 0x1.000p0
 ; check: return v4
 
 function %f16_fmax() -> f16 {
@@ -553,8 +553,8 @@ block0:
     return v3
 }
 
-; check: v4 = f16const -0x1.500p6
-; check: return v4  ; v4 = -0x1.500p6
+; check: v1 = f16const -0x1.500p6
+; check: return v1  ; v1 = -0x1.500p6
 
 function %f16_fmax_zero_1() -> f16 {
 block0:
@@ -564,8 +564,8 @@ block0:
     return v3
 }
 
-; check: v4 = f16const 0.0
-; check: return v4  ; v4 = 0.0
+; check: v1 = f16const 0.0
+; check: return v1  ; v1 = 0.0
 
 function %f16_fmax_zero_2() -> f16 {
 block0:
@@ -575,8 +575,8 @@ block0:
     return v3
 }
 
-; check: v4 = f16const 0.0
-; check: return v4  ; v4 = 0.0
+; check: v2 = f16const 0.0
+; check: return v2  ; v2 = 0.0
 
 function %f16_fneg() -> f16 {
 block0:
@@ -711,8 +711,8 @@ block0:
     return v3
 }
 
-; check: v4 = f32const 0x1.500000p6
-; check: return v4  ; v4 = 0x1.500000p6
+; check: v1 = f32const 0x1.500000p6
+; check: return v1  ; v1 = 0x1.500000p6
 
 function %f32_fmin_zero_1() -> f32 {
 block0:
@@ -722,8 +722,8 @@ block0:
     return v3
 }
 
-; check: v4 = f32const -0.0
-; check: return v4  ; v4 = -0.0
+; check: v2 = f32const -0.0
+; check: return v2  ; v2 = -0.0
 
 function %f32_fmin_zero_2() -> f32 {
 block0:
@@ -733,8 +733,8 @@ block0:
     return v3
 }
 
-; check: v4 = f32const -0.0
-; check: return v4  ; v4 = -0.0
+; check: v1 = f32const -0.0
+; check: return v1  ; v1 = -0.0
 
 function %f32_fmax() -> f32 {
 block0:
@@ -744,8 +744,8 @@ block0:
     return v3
 }
 
-; check: v4 = f32const 0x1.500000p7
-; check: return v4  ; v4 = 0x1.500000p7
+; check: v2 = f32const 0x1.500000p7
+; check: return v2  ; v2 = 0x1.500000p7
 
 function %f32_fmax_zero_1() -> f32 {
 block0:
@@ -755,8 +755,8 @@ block0:
     return v3
 }
 
-; check: v4 = f32const 0.0
-; check: return v4  ; v4 = 0.0
+; check: v1 = f32const 0.0
+; check: return v1  ; v1 = 0.0
 
 function %f32_fmax_zero_2() -> f32 {
 block0:
@@ -766,8 +766,8 @@ block0:
     return v3
 }
 
-; check: v4 = f32const 0.0
-; check: return v4  ; v4 = 0.0
+; check: v2 = f32const 0.0
+; check: return v2  ; v2 = 0.0
 
 function %f32_fneg() -> f32 {
 block0:
@@ -902,8 +902,8 @@ block0:
     return v3
 }
 
-; check: v4 = f64const -0x1.5000000000000p7
-; check: return v4  ; v4 = -0x1.5000000000000p7
+; check: v2 = f64const -0x1.5000000000000p7
+; check: return v2  ; v2 = -0x1.5000000000000p7
 
 function %f64_fmin_zero_1() -> f64 {
 block0:
@@ -913,8 +913,8 @@ block0:
     return v3
 }
 
-; check: v4 = f64const -0.0
-; check: return v4  ; v4 = -0.0
+; check: v2 = f64const -0.0
+; check: return v2  ; v2 = -0.0
 
 function %f64_fmin_zero_2() -> f64 {
 block0:
@@ -924,8 +924,8 @@ block0:
     return v3
 }
 
-; check: v4 = f64const -0.0
-; check: return v4  ; v4 = -0.0
+; check: v1 = f64const -0.0
+; check: return v1  ; v1 = -0.0
 
 function %f64_fmax() -> f64 {
 block0:
@@ -935,8 +935,8 @@ block0:
     return v3
 }
 
-; check: v4 = f64const -0x1.5000000000000p6
-; check: return v4  ; v4 = -0x1.5000000000000p6
+; check: v1 = f64const -0x1.5000000000000p6
+; check: return v1  ; v1 = -0x1.5000000000000p6
 
 function %f64_fmax_zero_1() -> f64 {
 block0:
@@ -946,8 +946,8 @@ block0:
     return v3
 }
 
-; check: v4 = f64const 0.0
-; check: return v4  ; v4 = 0.0
+; check: v1 = f64const 0.0
+; check: return v1  ; v1 = 0.0
 
 function %f64_fmax_zero_2() -> f64 {
 block0:
@@ -957,8 +957,8 @@ block0:
     return v3
 }
 
-; check: v4 = f64const 0.0
-; check: return v4  ; v4 = 0.0
+; check: v2 = f64const 0.0
+; check: return v2  ; v2 = 0.0
 
 function %f64_fneg() -> f64 {
 block0:
@@ -1000,8 +1000,8 @@ block0:
 }
 
 ; check: const0 = 0x40055000000000000000000000000000
-; check: v4 = f128const const0
-; check: return v4  ; v4 = 0x1.5000000000000000000000000000p6
+; check: v1 = f128const const0
+; check: return v1  ; v1 = 0x1.5000000000000000000000000000p6
 
 function %f128_fmin_zero_1() -> f128 {
 block0:
@@ -1012,8 +1012,8 @@ block0:
 }
 
 ; check: const1 = 0x80000000000000000000000000000000
-; check: v4 = f128const const1
-; check: return v4  ; v4 = -0.0
+; check: v2 = f128const const1
+; check: return v2  ; v2 = -0.0
 
 function %f128_fmin_zero_2() -> f128 {
 block0:
@@ -1024,8 +1024,8 @@ block0:
 }
 
 ; check: const0 = 0x80000000000000000000000000000000
-; check: v4 = f128const const0
-; check: return v4  ; v4 = -0.0
+; check: v1 = f128const const0
+; check: return v1  ; v1 = -0.0
 
 function %f128_fmax() -> f128 {
 block0:
@@ -1036,8 +1036,8 @@ block0:
 }
 
 ; check: const1 = 0x40065000000000000000000000000000
-; check: v4 = f128const const1
-; check: return v4  ; v4 = 0x1.5000000000000000000000000000p7
+; check: v2 = f128const const1
+; check: return v2  ; v2 = 0x1.5000000000000000000000000000p7
 
 function %f128_fmax_zero_1() -> f128 {
 block0:
@@ -1048,8 +1048,8 @@ block0:
 }
 
 ; check: const0 = 0x00000000000000000000000000000000
-; check: v4 = f128const const0
-; check: return v4  ; v4 = 0.0
+; check: v1 = f128const const0
+; check: return v1  ; v1 = 0.0
 
 function %f128_fmax_zero_2() -> f128 {
 block0:
@@ -1060,8 +1060,8 @@ block0:
 }
 
 ; check: const1 = 0x00000000000000000000000000000000
-; check: v4 = f128const const1
-; check: return v4  ; v4 = 0.0
+; check: v2 = f128const const1
+; check: return v2  ; v2 = 0.0
 
 function %f128_fneg() -> f128 {
 block0:
diff --git a/cranelift/filetests/filetests/egraph/icmp-parameterized.clif b/cranelift/filetests/filetests/egraph/icmp-parameterized.clif
index a99f4c0d8b4b..a1948019c9ef 100644
--- a/cranelift/filetests/filetests/egraph/icmp-parameterized.clif
+++ b/cranelift/filetests/filetests/egraph/icmp-parameterized.clif
@@ -761,8 +761,8 @@ block0(v0: i32, v1: i32):
 
 ; function %icmp_and_eq_ule(i32, i32) -> i8 fast {
 ; block0(v0: i32, v1: i32):
-;     v5 = icmp eq v0, v1
-;     return v5
+;     v2 = icmp eq v0, v1
+;     return v2
 ; }
 
 function %icmp_and_eq_ugt(i32, i32) -> i8 {
@@ -789,8 +789,8 @@ block0(v0: i32, v1: i32):
 
 ; function %icmp_and_eq_uge(i32, i32) -> i8 fast {
 ; block0(v0: i32, v1: i32):
-;     v5 = icmp eq v0, v1
-;     return v5
+;     v2 = icmp eq v0, v1
+;     return v2
 ; }
 
 function %icmp_and_eq_slt(i32, i32) -> i8 {
@@ -817,8 +817,8 @@ block0(v0: i32, v1: i32):
 
 ; function %icmp_and_eq_sle(i32, i32) -> i8 fast {
 ; block0(v0: i32, v1: i32):
-;     v5 = icmp eq v0, v1
-;     return v5
+;     v2 = icmp eq v0, v1
+;     return v2
 ; }
 
 function %icmp_and_eq_sgt(i32, i32) -> i8 {
@@ -845,8 +845,8 @@ block0(v0: i32, v1: i32):
 
 ; function %icmp_and_eq_sge(i32, i32) -> i8 fast {
 ; block0(v0: i32, v1: i32):
-;     v5 = icmp eq v0, v1
-;     return v5
+;     v2 = icmp eq v0, v1
+;     return v2
 ; }
 
 function %icmp_and_ne_eq(i32, i32) -> i8 {
@@ -887,8 +887,8 @@ block0(v0: i32, v1: i32):
 
 ; function %icmp_and_ne_ult(i32, i32) -> i8 fast {
 ; block0(v0: i32, v1: i32):
-;     v5 = icmp ult v0, v1
-;     return v5
+;     v3 = icmp ult v0, v1
+;     return v3
 ; }
 
 function %icmp_and_ne_ule(i32, i32) -> i8 {
@@ -915,8 +915,8 @@ block0(v0: i32, v1: i32):
 
 ; function %icmp_and_ne_ugt(i32, i32) -> i8 fast {
 ; block0(v0: i32, v1: i32):
-;     v5 = icmp ugt v0, v1
-;     return v5
+;     v3 = icmp ugt v0, v1
+;     return v3
 ; }
 
 function %icmp_and_ne_uge(i32, i32) -> i8 {
@@ -943,8 +943,8 @@ block0(v0: i32, v1: i32):
 
 ; function %icmp_and_ne_slt(i32, i32) -> i8 fast {
 ; block0(v0: i32, v1: i32):
-;     v5 = icmp slt v0, v1
-;     return v5
+;     v3 = icmp slt v0, v1
+;     return v3
 ; }
 
 function %icmp_and_ne_sle(i32, i32) -> i8 {
@@ -971,8 +971,8 @@ block0(v0: i32, v1: i32):
 
 ; function %icmp_and_ne_sgt(i32, i32) -> i8 fast {
 ; block0(v0: i32, v1: i32):
-;     v5 = icmp sgt v0, v1
-;     return v5
+;     v3 = icmp sgt v0, v1
+;     return v3
 ; }
 
 function %icmp_and_ne_sge(i32, i32) -> i8 {
@@ -1013,8 +1013,8 @@ block0(v0: i32, v1: i32):
 
 ; function %icmp_and_ult_ne(i32, i32) -> i8 fast {
 ; block0(v0: i32, v1: i32):
-;     v5 = icmp ult v0, v1
-;     return v5
+;     v2 = icmp ult v0, v1
+;     return v2
 ; }
 
 function %icmp_and_ult_ult(i32, i32) -> i8 {
@@ -1041,8 +1041,8 @@ block0(v0: i32, v1: i32):
 
 ; function %icmp_and_ult_ule(i32, i32) -> i8 fast {
 ; block0(v0: i32, v1: i32):
-;     v5 = icmp ult v0, v1
-;     return v5
+;     v2 = icmp ult v0, v1
+;     return v2
 ; }
 
 function %icmp_and_ult_ugt(i32, i32) -> i8 {
@@ -1147,8 +1147,8 @@ block0(v0: i32, v1: i32):
 
 ; function %icmp_and_ule_eq(i32, i32) -> i8 fast {
 ; block0(v0: i32, v1: i32):
-;     v5 = icmp eq v0, v1
-;     return v5
+;     v3 = icmp eq v0, v1
+;     return v3
 ; }
 
 function %icmp_and_ule_ne(i32, i32) -> i8 {
@@ -1175,8 +1175,8 @@ block0(v0: i32, v1: i32):
 
 ; function %icmp_and_ule_ult(i32, i32) -> i8 fast {
 ; block0(v0: i32, v1: i32):
-;     v5 = icmp ult v0, v1
-;     return v5
+;     v3 = icmp ult v0, v1
+;     return v3
 ; }
 
 function %icmp_and_ule_ule(i32, i32) -> i8 {
@@ -1309,8 +1309,8 @@ block0(v0: i32, v1: i32):
 
 ; function %icmp_and_ugt_ne(i32, i32) -> i8 fast {
 ; block0(v0: i32, v1: i32):
-;     v5 = icmp ugt v0, v1
-;     return v5
+;     v2 = icmp ugt v0, v1
+;     return v2
 ; }
 
 function %icmp_and_ugt_ult(i32, i32) -> i8 {
@@ -1365,8 +1365,8 @@ block0(v0: i32, v1: i32):
 
 ; function %icmp_and_ugt_uge(i32, i32) -> i8 fast {
 ; block0(v0: i32, v1: i32):
-;     v5 = icmp ugt v0, v1
-;     return v5
+;     v2 = icmp ugt v0, v1
+;     return v2
 ; }
 
 function %icmp_and_ugt_slt(i32, i32) -> i8 {
@@ -1443,8 +1443,8 @@ block0(v0: i32, v1: i32):
 
 ; function %icmp_and_uge_eq(i32, i32) -> i8 fast {
 ; block0(v0: i32, v1: i32):
-;     v5 = icmp eq v0, v1
-;     return v5
+;     v3 = icmp eq v0, v1
+;     return v3
 ; }
 
 function %icmp_and_uge_ne(i32, i32) -> i8 {
@@ -1499,8 +1499,8 @@ block0(v0: i32, v1: i32):
 
 ; function %icmp_and_uge_ugt(i32, i32) -> i8 fast {
 ; block0(v0: i32, v1: i32):
-;     v5 = icmp ugt v0, v1
-;     return v5
+;     v3 = icmp ugt v0, v1
+;     return v3
 ; }
 
 function %icmp_and_uge_uge(i32, i32) -> i8 {
@@ -1605,8 +1605,8 @@ block0(v0: i32, v1: i32):
 
 ; function %icmp_and_slt_ne(i32, i32) -> i8 fast {
 ; block0(v0: i32, v1: i32):
-;     v5 = icmp slt v0, v1
-;     return v5
+;     v2 = icmp slt v0, v1
+;     return v2
 ; }
 
 function %icmp_and_slt_ult(i32, i32) -> i8 {
@@ -1697,8 +1697,8 @@ block0(v0: i32, v1: i32):
 
 ; function %icmp_and_slt_sle(i32, i32) -> i8 fast {
 ; block0(v0: i32, v1: i32):
-;     v5 = icmp slt v0, v1
-;     return v5
+;     v2 = icmp slt v0, v1
+;     return v2
 ; }
 
 function %icmp_and_slt_sgt(i32, i32) -> i8 {
@@ -1739,8 +1739,8 @@ block0(v0: i32, v1: i32):
 
 ; function %icmp_and_sle_eq(i32, i32) -> i8 fast {
 ; block0(v0: i32, v1: i32):
-;     v5 = icmp eq v0, v1
-;     return v5
+;     v3 = icmp eq v0, v1
+;     return v3
 ; }
 
 function %icmp_and_sle_ne(i32, i32) -> i8 {
@@ -1831,8 +1831,8 @@ block0(v0: i32, v1: i32):
 
 ; function %icmp_and_sle_slt(i32, i32) -> i8 fast {
 ; block0(v0: i32, v1: i32):
-;     v5 = icmp slt v0, v1
-;     return v5
+;     v3 = icmp slt v0, v1
+;     return v3
 ; }
 
 function %icmp_and_sle_sle(i32, i32) -> i8 {
@@ -1901,8 +1901,8 @@ block0(v0: i32, v1: i32):
 
 ; function %icmp_and_sgt_ne(i32, i32) -> i8 fast {
 ; block0(v0: i32, v1: i32):
-;     v5 = icmp sgt v0, v1
-;     return v5
+;     v2 = icmp sgt v0, v1
+;     return v2
 ; }
 
 function %icmp_and_sgt_ult(i32, i32) -> i8 {
@@ -2021,8 +2021,8 @@ block0(v0: i32, v1: i32):
 
 ; function %icmp_and_sgt_sge(i32, i32) -> i8 fast {
 ; block0(v0: i32, v1: i32):
-;     v5 = icmp sgt v0, v1
-;     return v5
+;     v2 = icmp sgt v0, v1
+;     return v2
 ; }
 
 function %icmp_and_sge_eq(i32, i32) -> i8 {
@@ -2035,8 +2035,8 @@ block0(v0: i32, v1: i32):
 
 ; function %icmp_and_sge_eq(i32, i32) -> i8 fast {
 ; block0(v0: i32, v1: i32):
-;     v5 = icmp eq v0, v1
-;     return v5
+;     v3 = icmp eq v0, v1
+;     return v3
 ; }
 
 function %icmp_and_sge_ne(i32, i32) -> i8 {
@@ -2155,8 +2155,8 @@ block0(v0: i32, v1: i32):
 
 ; function %icmp_and_sge_sgt(i32, i32) -> i8 fast {
 ; block0(v0: i32, v1: i32):
-;     v5 = icmp sgt v0, v1
-;     return v5
+;     v3 = icmp sgt v0, v1
+;     return v3
 ; }
 
 function %icmp_and_sge_sge(i32, i32) -> i8 {
@@ -2225,8 +2225,8 @@ block0(v0: i32, v1: i32):
 
 ; function %icmp_or_eq_ule(i32, i32) -> i8 fast {
 ; block0(v0: i32, v1: i32):
-;     v5 = icmp ule v0, v1
-;     return v5
+;     v3 = icmp ule v0, v1
+;     return v3
 ; }
 
 function %icmp_or_eq_ugt(i32, i32) -> i8 {
@@ -2253,8 +2253,8 @@ block0(v0: i32, v1: i32):
 
 ; function %icmp_or_eq_uge(i32, i32) -> i8 fast {
 ; block0(v0: i32, v1: i32):
-;     v5 = icmp uge v0, v1
-;     return v5
+;     v3 = icmp uge v0, v1
+;     return v3
 ; }
 
 function %icmp_or_eq_slt(i32, i32) -> i8 {
@@ -2281,8 +2281,8 @@ block0(v0: i32, v1: i32):
 
 ; function %icmp_or_eq_sle(i32, i32) -> i8 fast {
 ; block0(v0: i32, v1: i32):
-;     v5 = icmp sle v0, v1
-;     return v5
+;     v3 = icmp sle v0, v1
+;     return v3
 ; }
 
 function %icmp_or_eq_sgt(i32, i32) -> i8 {
@@ -2309,8 +2309,8 @@ block0(v0: i32, v1: i32):
 
 ; function %icmp_or_eq_sge(i32, i32) -> i8 fast {
 ; block0(v0: i32, v1: i32):
-;     v5 = icmp sge v0, v1
-;     return v5
+;     v3 = icmp sge v0, v1
+;     return v3
 ; }
 
 function %icmp_or_ne_eq(i32, i32) -> i8 {
@@ -2351,8 +2351,8 @@ block0(v0: i32, v1: i32):
 
 ; function %icmp_or_ne_ult(i32, i32) -> i8 fast {
 ; block0(v0: i32, v1: i32):
-;     v5 = icmp ne v0, v1
-;     return v5
+;     v2 = icmp ne v0, v1
+;     return v2
 ; }
 
 function %icmp_or_ne_ule(i32, i32) -> i8 {
@@ -2379,8 +2379,8 @@ block0(v0: i32, v1: i32):
 
 ; function %icmp_or_ne_ugt(i32, i32) -> i8 fast {
 ; block0(v0: i32, v1: i32):
-;     v5 = icmp ne v0, v1
-;     return v5
+;     v2 = icmp ne v0, v1
+;     return v2
 ; }
 
 function %icmp_or_ne_uge(i32, i32) -> i8 {
@@ -2407,8 +2407,8 @@ block0(v0: i32, v1: i32):
 
 ; function %icmp_or_ne_slt(i32, i32) -> i8 fast {
 ; block0(v0: i32, v1: i32):
-;     v5 = icmp ne v0, v1
-;     return v5
+;     v2 = icmp ne v0, v1
+;     return v2
 ; }
 
 function %icmp_or_ne_sle(i32, i32) -> i8 {
@@ -2435,8 +2435,8 @@ block0(v0: i32, v1: i32):
 
 ; function %icmp_or_ne_sgt(i32, i32) -> i8 fast {
 ; block0(v0: i32, v1: i32):
-;     v5 = icmp ne v0, v1
-;     return v5
+;     v2 = icmp ne v0, v1
+;     return v2
 ; }
 
 function %icmp_or_ne_sge(i32, i32) -> i8 {
@@ -2477,8 +2477,8 @@ block0(v0: i32, v1: i32):
 
 ; function %icmp_or_ult_ne(i32, i32) -> i8 fast {
 ; block0(v0: i32, v1: i32):
-;     v5 = icmp ne v0, v1
-;     return v5
+;     v3 = icmp ne v0, v1
+;     return v3
 ; }
 
 function %icmp_or_ult_ult(i32, i32) -> i8 {
@@ -2505,8 +2505,8 @@ block0(v0: i32, v1: i32):
 
 ; function %icmp_or_ult_ule(i32, i32) -> i8 fast {
 ; block0(v0: i32, v1: i32):
-;     v5 = icmp ule v0, v1
-;     return v5
+;     v3 = icmp ule v0, v1
+;     return v3
 ; }
 
 function %icmp_or_ult_ugt(i32, i32) -> i8 {
@@ -2611,8 +2611,8 @@ block0(v0: i32, v1: i32):
 
 ; function %icmp_or_ule_eq(i32, i32) -> i8 fast {
 ; block0(v0: i32, v1: i32):
-;     v5 = icmp ule v0, v1
-;     return v5
+;     v2 = icmp ule v0, v1
+;     return v2
 ; }
 
 function %icmp_or_ule_ne(i32, i32) -> i8 {
@@ -2639,8 +2639,8 @@ block0(v0: i32, v1: i32):
 
 ; function %icmp_or_ule_ult(i32, i32) -> i8 fast {
 ; block0(v0: i32, v1: i32):
-;     v5 = icmp ule v0, v1
-;     return v5
+;     v2 = icmp ule v0, v1
+;     return v2
 ; }
 
 function %icmp_or_ule_ule(i32, i32) -> i8 {
@@ -2773,8 +2773,8 @@ block0(v0: i32, v1: i32):
 
 ; function %icmp_or_ugt_ne(i32, i32) -> i8 fast {
 ; block0(v0: i32, v1: i32):
-;     v5 = icmp ne v0, v1
-;     return v5
+;     v3 = icmp ne v0, v1
+;     return v3
 ; }
 
 function %icmp_or_ugt_ult(i32, i32) -> i8 {
@@ -2829,8 +2829,8 @@ block0(v0: i32, v1: i32):
 
 ; function %icmp_or_ugt_uge(i32, i32) -> i8 fast {
 ; block0(v0: i32, v1: i32):
-;     v5 = icmp uge v0, v1
-;     return v5
+;     v3 = icmp uge v0, v1
+;     return v3
 ; }
 
 function %icmp_or_ugt_slt(i32, i32) -> i8 {
@@ -2907,8 +2907,8 @@ block0(v0: i32, v1: i32):
 
 ; function %icmp_or_uge_eq(i32, i32) -> i8 fast {
 ; block0(v0: i32, v1: i32):
-;     v5 = icmp uge v0, v1
-;     return v5
+;     v2 = icmp uge v0, v1
+;     return v2
 ; }
 
 function %icmp_or_uge_ne(i32, i32) -> i8 {
@@ -2963,8 +2963,8 @@ block0(v0: i32, v1: i32):
 
 ; function %icmp_or_uge_ugt(i32, i32) -> i8 fast {
 ; block0(v0: i32, v1: i32):
-;     v5 = icmp uge v0, v1
-;     return v5
+;     v2 = icmp uge v0, v1
+;     return v2
 ; }
 
 function %icmp_or_uge_uge(i32, i32) -> i8 {
@@ -3069,8 +3069,8 @@ block0(v0: i32, v1: i32):
 
 ; function %icmp_or_slt_ne(i32, i32) -> i8 fast {
 ; block0(v0: i32, v1: i32):
-;     v5 = icmp ne v0, v1
-;     return v5
+;     v3 = icmp ne v0, v1
+;     return v3
 ; }
 
 function %icmp_or_slt_ult(i32, i32) -> i8 {
@@ -3161,8 +3161,8 @@ block0(v0: i32, v1: i32):
 
 ; function %icmp_or_slt_sle(i32, i32) -> i8 fast {
 ; block0(v0: i32, v1: i32):
-;     v5 = icmp sle v0, v1
-;     return v5
+;     v3 = icmp sle v0, v1
+;     return v3
 ; }
 
 function %icmp_or_slt_sgt(i32, i32) -> i8 {
@@ -3203,8 +3203,8 @@ block0(v0: i32, v1: i32):
 
 ; function %icmp_or_sle_eq(i32, i32) -> i8 fast {
 ; block0(v0: i32, v1: i32):
-;     v5 = icmp sle v0, v1
-;     return v5
+;     v2 = icmp sle v0, v1
+;     return v2
 ; }
 
 function %icmp_or_sle_ne(i32, i32) -> i8 {
@@ -3295,8 +3295,8 @@ block0(v0: i32, v1: i32):
 
 ; function %icmp_or_sle_slt(i32, i32) -> i8 fast {
 ; block0(v0: i32, v1: i32):
-;     v5 = icmp sle v0, v1
-;     return v5
+;     v2 = icmp sle v0, v1
+;     return v2
 ; }
 
 function %icmp_or_sle_sle(i32, i32) -> i8 {
@@ -3365,8 +3365,8 @@ block0(v0: i32, v1: i32):
 
 ; function %icmp_or_sgt_ne(i32, i32) -> i8 fast {
 ; block0(v0: i32, v1: i32):
-;     v5 = icmp ne v0, v1
-;     return v5
+;     v3 = icmp ne v0, v1
+;     return v3
 ; }
 
 function %icmp_or_sgt_ult(i32, i32) -> i8 {
@@ -3485,8 +3485,8 @@ block0(v0: i32, v1: i32):
 
 ; function %icmp_or_sgt_sge(i32, i32) -> i8 fast {
 ; block0(v0: i32, v1: i32):
-;     v5 = icmp sge v0, v1
-;     return v5
+;     v3 = icmp sge v0, v1
+;     return v3
 ; }
 
 function %icmp_or_sge_eq(i32, i32) -> i8 {
@@ -3499,8 +3499,8 @@ block0(v0: i32, v1: i32):
 
 ; function %icmp_or_sge_eq(i32, i32) -> i8 fast {
 ; block0(v0: i32, v1: i32):
-;     v5 = icmp sge v0, v1
-;     return v5
+;     v2 = icmp sge v0, v1
+;     return v2
 ; }
 
 function %icmp_or_sge_ne(i32, i32) -> i8 {
@@ -3619,8 +3619,8 @@ block0(v0: i32, v1: i32):
 
 ; function %icmp_or_sge_sgt(i32, i32) -> i8 fast {
 ; block0(v0: i32, v1: i32):
-;     v5 = icmp sge v0, v1
-;     return v5
+;     v2 = icmp sge v0, v1
+;     return v2
 ; }
 
 function %icmp_or_sge_sge(i32, i32) -> i8 {
diff --git a/cranelift/filetests/filetests/egraph/icmp.clif b/cranelift/filetests/filetests/egraph/icmp.clif
index e202251fabd1..9a0e57b7d4c7 100644
--- a/cranelift/filetests/filetests/egraph/icmp.clif
+++ b/cranelift/filetests/filetests/egraph/icmp.clif
@@ -545,8 +545,8 @@ block0(v0: i32, v1: i32):
 
 ; function %test_ult_ne_minus_one(i32, i32) -> i8 fast {
 ; block0(v0: i32, v1: i32):
-;     v6 = icmp ult v0, v1
-;     return v6
+;     v2 = icmp ult v0, v1
+;     return v2
 ; }
 
 function %smin_sgt_smax(i32, i32) -> i8 fast {
diff --git a/cranelift/filetests/filetests/egraph/spaceship.clif b/cranelift/filetests/filetests/egraph/spaceship.clif
index 7c1c8e2be099..3f8c0ff2cf3e 100644
--- a/cranelift/filetests/filetests/egraph/spaceship.clif
+++ b/cranelift/filetests/filetests/egraph/spaceship.clif
@@ -16,9 +16,9 @@ block0(v0: i32, v1: i32):
     v8 = select v2, v4, v7
     return v8
     ; check: v13 = icmp sgt v0, v1
-    ; check: v14 = icmp slt v0, v1
-    ; check: v15 = isub v13, v14
-    ; check: return v15
+    ; check: v2 = icmp slt v0, v1
+    ; check: v14 = isub v13, v2
+    ; check: return v14
 }
 
 function %cmp_s1b(i32, i32) -> i16 {
@@ -32,10 +32,10 @@ block0(v0: i32, v1: i32):
     v8 = select v2, v4, v7
     return v8
     ; check: v9 = icmp sgt v0, v1
-    ; check: v14 = icmp slt v0, v1
-    ; check: v15 = isub v9, v14
-    ; check: v16 = sextend.i16 v15
-    ; check: return v16
+    ; check: v2 = icmp slt v0, v1
+    ; check: v14 = isub v9, v2
+    ; check: v15 = sextend.i16 v14
+    ; check: return v15
 }
 
 function %cmp_s2a(i32, i32) -> i8 {
@@ -49,9 +49,9 @@ block0(v0: i32, v1: i32):
     v8 = select v2, v4, v7
     return v8
     ; check: v10 = icmp sgt v0, v1
-    ; check: v11 = icmp slt v0, v1
-    ; check: v12 = isub v10, v11
-    ; check: return v12
+    ; check: v2 = icmp slt v0, v1
+    ; check: v11 = isub v10, v2
+    ; check: return v11
 }
 
 function %cmp_s2b(i32, i32) -> i16 {
@@ -64,11 +64,11 @@ block0(v0: i32, v1: i32):
     v7 = select v3, v5, v6
     v8 = select v2, v4, v7
     return v8
-    ; check: v11 = icmp sgt v0, v1
-    ; check: v12 = icmp slt v0, v1
-    ; check: v13 = isub v11, v12
-    ; check: v14 = sextend.i16 v13
-    ; check: return v14
+    ; check: v3 = icmp sgt v0, v1
+    ; check: v2 = icmp slt v0, v1
+    ; check: v11 = isub v3, v2
+    ; check: v12 = sextend.i16 v11
+    ; check: return v12
 }
 
 function %cmp_s3a(i32, i32) -> i8 {
@@ -82,9 +82,9 @@ block0(v0: i32, v1: i32):
     v8 = select v2, v4, v7
     return v8
     ; check: v9 = icmp sgt v0, v1
-    ; check: v10 = icmp slt v0, v1
-    ; check: v11 = isub v9, v10
-    ; check: return v11
+    ; check: v3 = icmp slt v0, v1
+    ; check: v10 = isub v9, v3
+    ; check: return v10
 }
 
 function %cmp_s3b(i32, i32) -> i16 {
@@ -114,10 +114,10 @@ block0(v0: i32, v1: i32):
     v7 = select v3, v5, v6
     v8 = select v2, v4, v7
     return v8
-    ; check: v9 = icmp sgt v0, v1
-    ; check: v10 = icmp slt v0, v1
-    ; check: v11 = isub v9, v10
-    ; check: return v11
+    ; check: v3 = icmp sgt v0, v1
+    ; check: v9 = icmp slt v0, v1
+    ; check: v10 = isub v3, v9
+    ; check: return v10
 }
 
 function %cmp_s4b(i32, i32) -> i16 {
@@ -147,10 +147,10 @@ block0(v0: i32, v1: i32):
     v7 = select v3, v5, v6
     v8 = select v2, v4, v7
     return v8
-    ; check: v13 = icmp sgt v0, v1
-    ; check: v14 = icmp slt v0, v1
-    ; check: v15 = isub v13, v14
-    ; check: return v15
+    ; check: v2 = icmp sgt v0, v1
+    ; check: v3 = icmp slt v0, v1
+    ; check: v13 = isub v2, v3
+    ; check: return v13
 }
 
 function %cmp_s5b(i32, i32) -> i16 {
@@ -163,11 +163,11 @@ block0(v0: i32, v1: i32):
     v7 = select v3, v5, v6
     v8 = select v2, v4, v7
     return v8
-    ; check: v11 = icmp sgt v0, v1
-    ; check: v12 = icmp slt v0, v1
-    ; check: v13 = isub v11, v12
-    ; check: v14 = sextend.i16 v13
-    ; check: return v14
+    ; check: v2 = icmp sgt v0, v1
+    ; check: v11 = icmp slt v0, v1
+    ; check: v12 = isub v2, v11
+    ; check: v13 = sextend.i16 v12
+    ; check: return v13
 }
 
 function %cmp_s6a(i32, i32) -> i8 {
@@ -180,10 +180,10 @@ block0(v0: i32, v1: i32):
     v7 = select v3, v5, v6
     v8 = select v2, v4, v7
     return v8
-    ; check: v16 = icmp sgt v0, v1
+    ; check: v2 = icmp sgt v0, v1
     ; check: v9 = icmp slt v0, v1
-    ; check: v17 = isub v16, v9
-    ; check: return v17
+    ; check: v16 = isub v2, v9
+    ; check: return v16
 }
 
 function %cmp_s6b(i32, i32) -> i16 {
@@ -196,11 +196,11 @@ block0(v0: i32, v1: i32):
     v7 = select v3, v5, v6
     v8 = select v2, v4, v7
     return v8
-    ; check: v14 = icmp sgt v0, v1
-    ; check: v15 = icmp slt v0, v1
-    ; check: v16 = isub v14, v15
-    ; check: v17 = sextend.i16 v16
-    ; check: return v17
+    ; check: v2 = icmp sgt v0, v1
+    ; check: v14 = icmp slt v0, v1
+    ; check: v15 = isub v2, v14
+    ; check: v16 = sextend.i16 v15
+    ; check: return v16
 }
 
 ;; And again for unsigned...
@@ -216,10 +216,10 @@ block0(v0: i32, v1: i32):
     v8 = select v2, v4, v7
     return v8
     ; check: v14 = icmp ugt v0, v1
-    ; check: v15 = icmp ult v0, v1
-    ; check: v16 = isub v14, v15
-    ; check: v17 = sextend.i16 v16
-    ; check: return v17
+    ; check: v2 = icmp ult v0, v1
+    ; check: v15 = isub v14, v2
+    ; check: v16 = sextend.i16 v15
+    ; check: return v16
 }
 
 function %cmp_u1b(i32, i32) -> i8 {
@@ -233,9 +233,9 @@ block0(v0: i32, v1: i32):
     v8 = select v2, v4, v7
     return v8
     ; check: v9 = icmp ugt v0, v1
-    ; check: v13 = icmp ult v0, v1
-    ; check: v14 = isub v9, v13
-    ; check: return v14
+    ; check: v2 = icmp ult v0, v1
+    ; check: v13 = isub v9, v2
+    ; check: return v13
 }
 
 function %cmp_u2a(i32, i32) -> i16 {
@@ -249,10 +249,10 @@ block0(v0: i32, v1: i32):
     v8 = select v2, v4, v7
     return v8
     ; check: v11 = icmp ugt v0, v1
-    ; check: v12 = icmp ult v0, v1
-    ; check: v13 = isub v11, v12
-    ; check: v14 = sextend.i16 v13
-    ; check: return v14
+    ; check: v2 = icmp ult v0, v1
+    ; check: v12 = isub v11, v2
+    ; check: v13 = sextend.i16 v12
+    ; check: return v13
 }
 
 function %cmp_u2b(i32, i32) -> i8 {
@@ -265,10 +265,10 @@ block0(v0: i32, v1: i32):
     v7 = select v3, v5, v6
     v8 = select v2, v4, v7
     return v8
-    ; check: v10 = icmp ugt v0, v1
-    ; check: v11 = icmp ult v0, v1
-    ; check: v12 = isub v10, v11
-    ; check: return v12
+    ; check: v3 = icmp ugt v0, v1
+    ; check: v2 = icmp ult v0, v1
+    ; check: v10 = isub v3, v2
+    ; check: return v10
 }
 
 function %cmp_u3a(i32, i32) -> i16 {
@@ -282,10 +282,10 @@ block0(v0: i32, v1: i32):
     v8 = select v2, v4, v7
     return v8
     ; check: v9 = icmp ugt v0, v1
-    ; check: v10 = icmp ult v0, v1
-    ; check: v11 = isub v9, v10
-    ; check: v12 = sextend.i16 v11
-    ; check: return v12
+    ; check: v3 = icmp ult v0, v1
+    ; check: v10 = isub v9, v3
+    ; check: v11 = sextend.i16 v10
+    ; check: return v11
 }
 
 function %cmp_u3b(i32, i32) -> i8 {
@@ -314,11 +314,11 @@ block0(v0: i32, v1: i32):
     v7 = select v3, v5, v6
     v8 = select v2, v4, v7
     return v8
-    ; check: v9 = icmp ugt v0, v1
-    ; check: v10 = icmp ult v0, v1
-    ; check: v11 = isub v9, v10
-    ; check: v12 = sextend.i16 v11
-    ; check: return v12
+    ; check: v3 = icmp ugt v0, v1
+    ; check: v9 = icmp ult v0, v1
+    ; check: v10 = isub v3, v9
+    ; check: v11 = sextend.i16 v10
+    ; check: return v11
 }
 
 function %cmp_u4b(i32, i32) -> i8 {
@@ -347,11 +347,11 @@ block0(v0: i32, v1: i32):
     v7 = select v3, v5, v6
     v8 = select v2, v4, v7
     return v8
-    ; check: v11 = icmp ugt v0, v1
-    ; check: v12 = icmp ult v0, v1
-    ; check: v13 = isub v11, v12
-    ; check: v14 = sextend.i16 v13
-    ; check: return v14
+    ; check: v2 = icmp ugt v0, v1
+    ; check: v3 = icmp ult v0, v1
+    ; check: v11 = isub v2, v3
+    ; check: v12 = sextend.i16 v11
+    ; check: return v12
 }
 
 function %cmp_u5b(i32, i32) -> i8 {
@@ -364,10 +364,10 @@ block0(v0: i32, v1: i32):
     v7 = select v3, v5, v6
     v8 = select v2, v4, v7
     return v8
-    ; check: v13 = icmp ugt v0, v1
-    ; check: v14 = icmp ult v0, v1
-    ; check: v15 = isub v13, v14
-    ; check: return v15
+    ; check: v2 = icmp ugt v0, v1
+    ; check: v13 = icmp ult v0, v1
+    ; check: v14 = isub v2, v13
+    ; check: return v14
 }
 
 function %cmp_u6a(i32, i32) -> i16 {
@@ -380,11 +380,11 @@ block0(v0: i32, v1: i32):
     v7 = select v3, v5, v6
     v8 = select v2, v4, v7
     return v8
-    ; check: v14 = icmp ugt v0, v1
+    ; check: v2 = icmp ugt v0, v1
     ; check: v9 = icmp ult v0, v1
-    ; check: v15 = isub v14, v9
-    ; check: v16 = sextend.i16 v15
-    ; check: return v16
+    ; check: v14 = isub v2, v9
+    ; check: v15 = sextend.i16 v14
+    ; check: return v15
 }
 
 function %cmp_u6b(i32, i32) -> i8 {
@@ -397,10 +397,10 @@ block0(v0: i32, v1: i32):
     v7 = select v3, v5, v6
     v8 = select v2, v4, v7
     return v8
-    ; check: v16 = icmp ugt v0, v1
-    ; check: v17 = icmp ult v0, v1
-    ; check: v18 = isub v16, v17
-    ; check: return v18
+    ; check: v2 = icmp ugt v0, v1
+    ; check: v16 = icmp ult v0, v1
+    ; check: v17 = isub v2, v16
+    ; check: return v17
 }
 
 ;; Then a few of the simplifications
@@ -437,8 +437,8 @@ block0(v0: i32, v1: i32):
     v5 = iconst.i8 0
     v6 = icmp sgt v4, v5
     return v6
-    ; check: v7 = icmp sgt v0, v1
-    ; check: return v7
+    ; check: v2 = icmp sgt v0, v1
+    ; check: return v2
 }
 
 function %uge_via_cmp(i64, i64) -> i8 {