Invariant types not checked for function values

[nickbattle]

If a named type is declared with an invariant, and the base type is a function, the invariant is not checked when function values are converted to that type. For example:

types
    V = <V1> | <V2> | <V3>;

    R :: 
        x: set of V
        y: set of V;

    T = (R -> set of V)
    inv t == forall r:R &
        t(r) subset r.x inter r.y;

functions
    test1: () -> T
    test1() == lambda -:R & {<V1>};     -- Should fail to return a "T"

    test2: () -> T
    test2() == lambda a:R & a.x inter a.y;

Both of the test functions currently return a T value, but test1 should raise an invariant violation.

[nickbattle]

This was caused by the convertTo for function values, which currently intercepts the conversion in order to restrict the dom/range of the value to match the converted type. That is the right thing to do, but it then failed to check for invariance as well. The fix is to check for conversion to an invariant type and apply the invariant check to the converted value.

[nickbattle]

Fix now available in ncb/development.