```
typing_size: forall (Γ : context) (t T : term), typing Γ t T -> size
Γ: context
a: well_typed Γ
n := (fix well_typed_size (Γ : context) (w : well_typed Γ) {struct w} : size :=
match w with
| welltyped_nil => base
| welltyped_cons_abs Γ' t wt' p =>
(typing_size Γ' t p.2.π1 p.2.π2.2 + well_typed_size Γ' wt')%nat
| welltyped_cons_def Γ' b t wt' p =>
(typing_size Γ' b t p.1.1 +
typing_size Γ' t p.2.π1 p.2.π2.2 +
well_typed_size Γ' wt')%nat
end) Γ a : nat
```

I'm defining `typing_size`

as a fixpoint where the structural argument is `Constr Γ a`

(here destructured), and I want to return `n`

as defined here.

However, Coq tells me that the recursive definition is ill-formed. The issue specifically comes from `p.1.1`

as when I replace it with a dummy value, Coq doesn't complain anymore. I wonder why `p.2.π2.2`

is accepted but `p.1.1`

not

(`.1`

and `.2`

are `fst`

and `snd`

, `.π1`

and `.π2`

are the first and second projection on a sigT)

(Hopefully I didn't remove the issue when I simplified the example)

Do you have a small enough example that you could show here?

The standard counter-example to WN but non-SN is precisely due to the fact we (used to) not to reduce.

namely `fix F (u : unit) := (fun _ => 0) (F tt)`

.

@Yann Leray what version are you using? The guard condition was changed in 8.16 (IIRC) to handle this situation

Funny you should say that; I was porting code which worked in 8.14 to 8.16; I also just checked and it works as is with Coq 8.15.2

I'll make a small example now

I wouldn't know how to make this smaller :

```
Inductive two := A | B.
Implicit Types (t : two) (l : list two).
Definition P (on_list : list two -> Type) l t :=
prod unit (match t with A | B => on_list l end).
Definition P_size {on_list} (on_list_size : forall l, on_list l -> nat) l t (w : P on_list l t) : nat :=
match t return P _ _ t -> nat with
| A | B => fun tu => on_list_size _ (snd tu)
end w.
Inductive All_fold_two {P_on_list : list two -> two -> Type} : list two -> Type :=
| fold_nil : All_fold_two nil
| fold_cons_abs l : All_fold_two l -> P_on_list l A -> All_fold_two (cons A l)
| fold_cons_def l : All_fold_two l -> P_on_list l B -> All_fold_two (cons B l).
Arguments All_fold_two : clear implicits.
Definition All_fold_two_size0 P_on_list (P_on_list_size : forall l t, P_on_list l t -> nat) : forall l, All_fold_two P_on_list l -> nat :=
fix fold l w :=
match w with
| fold_nil => 0
| fold_cons_abs l' w' p
| fold_cons_def l' w' p => P_on_list_size _ _ p + fold _ w'
end.
Definition All_fold_two_size {on_list} on_list_size :=
(* Eval unfold All_fold_two_size0, P_size in *)
All_fold_two_size0 (P on_list) (P_size on_list_size).
Inductive on_list (l : list two) : Type :=
| on_list_intro : All_fold_two (P on_list) l -> on_list l.
Fixpoint on_list_size l (d : on_list l) {struct d} : nat :=
match d with
| on_list_intro _ a => All_fold_two_size on_list_size l a
end.
```

(In Coq 8.16, this doesn't compile until you uncomment the `Eval`

part, in Coq 8.15.2 it compiles no matter what)

Is it possible that unfolding removes an occurrence of on_list_size that violates the guard condition? If yes, the change seems to be intended based on the changelog?

https://coq.inria.fr/refman/changes.html#id2

Changed: Fixpoints are now expected to be guarded even in subterms erasable by reduction, thus getting rid of an artificial obstacle preventing to lift the assumption of weak normalization of Coq to an assumption of strong normalization; for instance (barring implementation bugs) termination of the type-checking algorithm of Coq is now restored (of course, as usual, up to the assumption of the consistency of set theory and type theory, i.e., equivalently, up to the weak normalization of type theory, a "physical" assumption, which has not been contradicted for decades and which specialists commonly believe to be a truth) (#15434, incidentally fixes the complexity issue #5702, by Hugo Herbelin).

I managed to simplify it down more and it does indeed appear that an occurence that violates the guard condition is erased by reduction.

My question is now why the following code violates the guard condition (this is pretty much what gets erased) :

```
Inductive box P := box_intro : P -> box P.
Inductive P := P_intro : box P -> P.
Fixpoint size (d : P) {struct d} : nat :=
match d with
| P_intro p =>
match tt as t
return box (match t with tt => P end) -> nat
with
| tt => fun tu =>
let 'box_intro _ tu' := tu in
size tu'
end p
end.
```

`Recursive call to size has principal argument equal to "tu'" instead of one of the following variables: "p" "tu".`

well, `tu'`

is a subterm of `tu`

, which isn't a subterm of `p`

until beta-reduction

but it seems _some_ reduction still happens during guard checking, and I wouldn't know why _this_ redex isn't reduced.

said otherwise, I don't know if the unreduced term admits an infinite reduction sequence — all I can say is that the guard condition isn't (AFAIK) expected to be complete

I guess I wouldn't be as surprised if `tu`

weren't cited in the list of possible variables, but now that it is I'm curious why my `tu'`

isn't accepted

It should also be noted that replacing `match t with tt => P end`

with `match tt with tt => P end`

makes Coq accept the function

The guard condition becomes really peculiar when the expression involves a `match`

with a `return`

clause. Here, by stating that `tu`

has type `box (match t with tt => P end)`

(instead of, e.g., `match t with tt => box P end`

), you are confusing the checker. I don't know if it is an implementation issue or if there is a good reason that makes this case hard to recognize.

Is there some documentation or paper I can read which would explain why `tu`

is a valid subterm but `tu'`

isn't ? I tried reading the code but I don't have enough background knowledge to understand the names used and lost myself as I tried to follow the flow

If you want something rigid, I would recommend reading Codifying Guarded Definitions with Recursive Schemes and then Structural Recursive Definitions in Type Theory. But, I guess the current implementation in Coq is explained nowhere (except for `inductive.ml`

in the kernel).

Anyways I do not think these papers explain what happens in your example.

Last updated: Feb 06 2023 at 13:03 UTC