[Agda] Why is "strictly positive" more strict for record types?

[Roman]

`R` doesn't correspond to `D` — it corresponds to

data D′ : Set₁ where
  d : ((Set → D′) → D′) → D′

which is not strictly positive. `R` that corresponds to `D` looks like this:

record R : Set₁ where
  inductive
  field
    r₁ : R
    r₂ : Set → R

A record can be represented as a one-constructor data type, and each
field of the record becomes an argument to this constructor.