Fix execute splitting to work when constructors have constraints.

Previously any constraints on constructors were just outright dropped
when splitting the execute function in Lem generation. Now we get the
constraints and type signature for each execute clause from the type
given by Env.get_union_constructor, rather than by inferring the type
of the pattern in each function clause.

Currently this can still fail in the case where we have

union U('x: Int), C1('x) = { ctor: {'y. C2('x, 'y), T('x, 'y)} }

and

val execute : forall 'z, C3('z). U('z) -> unit

when C3 implies C1, and the body of an excute clause relies on the
fact that C3 is stronger than C1, as each split function execute_ctor
is only guaranteed to be constrained by some subset of C1. This seems
unlikely to happen in practice though.

Also fix a bug when binding P as int('T) against int('T) and similar
cases, where the new type variable would cause the old type variable
to become shadowed, but the constraint that the bound type variable
and the old type variable are equal would not take this into account.

0 files changed, 0 insertions, 0 deletions