Subtypes as subsets of SML datatypes
These kinds of types -- where you define a subtype (basically) by giving a grammar of the acceptable values -- are called datasort refinements. 


They were introduced by Tim Freeman and Frank Pfenning, in their 1991 PLDI paper, Refinement Types for ML. 
Rowan Davies studied type inference for refinement types in his PhD thesis, Practical Refinement Type Checking. He also implemented it as an extension to SML, but I don't know if it is available online.
Joshua Dunfield studied how to combine datasort refinements with fancier lightweight type dependency in his thesis, A Unified System of Type Refinements. He also implemented it in his Stardust language, which is available online:

http://www.mpi-sws.org/~joshua/stardust/