The Coq mailing list

[Alexandre Pilkiewicz <alexandre.pilkiewicz AT polytechnique.org>]

Hi Micheal:

There are two types of implicit arguments: the "normal" ones, and the
"maximally inserted". The intuition is this: the normal ones are
automatically added (say, replace by _) by the system when an argument
after them is provided. The maximally inserted ones are added as soon
as all the arguments before are given. Let us see an example :)

Definition fst A B (ab:A * B) := let (a, _) := ab in a.

fst is of type forall A B : Type, A * B -> A

Say A and B are implicit:

Implicit Arguments fst [A B].

Then this works:
Eval compute in (fst (true, 5)).
and computes true: because the argument ab (here (true, 5)) is given,
A and B are "inserted" (it's equivalent to @fst _ _ (true, 5))

Now what about
Require Import List.
Notation "[ ]" := nil.
Notation "[ a ; .. ; b ]" := (a :: .. (b :: []) ..).
Eval compute in (map fst [(true, 5); (false, 6)]).

It fails, saying:
Error: The term "fst" has type "forall A B : Type, A * B -> A"
 while it is expected to have type "?21 -> ?22".

Here fst is by itself, without arguments: so A and B are *not*
inserted (remember that Implicit Arguments are inserted when an
argument following them is provided). So it has the "nude" type of
fst, which is not of the form _ -> _, and therefore cannot be an
argument of map.

Solution? The first is to go for
Eval compute in (map (@fst _ _) [(true, 5); (false, 6)]).

The second is to use maximally inserted arguments:
Implicit Arguments fst [[A] [B]].
Eval compute in (map fst [(true, 5); (false, 6)]).

Here it works, because A and B are immediately added.

So now what is the problem with apply? Basically, when you have
maximally inserted arguments
apply foo
is like
apply (@foo _ _).
But the systems tries to type (@foo _ _) *before* giving to apply
(which is good if you type something like "apply (5 false)", you
directly have a type error on the application of a nat to a bool). But
there, there is no context to type the _. Hence the type error.
If the arguments are only implicit, it's like typing "apply @foo",
which is typable.

Hopes this helps

Cheers, Alexandre



On Mon, Nov 21, 2011 at 7:08 PM, Michael Shulman 
<mshulman AT ucsd.edu>
 wrote:
> Hi,
>
> What is the difference between
>
> apply lemma.
>
> and
>
> apply @lemma.
>
> ?  I have encountered a few situations where the former fails but the
> latter succeeds.  This confuses me, because in both cases all the
> arguments of lemma (implicit or non-implicit) have to be deduced from
> context.  Is the first one somehow trying to guess the implicit
> arguments too soon or without enough information?
>
> Thanks!
> Mike
>