The following definition of D should be rejected:

{-# OPTIONS --type-in-type #-}

data ≡ {A : Set} (x : A) : A → Set where refl : x ≡ x

data ⊥ : Set where

data D : Set where abs : ∀ {E : Set} → D ≡ E → (E → ⊥) → D

D should not be strictly positive in equality.

Why? If you could do the same thing without --type-in-type, then I would understand. Can you?

I saw that you also posted a message to the mailing list. Please discuss there rather than here.

Now the pos. checker also looks into the indices of data types for occurences of the parameters. Since 'x' appears in an index in the type of constructor 'refl', equality is not monotone in its second argument.