universe error in definition generated by the equation compiler

This was found by Joseph Rotella. The equation compiler fails to create a helper definition because of a universe error, even though the definition itself is sensible.

-- fails to create a helper definition
def foldr_cps {α β γ : Sort*} (g : α → β → β) (z : β) : list α → (β → γ) → γ
| list.nil k := k z
| (list.cons x xs) k := foldr_cps xs (λz', k (g x z'))

-- succeeds
def foldr_cps' {α β γ : Sort*} (g : α → β → β) (z : β) (l : list α) : (β → γ) → γ :=
@list.rec_on α (λ _, (β → γ) → γ) l
  (λ k : β → γ, k z) 
  (λ x xs r k, r (λ z', k (g x z')))

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
    • Specifically, check out the wishlist, open RFCs,
      or feature requests.
  • Reduced the issue to a self-contained, reproducible test case.

Description

[Description of the issue]

Steps to Reproduce

1. [First Step]
2. [Second Step]
3. [and so on...]

Expected behavior: [What you expect to happen]

Actual behavior: [What actually happens]

Reproduces how often: [What percentage of the time does it reproduce?]

Versions

You can get this information from copy and pasting the output of lean --version,
please include the OS and what version of the OS you're running.

Additional Information

Any additional information, configuration or data that might be necessary to reproduce the issue.

Start with the equation compiler and the supplied foldr_cps and foldr_cps' reproductions. Compare why the pattern-matching definition fails while the explicit list.rec_on definition succeeds; done means the first definition creates its helper definition without a universe error.