invalid synthesis of `reflected` instances

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

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

1. Make a blank file containing only the above
2. 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

Create a blank Lean file containing the reproduction in the issue and run it under Lean 3.43.0 to confirm the reported error. Investigate instance synthesis for reflected γ and reflected a; done means the example constructs the expected reflected (γ a) instance using the stated substitution behavior without producing the type error.