Well, you can interpret the predicate function body as a set of constraints on the type. Of course, such predicate function would need to be restricted to what

Well, you can interpret the predicate function body as a set of constraints on the type. Of course, such predicate function would need to be restricted to what your type system can handle. Typed Racket does this, by allowing you to implement type refinements[1]. As long as the predicate only uses operations listed there, it can be used for type checking. Idris also lets you write functions that operate on types and that are used for type checking. [1] https://docs.racket-lang.org/ts-reference/Experimental_Features.html#%28form._%28%28lib._typed-racket%2Fbase-env%2Fbase-types-extra..rkt%29._.Refine%29%29 https://docs.racket-lang.org/ts-reference/Experimental_Featu...