Why do Agda and Coq disagree on strict positivity?

Question

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.

Thanks in advance.

Answer 1

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.

Answer 2

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!)

Quoting Adam Chlipala's book http://adam.chlipala.net/cpdt/html/Universes.html

The Coq tools support a command-line flag -impredicative-set, which modifies Gallina in a more fundamental way by making Set impredicative. A term like forall T : Set, T has type Set, and inductive definitions in Set may have constructors that quantify over arguments of any types. To maintain consistency, an elimination restriction must be imposed, similarly to the restriction for Prop. The restriction only applies to large inductive types, where some constructor quantifies over a type of type Type. In such cases, a value in this inductive type may only be pattern-matched over to yield a result type whose type is Set or Prop. This rule contrasts with the rule for Prop, where the restriction applies even to non-large inductive types, and where the result type may only have type Prop. In old versions of Coq, Set was impredicative by default. Later versions make Set predicative to avoid inconsistency with some classical axioms. In particular, one should watch out when using impredicative Set with axioms of choice. In combination with excluded middle or predicate extensionality, inconsistency can result. Impredicative Set can be useful for modeling inherently impredicative mathematical concepts, but almost all Coq developments get by fine without it.