From 74411aa472c7ff47cd59fcd7ee5c1b3bab133884 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 9 Mar 2022 12:32:11 -0800
Subject: [PATCH] fix: do not display implicit fields

---
 src/Lean/Elab/Deriving/Repr.lean      | 10 ++++++----
 tests/lean/tabulate.lean              | 13 +++++++++++++
 tests/lean/tabulate.lean.expected.out |  1 +
 3 files changed, 20 insertions(+), 4 deletions(-)
 create mode 100644 tests/lean/tabulate.lean
 create mode 100644 tests/lean/tabulate.lean.expected.out

diff --git a/src/Lean/Elab/Deriving/Repr.lean b/src/Lean/Elab/Deriving/Repr.lean
index 338ab60752..5e59d6a3af 100644
--- a/src/Lean/Elab/Deriving/Repr.lean
+++ b/src/Lean/Elab/Deriving/Repr.lean
@@ -68,10 +68,12 @@ where
           let x := xs[indVal.numParams + i]
           let a := mkIdent (← mkFreshUserName `a)
           ctorArgs := ctorArgs.push a
-          if (← inferType x).isAppOf indVal.name then
-            rhs ← `($rhs ++ Format.line ++ $(mkIdent auxFunName):ident $a:ident max_prec)
-          else
-            rhs ← `($rhs ++ Format.line ++ reprArg $a)
+          let localDecl ← getLocalDecl x.fvarId!
+          if localDecl.binderInfo.isExplicit then
+            if (← inferType x).isAppOf indVal.name then
+              rhs ← `($rhs ++ Format.line ++ $(mkIdent auxFunName):ident $a:ident max_prec)
+            else
+              rhs ← `($rhs ++ Format.line ++ reprArg $a)
         patterns := patterns.push (← `(@$(mkIdent ctorName):ident $ctorArgs:term*))
         `(matchAltExpr| | $[$patterns:term],* => Repr.addAppParen (Format.group (Format.nest (if prec >= max_prec then 1 else 2) ($rhs:term))) prec)
       alts := alts.push alt
diff --git a/tests/lean/tabulate.lean b/tests/lean/tabulate.lean
new file mode 100644
index 0000000000..06c7852355
--- /dev/null
+++ b/tests/lean/tabulate.lean
@@ -0,0 +1,13 @@
+inductive Vector (α : Type u) : Nat → Type u
+  | nil : Vector α 0
+  | cons : α → Vector α n → Vector α (n+1)
+  deriving Repr
+
+infix:67 " :: " => Vector.cons
+
+def tabulate (f : Fin n → α) : Vector α n :=
+  match n with
+  | 0   => Vector.nil
+  | n+1 => f 0 :: tabulate (f ∘ Fin.succ)
+
+#eval tabulate fun i : Fin 5 => i
diff --git a/tests/lean/tabulate.lean.expected.out b/tests/lean/tabulate.lean.expected.out
new file mode 100644
index 0000000000..5dcf25c211
--- /dev/null
+++ b/tests/lean/tabulate.lean.expected.out
@@ -0,0 +1 @@
+Vector.cons 0 (Vector.cons 1 (Vector.cons 2 (Vector.cons 3 (Vector.cons 4 (Vector.nil)))))