pyret-lang icon indicating copy to clipboard operation
pyret-lang copied to clipboard

Type checking `satisfies` fails in `where` blocks when used with `(Any -> Boolean)` predicates

Open ironm00n opened this issue 5 months ago • 0 comments

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
CPO Screenshots Image Image

ironm00n avatar Jul 24 '25 16:07 ironm00n