`fresh` name: use match result if variable, do something else if it's a constant

Question

In a solver tactic, I'm trying to generate reasonably readable names for the generated hypotheses (so things are at least somewhat readable in cases where the automation fails). fresh is happy with identifiers or strings, but doesn't like constants. So in the big match I have repeated cases like:

   match goal with
   | |- context [ if (?a + ?b <? ?a) then _ else _ ] =>
     let W := fresh "W" a b in solve_overflow_test W a b
(* | … *)
   end

which work fine if I get a situation like n + m <? n (generating Wnm as the name), but fail if I run into a n + 1 <? n, where fresh complains about the 1 being neither an identifier nor a string.

I can manually expand a test and substitute placeholders inline, as in

   match goal with
   | |- context [ if (?a + ?b <? ?a) then _ else _ ] =>
     tryif is_var a
       then
         tryif is_var b
         then let W := fresh "W" a b in solve_overflow_test W a b
         else let W := fresh "W" a "_" in solve_overflow_test W a b
       else
         tryif is_var b
         then let W := fresh "W" "_" b in solve_overflow_test W a b
         else let W := fresh "W" "_" "_" in solve_overflow_test W a b
(* | … *)
   end

but that's an exponential 2^n blowup in tactic size, which really isn't worth the slight improvement in readability of the generated proof.

So I'd like to tuck the test & substitution away into a helper tactic. is_var and friends aren't value tactics, and while there's apparently a workaround), I couldn't get it to work here. (I'm not returning values, but… ??? and CPS-ing everything after the fresh (if that's even an option) would also be too ugly.)

Is there a way that I missed, or should I rather just give up on including the matched identifiers in the generated names?