Imported definitions sometimes have the wrong type information

[nickbattle]

The following spec gives an incorrect warning:

module A
exports all
definitions 
values
    PERCENT: set1 of nat = {0,...,100};

end A

module B
imports from A values PERCENT renamed PERCENT;
exports all
definitions 
types
    T1 = nat
    inv t == (exists p in set PERCENT & p = t);     -- Empty set used in Bind for PERCENT here

end B 

Warning 5009: Empty set used in bind in 'B' (test.vdm) at line 16:35

This is because the imported definition is a clone of the original export, not a reference to it (as Overture's AST requires). So when the definition in A is type-resolved, that does not update the imported/renamed definition in B. Subsequently it treats PERCENT as an unknown type, which in the bind context looks like it could possibly be an empty set.

[nickbattle]

It ought to be possible to avoid the warning by explicitly re-stating the type of the import:

...
imports from A values PERCENT : set1 of nat renamed PERCENT;
...

But that currently fails too. That is because import/renames ignore the stated type, giving preference to the type of the definition referred to - though as above, that isn't working in some cases. I will push a small fix to allow these explicit re-stated types to take effect. That does not fix the underlying problem, but it gives us a work-around to avoid the warning.

[nickbattle]

The fix to use the type in the import is now pushed to ncb/development.