From 3388c63e1118c88746b399fce5eec292cd035261 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 11 Jan 2021 07:08:17 -0800
Subject: [PATCH] fix: typo at `ParamInfo.isExplicit`

---
 src/Lean/Meta/Basic.lean                |  2 +-
 src/Lean/Meta/FunInfo.lean              |  3 ++-
 tests/lean/funInfoBug.lean              | 13 +++++++++++++
 tests/lean/funInfoBug.lean.expected.out |  2 ++
 4 files changed, 18 insertions(+), 2 deletions(-)
 create mode 100644 tests/lean/funInfoBug.lean
 create mode 100644 tests/lean/funInfoBug.lean.expected.out

diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean
index 34a4ae7ee0..92c33ddd2e 100644
--- a/src/Lean/Meta/Basic.lean
+++ b/src/Lean/Meta/Basic.lean
@@ -63,7 +63,7 @@ structure ParamInfo where
   deriving Inhabited
 
 def ParamInfo.isExplicit (p : ParamInfo) : Bool :=
-  !p.implicit && p.instImplicit
+  !p.implicit && !p.instImplicit
 
 structure FunInfo where
   paramInfo  : Array ParamInfo := #[]
diff --git a/src/Lean/Meta/FunInfo.lean b/src/Lean/Meta/FunInfo.lean
index 16004ad2b1..c7d17a569a 100644
--- a/src/Lean/Meta/FunInfo.lean
+++ b/src/Lean/Meta/FunInfo.lean
@@ -64,7 +64,8 @@ private def getFunInfoAux (fn : Expr) (maxArgs? : Option Nat) : MetaM FunInfo :=
           pinfo := pinfo.push {
             backDeps     := backDeps,
             implicit     := decl.binderInfo == BinderInfo.implicit,
-            instImplicit := decl.binderInfo == BinderInfo.instImplicit }
+            instImplicit := decl.binderInfo == BinderInfo.instImplicit
+          }
         let resultDeps := collectDeps fvars type
         let pinfo      := updateHasFwdDeps pinfo resultDeps
         pure { resultDeps := resultDeps, paramInfo := pinfo }
diff --git a/tests/lean/funInfoBug.lean b/tests/lean/funInfoBug.lean
new file mode 100644
index 0000000000..a3efb6ba09
--- /dev/null
+++ b/tests/lean/funInfoBug.lean
@@ -0,0 +1,13 @@
+import Std.Data.AssocList
+
+def l : List (Prod Nat Nat) := [(1, 1), (2, 2)]
+#eval l -- works
+
+def Std.AssocList.ToList : AssocList α β → List (α × β)
+  | AssocList.nil => []
+  | AssocList.cons k v t => (k, v) :: ToList t
+
+instance [Repr α] [Repr β] : Repr (Std.AssocList α β) where
+  reprPrec f _ := repr f.ToList
+
+#reduce (l.toAssocList)
diff --git a/tests/lean/funInfoBug.lean.expected.out b/tests/lean/funInfoBug.lean.expected.out
new file mode 100644
index 0000000000..924299a583
--- /dev/null
+++ b/tests/lean/funInfoBug.lean.expected.out
@@ -0,0 +1,2 @@
+[(1, 1), (2, 2)]
+Std.AssocList.cons 1 1 (Std.AssocList.cons 2 2 Std.AssocList.nil)