overturetool / overture

The Overture Tool
http://overturetool.org
GNU General Public License v3.0
49 stars 25 forks source link

Function union parameters can produce errors #769

Closed nickbattle closed 3 years ago

nickbattle commented 3 years ago

The following spec produces runtime errors:

    f: (nat -> nat) | (char * char -> bool) +> bool
    f(x) ==
        if is_(x, nat -> nat) then true
        else if is_(x, char -> bool) then true
        else x('x', 'y');

> p f(lambda x:nat & x+1)
Error 4052: Wrong number of arguments passed to lambda in 'DEFAULT' (console) at line 1:3

That error is produced on the final "else" line, because the type of the "x" argument has been calculated to be "((char | nat) * char -> nat1)". That is attempting to use a blended union of the parameters, but that is clearly the wrong requirement here and the union should instead be treated as independent clauses.

nickbattle commented 3 years ago

Changing to a union of the separate types produces the expected result:

> p f(lambda x:nat & x+1)
= true
Executed in 0.048 secs. 

Change now available in ncb/development.