Automatically deduce type invariants across case splits

[gancherj]

Currently when we have many case splits, and an intermediate struct holding a state, we are in a situation like below:

struct S { 
  ...
  x : if ??? then T else Data<adv>
  ...
}

def foo() @ L : Option S = { 
   ... many case splits ... 
   in
   Some(S(..., x, ...))
}

where it is quite tricky to find out what ??? should be.
Currently, the strategy for doing so is as follows:

1. Instead of returning a value of type S at the end of the function, return a value of type Unit;
2. Use --log-typecheck to log all of the different case splits;
3. Insert the following debug command just before returning:

 debug hasType(x, T); 
 debug hasType(x, Data<adv>);

This will output a trace similar to below:

  Case split: is_e_init<>[msg1_ephemeral']
    Case split: [S_resp<@m>] <= adv
      Case split: [E_init<i@n>] <= adv
        Case split: [S_init<@n3>] <= adv
          Case split: n =idx n3
C3 has type Name(ODHName<L2<@n,m>;0>(C2, 0x)[0]): False
C3 has type Data<adv>: True
          Case split: n !=idx n3
C3 has type Name(ODHName<L2<@n,m>;0>(C2, 0x)[0]): False
C3 has type Data<adv>: True
        Case split: [S_init<@n3>] !<= adv
          Case split: n =idx n3
C3 has type Name(ODHName<L2<@n,m>;0>(C2, 0x)[0]): False
C3 has type Data<adv>: True

    ...

After obtaining this trace, I can manually deduce what ??? is by minimizing the trace, similar to a BDD. It would be really great if we could automate this process.