[Agda] Undocumented (Recursive?) Positivity Checking

[Nils Anders Danielsson]

On 15/10/2019 13.40, Yotam Dvir wrote:
> Have I hit the point here, i.e. Agda determines that the polarity of
> `List`’s first argument is strictly positive?

$ cat Test.agda
data List {a} (A : Set a) : Set a where
   []  : List A
   _∷_ : (x : A) (xs : List A) → List A
$ agda -vtc.polarity:10 Test.agda
Checking Test ([…]/Test.agda).
Polarity of Test.List: [*, +]
Polarity of Test.List.[]: [*, *]
Polarity of Test.List._∷_: [*, *]
Polarity of Test._∷_-0: [*, *, *]
Polarity of Test._∷_-1: [*, *, *]

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

I think these polarities are used by the sized types machinery.

-- 
/NAD