Coq strict positivity is puzzling

Question

I'm working on a development with a language with terms, variables, and nat literals, where the arity of language constructs in predefined:

Inductive sort : Set := TERM | VAR | NAT.

Inductive termArity : list sort -> Set :=
  | Var    : termArity [VAR]
  | Let    : termArity [VAR ; TERM ; TERM]
  | Lam    : termArity [VAR ; TERM]
  | Ap     : termArity [TERM ; TERM]
  | NumLit : termArity [NAT]
  | Plus   : termArity [TERM ; TERM]
  .

The definition of a term I'd like to use contains one child matching each type in its arity specification (hlist is heterogeneous lists from CPDT):

Inductive t : Type :=
| Node : forall (sorts : list sort) (code : termArity sorts),
    hlist (fun s : sort => match s with
                           | TERM => t
                           | VAR => String.string
                           | NAT => nat
                           end) sorts
          -> t.

But coq rejects it with 'Non strictly positive occurrence of "t"'.

As expected, replacing the t in the definition with nat convinces coq that it's okay:

Inductive t : Type :=
| Node : forall (sorts : list sort) (code : termArity sorts),
    hlist (fun s : sort => match s with
                           | TERM => nat
                           | VAR => String.string
                           | NAT => nat
                           end
          ) sorts
    -> t.

As does, surprisingly, always returning t.

Inductive t : Type :=
| Node : forall (sorts : list sort) (code : termArity sorts),
    hlist (fun s : sort => t) sorts
    -> t.

Why does my attempted definition fail, while this passes the positivity checker? How can I fix my definition?

Edit: another attempt which forgoes the codes but fails due to universe inconsistency:

Definition var : Set := String.string.

Inductive termArity : list Type -> Type :=
  | Var    : termArity [var]
  | Let    : termArity [t; t]
  | Lam    : termArity [var; t]
  | Ap     : termArity [t; t]
  | NumLit : termArity [nat]
  | Plus   : termArity [t; t]

with t : Type :=
| Node : forall (sorts : list Type) (code : termArity sorts),
    hlist (fun s : Type => s) sorts -> t.

Whole file:

Require Coq.Bool.Bool. Open Scope bool.
Require Coq.Strings.String. Open Scope string_scope.
Require Coq.Arith.EqNat.
Require Coq.Arith.PeanoNat.
Require Coq.Arith.Peano_dec. Open Scope nat_scope.
Require Coq.Lists.List. Open Scope list_scope.
Require Coq.Vectors.Vector. Open Scope vector_scope.
Require Fin.

Module Export LocalListNotations.
Notation " [ ] " := nil (format "[ ]") : list_scope.
Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) : list_scope.
Notation " [ x ; y ; .. ; z ] " := (cons x (cons y .. (cons z nil) ..)) : list_scope.
End LocalListNotations.

Module Core.
    Set Implicit Arguments.

    (* cpdt heterogeneous lists *)
    Section hlist.
      Variable A : Type.
      Variable B : A -> Type.

      Inductive hlist : list A -> Type :=
      | HNil : hlist nil
      | HCons : forall (x : A) (ls : list A), B x -> hlist ls -> hlist (x :: ls).

      Variable elm : A.

      Inductive member : list A -> Type :=
      | HFirst : forall ls, member (elm :: ls)
      | HNext : forall x ls, member ls -> member (x :: ls).

      Fixpoint hget ls (mls : hlist ls) : member ls -> B elm :=
        match mls with
          | HNil => fun mem =>
            match mem in member ls' return (match ls' with
                                              | nil => B elm
                                              | _ :: _ => unit
                                            end) with
              | HFirst _ => tt
              | HNext _ _ => tt
            end
          | HCons x mls' => fun mem =>
            match mem in member ls' return (match ls' with
                                              | nil => Empty_set
                                              | x' :: ls'' =>
                                                B x' -> (member ls'' -> B elm)
                                                -> B elm
                                            end) with
              | HFirst _ => fun x _ => x
              | HNext _ mem' => fun _ get_mls' => get_mls' mem'
            end x (hget mls')
        end.
    End hlist.

    Arguments HNil [A B].
    Arguments HCons [A B x ls].

    Arguments HFirst [A elm ls].
    Arguments HNext [A elm x ls].

    Module Exp.
      Inductive sort : Set := TERM | VAR | NAT.

      Inductive termArity : list sort -> Set :=
        | Var    : termArity [VAR]
        | Let    : termArity [VAR ; TERM ; TERM]
        | Lam    : termArity [VAR ; TERM]
        | Ap     : termArity [TERM ; TERM]
        | NumLit : termArity [NAT]
        | Plus   : termArity [TERM ; TERM]
        .

      (* coq complains this is not strictly positive. *)
      Inductive t : Type :=
      | Node3 : forall (sorts : list sort) (code : termArity sorts),
          hlist (fun s : sort => match s with
                                 | TERM => t
                                 | VAR => String.string
                                 | NAT => nat
                                 end) sorts
                -> t.

      (* exactly the same definition, but replacing t with nat, is
         not flagged as non-strictly-positive. this makes sense to me. *)
      Inductive t_not_quite_1 : Type :=
      | Node1 : forall (sorts : list sort) (code : termArity sorts),
          hlist (fun s : sort => match s with
                                 | TERM => nat
                                 | VAR => String.string
                                 | NAT => nat
                                 end
                ) sorts
          -> t_not_quite_1.

      (* this also (like the failed definition) returns t in the
         hlist type, but surprisingly typechecks! I don't understand
         how this is different *)
      Inductive t_not_quite_2 : Type :=
      | Node2 : forall (sorts : list sort) (code : termArity sorts),
          hlist (fun s : sort => t_not_quite_2) sorts
          -> t_not_quite_2.
    End Exp.
End Core.

Does your universe inconsistency go away if you replace var : Set with var : Type ? — Jason Gross
It becomes an anomaly: 'Anomaly "A universe comparison can only happen between variables." Please report at coq.inria.fr/bugs.' — Joel Burget
What version of Coq are you using? Does it say that in 8.7.1? If so, it's a bug that should be reported on GitHub — Jason Gross
Thanks -- the upgrade from 8.7.0 to 8.7.1 fixed the anomaly. It now just reports a universe inconsistency. — Joel Burget

Jason Gross Jason Gross · Accepted Answer · 2018-01-10T06:23:47

Coq does not see through match statements in the positivity checker; this is a long-standing feature request, see https://github.com/coq/coq/issues/4701 and https://github.com/coq/coq/issues/1433.

I believe that it will work if you turn it into an inductive:

Inductive kind_of_sort t : sort -> Type :=
| term_kind : t -> kind_of_sort t TERM
| var_kind : String.string -> kind_of_sort VAR
| nat_kind : nat -> kind_of_sort NAT.

and then use this in place of the match statement.

Coq strict positivity is puzzling

1 Answers