I think so. Using existential types, we can encode predicates in such a way that the type is inhabited (i.e. there is a value of that type) only if the predicate is true.

I am learning Forth and Idris in my spare time these days. I have tried writing merge of two sorted lists in Idris, with the constraint that the merged list must have the length equal to the sum of the lengths of the input lists etc. - frankly, I much prefer Forth :D

https://www.idris-lang.org/