fix: make Repr deriving instance handle explicit type parameters (#…

…5432)

The `Repr` deriving instance was assuming that all type parameters are
implicit. However, if the parameter came from a type index that was
promoted to be a parameter, then it is explicit. The result was that
some explicit constructor arguments were not being represented.

Reported [on
Zulip](https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/.23eval.20removes.20indexes.20inductive.20.20object.20descriptions/near/472301282).

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

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