Looks more like flow typing than refinement types to me.
The (static) type of 'y' changes seemingly implicitly in the body of the 'if'. It's an 'int' at assignment but needs to be an 'int {.requires ??? > 0.}' (or however the one would write that type literal in Nim), and some flow typing determines than that that cast form 'int' to 'int {.requires ??? > 0.}' is safe in the body of the 'if', and performs this cast implicitly.
The question now is: Is 'int {.requires ??? > 0.}' a type on its own in Nim? It doesn't seem like that as 'b' has 'int' ascribed as its type, and not 'int {.requires ??? > 0.}'.
It's also not dependent typing as the constraint on 'b' can't be an arbitrary function. (I guess, please correct me if I'm wrong; but in that case this typing wouldn't be decidable, even with the help of SMT).
The type of 'safeDivide' could be a "depended function type", tough.
The (static) type of 'y' changes seemingly implicitly in the body of the 'if'. It's an 'int' at assignment but needs to be an 'int {.requires ??? > 0.}' (or however the one would write that type literal in Nim), and some flow typing determines than that that cast form 'int' to 'int {.requires ??? > 0.}' is safe in the body of the 'if', and performs this cast implicitly.
The question now is: Is 'int {.requires ??? > 0.}' a type on its own in Nim? It doesn't seem like that as 'b' has 'int' ascribed as its type, and not 'int {.requires ??? > 0.}'.
It's also not dependent typing as the constraint on 'b' can't be an arbitrary function. (I guess, please correct me if I'm wrong; but in that case this typing wouldn't be decidable, even with the help of SMT).
The type of 'safeDivide' could be a "depended function type", tough.