Coq严格正性检查疑问：自定义term类型为何不通过？

Great question—this is a common pitfall when combining heterogeneous lists (hlists) and inductive types in Coq. Let's break down why your original definition fails, why the two "working" variants pass, and how to fix your term type to meet Coq's requirements.

Why Your Original Definition Fails #

Coq enforces strict positivity for inductive types: the type you're defining (in this case t) can only appear in positive positions in its constructors. A positive position means it's not on the left side of an arrow (->), and not nested inside a function that's used as a parameter to another type in a way that could create a negative occurrence.

Let's look at the problematic part of your definition:

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.

The issue is the function passed to hlist: fun s => match s with ... end. When s is TERM, this function returns t, but this function is used as the B parameter in the hlist definition (where B : A -> Type).

Coq's positivity checker can't see inside the match branch to confirm that t only appears in positive positions here. The hlist type's constructors take B x as an argument, so when B x is t, the checker interprets this as t appearing in a negative position (since it's part of the input to hlist, which is itself an input to Node3). This violates strict positivity, so Coq rejects the definition.

Why the "Working" Variants Pass #

• t_not_quite_1: Replacing t with nat removes the self-reference entirely. nat is a predefined inductive type with no dependencies on your new type, so there's no positivity issue to check.
• t_not_quite_2: Here, the function passed to hlist always returns t_not_quite_2, meaning every element of the hlist is of type t_not_quite_2. This is equivalent to a tuple of t_not_quite_2 values, where t_not_quite_2 clearly appears in a positive position (as the element type of the hlist, which is an input to the constructor). The checker can easily verify this meets strict positivity.

Fixing the Definition #

You have two solid paths forward, depending on whether you want to keep using hlist and termArity for meta-arity management.

Option 1: Ditch the Hlist for Explicit Constructors #

The simplest fix is to define each term constructor directly, which avoids the hlist-induced positivity ambiguity entirely:

Inductive t : Type :=
| Var : String.string -> t
| Let : String.string -> t -> t -> t
| Lam : String.string -> t -> t
| Ap : t -> t -> t
| NumLit : nat -> t
| Plus : t -> t -> t.

This is straightforward, easy to read, and fully compliant with Coq's rules. For a small set of language constructs like yours, this is often the best choice.

Option 2: Use a Wrapper Inductive Type for Strict Positivity #

If you want to keep using hlist and termArity, you can wrap each sort's corresponding type in an inductive type that explicitly places t in a positive position:

(* Wrap each sort's argument type to make positivity clear *)
Inductive sort_arg : sort -> Type :=
| TermArg : t -> sort_arg TERM
| VarArg : String.string -> sort_arg VAR
| NatArg : nat -> sort_arg NAT.

(* Now use hlist with sort_arg instead of the match function *)
Inductive t : Type :=
| Node : forall (sorts : list sort) (code : termArity sorts),
    hlist sort_arg sorts -> t.

Here, sort_arg TERM directly contains t in a positive position (as an argument to the TermArg constructor). The hlist now holds sort_arg s values, and Coq's checker can see that t only appears in positive positions throughout the definition.

You can still construct valid terms with this setup, for example:

Example let_term : t :=
  Node [VAR; TERM; TERM] Let 
    (HCons (VarArg "x") 
      (HCons (TermArg (Node [NAT] NumLit (HCons (NatArg 5) HNil))) 
        (HCons (TermArg (Node [TERM; TERM] Plus 
          (HCons (TermArg (Node [NAT] NumLit (HCons (NatArg 3) HNil))) 
            (HCons (TermArg (Node [VAR] Var (HCons (VarArg "x") HNil))) 
              HNil)))) 
        HNil))).

Fixing the Universe Inconsistency Issue #

Your alternative attempt (using list Type instead of sort) fails due to universe inconsistency because termArity is defined as list Type -> Type, and t is a Type that depends on termArity. This creates a circular dependency within the same universe (Type), which Coq's universe checker rejects.

The solution here is to stick with your original sort type (which lives in Set, a smaller universe than Type). This avoids the circular universe dependency entirely, as termArity now depends on list sort (a Set), not list Type.

Final Takeaways #

• The core issue with your original definition is that Coq's positivity checker can't verify t stays in positive positions when hidden inside a match function passed to hlist.
• Explicit constructors or a wrapper inductive type are both effective ways to enforce strict positivity.
• Using sort instead of directly referencing Type avoids universe inconsistency problems.

内容的提问来源于stack exchange，提问作者Joel Burget