Why is my definition not allowed because of strict positivity?

Question

I have the following two definitions that result in two different error messages. The first definition is declined because of strict positivity and the second one because of a universe inconsistency.

(* non-strictly positive *)
Inductive SwitchNSP (A : Type) : Type :=
| switchNSP : SwitchNSP bool -> SwitchNSP A.

Fail Inductive UseSwitchNSP :=
| useSwitchNSP : SwitchNSP UseSwitchNSP -> UseSwitchNSP.

(* universe inconsistency *)
Inductive SwitchNSPI : Type -> Type :=
| switchNSPI : forall A, SwitchNSPI bool -> SwitchNSPI A.

Fail Inductive UseSwitchNSPI :=
| useSwitchNSPI : SwitchNSPI UseSwitchNSPI -> UseSwitchNSPI.

Chatting on gitter revealed that universe (in)consistencies are checked first, that is, the first definition adheres this check, but then fails because of a strict positivity issue.

As far as I understand the strict positivity restriction, if Coq allows non-strictly positivity data type definitions, I could construct non-terminating functions without using fix (which is pretty bad).

In order to make it even more confusing, the first definition is accepted in Agda and the second one gives a strict positivity error.

data Bool : Set where
  True : Bool
  False : Bool

data SwitchNSP (A : Set) : Set where
  switchNSP : SwitchNSP Bool -> SwitchNSP A

data UseSwitchNSP : Set where
  useSwitchNSP : SwitchNSP UseSwitchNSP -> UseSwitchNSP

data SwitchNSPI : Set -> Set where
  switchNSPI : forall A -> SwitchNSPI Bool -> SwitchNSPI A

data UseSwitchNSPI : Set where
  useSwitchNSP : SwitchNSPI UseSwitchNSPI -> UseSwitchNSPI

Now my question is two-folded: first, what is the "evil example" I could construct with the above definition? Second, which of the rules applies to the above definition?

Some notes:

• To clarify, I think that I do understand why the second definition is not allowed type-checking-wise, but still feel that there is nothing "evil" happening here, when the definition is allowed.
• I first thought that my example is an instance of this question, but enabling universe polymorphism does not help for the second definition.
• Can I use some "trick" do adapt my definition such that it is accepted by Coq?

Answer 1

Unfortunately, there's nothing super deep about this example. As you noted Agda accepts it, and what trips Coq is the lack of uniformity in the parameters. For example, it accepts this:

Inductive SwitchNSPA (A : Type) : Type :=
| switchNSPA : SwitchNSPA A -> SwitchNSPA A.

Inductive UseSwitchNSPA :=
| useSwitchNSPA : SwitchNSPA UseSwitchNSPA -> UseSwitchNSPA.

Positivity criteria like the one used by Coq are not complete, so they will reject harmless types; the problem with supporting more types is that it often makes the positivity checker more complex, and that's already one of the most complex pieces of the kernel.

As for the concrete details of why it rejects it, well, I'm not 100% sure. Going by the rules in the manual, I think it should be accepted?

EDIT: The manual is being updated.

Specifically, using the following shorter names to simplify the following:

Inductive Inner (A : Type) : Type := inner : Inner bool -> Inner A.
Inductive Outer := outer : Inner Outer -> Outer.

1. Correctness rules

2. Positivity condition
   Here,

   X = Outer
   T = forall x: Inner X, X
   

   So we're in the second case with

   U = Inner X
   V = X
   

   1. V is easy, so let's do that first: V = (X) falls in the first case, with no t_i, hence is positive for X
   2. For U: is U = Inner X strictly positive wrt X? Here,

      T = Inner X
      

      Hence we're in the last case: T converts to (I a1) (no t_i) with

      I = Inner
      a1 = X
      

      and X does not occur in the t_i, since there are no t_i. Do the instantiated types of the constructors satisfy the nested positivity condition? There is only one constructor:
      1. inner : Inner bool -> Inner X. Does this satisfy the nested positivity condition? Here,

         T = forall x: Inner bool, Inner X.
         

         So we're in the second case with

         U = Inner bool
         V = Inner X
         

         1. X does not occur in U, so X is strictly positive in U.
         2. Does V satisfy the nested positivity condition for X? Here,

            T = Inner X
            

            Hence we're in the first case: T converts to (I b1) (no u_i) with

            I = Inner
            b1 = X
            

            There are no u_i, so V satisfies the nested positivity condition.

I have opened a bug report. The manual is being fixed.

Two more small things:

1. I can't resist pointing that your type is empty:

   Theorem Inner_empty: forall A, Inner A -> False.
   Proof. induction 1; assumption. Qed.
   

2. You wrote:

   if Coq allows non-strictly positivity data type definitions, I could construct non-terminating functions without using fix (which is pretty bad).

   That's almost correct, but not exactly: if Coq didn't enforce strict positivity, you could construct non-terminating functions period, which is bad. It doesn't matter whether they use fix or not: having non-termination in the logic basically makes it unsound (and hence Coq prevents you from writing fixpoints that do not terminate by lazy reduction).