[Agda] Problems with strict positivity

[Manuel Bärenz]

Dear list,

I'm experiencing strange behaviour with strict positivity. It seems to
me that in some cases, the strict positivity test is different for
records than for algebraic datatypes.

Consider this example, which might need a fairly recent development
version of the standard library:

A : ∀ {c ℓ} {C : Container c} → ⟦ C ⟧ (Set ℓ) → Set (c ⊔ ℓ)
A (s , f) = ∀ p → f p

record thing {ℓ} (C : Container ℓ) : Set ℓ where
  coinductive
  field
    getThing : ⟦ C ⟧ (thing C)
open thing

record testRecord {ℓ} {C : Container ℓ} (aThing : thing C) : Set ℓ where
  inductive
  field
    testField : A (map testRecord (getThing aThing))

data testData {ℓ} {C : Container ℓ} (aThing : thing C) : Set ℓ where
  testCons : A (map testData (getThing aThing)) → testData aThing

I'm sorry for not being able to condense it further.

The strange behaviour is this: The definition of testRecord is rejected
with the following error message:

testRecord is not strictly positive, because it occurs
in the 7th argument to map
in the 4th argument to A
in the definition of testRecord.

But the definition of testData goes through without a problem! Is there
an actual difference between the two? Should there be one?

(The reason why I'm worrying about this is because I need a record for
coinduction.)

Best regards, Manuel

-- 
I'm using Enigmail on Thunderbird to sign and encrypt my emails with GPG! Why not try it yourself? https://enigmail.net/


-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: OpenPGP digital signature
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170425/235481fc/attachment.sig>