[Agda] Undocumented (Recursive?) Positivity Checking

[Yotam Dvir]

Hi there,

I was wondering how it is that Agda accepts the following:

```agda
data RoseTree (A : Set) : Set where
  node : A → (List (RoseTree A)) → RoseTree A
```

I couldn’t find any literature on this, nor does the documentation explain this.
In fact, the documentation rules this out!
(see https://agda.readthedocs.io/en/v2.6.0.1/language/data-types.html#strict-positivity <https://agda.readthedocs.io/en/v2.6.0.1/language/data-types.html#strict-positivity>)

However, the `POLARITY` pragma helped:
(see https://agda.readthedocs.io/en/v2.6.0.1/language/positivity-checking.html#polarity-pragmas <https://agda.readthedocs.io/en/v2.6.0.1/language/positivity-checking.html#polarity-pragmas>)

```agda
postulate
  F : Set → Set

{-# POLARITY F ++ #-} -- does not compile otherwise

data RoseFree (A : Set) : Set where
  node : A → (F (RoseFree A)) → RoseFree A
```

Have I hit the point here, i.e. Agda determines that the polarity of `List`’s first argument is strictly positive?
Any explanation or reference will be appreciated.

A related less important question: what is the purpose of the polarities `+` and `-`?
Seems to me that using  `*` instead would never make any difference.

Cheers,
Yotam
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20191015/8662e4d4/attachment.html>