bosatsu
bosatsu copied to clipboard
tighter totality checking
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.
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.