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

[Fredrik Nordvall Forsberg]

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)...

>     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.
> 


-- 
Fredrik Nordvall Forsberg,
Department of Computer and Information Sciences,
University of Strathclyde.
The University of Strathclyde is a charitable body, registered in
Scotland, with registration number SC015263.