fix: derive Repr missing a comma

src/Lean/Elab/Deriving/Repr.lean

@@ -32,7 +32,7 @@ def mkBodyForStruct (header : Header) (indVal : InductiveVal) : TermElabM Term :
       let fieldName := fieldNames[i]!
       let fieldNameLit := Syntax.mkStrLit (toString fieldName)
       let x := xs[numParams + i]!
-      if i > numParams then
+      if i != 0 then
         fields ← `($fields ++ "," ++ Format.line)
       if (← isType x <||> isProof x) then
         fields ← `($fields ++ $fieldNameLit ++ " := " ++ "_")

tests/lean/1668.lean

@@ -0,0 +1,18 @@
+structure Point where
+  x : Nat
+  y : Nat
+deriving Repr
+
+structure PPoint (α : Type) where
+  x : α
+  y : α
+deriving Repr
+
+def origin : Point :=
+  { x := Nat.zero, y := Nat.zero }
+
+def natOrigin : PPoint Nat :=
+  { x := Nat.zero, y := Nat.zero }
+
+#eval origin
+#eval natOrigin

tests/lean/1668.lean.expected.out

@@ -0,0 +1,2 @@
+{ x := 0, y := 0 }
+{ x := 0, y := 0 }