Spurious coercion insertion when elaborating binops

Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

Binop elaboration (in that case ++) introduces non-sensical coercions, that do not appear when using hAppend directly.

In the following example:

set_option pp.coercions true

namespace Out.Functions

instance : CoeDep (BitVec n) x (BitVec m) where
  coe := x.setWidth m

def mask (n : Nat) (x : BitVec w) : BitVec n := sorry

def good : String :=
    if HAppend.hAppend (mask 1 0x0#4) (mask 5 0x1E#8) = mask 6 0x1E#8
    then "ok"
    else "bad"

def bad : String :=
    if (mask 1 0x0#4) ++ (mask 5 0x1E#8) = mask 6 0x1E#8
    then "ok"
    else "bad"

#print good
#print bad

the bad example has the following corections on the RHS of the equality BitVec.setWidth (1 + 5) (BitVec.setWidth 1 (mask 6 30#8)).

This seems to come from the fact that binop elaboration tries the homogeneous case HAppend (BitVec 1) (BitVec 1) (BitVec 1), and introcuces a coercion from BitVec 6 to BitVec 1 in the process, which is not removed when no such typeclass instance is found.

Context

This happens in the output of the lean backend of the sail compiler. cf https://github.com/rems-project/sail/issues/1630

Steps to Reproduce

1. Add coercion instances
2. Use them together with builtin binops such as ++

Expected behavior:
No unnecessary coercions are inserted.

Actual behavior:
Unnecessary coercions are inserted.

Versions

"4.28.0-nightly-2026-01-22" and the current live version.

Additional Information

[Additional information, configuration or data that might be necessary to reproduce the issue]

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start by running the minimal reproducer and comparing the ++ expression with direct HAppend.hAppend elaboration, inspecting the binop elaboration path. The fix is complete when the bad example no longer contains unnecessary BitVec.setWidth coercions in its printed core output, while direct hAppend behavior remains unchanged.