 (defun fstar--destruct-var-continuation (from to type response)
   "Replace FROM..TO (with TYPE) with match from RESPONSE."
   (pcase (and response (split-string response "\n"))
-    (`nil (message "No match found for type `%s'." type))
-    (`(,_ ,_ . ,_) (message "Can't destruct `%s' in place (it has more than one constructor)" type))
-    (`(,branch)
+    (`nil
+     (message "No match found for type `%s'." type))
+    (`(,_name ,branch)
      (remove-text-properties from to '(fstar--match-var-type nil))
      (let ((yas-indent-line nil)
            (snip (fstar--prepare-match-snippet branch)))
-       (fstar--expand-snippet snip from to)))))
-
-(defun fstar--destruct-match-var-1 (from to type)
-  "Replace FROM..TO by pattern matching on TYPE."
+       (fstar--expand-snippet snip from to)))
+    (_
+     (message "Can't destruct `%s' in place (it has more than one constructor)" type))))
+
+(defun fstar--destruct-match-var-1 (from to type closed-type)
+  "Replace FROM..TO by pattern matching on TYPE/CLOSED-TYPE.
+TYPE is for display (tuple2 a int); CLOSED-TYPE is reparseable by
+F* (fun a -> (tuple2 a int))."
   (fstar-subp--ensure-available #'user-error 'match)
   (fstar-subp--query
-   (fstar-subp--show-match-query type)
+   (fstar-subp--show-match-query closed-type)
    (fstar-subp--pos-check-wrapper (point)
      (apply-partially #'fstar--destruct-var-continuation from to type))))
 
 (defun fstar--destruct-match-var-at-point ()
   "Destruct match variable inserted with `fstar-insert-match'."
   (pcase (fstar--property-range (point) 'fstar--match-var-type)
-    (`(,from ,to ,type)
-     (fstar--destruct-match-var-1 from to type)
+    (`(,from ,to (,type . ,closed-type))
+     (fstar--destruct-match-var-1 from to type closed-type)
      t)))
 
 (defun fstar-insert-match-dwim ()

  "Handle RESPONSE to a #show-match query.
TYPE is used in error messages"
  (-if-let* ((branches (and response (split-string response "\n"))))
      (let* ((name-str (if (string-match fstar-syntax-id type)
                           (match-string 0 type)
                         "expr"))
             (branch-strs (mapconcat #'fstar--format-one-branch branches "\n"))
             (match (format "match ${%s} with\n%s" name-str branch-strs))
             (indented (fstar--indent-str match (current-column))))
        (let ((yas-indent-line nil))

Briefly tries to get results synchronously to reduce flicker, and
then returns nil (in that case, results are displayed
asynchronously after the fact)."
  (-if-let* ((hole-info (get-text-property (point) 'fstar--match-var-type)))
      ;; FIXME Yasnippet hides this message
      (format "This hole has type `%s'" (car hole-info))
    (when (and (fstar--has-feature 'info) (fstar-subp-available-p)
               (not (fstar-subp--in-issue-p (point))))
      (let* ((query (fstar-subp--positional-info-query (point)))
             (retv (fstar-subp--query-and-wait query 0.01)))
        (pcase retv
          (`(t . (,success ,results))
           (funcall (fstar-subp--info-wrapper
                     (apply-partially #'fstar--eldoc-continuation #'identity)
                     (point))
                    success results))
          (`(needs-callback . ,_)
           (setf (cdr retv)
                 (fstar-subp--info-wrapper
                  (apply-partially #'fstar--eldoc-continuation #'eldoc-message)
                  (point)))))))))

(defun fstar--eldoc-truncate-message (fn &rest args)
  "Forward ARGS to FN within scope of binding for `message-truncate-lines'."
