<html><head><meta http-equiv="Content-Type" content="text/html; charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">Hi there,<div class=""><br class=""></div><div class="">I was wondering how it is that Agda accepts the following:</div><div class=""><br class=""></div><div class="">```agda</div><div class=""><div class="">data RoseTree (A : Set) : Set where</div><div class=""> node : A → (List (RoseTree A)) → RoseTree A</div></div><div class="">```</div><div class=""><br class=""></div><div class="">I couldn’t find any literature on this, nor does the documentation explain this.</div><div class="">In fact, the documentation rules this out!</div><div class="">(see <a href="https://agda.readthedocs.io/en/v2.6.0.1/language/data-types.html#strict-positivity" class="">https://agda.readthedocs.io/en/v2.6.0.1/language/data-types.html#strict-positivity</a>)</div><div class=""><br class=""></div><div class="">However, the `POLARITY` pragma helped:</div><div class="">(see <a href="https://agda.readthedocs.io/en/v2.6.0.1/language/positivity-checking.html#polarity-pragmas" class="">https://agda.readthedocs.io/en/v2.6.0.1/language/positivity-checking.html#polarity-pragmas</a>)</div><div class=""><br class=""></div><div class="">```agda</div><div class=""><div class="">postulate</div><div class=""> F : Set → Set</div><div class=""><br class=""></div><div class="">{-# POLARITY F ++ #-} -- does not compile otherwise</div></div><div class=""><br class=""></div><div class=""><div class="">data RoseFree (A : Set) : Set where</div><div class=""> node : A → (F (RoseFree A)) → RoseFree A</div></div><div class="">```</div><div class=""><br class=""></div><div class="">Have I hit the point here, i.e. Agda determines that the polarity of `List`’s first argument is strictly positive?</div><div class="">Any explanation or reference will be appreciated.</div><div class=""><br class=""></div><div class="">A related less important question: what is the purpose of the polarities `+` and `-`?</div><div class="">Seems to me that using `*` instead would never make any difference.</div><div class=""><br class=""></div><div class="">Cheers,</div><div class="">Yotam</div></body></html>