diff --git a/src/ast/compiler/type_checker.rs b/src/ast/compiler/type_checker.rs
index 87927bd..f09ed39 100644
--- a/src/ast/compiler/type_checker.rs
+++ b/src/ast/compiler/type_checker.rs
@@ -331,6 +331,46 @@ impl TypeChecker {
         !matches!(ty, StaticType::Any | StaticType::TypeVar(_) | StaticType::Error)
     }
 
+    /// Returns the widened numeric type when one side is `Int` and the other `Float`.
+    /// This is the only implicit numeric promotion in Myc: Int is a subtype of Float.
+    fn numeric_widen(a: &StaticType, b: &StaticType) -> Option<StaticType> {
+        match (a, b) {
+            (StaticType::Int, StaticType::Float) | (StaticType::Float, StaticType::Int) => {
+                Some(StaticType::Float)
+            }
+            _ => None,
+        }
+    }
+
+    /// If both types are Records with the same field names and compatible types
+    /// (same type or Int→Float widening), returns the promoted Record type.
+    fn record_promote(a: &StaticType, b: &StaticType) -> Option<StaticType> {
+        let (StaticType::Record(la), StaticType::Record(lb)) = (a, b) else {
+            return None;
+        };
+        if la == lb {
+            return None;
+        }
+        if la.fields.len() != lb.fields.len() {
+            return None;
+        }
+        let mut promoted_fields = Vec::with_capacity(la.fields.len());
+        for ((ka, ta), (kb, tb)) in la.fields.iter().zip(lb.fields.iter()) {
+            if ka != kb {
+                return None;
+            }
+            let t = if ta == tb {
+                ta.clone()
+            } else if let Some(w) = Self::numeric_widen(ta, tb) {
+                w
+            } else {
+                return None;
+            };
+            promoted_fields.push((*ka, t));
+        }
+        Some(StaticType::Record(RecordLayout::get_or_create(promoted_fields)))
+    }
+
     /// Converts a resolved series element type to the schema `Value` passed to the
     /// `series` runtime: a type keyword (`:float`, `:int`, …) for scalar types, or a
     /// schema record (`{:price :float …}`) for record types.
