How Agda's --type-in-type can lead to a contradiction.

Main.agda

{-# OPTIONS --type-in-type #-}
module Main where

open import Data.Empty


data _≡_ (A : Set) : Set → Set where
  refl : A ≡ A

subst : {P : Set → Set} → {x y : Set} → x ≡ y → P y → P x
subst refl p = p


data Con : Set where
  con : (A : Set) → Con ≡ A → (A → ⊥) → Con

mkCon : (Con → ⊥) → Con
mkCon f = con Con refl f

unCon : Con → (Con → ⊥)
unCon (con A eq f) = subst {\x → x → ⊥} eq f

σ : Con → ⊥
σ c = unCon c c

ω : ⊥
ω = σ (mkCon σ)

Turns out this was a bug in the type-checker; with the latest version of Agda, the above program is no longer accepted unless --no-positivity-check is also added.