[Agda] Non-termination change in Agda 2.3.3

[Nicolas Pouillard]

Quoting Ulf Norell (2014-03-26 07:19:19)
> This is a consequence of the new termination checking of with functions [1].
> The problem in this case is that the termination checker doesn't see the
> relationship
> between as and bs. I don't think this is a big problem though, since it's
> only an
> issue if you with-abstract over variables (or constructor patterns), which
> it doesn't
> make much sense to do.

What about recursive calls in anonymous function definitions (e.g. λ { pat ... }),
I realized a regression where I had to change such a definition on _⊎_ into an
eliminator.

Can this be related?

The code:
https://github.com/crypto-agda/protocols/blob/master/Control/Protocol/Multiplicative.agda#L74

Cheers,
-- NP