bosatsu icon indicating copy to clipboard operation
bosatsu copied to clipboard

tighter totality checking

Open johnynek opened this issue 4 years ago • 1 comments

if we have:

match foo:
  x@[_, _]:
    # this match is now total
    [a, b] = x
    gn(a, b)
  _:
    fn(foo)

We could potentially check this by propagating a new top value for each binding into the branches. To do this, I guess we need to have a way to compute the top for each match scrutinee. Currently we just use _ for that value, but a kind of flow typing would be to propagate tops into each of the branches.

So, when we have match Some(x): we know that the Some(_) pattern is the top.

This relates to #456 since we might want better range propagation to do this better.

johnynek avatar Dec 16 '19 20:12 johnynek

one challenge of this is it could make unreachable branches quite confusing. Unreachable branches are currently an error, but if by doing some complex computation we can prove a branch is unreachable, we should probably not error in that case. Maybe just error on the ones that would be unreachable starting with _ as the top since those can never be reached. The others, are just optimizations that can be removed by normalization.

johnynek avatar Dec 16 '19 20:12 johnynek