unexpected occurrence of recursive function in tauto

Stream: general

[Eric Wieser]

This commit in #15170 fails with the error "unexpected occurrence of recursive function", which seems to be originating from the tauto tactic. Is this a bug in tauto?