lean
lean copied to clipboard
invalid synthesis of `reflected` instances
Prerequisites
- [x] 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.
- Checked that your issue isn't already filed.
Description
The following code:
meta example {α β : Type} (a : α) (γ : α → β → Type)
[reflected γ] [reflected a] : reflected (γ a) :=
by apply_instance
produces the error
type expected at
α
term has type
1
under the second α
on the first line
Steps to Reproduce
- Make a blank file containing only the above
- Observe the error message
Expected behavior: Lean should construct an instance using `(γ).subst `(a)
Actual behavior: Lean spits out the nonsense error message above
Reproduces how often: Every time
Versions
Lean 3.43.0