              (when (fstar--in-code-p)
                (substring-no-properties prefix))))))
       (`candidates
-       (fstar-subp-company-candidates arg))
+       (fstar-subp-company-candidates arg (fstar-subp-company--completion-kind-at-point)))
       (`meta
        `(:async . ,(apply-partially #'fstar-subp-company--async-meta arg)))
       (`doc-buffer

  (fstar-subp-company--async-lookup candidate '(defined-at)
    (apply-partially #'fstar-subp-company--location-continuation callback)))

(defun fstar-subp-company-candidates (prefix)
  "Compute candidates for PREFIX.
Briefly tries to get results synchronously to reduce flicker (see
URL https://github.com/company-mode/company-mode/issues/654), and
then returns an :async cons, as required by company-mode."
  (let ((retv (fstar-subp--query-and-wait (fstar-subp--completion-query prefix) 0.03)))
    (pcase retv
      (`(t . (,status ,results))
       (fstar-subp-company--candidates-continuation #'identity status results))

                     (setf (cdr retv)
                           (apply-partially
                            #'fstar-subp-company--candidates-continuation cb))))))))

(defun fstar-subp-company--completion-kind-at-point ()
  "Compute kind of prefix at point.
Must be called with syntax table `fstar--fqn-at-point-syntax-table'"
  (save-excursion
    (goto-char (point-at-bol))
    (cond
     ((looking-at-p "open ") "open")
     ((looking-at-p "include ") "include")
     ((looking-at-p "module \\(?:\\s_\\|\\sw\\)+ *=") "module-alias")
     ((looking-at-p ".* let open \\s_*\\=") "let-open")
     (t "symbol"))))

(defun fstar-subp-company-backend (command &optional arg &rest _)
  "Company backend for F*.
