The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Hi,

> (if we forget about the complications in Coq's extraction code itself).

Thanks for clarifying. This last sentence is indeed what I meant.

> Whether it is a good idea for Coq to ignore the type annotation
> explicitly given by the user is an orthogonal issue. I thought this bug
> had been fixed some times ago.

Facing the counter-intuitive display, different approaches are possible.

Let me give one which may finally be easy to teach.

Let's just give a name of the form Type to "proof-irrelevant Prop"
rather than approximating it with Prop. In the Coq kernel, there is
actually already such as a name which is Type(0-), but referring to
Vladimir Voevodsky's terminology for homotopy levels, let's rather
call it Type(-1).

Let's also give a name of the form Type to "predicative
Set". Internally, as mentioned in an earlier discussion, the name
Type(0) is already used for that. Let's keep the name Set so that it
can be thought as either predicative Set or impredicative Set.

Let's then extend the hierarchy of subtyping as follows:

             Prop   
Type(-1) <=         <= Set <= Type(1) <= Type(2) <= ...
            Type(0)

This step being done, we can change the printing so that it reflects
the internal hierarchy rather than confusingly approximating it with
Prop and Set. Given

  Record R (P : Prop) : Type := { f : P -> P }.
  Record R' (P : nat -> Prop) : Type :=  { f' : nat -> nat }.

we would see the following:

  Check R.
  (* R : Prop -> Type *)
  Check R'.
  (* R' : (nat -> Prop) -> Type *)

  Set Printing Universes.
  Check R.
  (* R : Prop -> Type@{-1} *)
  Check R'.
  (* R' : (nat -> Prop) -> Type@{0} *)

but still have (by subtyping):

  Check R True : Prop.
  (* R : Prop *)
  Check R' (fun _ => True) : Set.
  (* R' : Set *)

Would it be clearer?

If yes, the only price to pay is to give a proper status to these
constant levels -1 and 0 of the Type hierarchy, and to make it part of
the pedagogy of Coq.

Hope it helps,

Hugo