diff --git a/src/Lean/Elab/Deriving/Repr.lean b/src/Lean/Elab/Deriving/Repr.lean
index 0a03ed1cc0e3..18ebfd850103 100644
--- a/src/Lean/Elab/Deriving/Repr.lean
+++ b/src/Lean/Elab/Deriving/Repr.lean
@@ -59,15 +59,17 @@ where
         let mut ctorArgs := #[]
         let mut rhs : Term := Syntax.mkStrLit (toString ctorInfo.name)
         rhs ← `(Format.text $rhs)
-        -- add `_` for inductive parameters, they are inaccessible
-        for _ in [:indVal.numParams] do
-          ctorArgs := ctorArgs.push (← `(_))
-        for i in [:ctorInfo.numFields] do
-          let x := xs[indVal.numParams + i]!
-          let a := mkIdent (← mkFreshUserName `a)
-          ctorArgs := ctorArgs.push a
-          let localDecl ← x.fvarId!.getDecl
-          if localDecl.binderInfo.isExplicit then
+        for i in [:xs.size] do
+          -- Note: some inductive parameters are explicit if they were promoted from indices,
+          -- so we process all constructor arguments in the same loop.
+          let x := xs[i]!
+          let a ← mkIdent <$> if i < indVal.numParams then pure header.argNames[i]! else mkFreshUserName `a
+          if i < indVal.numParams then
+            -- add `_` for inductive parameters, they are inaccessible
+            ctorArgs := ctorArgs.push (← `(_))
+          else
+            ctorArgs := ctorArgs.push a
+          if (← x.fvarId!.getBinderInfo).isExplicit then
             if (← inferType x).isAppOf indVal.name then
               rhs ← `($rhs ++ Format.line ++ $(mkIdent auxFunName):ident $a:ident max_prec)
             else if (← isType x <||> isProof x) then
diff --git a/tests/lean/run/derivingRepr.lean b/tests/lean/run/derivingRepr.lean
index 37ef4c2b562e..897669794a0f 100644
--- a/tests/lean/run/derivingRepr.lean
+++ b/tests/lean/run/derivingRepr.lean
@@ -88,3 +88,25 @@ structure test2 : Type 1 where
 #guard_msgs in #eval test1.wrap Nat (by simp)
 /-- info: { ty := _, wrap := _ } -/
 #guard_msgs in #eval test2.mk Nat (by simp)
+
+/-!
+Indices promoted to parameters are still explicit. Need to include them as arguments.
+-/
+
+inductive Promote : (loc : Int) -> (state : Nat) -> Type where
+  | mk : (loc : Int) -> (state : Nat) -> (id : Nat) -> Promote loc state
+  deriving Repr
+
+/-- info: Promote.mk 3 2 1 -/
+#guard_msgs in #eval Promote.mk 3 2 1
+
+/-!
+Promoted indices that are types are represented as `_`.
+-/
+
+inductive Promote2 : Type → Type where
+  | mk : (α : Type) → Promote2 α
+  deriving Repr
+
+/-- info: Promote2.mk _ -/
+#guard_msgs in #eval Promote2.mk Nat