15 Limitations
Only integers: Shplait has no other numbers, so amounts of money, for instance, must be integers (e.g., represented as cents).
No refinements on Listof or Mapof elements. You can, however, write a custom datatype with refined fields, as in OList above.
No refinements on a definition inside another definition, on an anonymous fun (a lambda), on a let, or in a function type.
No calls to functions outside the module, beyond the modelled builtins.
No measures that look inside a list: e.g., “the result has the same elements as the input” cannot be stated.
No refinements that are themselves parameters (abstract refinements), and no quantified refinements.
No measures over a polymorphic datatype.
No nested match patterns.
No checks at module boundaries. Refinements are proved for the code in a module, but values that come from code the checker did not see (another module, or another language) are not checked. A constructor with a refined field can be called from such code with any arguments, and a function’s refinements are not checked when it is called from there. So the guarantees hold only when a module’s functions and constructors are used from checked code. (Shplait does not check values at module boundaries either.)
A value whose refinement was proved when it was made keeps that refinement, even after an operation has produced a newer value from it. So a refinement cannot stop a program from using an old value, such as a turnstile that has already let someone through: "turnstile.rhm". Preventing that requires additional type system features to deal with aliasing, such as linearity or separation logic.