[Agda] Bug in the strictly positivity check

[Dan Doel]

On Wednesday 29 September 2010 8:23:43 am Florent Balestrieri wrote:
> I thought records and data definitions should be treated in the same
> way, but the attached program shows Agda makes a difference.

How old is your 2.2.7 copy?

Until relatively recently, records were not positivity checked at all. 
Presumably this was because recursive records weren't intended to be allowed, 
but they nevertheless were.

However, the bug has been fixed (by positivity checking, not disabling 
recursive records). You may not have rebuilt since it was, though.

-- Dan