## Stream: Coq users

### Topic: Unguarded recursive calls

#### Rudy Peterson (Oct 26 2022 at 21:46):

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!

#### Gaëtan Gilbert (Oct 26 2022 at 22:01):

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

#### Rudy Peterson (Oct 26 2022 at 23:04):

Interesting. I tried something similar in `agda` but it didn't accept it unless I inlined it myself.

#### Li-yao (Oct 27 2022 at 01:26):

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

#### Paolo Giarrusso (Oct 27 2022 at 09:55):

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