diff --git a/src/Lean/Compiler/IR/ToIR.lean b/src/Lean/Compiler/IR/ToIR.lean
index e826886fee..5a484c0d70 100644
--- a/src/Lean/Compiler/IR/ToIR.lean
+++ b/src/Lean/Compiler/IR/ToIR.lean
@@ -175,36 +175,27 @@ partial def lowerLet (decl : LCNF.LetDecl) (k : LCNF.Code) : M FnBody := do
 
       assert! type == .object
       let ⟨ctorInfo, fields⟩ ← getCtorLayout name
-      let args := args.extract (start := ctorVal.numParams)
+      let irArgs := irArgs.extract (start := ctorVal.numParams)
       let objArgs : Array Arg ← do
         let mut result : Array Arg := #[]
         for i in *...fields.size do
-          match args[i]! with
-          | .fvar fvarId =>
-            if let some (.var varId) := (← get).fvars[fvarId]? then
-              if fields[i]! matches .object .. then
-                result := result.push (.var varId)
-          | .type _ | .erased =>
-            if fields[i]! matches .object .. then
-              result := result.push .irrelevant
+          if fields[i]! matches .object .. then
+            result := result.push irArgs[i]!
         pure result
       let objVar ← bindVar decl.fvarId
       let rec lowerNonObjectFields (_ : Unit) : M FnBody :=
         let rec loop (usizeCount : Nat) (i : Nat) : M FnBody := do
-          match args[i]? with
-          | some (.fvar fvarId) =>
-            match (← get).fvars[fvarId]? with
-            | some (.var varId) =>
-              match fields[i]! with
-              | .usize .. =>
-                let k ← loop (usizeCount + 1) (i + 1)
-                return .uset objVar (ctorInfo.size + usizeCount) varId k
-              | .scalar _ offset argType =>
-                let k ← loop usizeCount (i + 1)
-                return .sset objVar (ctorInfo.size + ctorInfo.usize) offset varId argType k
-              | .object .. | .irrelevant => loop usizeCount (i + 1)
-            | _ => loop usizeCount (i + 1)
-          | some (.type _) | some .erased => loop usizeCount (i + 1)
+          match irArgs[i]? with
+          | some (.var varId) =>
+            match fields[i]! with
+            | .usize .. =>
+              let k ← loop (usizeCount + 1) (i + 1)
+              return .uset objVar (ctorInfo.size + usizeCount) varId k
+            | .scalar _ offset argType =>
+              let k ← loop usizeCount (i + 1)
+              return .sset objVar (ctorInfo.size + ctorInfo.usize) offset varId argType k
+            | .object .. | .irrelevant => loop usizeCount (i + 1)
+          | some .irrelevant => loop usizeCount (i + 1)
           | none => lowerCode k
         loop 0 0
       return .vdecl objVar type (.ctor ctorInfo objArgs) (← lowerNonObjectFields ())
diff --git a/tests/lean/run/ctorMixedRelevance.lean b/tests/lean/run/ctorMixedRelevance.lean
new file mode 100644
index 0000000000..4dbf4fa774
--- /dev/null
+++ b/tests/lean/run/ctorMixedRelevance.lean
@@ -0,0 +1,39 @@
+structure Value1 (α : Type) where
+  fst : α
+
+structure Value2 (α : Type) where
+  snd : α
+
+structure TwoThingies (α : Type) where
+  value1 : Value1 α
+  value2 : Value2 α
+
+/--
+trace: [Compiler.IR] [result]
+    def test1._closed_0 : obj :=
+      let x_1 : obj := ctor_0[TwoThingies.mk] ◾ ◾;
+      ret x_1
+    def test1 : obj :=
+      let x_1 : obj := test1._closed_0;
+      ret x_1
+-/
+#guard_msgs in
+set_option trace.compiler.ir.result true in
+def test1 : TwoThingies Prop := { value1.fst := True, value2.snd := False }
+
+/--
+trace: [Compiler.IR] [result]
+    def test2._closed_0 : obj :=
+      let x_1 : u8 := 0;
+      let x_2 : u8 := 1;
+      let x_3 : obj := box x_2;
+      let x_4 : obj := box x_1;
+      let x_5 : obj := ctor_0[TwoThingies.mk] x_3 x_4;
+      ret x_5
+    def test2 : obj :=
+      let x_1 : obj := test2._closed_0;
+      ret x_1
+-/
+#guard_msgs in
+set_option trace.compiler.ir.result true in
+def test2 : TwoThingies Bool := { value1.fst := true, value2.snd := false }