Propagate constructor refinements in branches

[natefaubion]

Given code like:

foo expr = case expr of
  Baz _ -> 1
  Qux _ -> 2

bar expr = case expr of
  Baz _ -> 1 + foo expr
  Qux _ -> 2 + foo expr

Where foo is inline always, one would hope that the branches would fuse together, yielding an optimized:

bar expr = case expr of
  Baz _ -> 2
  Qux _ -> 4

But this doesn't currently happen, since expr is opaque. To make this work we would need to propagate refinement information in each branch on the opaque term, saying that in the Baz branch, any subsequent OpIsTag operation on expr can be statically compared against Baz.

One way to do this would be to change SemConditional. Currently it is:

data SemConditional a = SemConditional (Lazy a) (Lazy a)

Which means that the branch is completely closed wrt evaluation, and so can't admit any new refinement information. We could change that so the branch is a function instead, taking some refinement:

data SemConditional a = SemConditional (Lazy a) (Refinement -> a)

I'm not sure if this information should just be tracked in a Map in the Env, or if the locals could potentially be updated in such a way that derefing the binding in that branch can yield a term that fits the refinement.