The Coq mailing list

[Guillaume Brunerie <guillaume.brunerie AT gmail.com>]

Hi,
The following does not work as expected:

> Parameter f : Type -> Type.
> Notation s := (f Type).
>
> Check s.

Indeed the result is 

> f Type
>     : Type

instead of

> s

    : Type

I guess the reason is that "Type" is polymorphic, and is never considered to be the same as itself (my example works if you replace "f Type" by "f Set").

Is there a way to make Coq display the notation "s"?

I do not want to use explicit universes ("Definition U := Type"), because I would then need to keep track by hand of the levels to avoid universe inconsistencies.
I tried to make the argument of "f" implicit, but this does not work.

Thanks,


Guillaume