The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

Le jeudi 10 mars 2011 à 19:56 +0100, Stéphane Lescuyer a écrit :
> Hi Guillaume,
> 
> There's a non-implicit argument (f) to your lemma before the maximal
> implicit typeclass argument (P f).
> If you make this argument implicit as well, everything works fine:
> 
> Implicit Arguments l [[f] [p']].
> 
> Not sure if that's intuitive behaviour or not, but as a rule of thumb,
> if you expect (P f) to be determined automatically from context, then
> f as well should be inferrable from context.

Matthieu Sozeau gave a similar answer in a private (?) mail, and the
issue now makes sense to me. Thanks.

Unfortunately, this approach turns out to be unpractical on the actual
code where theorems are more complicated. Indeed, it requires all the
preceding arguments (including unrelated ones!) to be implicit and
maximally inserted too, just to be sure Coq doesn't stop prematurely
from inserting evars. Unfortunately, some of them cannot be inferred
automatically in most cases and have to be specified, so the user is
forced to use a cumbersome syntax (either @... or (...:=...)), which
defeats the whole point.

Best regards,

Guillaume