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 (typo: `(fun f0 => match ... => f0 x end) f`

`(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.

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?

Sure thing

Last updated: Jan 29 2023 at 15:02 UTC