Recursive fixpoint: Inductive argument is not detected as a switch pattern var.

[necto]

I am building a large fixpoint, that contains nested switch statements. For some reason the code below fails with the following

"Inductive argument of recursive call must be switch clause pattern variable."

Although, the two_switch_fp(bt, nil) does use the switch clause pattern variable bt.

/*@
  fixpoint list<kt> two_switch_fp<kt>(list<kt> current_bucket, list<int> start) {
    switch(start) {
      case nil:
        return switch(current_bucket) {
          case nil:
            return nil;
          case cons(bh, bt):
            return two_switch_fp(bt, nil);
        };
      case cons(h,t):
        return nil;
    }
  }
  @*/

How can I make it more explicit?

[btj]

The error message is not precise: the inductive argument of a recursive call must be a switch clause pattern variable of the outermost switch statement (or a component thereof).

So the fix in this case is simply to swap the nesting order of the two switch statements.

[necto]

That works. Thank you!