pyret-lang
pyret-lang copied to clipboard
Type checking `satisfies` fails in `where` blocks when used with `(Any -> Boolean)` predicates
Remember that the is-number function is typed as (Any -> Boolean), so as, expected we can write the following check:
check:
1 satisfies is-number
end
You can still do this with basic functions in a function's where block, such as:
fun is-even(n :: Number) -> Boolean:
num-modulo(n, 2) == 0
end
fun add1(x :: Number) -> Number:
x + 1
where:
add1(1) satisfies is-even # works
end
But some this does not work when using a predicate expecting Any, such as is-number, meaning that the following fails to type check:
fun add1(x :: Number) -> Number:
x + 1
where:
is-number(1) is true # works
1 satisfies is-number # type error
end
resulting in the following message:
Type checking failed because of a type inconsistency.
The type constraint `Number` at file:///path/to/repro1.arr:5:2-5:3 was incompatible with the type constraint `Any` at file:///path/to/repro1.arr:5:14-5:23
Thinking that satisfies maybe doesn't downcast correctly in this context, I tried doing so explicitly:
fun upcast<T>(x :: T) -> Any:
x
end
fun func() -> Nothing:
nothing
where:
upcast(1) satisfies is-number # type error
end
which results in a pretty revealing error:
Type checking failed because of a type inconsistency.
The type constraint `Any` at file:///path/to/repro2.arr:8:2-8:11 was incompatible with the type constraint `Any` at file:///path/to/repro2.arr:8:22-8:31