feat: consistent type ABI regardless of transparency

Author: hargoniX

src/Lean/Compiler/LCNF/Types.lean

@@ -166,8 +166,12 @@ where
     | .proj ``Subtype 0 (.const ``IO.RealWorld.nonemptyType []) =>
       return mkConst ``lcRealWorld
     | _        => return mkConst ``lcAny
+
   whnfEta (type : Expr) : MetaM Expr := do
-    let type ← whnf type
+    -- We increase transparency here to unfold type aliases of functions that are declared as
+    -- `irreducible`, such that they end up being represented as C functions.
+    let type ← withTransparency .all do
+      whnf type
     let type' := type.eta
     if type' != type then
       whnfEta type'

tests/lean/run/compiler_type_transparency.lean

@@ -0,0 +1,61 @@
+/-!
+This test ensures that the code generator sees the same type representation regardless of
+transparency setting in the elaborator. If this test ever breaks you should ensure that the IR
+between A and B is in sync.
+-/
+
+namespace A
+
+@[irreducible] def Function (α β : Type) := α → β
+
+namespace Function
+
+attribute [local semireducible] Function
+
+@[inline]
+def id : Function α α := fun x => x
+
+end Function
+
+/--
+trace: [Compiler.IR] [result]
+    def A.foo (x_1 : @& tobj) : tobj :=
+      inc x_1;
+      ret x_1
+    def A.foo._boxed (x_1 : tobj) : tobj :=
+      let x_2 : tobj := A.foo x_1;
+      dec x_1;
+      ret x_2
+-/
+#guard_msgs in
+set_option trace.compiler.ir.result true in
+def foo : Function Nat Nat := Function.id
+
+end A
+
+namespace B
+
+def Function (α β : Type) := α → β
+
+namespace Function
+
+@[inline]
+def id : Function α α := fun x => x
+
+end Function
+
+/--
+trace: [Compiler.IR] [result]
+    def B.foo (x_1 : @& tobj) : tobj :=
+      inc x_1;
+      ret x_1
+    def B.foo._boxed (x_1 : tobj) : tobj :=
+      let x_2 : tobj := B.foo x_1;
+      dec x_1;
+      ret x_2
+-/
+#guard_msgs in
+set_option trace.compiler.ir.result true in
+def foo : Function Nat Nat := Function.id
+
+end B