fix: better types when creating boxed decls (#11445)

This PR slightly improves the types involved in creating boxed
declarations. Previously the type of
the vdecl used for the return was always `tobj` when returning a boxed
scalar. This is not the most
precise annotation we can give.

Author: hargoniX

src/Lean/Compiler/IR/Boxing.lean

@@ -53,7 +53,7 @@ def mkBoxedVersionAux (decl : Decl) : N Decl := do
     pure <| reshape newVDecls (.ret (.var r))
   else
     let newR ← N.mkFresh
-    let newVDecls := newVDecls.push (.vdecl newR .tobject (.box decl.resultType r) default)
+    let newVDecls := newVDecls.push (.vdecl newR decl.resultType.boxed (.box decl.resultType r) default)
     pure <| reshape newVDecls (.ret (.var newR))
   return Decl.fdecl (mkBoxedName decl.name) qs decl.resultType.boxed body decl.getInfo
 

tests/lean/4240.lean.expected.out

@@ -16,10 +16,10 @@
     def isSomeWithInstanceNat._boxed (x_1 : obj) : tagged :=
       let x_2 : u8 := isSomeWithInstanceNat x_1;
       dec x_1;
-      let x_3 : tobj := box x_2;
+      let x_3 : tagged := box x_2;
       ret x_3
     def MyOption.isSomeWithInstance._at_.isSomeWithInstanceNat.spec_0._boxed (x_1 : tobj) : tagged :=
       let x_2 : u8 := MyOption.isSomeWithInstance._at_.isSomeWithInstanceNat.spec_0 x_1;
       dec x_1;
-      let x_3 : tobj := box x_2;
+      let x_3 : tagged := box x_2;
       ret x_3

tests/lean/computedFieldsCode.lean.expected.out

@@ -287,7 +287,7 @@
     def g._boxed (x_1 : tobj) : tagged :=
       let x_2 : u8 := g x_1;
       dec x_1;
-      let x_3 : tobj := box x_2;
+      let x_3 : tagged := box x_2;
       ret x_3
 [Compiler.IR] [result]
     def hash' (x_1 : @& tobj) : tobj :=

tests/lean/run/10934.lean

@@ -17,7 +17,7 @@ trace: [Compiler.IR] [result]
       let x_3 : u8 := unbox x_1;
       let x_4 : u8 := unbox x_2;
       let x_5 : u8 := _example x_3 x_4;
-      let x_6 : tobj := box x_5;
+      let x_6 : tagged := box x_5;
       ret x_6
 -/
 #guard_msgs in
@@ -36,7 +36,7 @@ trace: [Compiler.IR] [result]
       let x_3 : u8 := unbox x_1;
       let x_4 : u8 := unbox x_2;
       let x_5 : u8 := _example x_3 x_4;
-      let x_6 : tobj := box x_5;
+      let x_6 : tagged := box x_5;
       ret x_6
 -/
 #guard_msgs in
@@ -54,7 +54,7 @@ trace: [Compiler.IR] [result]
       let x_3 : u8 := unbox x_1;
       let x_4 : u8 := unbox x_2;
       let x_5 : u8 := _example x_3 x_4;
-      let x_6 : tobj := box x_5;
+      let x_6 : tagged := box x_5;
       ret x_6
 -/
 #guard_msgs in
@@ -67,7 +67,7 @@ trace: [Compiler.IR] [result]
     def _example._boxed (x_1 : tagged) : tagged :=
       let x_2 : u8 := unbox x_1;
       let x_3 : u8 := _example x_2;
-      let x_4 : tobj := box x_3;
+      let x_4 : tagged := box x_3;
       ret x_4
 -/
 #guard_msgs in

tests/lean/sint_basic.lean.expected.out

@@ -78,7 +78,7 @@ true
     def _private.lean.sint_basic.0.myId8._boxed (x_1 : tagged) : tagged :=
       let x_2 : u8 := unbox x_1;
       let x_3 : u8 := _private.lean.sint_basic.0.myId8 x_2;
-      let x_4 : tobj := box x_3;
+      let x_4 : tagged := box x_3;
       ret x_4
 Int16 : Type
 20
@@ -160,7 +160,7 @@ true
     def _private.lean.sint_basic.0.myId16._boxed (x_1 : tagged) : tagged :=
       let x_2 : u16 := unbox x_1;
       let x_3 : u16 := _private.lean.sint_basic.0.myId16 x_2;
-      let x_4 : tobj := box x_3;
+      let x_4 : tagged := box x_3;
       ret x_4
 Int32 : Type
 20