No diagnostic when target-context widening is blocked by `.sel`, silently truncating a narrow arithmetic chain

[soronpo]

Describe the bug

Automatic target-context widening applies to an anonymous +/-/* expression assigned to a wider target, but it does not reach an identical expression sitting inside a .sel. The .sel arguments are evaluated modularly at the operand width and only the .sel result is extended to the target width.

That behavior may well be intended, but it is silent — nothing is reported at elaboration — and it is a trap when porting Verilog, because Verilog's context-dependent width propagation does cross the ?: it corresponds to. A faithful, line-for-line translation of

logic signed [W:0] dx;                 // W+1 bits
dx <= right ? xb - xa : xa - xb;       // xa, xb are W bits

into

dx :== right.sel(xb - xa, xa - xb)

changes the meaning of the design with no indication that anything happened. The two forms differ whenever |xb - xa| does not fit in W-bit signed.

This is the same class of divergence that the existing "Implicit Scala Int and Verilog-semantics mismatch" elaboration warning already covers — a narrow non-carry chain where Verilog would have widened — but the current patterns are keyed on an implicit Int operand, so a chain of two bit-accurate operands inside a .sel falls outside them.

DFHDL and Scala versions

DFHDL version: 0.22.0+58-520fd8db-SNAPSHOT
Scala version: 3.8.4

To Reproduce

Minimized code to reproduce the behavior:

import dfhdl.*

class SelWiden(val W: Int <> CONST = 4) extends EDDesign:
  val a, b = SInt(W) <> IN
  val c    = Bit <> IN
  val viaSel = SInt(W + 1) <> OUT
  val bare   = SInt(W + 1) <> OUT

  process(all):
    // (1) bare anonymous arithmetic expression -> target-context widening applies
    bare := b - a

    // (2) the SAME arithmetic, one `.sel` away from the assignment
    viaSel := c.sel(b - a, a - b)

Elaborates and compiles with no warning. Emitted SystemVerilog:

  logic signed [W - 1:0] viaSel_part;      // <-- W bits, not W+1
  always_comb
  begin
    bare        = b - a;
    viaSel_part = c ? (b - a) : (a - b);   // subtract truncated here
    viaSel      = `EBY_S(viaSel_part, 1);  // sign-extended after the fact
  end

With W = 4, a = 4'b1000 (-8), b = 4'b0000 (0), c = 1, the two outputs disagree on the same source expression b - a (via Yosys sat):

  Signal Name             Dec       Hex           Bin
  --------------- ----------- --------- -------------
  \a                        8         8          1000
  \b                        0         0          0000
  \bare                     8         8         01000     <-- +8
  \viaSel                  24        18         11000     <-- -8

Writing c.sel(b -^ a, a -^ b) gives the widened result and matches the Verilog.

Expected behavior

An elaboration warning when an anonymous narrow +/-/* chain is nested inside a .sel (and presumably other value-level combinators that terminate the widening context) whose result is assigned or connected to a strictly wider target — i.e. exactly the case where target-context widening would have applied had the operation been directly on the right-hand side, but did not. As with the existing warning, it should be silenceable both ways: by carry ops (+^/-^/*^) to take the widening, or by an explicit .resize/bit-accurate form to accept the modular result.

Documenting where the widening context stops would help too — the current description says widening applies to an anonymous arithmetic expression assigned to a wider variable, but does not say what counts as breaking "anonymous".

How this was found

Translating draw_line.sv from Project F to DFHDL. The .sel line above was the only defect in the module, and it is invisible in review — the very next line, dy :== ya - yb, is a bare expression and widens correctly, so the two adjacent lines look alike but do not behave alike. Formal equivalence against the original did not report a mismatch either; equiv_induct simply never converged (the design is not equivalent, so there was nothing to prove), which reads as a solver capacity limit rather than a translation bug. With -^ in place the same check proves in 14s.

[soronpo]

Fixed in #465