[Agda-dev] Positivity checker and abstract blocks

[Andrés Sicard-Ramírez]

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)


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)

?

Best,

-- 
Andrés