diff --git a/src/Lean/Server/Completion.lean b/src/Lean/Server/Completion.lean
index 75623140c28c..0312a117145c 100644
--- a/src/Lean/Server/Completion.lean
+++ b/src/Lean/Server/Completion.lean
@@ -211,10 +211,13 @@ private def getCompletionKindForDecl (constInfo : ConstantInfo) : M CompletionIt
     return CompletionItemKind.event
   else if (← isProjectionFn constInfo.name) then
     return CompletionItemKind.field
-  else if (← whnf constInfo.type).isForall then
-    return CompletionItemKind.function
   else
-    return CompletionItemKind.constant
+    let isFunction : Bool ← withTheReader Core.Context ({ · with maxHeartbeats := 0 }) do
+      return (← whnf constInfo.type).isForall
+    if isFunction then
+      return CompletionItemKind.function
+    else
+      return CompletionItemKind.constant
 
 private def addUnresolvedCompletionItemForDecl (label : Name) (declName : Name) (score : Float) : M Unit := do
   if let some c := (← getEnv).find? declName then