chore: legitimize projections on tagged values (#11586)

This PR allows projections on `tagged` values in the IR type system.

While executing this branch of code should indeed never happen in
practice, enforcing this through
the type system would require the compiler to always optimize code to
the point where this is not
possible. For example in the code:
```
cases x with
| none => ....
| some =>
    let val : obj := proj[0] x
    ...
```
static analysis might learn that `x` is always none and transform this
to:
```
let x : tagged := none
cases x with
| none => ....
| some =>
    let val : obj := proj[0] x
    ...
```
Which would be type incorrect if projections on `tagged` were
illegitimate. However, we don't want
to force static analysis to always simplify code far enough on its own
to enforce this invariant.

Author: hargoniX

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