simp type annotations

Stream: lean4

[Chris B]

Is the process by which simp checks type annotations different from the process it uses to find patterns in a term? I have a term that's elaborating to two different things depending on whether it's in a have statement, or whether it's used in a simp list, where the simp one won't actually match the term in the goal, while the have item does. When I take the full type from the have statement and try to annotate the simp item with it I get no errors, but hovering over the expression in the simp list shows the old type and seems to ignore the annotation.

lemma UInt8.add_zero (a b c : UInt8) : a + 0 = a := by
  simp only [UInt8.add_def]
  have h0 : a.val + (0 : UInt8).val = a.val := AddMonoid.add_zero a.val
  /-
  h0 has type:
  @Eq (Fin size)
  (@HAdd.hAdd (Fin size) (Fin size) (Fin size) (@instHAdd (Fin size) (@Fin.instAddFin size))
    (val a) (val (@OfNat.ofNat UInt8 0 (@instOfNatUInt8 0))))
  (val a)
  -/

  simp only [
    (AddMonoid.add_zero a.val : (@Eq (Fin size)
      (@HAdd.hAdd (Fin size) (Fin size) (Fin size) (@instHAdd (Fin size) (@Fin.instAddFin size))
        (val a)
        (val (@OfNat.ofNat UInt8 0 (@instOfNatUInt8 0))))
      (val a)))
  ]
  /-
  hovering over the simp term shows this type, which is not the ascribed type:
  @Eq (Fin size)
    (@HAdd.hAdd (Fin size) (Fin size) (Fin size)
      (@instHAdd (Fin size) (@AddSemigroup.toAdd (Fin size) (@AddMonoid.toAddSemigroup (Fin size) instAddMonoidFinSize)))
      (val a) (@OfNat.ofNat (Fin size) 0 (@instOfNat (Fin size) (@AddMonoid.toZero (Fin size) instAddMonoidFinSize))))
    (val a)
  -/