Broken type inference with --type-system-refresh

[josedusol]

Dafny version

4.11.0

Code to produce this issue

lemma StrictIncrImpliesInjection(f:nat->nat)
  requires forall x, y :: x < y ==> f(x) < f(y)
  ensures  forall x, y :: f(x) == f(y) ==> x == y
{ }

Command to run and resulting output

$ dafny verify --type-system-refresh example.dfy                                             
example.dfy(3,38): Error: value does not satisfy the subset constraints of 'nat'
  |
3 |   requires forall x, y :: x < y ==> f(x) < f(y)
  |                                       ^

example.dfy(4,28): Error: value does not satisfy the subset constraints of 'nat'
  |
4 |   ensures  forall x, y :: f(x) == f(y) ==> x == y
  |                             ^

example.dfy(4,36): Error: value does not satisfy the subset constraints of 'nat'
  |
4 |   ensures  forall x, y :: f(x) == f(y) ==> x == y
  |                                     ^


Dafny program verifier finished with 1 verified, 3 errors

What happened?

I expected the code to type check, but Dafny can't infer bound variables x and y are nat. This only happens with --type-system-refresh option.

Moreover, i have lot's of lines of code that also have issues when using this option, all of them seem to be related to subset constraints.

What type of operating system are you experiencing the problem on?

Windows