A simple Ltac2 tactic to debug broken "refine" statements

[patrick-nicodemus]

I often run into errors when using refine but sometimes the error messages are a little bit overwhelming. One of the uses I see for writing custom tactics is to basically just reimplement tactics which already exist but inserting handwritten error messages to indicate the point of failure, and make the problem easier to fix.

I decided to implement my own fairly naive refine_debug tactic as follows:
refine_debug(s) computes the type of the term s and tries to unify it with the goal type g by calling unify_debug.
unify_debug t g works as follows:

• if t and g are both applications f x1 x2... xn, then first try to unify the heads of both applications, then check that the argument lists are the same length, and recursively call unify_debug on each parallel pair of arguments. Otherwise just try to unify them using the standard tactic.

Ideally, if the type of your term has broadly the same shape as the shape of the goal, calling this function will tend to recurse through the subterms, unifying as they go, and when it fails it will fail at the smallest pair of parallel subterms in the structure which failed to unify, so you'll have a more readable error message. In addition, because unify succeeded at all previous terms, you'll have a clear picture of which unification variables were already solved, whereas when you just try to unify both terms all at once, it reports "t failed to unify with g" where t contains all the holes that were present originally (since unification failed, it is regarded as solving none of these holes, when in reality it probably solved many of them.)

Right now I'm just copy-pasting this snippet into the library temporarily when I am having trouble getting refine to work. I highly recommend upgrading to Rocq 9.0 before trying this because of the typeclass hintdb bug in Coq 8.20 and below.

Module Refine_debug.
Require Import Ltac2.Ltac2.
Ltac2 typeof x := Constr.type x.
Ltac2 println s := Message.print (Message.of_string s).
Import Constr.Unsafe.
Ltac2 rec unify_debug x y :=
  match Constr.Unsafe.kind x, Constr.Unsafe.kind y with
  | App xhd xargs, App yhd yargs => 
                      println "Both applications.";
                      match Control.case (fun () => (unify $xhd $yhd)) with
                      | Val ((), _) =>
                          let x := Message.of_constr xhd in
                          Message.print
                            (Message.concat (Message.of_string "Same hd:") x);
                          if Int.equal (Array.length xargs) (Array.length yargs) then
                            Array.iter2 unify_debug xargs yargs
                          else
                            (println "Different lengths, aborting."; fail)
                      | Err (exn) => unify $x $y
                      end
  | _, _ => unify $x $y
  end.

Ltac2 refine_debug x :=
  match! goal with
  | [|- ?g ] => let y := typeof x in
               unify_debug y g
  end.
End Refine_debug.
Import Refine_debug.

[JasonGross]

There is also Set Debug "unification" and Set Debug "tactic-unification" I believe.

[patrick-nicodemus]

@JasonGross I'm aware of Set Debug "unification" but I'm afraid I don't fully understand how to read the output. It prints what goal it's trying to solve at any given time, but it isn't clear to me whether it succeeds in solving those goals or gives up and moves onto the next goal, or if it is backtracking, etc., so at any given point it's not clear to me how to tell what the current stage in the algorithm is and what has currently been solved.

Also there are some symbols like | in the output that I'm not sure how to interpret. The developers encouraged me to read the Coq source code for the evar_conv algorithm to understand what triggers the debug instrumentation to print various symbols, but this seems like a lot of work.

[JasonGross]

It might be worth opening an issue on the Coq bug tracker requesting a "unification-simple" debug option that matches the format and level of information of this tactic