The Coq mailing list

[Michael Shulman <mshulman AT ucsd.edu>]

Hi Arnaud,

Thanks for your reply.  The case I encountered involved no
typeclasses, however, so that can't be the problem.  Unfortunately, it
is in the middle of a lengthy development, and without any
understanding of what the underlying issue might be, it is hard for me
to come up with a simpler example.  I realize that's not very helpful;
sorry.

Mike

On Mon, Nov 21, 2011 at 22:54, Arnaud Spiwack
<aspiwack AT lix.polytechnique.fr>
 wrote:
> Hi Mike,
>
> Here is another working script that may illuminate what's happening:
>
> Definition idmap {A} : A -> A := fun x => x.
>
> Theorem thm A (x:A) : A.
> Proof.
>   apply (@idmap _).
>   assumption.
> Defined.
>
> Coq uses type information from the goal to try and solve the holes properly.
> That said, last time I checked, it didn't interact well with typeclasses,
> which are solved too eagerly (an improper typeclass can then be inferred
> before the goal is inspected). I suspect this is what's hitting you. Though
> this is pure guesswork.
>
>
> Arnaud
>
>
> On 21 November 2011 23:35, Michael Shulman 
> <mshulman AT ucsd.edu>
>  wrote:
>>
>> Hi Alexandre,
>>
>> Thanks for your reply!  Something like that was my first guess as to
>> what was going on.  But it seems to me that there must be something
>> more than that (or else I am just not understanding), because "apply
>> lemma" sometimes (indeed, usually) does work, even when 'lemma' has
>> maximally inserted implicit arguments.  For instance:
>>
>>  Definition idmap {A} : A -> A := fun x => x.
>>
>>  Theorem thm A (x:A) : A.
>>  Proof.
>>    apply idmap.
>>    assumption.
>>  Defined.
>>
>> Here the argument A is maximally inserted to idmap.  So if "apply
>> idmap" is immediately converted to "apply (@idmap _)", then how can
>> Coq determine that the _ there should be A before it passes the term
>> off to 'apply'?
>>
>> Mike
>>
>> On Mon, Nov 21, 2011 at 13:29, Alexandre Pilkiewicz
>> <alexandre.pilkiewicz AT polytechnique.org>
>>  wrote:
>> > 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
>> >>
>> >
>> >
>>
>
>