[Agda] Why does Agda think this is not strictly positive?

[Frédéric Blanqui]

Hi.


Le 20/07/2016 à 11:22, Fredrik Nordvall Forsberg a écrit :
> Hi Roman,
>
> On 20/07/16 09:57, Roman wrote:
>> Is Agda correct that D is not strictly positive? Is there something I
>> can do to make positivity check pass?
>>      data Coerce β : ∀ {α} -> Set α -> Set β where
>>        coerce : ∀ {A} -> A -> Coerce β A
> This implies that Coerce β A is equivalent to (A -> Coerce β A)...
Could you please give more explanation about that?

Regards,

Frédéric.

>>      data D : Set where
>>        C : Coerce zero D -> D
> ...which means that the type of C is equivalent to
> (D -> Coerce zero D) -> D. Doesn't look very positive, and indeed, if we
> allow the definition of D, it is very easy to define
>
> open import Data.Empty
>
> oops : D -> ⊥
> oops (C (coerce x)) = oops x
>
> Cheers,
> Fredrik
>
>> Agda reports
>>
>>      D is not strictly positive, because it occurs
>>      in the third argument to Coerce
>>      in the type of the constructor C
>>      in the definition of D.
>>
>