fix: filter declarations that are not valid dot methods

src/Lean/Server/Completion.lean

@@ -176,23 +176,32 @@ private def idCompletion (ctx : ContextInfo) (lctx : LocalContext) (stx : Syntax
   runM ctx lctx do
     idCompletionCore ctx stx expectedType?
 
+private def isDotCompletionMethod (info : ConstantInfo) : MetaM Bool :=
+  forallTelescopeReducing info.type fun xs _ => do
+    for x in xs do
+      let localDecl ← getLocalDecl x.fvarId!
+      if localDecl.type.getAppFn.isConstOf info.name.getPrefix then
+        return true
+    return false
+
 private def dotCompletion (ctx : ContextInfo) (info : TermInfo) (expectedType? : Option Expr) : IO (Option CompletionList) :=
   runM ctx info.lctx do
     let name? ←
       try
         let type ← instantiateMVars (← inferType info.expr)
+        -- dbg_trace "dot >> {info.stx}, {info.expr} : {type}, {info.stx.isIdent}"
         match type.getAppFn with
         | Expr.const name .. => pure (some name)
         | _ => pure none
       catch _ =>
         pure none
-    -- dbg_trace "dot >> {info.stx}, {info.expr} : {type}, {info.stx.isIdent}"
     match name? with
     | some name =>
       (← getEnv).constants.forM fun declName c => do
         if  declName.getPrefix == name then
           unless (← isBlackListed c.name) do
-            addCompletionItem c.name.getString! c.type expectedType?
+            if (← isDotCompletionMethod c) then
+              addCompletionItem c.name.getString! c.type expectedType?
     | _ =>
       if info.stx.isIdent then
         idCompletionCore ctx info.stx expectedType?

tests/lean/interactive/completion.lean.expected.out

@@ -1,24 +1,12 @@
 {"textDocument": {"uri": "file://completion.lean"},
  "position": {"line": 3, "character": 22}}
-{"items":
- [{"label": "foo", "detail": "Foo → Nat"},
-  {"label": "mk", "detail": "Nat → Foo"}],
- "isIncomplete": true}
+{"items": [{"label": "foo", "detail": "Foo → Nat"}], "isIncomplete": true}
 {"textDocument": {"uri": "file://completion.lean"},
  "position": {"line": 5, "character": 23}}
-{"items":
- [{"label": "foo", "detail": "Foo → Nat"},
-  {"label": "mk", "detail": "Nat → Foo"}],
- "isIncomplete": true}
+{"items": [{"label": "foo", "detail": "Foo → Nat"}], "isIncomplete": true}
 {"textDocument": {"uri": "file://completion.lean"},
  "position": {"line": 7, "character": 28}}
-{"items":
- [{"label": "foo", "detail": "Foo → Nat"},
-  {"label": "mk", "detail": "Nat → Foo"}],
- "isIncomplete": true}
+{"items": [{"label": "foo", "detail": "Foo → Nat"}], "isIncomplete": true}
 {"textDocument": {"uri": "file://completion.lean"},
  "position": {"line": 9, "character": 29}}
-{"items":
- [{"label": "foo", "detail": "Foo → Nat"},
-  {"label": "mk", "detail": "Nat → Foo"}],
- "isIncomplete": true}
+{"items": [{"label": "foo", "detail": "Foo → Nat"}], "isIncomplete": true}

tests/lean/interactive/completion3.lean.expected.out

@@ -2,7 +2,6 @@
  "position": {"line": 7, "character": 9}}
 {"items":
  [{"label": "b", "detail": "S → Bool"},
-  {"label": "mk", "detail": "Nat → String → Bool → S"},
   {"label": "x", "detail": "S → Nat"},
   {"label": "y", "detail": "S → String"}],
  "isIncomplete": true}
@@ -10,7 +9,6 @@
  "position": {"line": 12, "character": 5}}
 {"items":
  [{"label": "b", "detail": "S → Bool"},
-  {"label": "mk", "detail": "Nat → String → Bool → S"},
   {"label": "x", "detail": "S → Nat"},
   {"label": "y", "detail": "S → String"}],
  "isIncomplete": true}