@@ -1021,7 +1061,9 @@ impl TypeChecker {
                 if let Some(e) = else_br {
                     let et = self.check_node(e, ctx, diag);
                     if et.ty != final_ty {
-                        final_ty = StaticType::Any;
+                        final_ty = Self::numeric_widen(&final_ty, &et.ty)
+                            .or_else(|| Self::record_promote(&final_ty, &et.ty))
+                            .unwrap_or(StaticType::Any);
                     }
                     else_typed = Some(Rc::new(et));
                 } else {
@@ -1193,7 +1235,13 @@ impl TypeChecker {
                 }
 
                 // HM: (push series val) — unify the series element TypeVar with the value
-                // type and propagate the resolved type back to the binding in the context.
+                // type, applying Int→Float numeric promotion when needed.
+                //
+                // We intentionally do NOT bake the resolved type into ctx after normal
+                // unification. Keeping `Series(TypeVar(n))` in ctx allows a later push
+                // to recover the TypeVar ID and rebind it (e.g. Int → Float promotion).
+                // All identifier lookups call `apply_subst`, so the resolved type is
+                // always correct regardless of what ctx stores.
                 if Self::is_identifier_named("push", &callee_typed)
                     && let NodeKind::Tuple { elements } = &args_typed.kind
                     && elements.len() >= 2
@@ -1203,15 +1251,33 @@ impl TypeChecker {
                     if let StaticType::Series(inner) = &series_arg.ty {
                         let inner_ty = (**inner).clone();
                         let val_ty = value_arg.ty.clone();
-                        self.unify(inner_ty, val_ty, diag);
+
                         if let NodeKind::Identifier {
                             binding: IdentifierBinding::Reference(addr),
                             ..
                         } = &series_arg.kind
                         {
-                            let resolved =
-                                Self::apply_subst(series_arg.ty.clone(), &self.subst.borrow());
-                            ctx.set_type(*addr, resolved);
+                            // Recover the raw inner type from ctx (before apply_subst) so
+                            // we can find the TypeVar ID even after the first push resolved it.
+                            let raw_inner = match ctx.get_type(*addr) {
+                                StaticType::Series(ri) => *ri,
+                                _ => inner_ty.clone(),
+                            };
+
+                            if let Some(promoted) = Self::numeric_widen(&inner_ty, &val_ty)
+                                .or_else(|| Self::record_promote(&inner_ty, &val_ty))
+                            {
+                                // Rebind the TypeVar to the promoted type so that finalize
+                                // injects the correct schema (e.g. :float instead of :int).
+                                if let StaticType::TypeVar(n) = raw_inner {
+                                    self.subst.borrow_mut().insert(n, promoted.clone());
+                                }
+                                ctx.set_type(*addr, StaticType::Series(Box::new(promoted)));
+                            } else {
+                                self.unify(inner_ty, val_ty, diag);
+                            }
+                        } else {
+                            self.unify(inner_ty, val_ty, diag);
                         }
                     }
                 }
diff --git a/tests/rtl_series.rs b/tests/rtl_series.rs
index 3252255..f883bbd 100644
--- a/tests/rtl_series.rs
+++ b/tests/rtl_series.rs
@@ -65,6 +65,140 @@ fn test_series_typevar_resolved_through_while_upvalue() {
     }
 }
 
+// ── Numeric promotion (Int → Float widening) ────────────────────────────────
+
+/// Push int first, then float: series element type should widen to Float.
+/// The int value must be readable back as a float (no truncation).
+#[test]
+fn test_series_promote_int_then_float() {
+    let env = Environment::new();
+    let source = r#"
+    (do
+      (def s (series 5))
+      (push s 1)
+      (push s 2.5)
+      (+ (s 0) (s 1))
+    )
+    "#;
+    let result = env.run_script(source);
+    match result {
+        Ok(Value::Float(v)) if (v - 3.5).abs() < 1e-9 => {}
+        other => panic!("Expected Float(3.5), got {:?}", other),
+    }
+}
+
+/// Push float first, then int: same widening, other direction.
+#[test]
+fn test_series_promote_float_then_int() {
+    let env = Environment::new();
+    let source = r#"
+    (do
+      (def s (series 5))
+      (push s 2.5)
+      (push s 1)
+      (+ (s 0) (s 1))
+    )
+    "#;
+    let result = env.run_script(source);
+    match result {
+        Ok(Value::Float(v)) if (v - 3.5).abs() < 1e-9 => {}
+        other => panic!("Expected Float(3.5), got {:?}", other),
+    }
+}
+
+/// `if` branches with int/float: the join type must be Float, not Any.
+/// A Float series is expected — the pushed value must be accessible as float.
+#[test]
+fn test_series_promote_if_int_float_branch() {
+    let env = Environment::new();
+    let source = r#"
+    (do
+      (def s (series 5))
+      (push s (if true 1 2.5))
+      (push s (if false 1 2.5))
+      (+ (s 0) (s 1))
+    )
+    "#;
+    let result = env.run_script(source);
+    match result {
+        Ok(Value::Float(v)) if (v - 3.5).abs() < 1e-9 => {}
+        other => panic!("Expected Float(3.5), got {:?}", other),
+    }
+}
+
+/// Int variable pushed into a float-inferred series must be promoted.
+#[test]
+fn test_series_promote_int_variable_into_float_series() {
+    let env = Environment::new();
+    let source = r#"
+    (do
+      (def s (series 5))
+      (def n 3)
+      (push s 1.5)
+      (push s n)
+      (+ (s 0) (s 1))
+    )
+    "#;
+    let result = env.run_script(source);
+    match result {
+        Ok(Value::Float(v)) if (v - 4.5).abs() < 1e-9 => {}
+        other => panic!("Expected Float(4.5), got {:?}", other),
+    }
+}
+
+/// Record field promotion: pushing records where one field is int, another float.
+/// The field type must widen to Float.
+#[test]
+fn test_series_promote_record_field_int_float() {
+    let env = Environment::new();
+    let source = r#"
+    (do
+      (def s (series 5))
+      (push s {:v 1})
+      (push s {:v 2.5})
+      (def v (.v s))
+      (+ (v 0) (v 1))
+    )
+    "#;
+    let result = env.run_script(source);
+    match result {
+        Ok(Value::Float(v)) if (v - 3.5).abs() < 1e-9 => {}
+        other => panic!("Expected Float(3.5), got {:?}", other),
+    }
+}
+
+/// Sanity check: Bool → Int is NOT a valid promotion (different semantic type).
+#[test]
+fn test_series_no_promotion_bool_int() {
+    let env = Environment::new();
+    let source = r#"
+    (do
+      (def s (series 5))
+      (push s true)
+      (push s 1)
+      (s 0)
+    )
+    "#;
+    let result = env.compile(source).into_result();
+    assert!(result.is_err(), "Bool->Int promotion must not be allowed");
+}
+
+/// Sanity check: Float → Bool is NOT a valid promotion.
+#[test]
+fn test_series_no_promotion_float_bool() {
+    let env = Environment::new();
+    let source = r#"
+    (do
+      (def s (series 5))
+      (push s 1.5)
+      (push s true)
+      (s 0)
+    )
+    "#;
+    let result = env.compile(source).into_result();
+    assert!(result.is_err(), "Float->Bool promotion must not be allowed");
+}
+
 #[test]
 fn test_record_structural_equality_order() {
     let env = Environment::new();