perf: infer better IR types to reduce refcounting

Author: hargoniX

src/Lean/Compiler/IR/Boxing.lean

@@ -280,7 +280,10 @@ def tryCorrectVDeclType (ty : IRType) (e : Expr) : M IRType :=
   match e with
   | .fap f _ => do
     let decl ← getDecl f
-    return decl.resultType
+    match decl.name with
+    | ``FloatArray.size | ``ByteArray.size | ``Array.size | ``String.length | ``String.utf8ByteSize
+    | ``String.Pos.next | ``UInt8.toNat | ``UInt16.toNat => return .tagged
+    | _ => return decl.resultType
   | .pap .. => return .object
   | .uproj .. => return .usize
   | .ctor .. | .reuse .. | .ap .. | .lit .. | .sproj .. | .proj .. | .reset .. =>

tests/lean/run/unbox_sizes.lean

@@ -0,0 +1,16 @@
+/--
+trace: [Compiler.IR] [result]
+    def test (x_1 : @& obj) : tobj :=
+      let x_2 : tagged := Array.size ◾ x_1;
+      let x_3 : tobj := Nat.add x_2 x_2;
+      ret x_3
+    def test._boxed (x_1 : obj) : tobj :=
+      let x_2 : tobj := test x_1;
+      dec x_1;
+      ret x_2
+-/
+#guard_msgs in
+set_option trace.compiler.ir.result true in
+def test (xs : Array Int) :=
+  let size := xs.size
+  size + size