[Agda] More heterogeneous equality.

[effectfully]

Hi. Agda 2.4.3 allows to define

    data _≅_ {α} {A : Set α} (x : A) : ∀ {β} {B : Set β} -> B -> Set where
      refl : x ≅ x

`A' and `B' lie in different universes and the whole thing lies in
`Set'. This is very convenient, but is it reliable? If so, can the
definition in the standard library be replaced by this one?

Agda rejects

    eq : ∀ {α β} -> Set α ≅ Set β -> α ≅ β
    eq refl = refl

      -- Refuse to solve heterogeneous constraint Set α : Set (lsuc α) =?=
      -- Set β : Set (lsuc β)

Is it a natural restriction?

Also, can somebody explain how Agda infers levels in data/record
declarations now? Is there a paper?