Take previous control flow into consideration when deciding a case statement's exhaustiveness

[RSDuck]

Currently code like this doesn't compile:

case x
of 2, 4, 8:
  case x
  of 2: echo "2"
  of 4: echo "4"
  of 8: echo "8"
else:
  echo "other"

if x >= 0 and x < 3 and otherCondition:
  case x
  of 0: echo "all"
  of 1: echo "values"
  of 2: echo "are covered!"

eventhough it can be deducted at compiletime that all possible values x can have are covered by the case statements. This is especially annoying with case expressions where to my knowledge the only workaround is to raise a defect e.g. via raiseAssert for the else case.

There is already some kind of analysis like this which is used when constructing case objects, but I think it doesn't take if statements into consideration.

[beef331]

I've recently thought about this, I think a range/value narrowing system like this would be quite nice. Increasing the intelligence of compile time, being able to implicitly run static code at compile time. The following may be ill thought out and mostly a pipe dream but anywho, my ideas. I atleast think it's a better solution to the problem at hand.

Range narrowing:

Any type with low high succ < and == accessible from the flow control would be usable for range(assuming they return T T T bool bool respectively of course). ie:

var a = someProc()
if a in 0..3:
  # `a` is narrowed to `0..3` in this scope until mutated or narrowed further
  discard
  case a
  of 1, 2:
    # narrowed to `1..2`
    discard
  else:
    # narrowed to `0..0` `3..3`
    discard

Value narrowing:

On ==/= if from static sources it's narrowed to that value for all uses(since this can all be resolved/done statically). ie:

var 
  a = @[1] # `a` is narrowed to a value `@[1]` as it's a static value
  b = someRuntimeProc()
if b.len == @[]:
 # `b` is now value narrowed to `@[]`
 echo b[0] # can run `@[][0]` at compile time and know it's wrong

Examples

var
  a: 0..3 = 2
  b = 10 # 10 is attached to `b` as it comes from literal
a = b # Compile time error `b: 10` is not in range 0..3
if b in 0..3:
  case b   # Inside this scope b is narrowed to `0..3` so this works
  of 0, 1, 2, 3: discard

proc addStuff(s: var seq[int], b: int) =
  assert 0 notin s # 0 is in `@[0, 20, 30]`
  s.add b
var s = @[0, 20, 30] 
# s comes from static sources(no importC, nosideeffect) it can be narrowed
# typeof(s) does not have `low`/ `high` in this module as such this doesnt get ranged.
# instead it's given the value `@[0, 20, 30]`
s.addStuff(30) # Proc can be run at compile time, so assertion raised here

Finally a silly example that is more for thought than an actual suggestion, mostly due to complexity:

proc doThing(a: int) = 
  assert a in 20..30

var a = someNonStaticInput()
if a > 30 or a < 20:
  # A is narrowed to two ranges `int.low .. 19` and `31 .. int.high`
  doThing(a) # Assertion could be raised at CT since we know the ranges dont overlap

if a > 30 or a < 20 or a < 25:
  # A is narrowed to two ranges `int.low ..< 25` and `31 .. int.high`
  doThing(a) # A warning would be produced since there is an overlap

[Araq]

You can take this further and eliminate most array index checks, I had it working in a branch...

[Menduist]

To build on top of @beef331 silly example with more silliness:

let a = procReturningAnOption()
if a.isSome:
  echo a.get() # works

echo a.get() # isSome may be false, which would raise a Defect in Option.get
             # So CT error (or warning)

I imagine this is pretty complex to implement, but pretty cool if it worked