[Agda] [newbie] universe levels and BUILTIN EQUALITY

[Roman]

Andreas, it wasn't previously possible to define

    data _≡_ {a} {A : Set a} : A → A → Set where
      refl : ∀ x → x ≡ x

because this requires forcing of `x` to type check. IIRC, it wasn't
possible to define

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

either (or was it?). Hence I assumed that both the definitons require
forcing (which is a poorly documented feature, so I don't really
know).

But anyway, both the definitions type check currently, so does Agda
approve something hazardous that should be rejected instead? But if
Agda justifies this, then how many other hazardous definitions pass
the type checker as well? Or did I just misunderstand you completely?