https://blog.racket-lang.org/2017/10/racket-v6-11.html

Typed Racket supports refinement types and dependent function types. Previously
an experimental feature, refinement types allow types to describe more
interesting properties of values, especially integers. For example, this type
shows that the max function always produces a number at least as big as its
inputs:

(-> ([x : Integer] [y : Integer])
(Refine [z : Integer]
(and (>= z x) (>= z y))))