The Coq mailing list

[Jan-Oliver Kaiser <janno AT mpi-sws.org>]

I think Coq always tries to find the smallest type possible for records 
(and inductives?), mostly ignoring the annotation given by the user.

Related to this is the following example, which can be very annoying 
when doing meta programming:

Record R (P : Prop) : Type := { f : P -> P }.
Check R.
(* R : Prop -> Prop *)

The elim restriction does not apply to these types. The record can be 
used as if it had the annotated type. However, typeclasses and canonical 
structures defined for "Type"s won't trigger.

Best,
Jan-Oliver


On 01/28/2017 01:19 AM, Vadim Zaliva wrote:
> I do not understand why when I define a Record in sort "Type" it ends up in
> "Set"?
>
> Welcome to Coq 8.6 (January 2017)
>
> Coq < Record R (P: nat -> Prop) : Type :=  {f: nat -> nat}.
> R is defined
> f is defined
>
> Coq < Check R.
> R
>      : (nat -> Prop) -> Set
>
> Vadim
>
> --
> CMU ECE PhD candidate
> Mobile: +1(510)220-1060