Consider the following Inductive definitions. The first one is simply a generalization of the second one, but Coq complains that the first one does not have "strictly positive" occurrences. As you can see from the demonstration in the second version, *semantically* it's strictly positive, but Coq somehow can't see that. And also as you can see, the second one is less general than the first one (works only for n=1,2 instead of any natural-number length), so I would *really* like to use the first one. Does anyone have a suggestion?

```
Require Import List.
Axiom type: Type.
Axiom ftype: type -> Type.
Fail Inductive expr (ty: type): Type :=
| Const (c: ftype ty)
| Func (argt: list type) (args: fold_right (fun t => prod (expr t)) unit argt).
(*The command has indeed failed with message:
Non strictly positive occurrence of "expr" in
"forall argt : list type,
fold_right (fun t : type => prod (expr t)) unit argt ->
expr ty". *)
Inductive expr (ty: type): Type :=
| Const (c: ftype ty)
| Func1 (argt: type) (arg: expr argt)
| Func2 (argt1 argt2: type) (arg1: expr argt1) (arg2: expr argt2).
```

what about using something `hlist`

-like?

```
Require Import List.
Import ListNotations.
Axiom type: Type.
Axiom ftype: type -> Type.
Inductive klist (k : type -> Type) : list type -> Type :=
| Nil : klist k []
| Cons {ty tys} : k ty -> klist k tys -> klist k (ty :: tys).
Inductive expr (ty : type): Type :=
| Const (c: ftype ty)
| Func {tys : list type} (x : klist expr tys).
```

I've also tried an `hlist`

indexed by a `list Type`

directly, which seems more standard, but that gave a universe inconsistency — possibly because packing types makes `hlist`

a "large" datatype, but I try to stay away from universes whenever I can:

```
Inductive hlist : list Type -> Type :=
| Nil : hlist []
| Cons {ty tys} : ty -> hlist tys -> hlist (ty :: tys).
Inductive expr (ty : type): Type :=
| Const (c: ftype ty)
| Func {tys : list type} (x : hlist (map expr tys)).
(*
Error: Universe inconsistency. Cannot enforce hlist.u0 =
max(Set, type.u0, ftype.u0, hlist.u0+1, hlist.u1+1).
*)
```

I wanted to double-check I didn't fool myself somehow and my proposal makes sense, so here's a possible development:

```
Require Import List.
Import ListNotations.
Inductive type :=
| Bool
| Fun (dom cod : type).
Fixpoint ftype (ty : type) : Type :=
match ty with
| Bool => bool
| Fun dom cod => ftype dom -> ftype cod
end.
Inductive klist {k : type -> Type} : list type -> Type :=
| Nil : klist []
| Cons {ty tys} : k ty -> klist tys -> klist (ty :: tys).
Arguments klist : clear implicits.
Inductive expr {ty : type}: Type :=
| Const (c: ftype ty)
| Func {tys : list type} (x : klist (@expr) tys).
Arguments expr : clear implicits.
Definition test : expr (Fun Bool Bool) :=
Func (Cons (@Const Bool false) (Cons (@Const Bool true) Nil)).
```

@Pierre-Marie Pédrot I think you had ideas how to extend positivity to match, maybe fix is also possible in some cases ? I wonder what the generated induction principle would look like here.

My plan was to allow at least the stuff we know how to encode via a nested indirection.

(That's basically @Paolo Giarrusso 's solution above.)

Last updated: Jun 24 2024 at 00:02 UTC