overturetool / vdm-vscode

Visual Studio Code extension for VDM language support
GNU General Public License v3.0
21 stars 6 forks source link

Duplicate type checking errors #33

Closed paulch42 closed 3 years ago

paulch42 commented 3 years ago

At times a type checking error is duplicated, as in the example below:

Screen Shot 2021-02-06 at 8 19 25 am

In the first case, the module does not exist. In the second case, the function does not exist. This is part of a somewhat larger and complex specification. I haven't been able to repeat it in a simpler situation, such as:

Screen Shot 2021-02-06 at 8 31 57 am
nickbattle commented 3 years ago

Good spot. If you look very closely, the duplicates have different error numbers (3430 and 3431), but I agree that they are essentially saying the same thing and we ought to have only one. It's caused by the way type resolution works, but it should be possible to clean it up.

nickbattle commented 3 years ago

OK, this is now fixed. It is quite hard to reproduce, but luckily one of the tests in the CSK test suite had a duplicate. Now it just has the one.