The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

If/when you have time, if you don't mind, I'd appreciate an example.  I tried the following, which was the first thing that came to mind when you said "partial application", but it behaved as expected:

  Polymorphic Definition typeof {A : Type} (_ : A) := A.

  Polymorphic Definition typeof' := @typeof.

  Check @typeof. (* forall A : Type (* Top.7 *), A -> Type (* Top.7 *) *)
  Check @typeof'. (* forall A : Type (* Top.7 *), A -> Type (* Top.7 *) *) 
  Check @typeof. (* forall A : Type (* Top.7 *), A -> Type (* Top.7 *) *)

  Definition typeofnat := @typeof nat.

  Check typeofnat. (* nat -> Set *)

I tested a similar thing with two type arguments, and only giving it one of them, and it still worked.

Thanks.

-Jason

On Thu, Jul 26, 2012 at 12:34 AM, Tom Prince <tom.prince AT ualberta.net> wrote:

Jason Gross <jasongross9 AT gmail.com> writes:

> Was there some other problem with it?

It has been a long time since I looked at this, and I don't have time to
test it now, but vaguely recall that the issue is that partial
application (which is the only type of application) loses the
polymorpism.

  Tom