Stream: Coq users

Topic: Unguarded recursive calls


view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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: Feb 01 2023 at 11:04 UTC