"Non strictly positive occurrence of ..."

Question

I try to define the following type

Inductive t : Type -> Type :=
  | I : t nat
  | F : forall A, (t nat -> t A) -> t A.

and I get the following error:

Non strictly positive occurrence of "t" in "forall A : Type, (t nat -> t A) -> t A".

• What does this error mean?
• Is there a way to "fix" the definition to make it valid?
• Where can I learn more about this?

Thanks!

Answer 1

You can look up common error messages in the Coq reference manual: https://coq.inria.fr/distrib/current/refman/language/gallina-specification-language.html?highlight=positive#coq:exn.non-strictly-positive-occurrence-of-ident-in-type

Essentially, if a constructor contains functions (such as t nat -> t A), they cannot mention the inductive type being defined as part of an argument (t nat).

        vvvvvvvvvvvvvv argument
F : ... (t nat -> t A)               -> t A
                  ^ OK ("positive occurence")
         ^ Not OK ("negative occurence")

This section in Certified Programming with Dependent Types (CPDT) explains the problem with a simplified example: http://adam.chlipala.net/cpdt/html/Cpdt.InductiveTypes.html#lab30

If you could define the type

Inductive term : Set :=
| App : term -> term -> term
| Abs : (term -> term) -> term.

then you could define the function

Definition uhoh (t : term) : term :=
  match t with
    | Abs f => f t
    | _ => t
  end.

and uhoh (Abs uhoh) would diverge.