Integer bit width rules implicitly endorse overflow

When making a type system that deals with integers of different bit widths, it seems to me that you have two choices:

The "normal" way, like in C or Rust or anything else in software land: preserve the bit width for your data type, even if it might overflow. For example, if a and b have type bit<32>, then both a + b and a * b also have type bit<32>. This is nice because it lets you keep all your values within a consistent type. No constantly needing to round/check for overflow/narrow the values after doing computations—if you want to work on 16-bit data, then all your variables are 16-bit variables, and if you want to switch to 8-bit data, you can easily just switch all your variables to an 8-bit type.
The "right" way, which is more hardwarey, and avoids overflow. If a and b have type bit<32>, then a + b has type bit<33> in case the carry goes beyond the highest-order bit. And of course a * b has type bit<64> because that's what you need to represent the largest possible product of two 32-bit numbers, as noted in calyxir/calyx@b311ace#r45061991.

Dahlia currently uses option 1. See this line:

dahlia/src/main/scala/typechecker/Subtyping.scala

Line 94 in ee78f8b

if (un1 == un2) Some(TSizedInt(max(s1, s2), un1))

Every binary arithmetic operator gets the same bit width as the maximum of its operands. There are advantages to this, as outlined above, but also disadvantages when you really want to represent the full range of results and really do not want overflow.

I think we could benefit from thinking in a kind of clean-slate way about how this should work. Some rough thoughts:

As always with bit width stuff, it's "just" a matter of defaults and as should let you get the other behavior when you want it, even if it's inconvenient.
Maybe we even want two different types that behave in the two different ways. When you are treating ints as a kind of "content" data type, the same way you may use a float, you probably want option 1. But when you are using an int as an iterator or otherwise doing index-related stuff, you probably want option 2.
An easy way to get a checked overflow, signaling an error at least in development, as in Rust, would be super nice.

Two extra thoughts on this:

One way to do about the two-type solution would be that bit or something called int behaves in the "correct" way, whereas fixed<32, 0> (i.e., a fixed-point number with no fractional bits) follows the "normal" rules above and is the right type for representing "content" data.
Just for reference, Mentor's ac_int uses the "correct" way. Their docs have a handy table showing how they calculate the bit widths for operations.

I wonder why division is chosen to be W1 + W2, instead of what I believe is the right answer, W1. It mentions that & is the way it is for consistency purposes with | and ^, so perhaps / is the same way. Or, I'm missing something simple here.

Just for fun: a new CIRCT thread refers to the same decision.