## Stream: Equations devs & users

### Topic: Can where definitions make recursive calls in a with node?

#### Kevin Orr (Sep 29 2020 at 21:00):

Hello, I'm trying to write a `where` clause that makes a recursive call to itself in a `with` node. Here's a simplified version:

``````Require Import List.
Import ListNotations.
Require Import Equations.Equations.

Fail Equations ok_clause (e : nat -> option bool) (xs : list nat) : bool by struct xs :=
ok_clause => ok_clause'
where
ok_clause' (e : nat -> option bool) (xs : list nat) : bool by struct xs :=
ok_clause' _ [] => true;
ok_clause' e (x::xs) with e x =>
{ | Some _ => ok_clause' e xs;
| _ => false }.
``````

This fails with the message

``````Error:
Recursive definition of ok_clause' is ill-formed.
In environment
ok_clause : let H := fixproto in (nat -> option bool) -> list nat -> bool
ok_clause' : (nat -> option bool) -> list nat -> bool
e : nat -> option bool
xs : list nat
n : nat
l : list nat
Recursive call to ok_clause' has not enough arguments.
Recursive definition is:
"fun (e : nat -> option bool) (xs : list nat) =>
match xs with
| [] => true
| n :: l =>
(fun (_ : let H := fixproto in (nat -> option bool) -> list nat -> bool) (e0 : nat -> option bool)
(_ : nat) (refine : option bool) (ok_clause' : (nat -> option bool) -> list nat -> bool)
(l0 : list nat) =>
match refine with
| Some _ => fun (ok_clause'0 : (nat -> option bool) -> list nat -> bool) (l1 : list nat) => ok_clause'0 e0 l1
| None => fun (_ : (nat -> option bool) -> list nat -> bool) (_ : list nat) => false
end ok_clause' l0) ok_clause e n (e n) ok_clause' l
end".
``````

As the error indicates, `ok_clause'` is being passed as an argument to the lambda, and then this argument is being called as the recursive call. I suppose the fixpoint checker doesn't allow `(fun f0 => match ... => f0 x end) f` (typo: `(match ... => fun f0 => (f0 x) end) f`), where `f` is the fixpoint.

Interestingly enough, `ok_clause'` works as a top-level definition:

``````Require Import List.
Import ListNotations.
Require Import Equations.Equations.

Equations ok_clause' (e : nat -> option bool) (xs : list nat) : bool by struct xs :=
ok_clause' _ [] => true;
ok_clause' e (x::xs) with e x =>
{ | Some _ => ok_clause' e xs;
| _ => false }.
``````

So is there some weird interaction happening between `where`, `with`, and a recursive call? Or is this just something that's not supported?

Thanks.

P.S. this is easy to work around by just using an explicit `match` instead of a `with` clause, or by extracting out the subprogram into its own definition.

#### Matthieu Sozeau (Sep 30 2020 at 08:06):

Sadly yes, this is not supported by the core calculus: it requires all recursive calls be full applications, and cannot handle this commutation of match and lambda. We might be able to do better here though: there is no reason to abstract on the recursive function ok_clause' in the match branches, as its type is independent of the the scrutinee of the pattern-matching. So could you please report this as an issue of Equations github page?

#### Kevin Orr (Oct 01 2020 at 22:12):

Sure thing

Last updated: Nov 29 2023 at 19:01 UTC