From 5ee1967d15cd4b31f16365ef0d9dc0a359312a9c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Wed, 10 Dec 2025 13:15:38 +0000
Subject: [PATCH] chore: legitimize projections on tagged values

---
 src/Lean/Compiler/IR/Checker.lean | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/src/Lean/Compiler/IR/Checker.lean b/src/Lean/Compiler/IR/Checker.lean
index 1d391ada3091..6bfe759f4c1a 100644
--- a/src/Lean/Compiler/IR/Checker.lean
+++ b/src/Lean/Compiler/IR/Checker.lean
@@ -159,6 +159,11 @@ def checkExpr (ty : IRType) (e : Expr) : M Unit := do
     checkObjVar x
   | .proj i x =>
     let xType ← getType x;
+    /-
+    Projections are a valid operation on `tobject`. Thus they should also
+    be a valid operation for both `object`, `tagged` and unboxed values
+    as they are subtypes.
+    -/
     match xType with
     | .object | .tobject =>
       checkObjType ty
@@ -167,6 +172,7 @@ def checkExpr (ty : IRType) (e : Expr) : M Unit := do
         checkEqTypes (tys[i]) ty
       else
         throwCheckerError "invalid proj index"
+    | .tagged => pure ()
     | _ => throwCheckerError s!"unexpected IR type '{xType}'"
   | .uproj _ x =>
     checkObjVar x