From ed24924dbba06a2334355dfdc619c3287b29e579 Mon Sep 17 00:00:00 2001
From: Aletheia-Prime <221768278+Aletheia-Prime@users.noreply.github.com>
Date: Wed, 15 Apr 2026 12:08:45 -0300
Subject: [PATCH] fix: prevent Any type from shadowing type errors in match
 arms

When unreachable() was used in a match arm, the type checker would infer Any
as the return type. Since Any can unify with anything, it would absorb
type constraints from other arms, allowing invalid types to pass without error.

This fix preserves type constraints from non-Any arms when the final unified type
is Any but a previous arm has free type variables.
---
 src/fun/check/type_check.rs | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/src/fun/check/type_check.rs b/src/fun/check/type_check.rs
index 63fc3c34..31301e68 100644
--- a/src/fun/check/type_check.rs
+++ b/src/fun/check/type_check.rs
@@ -593,6 +593,15 @@ fn infer_match_cases(
       let (s_rest, t_rest) = infer_match_cases(env.subst(&s), book, types, adt, rest, adt_s, var_gen)?;
       let (t_final, s_final) = unify_term(&t1.subst(&s), &t_rest, bod)?;
 
+      // If the final type is `Any` but t1 (from non-unreachable arm) has type variables,
+      // we need to use t1's type to preserve those constraints
+      if let Type::Any = &t_final {
+        let t1_vars = t1.free_type_vars();
+        if !t1_vars.is_empty() {
+          return Ok((s_final.compose(s_rest).compose(s.clone()), t1.subst(&s)));
+        }
+      }
+
       Ok((s_final.compose(s_rest).compose(s), t_final))
     } else {
       Ok((Subst::default(), var_gen.fresh()))