[Agda] Undocumented (Recursive?) Positivity Checking

[Nils Anders Danielsson]

On 15/10/2019 14.11, Nils Anders Danielsson wrote:
> $ 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: [*, *, *]

This answer may have been somewhat misleading. As far as I recall the
polarities are not used by the positivity checker. I think the following
information might be more relevant to your question:

$ agda -vtc.pos:10 --ignore-interfaces Test.agda | grep "args of List"
checking args of List
args of List = [-[_]->, -[g+]->]

-- 
/NAD