universe error in definition generated by the equation compiler

[robertylewis]

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.