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 {