@@ -18,7 +16,6 @@
  "position": {"line": 16, "character": 5}}
 {"items":
  [{"label": "b", "detail": "S → Bool"},
-  {"label": "mk", "detail": "Nat → String → Bool → S"},
   {"label": "x", "detail": "S → Nat"},
   {"label": "y", "detail": "S → String"}],
  "isIncomplete": true}
@@ -27,6 +24,5 @@
 {"items":
  [{"label": "x", "detail": "S → Nat"},
   {"label": "b", "detail": "S → Bool"},
-  {"label": "mk", "detail": "Nat → String → Bool → S"},
   {"label": "y", "detail": "S → String"}],
  "isIncomplete": true}

tests/lean/interactive/completion4.lean.expected.out

@@ -3,8 +3,6 @@
 {"items":
  [{"label": "fn1", "detail": "S → Nat → IO Unit"},
   {"label": "fn2", "detail": "S → Bool → IO Unit"},
-  {"label": "mk",
-   "detail": "(Nat → IO Unit) → (Bool → IO Unit) → (String → Bool) → S"},
   {"label": "pred", "detail": "S → String → Bool"}],
  "isIncomplete": true}
 {"textDocument": {"uri": "file://completion4.lean"},
@@ -12,8 +10,6 @@
 {"items":
  [{"label": "fn1", "detail": "S → Nat → IO Unit"},
   {"label": "fn2", "detail": "S → Bool → IO Unit"},
-  {"label": "mk",
-   "detail": "(Nat → IO Unit) → (Bool → IO Unit) → (String → Bool) → S"},
   {"label": "pred", "detail": "S → String → Bool"}],
  "isIncomplete": true}
 {"textDocument": {"uri": "file://completion4.lean"},
@@ -21,16 +17,12 @@
 {"items":
  [{"label": "fn1", "detail": "S → Nat → IO Unit"},
   {"label": "fn2", "detail": "S → Bool → IO Unit"},
-  {"label": "mk",
-   "detail": "(Nat → IO Unit) → (Bool → IO Unit) → (String → Bool) → S"},
   {"label": "pred", "detail": "S → String → Bool"}],
  "isIncomplete": true}
 {"textDocument": {"uri": "file://completion4.lean"},
  "position": {"line": 20, "character": 21}}
 {"items":
- [{"label": "mk",
-   "detail": "(Nat → IO Unit) → (Bool → IO Unit) → (String → Bool) → S"},
-  {"label": "fn1", "detail": "S → Nat → IO Unit"},
+ [{"label": "fn1", "detail": "S → Nat → IO Unit"},
   {"label": "fn2", "detail": "S → Bool → IO Unit"},
   {"label": "pred", "detail": "S → String → Bool"}],
  "isIncomplete": true}

tests/lean/interactive/completion5.lean.expected.out

@@ -1,8 +1,7 @@
 {"textDocument": {"uri": "file://completion5.lean"},
  "position": {"line": 9, "character": 15}}
 {"items":
- [{"label": "mk", "detail": "Nat → Bool → String → C"},
-  {"label": "b1", "detail": "C → String"},
+ [{"label": "b1", "detail": "C → String"},
   {"label": "f1", "detail": "C → Nat"},
   {"label": "f2", "detail": "C → Bool"}],
  "isIncomplete": true}

tests/lean/interactive/editCompletion.lean.expected.out

@@ -6,7 +6,4 @@
     "end": {"line": 3, "character": 22}}}]}
 {"textDocument": {"uri": "file://editCompletion.lean"},
  "position": {"line": 3, "character": 22}}
-{"items":
- [{"label": "foo", "detail": "Foo → Nat"},
-  {"label": "mk", "detail": "Nat → Foo"}],
- "isIncomplete": true}
+{"items": [{"label": "foo", "detail": "Foo → Nat"}], "isIncomplete": true}