broaden type inference from context (arithmetic expressions)

TODO.md

@@ -214,13 +214,14 @@
     bare-name typed declarations, call arguments (a concrete parameter type demands its
     argument, e.g. `take_u16(a)`), and returns — including from inside a function body
     back onto a referenced global
-  - demands flow only through bare names; they do not cross arithmetic or other operators,
-    nor back across a call's result (the result-to-argument direction is milestone 14.5)
+  - at this milestone, demands flow only through bare names; they do not cross arithmetic
+    or other operators, nor back across a call's result (arithmetic is milestone 15;
+    result-to-argument direction is milestone 14.5)
   - a non-fitting or family-conflicting demand is not applied (first demand wins); the
     genuine mismatch then surfaces as the usual boundary coercion error at the use
     (e.g. `C u8 :: BIG` where `BIG :: 100000`)
 
-14.5. backward type-demand propagation through call boundaries (deferred)
+14.5. backward type-demand propagation through call boundaries (DEFERRED)
   - a callee's result/return demand flows back through the function body to constrain
     the caller's arguments, so `R u32 :: echo(A)` (with `echo :: func(p int) int`)
     resolves A to u32 instead of erroring at the call's result coercion
@@ -229,7 +230,17 @@
     through every call site and the specialization fixpoint
   - only meaningful on top of milestone 14's open constants
 
-15. broaden type inference to infer type of declaration based on arithmetic expressions too
+15. broaden type inference to infer type of declaration based on arithmetic expressions too (implemented)
+  - backward contextual demands now flow through numeric arithmetic (`+`, `-`, `*`, `/`, unary `-`)
+    for integer and float open constants
+  - integer literals can adopt integer or float arithmetic context; float literals can adopt `f32`/`f64`
+  - unannotated declarations initialized by arithmetic expressions adopt the concrete numeric operand type
+  - e.g.
+    ```
+    a :: 1
+    b i32 :: a + 2 # a is constrained to `i32`
+    c :: b + 3     # c is constrained to `i32`
+    ```
 
 16. add slice-by-range
   - allow the use of a range in slice expressions: