The Coq mailing list

[Michael Shulman <mshulman AT ucsd.edu>]

I have managed to extract a fairly small example which exhibits the
behavior I mentioned.  There are no typeclasses or coercions.

~~~

Definition compose {A B C} (g : B -> C) (f : A -> B) (x : A) := g (f x).

Axiom reflect : Type -> Type.
Axiom reflect_factor : forall {X Y}, (X -> Y) -> (reflect X -> Y).
Axiom map_to_reflect : forall X, X -> reflect X.

Definition reflect_functor {X Y} (f : X -> Y) : reflect X -> reflect Y
  := reflect_factor (compose (map_to_reflect Y) f).

Axiom reflect_factoriality : forall {X Y Z} (g : Y -> Z) (f : X -> Y)
(rx : reflect X),
  (reflect_factor g (reflect_functor f rx)) = (reflect_factor (compose g f) 
rx).

Definition reflect_functoriality {X Y Z} (g : Y -> Z) (f : X -> Y) (rx
: reflect X) :
  (reflect_functor g (reflect_functor f rx)) = (reflect_functor
(compose g f) rx).
Proof.
  apply @reflect_factoriality.
Defined.

~~~

In the proof above, "apply reflect_factoriality" fails with the
message 'Error: Impossible to unify "Y" with "Z".' whereas "apply
@reflect_factoriality" succeeds.  Can anyone explain the difference?

Thanks!
Mike

On Mon, Nov 21, 2011 at 10:08, 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
>