[Agda] Problems with strict positivity

[Andreas Abel]

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
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www.cse.chalmers.se/~abela/