[Agda] Simple contradiction from type-in-type

[Dominique Devriese]

Samuel,

2013/3/14 Samuel Gélineau <gelisam at gmail.com>:
>     data Con : Set where
>       -- curry's paradox would use this.
>       --   mkCon : (Con → ⊥) → Con
>       -- since we have type-in-type but not negative occurrences,
>       -- fake it using propositional equality.
>       con : (A : Set) → Con ≡ A → (A → ⊥) → Con

Interesting!  But actually, the above does not seem to be accepted by
the latest (darcs) version of Agda, even when I specify to allow
type-in-type.  I need to also turn off the positivity checker, despite
what your comment suggests.

Regards,
Dominique