Hello!

I am trying to understand what triggers "unguarded recursive call" failures.

In my example:

```
Section Tree.
Variable A : Set.
Variant branch (T : Set) : Set :=
| elem (a : A)
| rest (t : T).
CoInductive tree : Set :=
mk { obs : branch tree }.
End Tree.
Arguments elem {_} {_}.
Arguments rest {_} {_}.
Arguments mk {_}.
Arguments obs {_}.
CoFixpoint bind
{A B : Set}
(t : tree A)
(f : A -> tree B)
: tree B :=
match obs t with
| elem a => f a
| rest t => mk (rest (bind t f))
end.
Fail CoFixpoint iter
{A I : Set}
(f : I -> tree (A + I))
(i : I) : tree A :=
bind
(f i)
(fun ai =>
match ai with
| inl a => mk (elem a)
| inr i => mk (rest (iter f i))
end).
```

`itrer`

fails with

```
The command has indeed failed with message:
Recursive definition of iter is ill-formed.
In environment
iter : forall A I : Set, (I -> tree (A + I)) -> I -> tree A
A : Set
I : Set
f : I -> tree (A + I)
i : I
Unguarded recursive call in
"cofix bind (A B : Set) (t : tree A) (f : A -> tree B) : tree B :=
match obs t with
| elem a => f a
| rest t0 => {| obs := rest (bind A B t0 f) |}
end".
Recursive definition is:
"fun (A I : Set) (f : I -> tree (A + I)) (i : I) =>
bind (f i)
(fun ai : A + I =>
match ai with
| inl a => {| obs := elem a |}
| inr i0 => {| obs := rest (iter A I f i0) |}
end)".
```

However if I change `bind`

as:

```
Reset bind.
Definition bind
{A B : Set}
(t : tree A)
(f : A -> tree B)
: tree B :=
let cofix help
(t : tree A) : tree B :=
match obs t with
| elem a => f a
| rest t => mk (rest (help t))
end in
help t.
CoFixpoint iter
{A I : Set}
(f : I -> tree (A + I))
(i : I) : tree A :=
bind
(f i)
(fun ai =>
match ai with
| inl a => mk (elem a)
| inr i => mk (rest (iter f i))
end).
```

`iter`

successfully types.

Why does one version of `bind`

allow `iter`

to type whereas another doesn't?

Thanks!

the second one reduces to

```
CoFixpoint iter
{A I : Set}
(f : I -> tree (A + I))
(i : I) : tree A :=
(cofix help t := match obs t with
| elem ai => match ai with
| inl a => mk (elem a)
| inr i => mk (rest (iter f i))
end
| rest t => mk (rest (help t))
end)
(f i)
.
```

and the guard condition is smart enough to understand that

the first one reduces to `cofix bind ...`

applied to the `fun ai => ... iter ...`

which to the guard condition looks like an arbitrary function applied to something containing the recursive call and cannot be accepted

Interesting. I tried something similar in `agda`

but it didn't accept it unless I inlined it myself.

Indeed nested recursive types is the one place where Agda is less smart than Coq in guard checking.

More simply, Coq's guard checking does inlining, Agda doesn't, and does compositional typechecking instead

Last updated: Jun 18 2024 at 20:02 UTC