[Agda] Problems with strict positivity

[Manuel Bärenz]

Yes, that seems to fix it! Thank you very much.

On 25/04/17 17:11, Andreas Abel wrote:
> Hello Manuel,
>
> I recently fixed
>
>   https://github.com/agda/agda/issues/1899
>
> The fix has not been released yet, it will be part of Agda 2.5.3 or
> 2.6.0.
>
> Could you try your example with the development version of Agda?
>
> Best,
> Andreas
>
> On 25.04.2017 16:50, Manuel Bärenz wrote:
>> 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
>>
>>
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>
>

-- 
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/20170504/42f92bf8/attachment-0001.sig>