[Agda-dev] Positivity checker and abstract blocks

[Andreas Abel]

Andres,

 From what you quote, both seem to be GuardPos...

On 02.01.2016 17:31, Andrés Sicard-Ramírez wrote:
> Hi,
>
> Given the data constructors of `Occurrence` (
> https://github.com/agda/agda/blob/master/src/full/Agda/TypeChecking/Positivity/Occurrence.hs#L20-L27
> )
> why `Foo` is `StrictPos` in
>
>    {-# OPTIONS -v tc.pos:25 #-}
>
>    data Foo : Set where
>      foo : Foo → Foo
>
> that is,
>
>    $ agda Test.agda
>    ...
>    positivity graph for Foo foo
>    Foo
>      -[g+]-> Foo InDefOf Test.Foo (ConArgType
>                  Test.Foo.foo Here)

g+ means GuardPos

>
>
> but `Foo` is `GuardPos` in an abstract block, that is,
>
>    {-# OPTIONS -v tc.pos:25 #-}
>
>    abstract
>      data Foo : Set where
>        foo : Foo → Foo
>
>    $ agda Test.agda
>    ...
>    positivity graph for Foo foo
>
>    Foo
>      -[g+]-> Foo InDefOf Test.Foo (ConArgType
>                  Test.Foo.foo Here)

same here.

>
> ?
>
> Best,
>

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

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

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/