Type Variables invariants seem to be broken when used as type variables in further function calls

[JaScMiller]

Description

Tricky one today I think:

I seem to have a problem using type variables as type variables in further functions when the functions use similar names to each other for their type variables. I came accross this issue in a real specification I am creating and have produced the issue artificially here in a minimum example.

Steps to Reproduce

Here is a minimum example I was able to create. Notice how broken_function and fixed_function are fundamentally the same.

module ModuleA

exports all

definitions

    types

        MoreThan5 = real
        inv mt0 == mt0 > 5;

        LessThan5 = real
        inv mt0 == mt0 < 5;

    functions

        identity[@a, @b]: (@a * @b) -> (@a * @b)
        identity(mk_(itemA, itemB)) ==
            mk_(itemA, itemB)
        ;

        working_function[@a, @b]: @a * @b -> bool
        working_function(itemA, itemB) ==
            let y = identity[@a, @b](mk_(itemA, itemB)) in
            true
        ;

        broken_function[@a, @b]: @a * @b -> bool
        broken_function(itemA, itemB) ==
            let y = identity[@b, @a](mk_(itemB, itemA)) in
            true
        ;

        fixed_function[@aa, @bb]: @aa * @bb -> bool
        fixed_function(itemA, itemB) ==
            let y = identity[@bb, @aa](mk_(itemB, itemA)) in
            true
        ;

end ModuleA

Try out the following commands, noticing how the second one fails.

1. print working_function[MoreThan5, LessThan5](6, 4)
2. print broken_function[MoreThan5, LessThan5](6, 4)
3. print fixed_function[MoreThan5, LessThan5](6, 4)

Expected behavior: Local type variable names should only have influence locally

Actual behavior: Type variable names seems to affect subsequent function calls.

Reproduces how often: 100%

Versions

Overture Platform

Version: 3.0.2 Build date: 2020 Nov 10 15:51 CET Git commit description: Release/3.0.2 Windows 10 Home

Additional Information

It might be possible to work around this issue by trying to rename type variables, or it might be that I have misunderstood and type variables are not local to a function unlike regular variables. Either way though, this means that a specification writer utilising a library function that utilises other library functions has to have a deep knowledge of the implementation for every underlying function.

[JaScMiller]

Sorry, to clarify by failure I mean that broken_function produces an error due to a failing invariant check that I believe is incorrect:

Error 4060: Type invariant violated for MoreThan5 in 'ModuleA' (blah\blah\Overture\workspace\sandbox\moduleA.vdmsl) at line 30:8

[nickbattle]

Interesting case. The type variables should definitely be local, so the broken_function should be fine. All three functions work correctly on VDMJ, so this might be just something with Eclipse Overture's interpreter. That said, the VSCode extension is having trouble with your spec for some reason (though that is probably unrelated to the issue here!).

With a reproducible example, it should be possible to find/fix, though going forward we will only be applying fixes to the VSCode extension.

[leouk]

This is an interesting situation. As Nick says, it works in VSCode. @nickbattle param names seem to loose the "@", so if I had used f[@a, @b](a, b) it would fail saying names are mixed up.

The function fails with "print broken_function[MoreThan5, LessThan5](6, 4)" as you would expect. In fact, a possible extension here Nick might be to have within the --strict flag the warning that the let expression has no declared type? (i.e. let y : T = V, as opposed to let y = V)?

[nickbattle]

My mistake... the VSCode extension works fine:

*
* VDMJ VDM_SL Interpreter
* DEBUG enabled
*

Default module is ModuleA
Initialized in ... 0.001 secs.
print working_function[MoreThan5, LessThan5](6, 4)
= true
Executed in 0.007 secs.
print broken_function[MoreThan5, LessThan5](6, 4)
= true
Executed in 0.009 secs.
print fixed_function[MoreThan5, LessThan5](6, 4)
= true
Executed in 0.006 secs.

I'll take a look at Overture, but as I said, we're trying to move to the new platform whenever possible.

[leouk]

This situation also reminds me of scenarios in VDMToolkit Support library, where seqMap or split applied to non-union type parameters leads to quite weird behaviours. So some similar kind of warning in these cases would be useful?

[nickbattle]

a possible extension here Nick might be to have within the --strict flag the warning that the let expression has no declared type?

Mmm... though that's more of a "style" thing than a "strict" thing. You are allowed to declare variables without a type and have that type inferred, though style-wise (as we know!) adding them can save you a lot of trouble. Currently, the strict flag is used to cover things that VDMJ allows that are, strictly, wrong - like putting imports and exports in either order.

With the new VSCode plugin architecture, it would be fairly easy to create a style plugin :-)

[JaScMiller]

My mistake... the VSCode extension works fine:

*
* VDMJ VDM_SL Interpreter
* DEBUG enabled
*

Default module is ModuleA
Initialized in ... 0.001 secs.
print working_function[MoreThan5, LessThan5](6, 4)
= true
Executed in 0.007 secs.
print broken_function[MoreThan5, LessThan5](6, 4)
= true
Executed in 0.009 secs.
print fixed_function[MoreThan5, LessThan5](6, 4)
= true
Executed in 0.006 secs.

I'll take a look at Overture, but as I said, we're trying to move to the new platform whenever possible.

Ah, forgive me the VSCode Extension was not even something I was aware of. If it works fine there and this is purely an Overture problem then I am happy to look into the extension and move environments to VSCode, so perhaps this is a non issue :)

[nickbattle]

Well, it's a valid bug, but only on a platform with a limited lifetime. If I can quickly find/fix it, we might squeeze out an Overture maintenance release, but otherwise... moving to VSCode is a good idea!

[nickbattle]

I've had a look at the Overture implementation. I can see that there are differences in the way Overture and VDMJ handle polymorphic parameter substitution, but there isn't an obvious change that accounts for the bug (that I can see). I attempted to update Overture to do things the same way as VDMJ, but that had a lot of knock-on changes that affect some fundamentals, like how a function value is represented. There is considerable risk when changing this - that is, I may fix this bug, but introduce a few new ones.

So unless there is a hard requirement to fix this bug for Overture, I propose to leave it as a known fault.

[JaScMiller]

Thanks for taking a look at that, I appreciate the effort made for me on a nearly unsupported tool. A very reasonable course of action considering everything.

I have installed the VS Code extension which as you say I cannot see this issue on my project, so probably the best outcome from this bug that I could have asked for I have acheived by both working around the bug and gaining more future proof tools.

Thanks again :)

[nickbattle]

As an aside, we're always interested to hear/understand how new users react to the (very different) VSCode environment. There may be things that we can change or simplify if they're confusing.

This issue isn't the place to discuss it, but if you have any thoughts please let me know (nick.battle@gmail.com).

[nickbattle]

Just for the record, it looks like the error here is to do with the way that Overture typechecks the function instantiation, identity[@b, @a] in order to infer the type of "y". The error then occurs when the result is being coerced into that incorrect type.

The process for type checking here is relatively simple in VDMJ. But Overture does the work using an assistant's getType method, which eventually calls a visitor (or three) to "polymorph" (ie. set the actual type of @T) the parameters. An outer loop does @b then @a, but applies each loop to the whole function type like (@b * @a) -> (@a * @b). So after the first loop, it is turned into (@a * @a) -> (@a * @a), which completely destroys the original function's meaning. The upshot is that the let expression's inference of the type of "y" is (@a * @a)... and it's all downhill from there.

So without spending far more time unpicking this, I think the type processing is wrong here and most of the time we "get away with it". VDMJ works fine because it does the work in a more direct way, probably because the type checker hasn't been split into a core and assistants.

I'll close the issue here :-)