What is a common problem in programming is to use types that are too generic for a particular problem. If a too generic type is used, it leads to allowing values in types that don’t make any sense for the particular problem at hand, which leads to unforeseeable errors at runtime. For example, you might want to say that a particular number has to be greater than 5, i.e., x > 5. This kind of constraint is nice to have because it supports a pattern where illegal values are not representable. That way you avoid throwing exceptions at runtime when you get a value that doesn’t meet needed constraints, which allows for referential transparency, which allows for functional programming, which in turn allows for easier reasoning about your programs. In general, type systems in programming languages don’t have a way of representing a constraint like x > 5.
Types in type theory that allow for such constraints are called refinement types. Languages that I have been working with support refinement types via libraries. In Haskell, the library (Hackage link) is called refined. In Scala, the library is also called refined and it is inspired by the Haskell equivalent. Finally, in Idris there is a library with the same name and it is inspired by its equivalents in Haskell and Scala. For a nice motivation for refinement types with examples in Haskell, see Nikita Volkov’s announcement of the Haskell refinement types library.
The gist is that at runtime you use smart constructors that instead of throwing an exception when constrains are not met, they return an error (via the Either type constructor). If constraints are met, they return the intended value on the right of the Either constructor. With that you can easily pass around such a value and pattern-match on it.