simps sometimes gets types confused

mwe:

import Mathlib.Tactic
import Mathlib.Logic.Equiv.Basic

@[simps]
def univRefl : (Set.univ : Set ℕ) ≃ (Set.univ : Set ℕ) where
  toFun x := x 
  invFun x := x
  left_inv _ := rfl
  right_inv _ := rfl

@[simps!]
def subtypeTrueRefl : Subtype (⊤ : ℕ → Prop) ≃ Subtype (⊤ : ℕ → Prop) where
  __ := univRefl

#check subtypeTrueRefl_apply
/-
subtypeTrueRefl_apply (a✝ : ↑Set.univ) : ↑subtypeTrueRefl a✝ = a✝
-/

The result has a binder a : Set.univ, but this is poorly-typed and should be a : Subtype ⊤

EDIT by Floris: Zulip

Start with the provided minimal Lean example and inspect the simps and simps! behavior around subtypeTrueRefl_apply. The fix is complete when the generated declaration's binder is typed as Subtype ⊤ rather than Set.univ, while the example still elaborates and #check subtypeTrueRefl_apply reports the corrected type.