       (format "This hole has type `%s'" (car hole-info))
     (when (and (fstar--has-feature 'lookup) (fstar-subp-available-p)
                (not (fstar-subp--in-issue-p (point))))
-      (let* ((query (fstar-subp--positional-lookup-query (point)))
+      (let* ((query (fstar-subp--positional-lookup-query (point) '(type)))
              (retv (fstar-subp--query-and-wait query 0.01)))
         (pcase retv
           (`(t . (,status ,results))

                  (delq nil (mapcar #'fstar-subp-company-legacy--prepare-candidate
                                    (split-string response "\n")))))))))

(defun fstar-subp--positionless-lookup-query (symbol)
  "Prepare a header for an info query for SYMBOL."
  (when (equal symbol "")
    (user-error "Looking up an empty name"))
  (if (fstar--has-feature 'json-subp)
      (make-fstar-subp-query
       :query "lookup"
       :args `(("symbol" . ,symbol)))
    (format "#info %s" symbol)))

(defun fstar-subp-company--candidate-fqn (candidate)

  "\\([^\0]+?\\)\\(?:#doc \\([^\0]+?\\)\\)?\\'")

(cl-defstruct fstar-lookup-result
  source-file name def-start def-end type doc def)

(defun fstar-lookup-result-sig (info &optional help-kbd)
  "Format signature of INFO.
