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?

Whopper

Regarding Agda it's simple: Agda keeps track of polarities of parameters of data types, but not those of indices -- that's why your first definition is accepted and the second one is not, even though they're clearly isomorphic. It's just a deficiency in the type checker -- not a theoretically justified rejection. – Crime

That is, it is wrong to reject the second definition? – Whopper

UseSwitchNSPI does not add inconsistency to the language. I.e. if the language is consistent, then it's not possible to construct a closed proof of false having UseSwitchNSPI accepted, if that's what you're after. "wrong" is a bit strong word, there can be technical reasons not to allow UseSwitchNSPI (e.g. it might not play well with some other features of the language, might be too hard to implement, etc). – Crime

Bad phrasing from my side, but yes, that's exactly what I'm after. I didn't understand why the definition is rejected, because I couldn't construct anything "evil" with it, what I usually can, if I get a NSP-error. – Whopper

The bug has been fixed in Agda (cf. github.com/agda/agda/issues/3778). – Almagest

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

Ironmaster

Thanks for your reply, opening the associated bug report (and solving the issue yourself : )) -- and sorry for the late response, didn't check SO for a long time! – Whopper