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

[Martin Stone Davis]

The definition of "strictly positive" for data types is given here 
<https://agda.readthedocs.io/en/latest/language/data-types.html#strict-positivity>, 
but apparently it's different for record types, ruling out *any* 
occurrence to the left of an arrow (not just those in negative 
positions). I doubt that allowing such occurrences could lead to an 
inconsistency. What's the rationale for being so strict about positivity?

--okay
data D : Set₁ where
   d : D → (Set → D) → D

--fails
record R : Set₁ where
   inductive
   field
     r : (Set → R) → R

--R is not strictly positive, because it occurs
--to the left of an arrow
--in the definition of R.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20161102/13388e68/attachment.html