The Coq mailing list

[Andrej Bauer <andrej.bauer AT andrej.com>]

Here is another way to circumvent the problem, I think. First we
define the offending type which lands in Prop, then we define an alias
for it:

Parameter A : Type.
Definition cow (P : forall (x : A), A -> Type) : Type := forall x y : A, P x 
y.
Inductive Q' (x : A) : A -> Type := horn : Q' x x.
Definition Q : A -> A -> Type := Q'.
Definition q := cow Q.
Definition r := forall x y : A, Q x y.

Now r is in Type. But this still deserves to be a bug.

With kind regards,

Andrej