The code specify only basic types, then compile-time and run-time assertions are added to the code.
Refinement types are more useful in context like relational DSL, and data-science DSL, because the final type of the resulting data structure, depends from the expressions calculating it.
TODO The authors of Liquid Haskell created a tutorial based on OCaml code, about the implementation of refinement types. “Refinement types” by Ramjit Jhala.
TODO study also the papers about Typed Racket, because it is a very advanced system
NOTE: in CL values has types at run-time, but variables have no type at compile-time. A variable can contain a reference to every value of every type. Also numbers. So a variable can contain both a reference or a value.