Ssreflect Users Discussion List

[Cyril Cohen <>]

Hi Yves,

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?

Good question, I guess that keyed matching already identified
(size l == 0)%B as a possible match. So, if the matching algorithm
displayed its attempt and explained it failed because (size l == 0)%B
and (size _ == 0)%B didn't match, it would a first good step?

Maybe this is enough for the user to realize he should print the
implicit arguments in order to realize that the implicit argument of
size required by size_eq0 is of the form (Equality.sort _). Leading him
to (immediately? :)) understand that BigQ is not the Equality.sort of
anything.

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?

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?

Best,
-- 
Cyril