Recent paper on this topic
First-Class Refinement Types for Scala
I gather this feature is implemented by forking the scala compiler. Not as a compiler plugin or as user side library
If anyone from the paper is here. I have a couple of questions.
-The tecnique does not depend on totality checking to be sound ( like liquid haskell does )
But could it support totality checking anyways? If so, how hard would be to add the feature
-A custom solver is being used. But it is mentioned, is far less powerfull than one based on SMT. Have you considered using SMT.