diff --git a/crates/ailang-check/src/builtins.rs b/crates/ailang-check/src/builtins.rs
index 9d2814f..8111e0b 100644
--- a/crates/ailang-check/src/builtins.rs
+++ b/crates/ailang-check/src/builtins.rs
@@ -511,4 +511,47 @@ mod tests {
             "io/print_float must accumulate IO effect, got {effects:?}"
         );
     }
+
+    /// Iter 22-floats.3: pattern-matching on Float literals is hard-
+    /// rejected at typecheck per spec line 723-735 recommendation (a).
+    /// IEEE-`==` semantics make Float patterns semantically dubious
+    /// (NaN never matches; equality is bit-exact not approximate).
+    /// Surface lex / parser accept the syntax (iter 2); typecheck
+    /// surfaces the error here.
+    #[test]
+    fn reject_float_pattern_in_match() {
+        use ailang_core::ast::{Arm, Pattern};
+        let bits = 1.5_f64.to_bits();
+        let scrut = lit_float(bits);
+        let arm = Arm {
+            pat: Pattern::Lit { lit: Literal::Float { bits } },
+            body: lit_int(0),
+        };
+        let term = Term::Match {
+            scrutinee: Box::new(scrut),
+            arms: vec![arm],
+        };
+        let mut env = Env::default();
+        install(&mut env);
+        let mut locals: IndexMap<String, Type> = IndexMap::new();
+        let mut effects: BTreeSet<String> = BTreeSet::new();
+        let mut subst = Subst::default();
+        let mut counter: u32 = 0;
+        let mut residuals = Vec::new();
+        let err = crate::synth(
+            &term,
+            &env,
+            &mut locals,
+            &mut effects,
+            "<test>",
+            &mut subst,
+            &mut counter,
+            &mut residuals,
+        )
+        .expect_err("must reject");
+        assert!(
+            matches!(err, crate::CheckError::FloatPatternNotAllowed),
+            "expected FloatPatternNotAllowed, got {err:?}"
+        );
+    }
 }
diff --git a/crates/ailang-check/src/lib.rs b/crates/ailang-check/src/lib.rs
index 2cdb61d..b4a1697 100644
--- a/crates/ailang-check/src/lib.rs
+++ b/crates/ailang-check/src/lib.rs
@@ -370,6 +370,15 @@ pub enum CheckError {
     #[error("primitive type `{0}` requires a wildcard or variable arm in match")]
     PrimitiveNeedsWildcard(String),
 
+    /// A `Pattern::Lit` matched against a `Literal::Float`. Float
+    /// patterns are semantically dubious (NaN never matches via
+    /// IEEE-`==`; equality is bit-exact not approximate), so the
+    /// typechecker hard-rejects them. The surface lex / parser
+    /// accept the syntax (iter 2); this diagnostic surfaces at
+    /// typecheck time. Code: `float-pattern-not-allowed`.
+    #[error("float-literal patterns are not allowed: use ordering operators (`<`, `>`, ...) and `is_nan` to discriminate floats")]
+    FloatPatternNotAllowed,
+
     /// A `Pattern::Ctor` was matched against a value of a different ADT.
     /// Code: `pattern-type-mismatch`.
     #[error("cannot match constructor pattern `{ctor}` against type `{ty}`")]
@@ -521,6 +530,7 @@ impl CheckError {
             CheckError::CtorArity { .. } => "arity-mismatch",
             CheckError::NonExhaustive { .. } => "non-exhaustive-match",
             CheckError::PrimitiveNeedsWildcard(_) => "primitive-needs-wildcard",
+            CheckError::FloatPatternNotAllowed => "float-pattern-not-allowed",
             CheckError::PatternTypeMismatch { .. } => "pattern-type-mismatch",
             CheckError::DuplicateType(_) => "duplicate-type",
             CheckError::DuplicateCtor { .. } => "duplicate-ctor",
@@ -2309,7 +2319,9 @@ fn type_check_pattern(
                 Literal::Bool { .. } => Type::bool_(),
                 Literal::Str { .. } => Type::str_(),
                 Literal::Unit => Type::unit(),
-                Literal::Float { .. } => Type::float(),
+                Literal::Float { .. } => {
+                    return Err(CheckError::FloatPatternNotAllowed);
+                }
             };
             expect_eq(expected, &lt)?;
             Ok(vec![])