The Coq mailing list

[Christian Doczkal <christian.doczkal AT inria.fr>]

Hi

> > Variable classic_dec : forall P : Prop, {P} + {~P}.
> > Fail Check forall (X : Type), classic_dec (bool = X).
> > (* The term "X" has type "Type" while it is expected to have type
> > Set *)

> I think this is because bool has sort Set and we thus can't compare
> bool and Type. I don't know enough about universes, but maybe there
> is something like a universe polymorphic version of bool, such that
> this equality is well-typed?

This is just an artifact of type inference for "eq", which always tries
to type the RHS with the type assigned to the LHS ("Set" in this case).
The variants below are accepted:

Variable classic_dec : forall P : Prop, {P} + {~P}.
Check fun (X : Type) => classic_dec (bool = X :> Type).
Check fun (X : Type) => classic_dec (X = bool).

(Note that you also need a (fun => _) as (classic_dec P) is not a
type.)

Best,
Christian