elaborator doesn't unify universe metavariable

The following fails

-- set_option trace.elaborator_detail true

def my_eq {A : Type*} (a b : A) : Prop := true

lemma id_map_is_right_neutral {A : Type} (map : A -> A) :
  my_eq (function.comp.{1 1 _} map map) map :=
sorry

with the error

kernel failed to type check declaration 'id_map_is_right_neutral' this is usually due to a buggy tactic or a bug in the builtin elaborator
elaborated type:
  ∀ {A : Type} (map : A → A), my_eq (map ∘ map) map
elaborated value:
  λ {A : Type} (map : A → A), sorry
nested exception message:
type mismatch at application
  @my_eq (A → A)
term
  A → A
has type
  Type
but is expected to have type
  Type u_1

It works if the _ is replaced by 1.

It seems like the elaborator has taken a wrong turn somewhere, by not unifying u_1 with 1.
See https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/HoTT3.20universe.20errors

Start by reproducing the declaration in the issue and compare elaboration with the _ and 1 universe arguments. Trace the elaborator's universe metavariable handling, then verify that the example type-checks without the kernel error while preserving the reported behavior.