[Agda] Prop in Agda 2.6 - again

[Andrew Pitts]

Here is another question about Prop in Agda 2.6. Can anyone enlighten me?

The documentation says

"Just as for Set, we can define new types in Prop’s as data or record types”

However, although Agda 2.6 allows the declaration of the following one-constructor datatype

data ∃ {l m}(A : Set l)(P : A → Prop m) : Prop (l ⊔ m) where
  _,_ : (x : A)(p : P x) → ∃ A P

if instead I try to define a record type

record ∃ {l m : Level}(A : Set l)(B : A → Prop m) : Prop (l ⊔ m) where
  constructor _,_
  field
    fst : A
    snd : B fst

Agda complains (somewhat ungrammatically) that 

"Set l is not less or equal than Prop (l ⊔ m) when checking the definition of ∃”

So it doesn’t mind the parameter (A : Set l) when defining a datatype in Prop (l ⊔ m), but does mind it when defining a record type.

Why is that?

Andy