# Why do Agda and Coq disagree on strict positivity?

I've stumbled across a confusing disagreement between Agda and Coq that is not obviously related to the most well known distinctions between their type theories (e.g., (im)predicativity, induction-recursion, etc.).

In particular, the following definition is accepted by Agda:

  data Ty : Set0 -> Set0 where
c1 : Ty ℕ
c2 : Ty (Ty ℕ)


whereas the equivalent Coq definition is rejected because the appearance of [Ty _] as an index of itself in c2 is considered to violate strict positivity.

  Inductive Ty : Set -> Set :=
| c1 : Ty nat
| c2 : Ty (Ty nat).


In fact, this case is almost verbatim an example from Coq'Art Section 14.1.2.1 of violating strict positivity:

  Inductive T : Set -> Set := c : (T (T nat)).


But I don't see the reasons for this difference between the type theories. The classic example of proving False using a negative occurrence of a type in a constructor argument is clear to me, but I can't see how one might derive a contradiction from this style of indexing (regardless of otherwise strictly positive constructor arguments).

Poking around the literature, Dybjer's early Inductive Families paper makes an offhand comment about Paulin-Mohring's solution in the CID paper having slightly different restrictions, and vaguely suggests the differences might be related to impredicativity, but doesn't elaborate further. Dybjer's paper seems to allow this, while Paulin-Mohring's clearly prohibits it.

Apparently I'm not the first to notice this difference of opinion, and some believe this definition shouldn't be permitted in either system (https://lists.chalmers.se/pipermail/agda/2012/004249.html), but I haven't found any explanations of why it is either sound in one system but not the other, or just a difference of opinion.

So I suppose I have several questions:

1. Is this an example of a monotone, but non-strictly-positive type? (In Coq; clearly Agda considers it strictly positive)
2. Why does Agda permit this while Coq rejects it? It is simply an idiosyncratic difference in the interpretation of "strictly positive," is there a subtle difference between Coq and Agda that makes it sound in Agda and unsound in Coq, or is it a matter of taste driven by particular theoretical preferences?
3. Is there a meaningful difference between the first definition above, and the equivalent inductive-recursive definition below?

Inductive-recursive definition:

  mutual
data U : Set0 -> Set0 where
c : (i : Fin 2) -> U (T i)
T : Fin 2 -> Set0
T zero = ℕ
T (suc zero) = U ℕ


I'm happy to have pointers to relevant literature.

• As far as I know, Coq is stricter than what the underlying theory allows, because it was easier to implement and useful enough in practice. This answer about a different but related case is as far as my understanding goes. – Gilles Aug 29 '13 at 23:43
• This definition is not accepted by the current dev version of Agda: Ty is not strictly positive, because it occurs in an index of the target type of the constructor c2 in the definition of Ty. – gallais Aug 30 '13 at 16:42
• Yes, you're right, someone else pointed this out to me last night. I had been using Debian's 2.3.0.1 package, but 2.3.2.1 from Cabal rejects both the direct and IR definitions. It looks like a seemingly unrelated bug made positivity checking on indices stricter: code.google.com/p/agda/issues/detail?id=690 Since it was discussed on the list without explicitly being marked a soundness issue, I'm still wondering if the type itself is sound. – Colin Gordon Aug 30 '13 at 18:03

The issue seems to be confusion resulting from a confluence of two factors:

1. I was using a stale version of Agda (2.3.0.1). It appears that prior to 2.3.2, Agda simply wasn't checking strict positivity of the indices of constructor results (see the bug I linked elsewhere in the thread).
2. A closer reading of Dybjer's Inductive Families paper suggests that he may have intended that the inductive type being defined not be bound when typing the indices of a constructor result. Section 3.2.1 gives the scheme for inductive constructors in prose, and apparently I misread the language describing the binding environments of each portion of the scheme.

This closer reading is of course consistent with the check that Coq and (recent versions of) Agda perform, that prohibit any appearance of T in its own indices.

A possible reason for the difference, as your own remarks hint, is impredicativity. Coq historically had an impredicative set (still available as a flag i believe!)