diff --git a/src/Lean/Compiler/LCNF/Types.lean b/src/Lean/Compiler/LCNF/Types.lean
index 6d0fcbe6b9..ebeb07598f 100644
--- a/src/Lean/Compiler/LCNF/Types.lean
+++ b/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'
diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h
index 79a0e58edd..95435a3c60 100644
--- a/stage0/src/stdlib_flags.h
+++ b/stage0/src/stdlib_flags.h
@@ -1,5 +1,7 @@
 #include "util/options.h"
 
+// please update stage0 good sir
+
 namespace lean {
 options get_default_options() {
     options opts;
diff --git a/tests/lean/run/compiler_type_transparency.lean b/tests/lean/run/compiler_type_transparency.lean
new file mode 100644
index 0000000000..150d4a2b0b
--- /dev/null
+++ b/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