assert (lambda f : Int -> * -> Int . f 2 Int) (lambda (x y : _7) . add x 1) = 5;
That is, _7 is both Int and *. This works because type inference is local and the underscore names do not actually have a meaning.
In the future there might be more complete type inference. In the interest of forward compatibility we want to prevent users from using this "feature".
Currently this works:
That is,
_7is bothIntand*. This works because type inference is local and the underscore names do not actually have a meaning.In the future there might be more complete type inference. In the interest of forward compatibility we want to prevent users from using this "feature".