Ssreflect Users Discussion List

[Enrico Tassi <>]

On Thu, Nov 06, 2014 at 02:41:47PM +0100, Cyril Cohen wrote:
> On 06/11/2014 14:08, bertot wrote:
> > The error message should help users understand that
> > size l == 0 does not match because bigQ  is not an EqType.
> > 
> > How shall we do that?
>
> The problem with this kind of more explanatory error message is to avoid
> showing all the time the full trace of matching attempts. Maybe we could
> provide debug flags with some granularity and encourage the user to use it?

I could imagine a UI where the user drags the pattern
  
  (size _ == 0)

from the error message to the subterm of the goal window that should
match (in his opinion) and receive a more detailed error message.

This should reduce the verbosity of the log (only 1 toplevel match has
to be tried).

> Another way to see it, is that this kind of match failure happens a lot
> in mathcomp, so maybe pattern matching could be tweek to add a remark to
> check for missing canonical structures in some particular cases. For
> example: how easy would it be to see that unification failed where it
> could have succeeded if there were a canonical projection registered?

I had the same feeling while discussing with Yves in person: pattern
matching and canonical structures are so pervasives in mathcomp that
improving these error messages, even if in an ad-hoc mode, is probably
worth it and doable (only few routines need to be traced).

Logging canonical structure inference failures is relatively easy.
Unfortunately due to backtracking the trace would probably contain many
duplicates/bogus failures, and I don't know what can be done in order to
make readable.  Some of the ideas that were used to report
"disambiguation error" in Matita can be surely reused, but I don't know
if they are easy to transpose.  E.g. if A := B, and the structure is on B one
gets an error "proj _ == A" even if after unfolding A the "same"
unification problem succeeds.  In Matita we were trying to rate such
errors with a low relevance, but the link between the success and the
(hence spurious) failure were purely spacial as in "the same piece of
source text", while here it is not clear how to keep the link between
the two unif problems.  HO unification can move (by firing a
delta-beta redex for example) terms around and create terms that are
not part of the input text.

Best,
-- 
Enrico Tassi