fix: typo at ParamInfo.isExplicit

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 := #[]

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 }

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)

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)