The Clay approach to type parametrization and requirements sounds
interesting. I found that for my Haskell experiments I had to use many
of the GHC pragmas related to type classes. For example, for Chapter
5, I needed TypeFamilies, FlexibleInstances, UndecidableInstances,
MultiParamTypeClasses, and FlexibleContexts. But it was possible.

Do you have something like type functions, so that requirements can be
expressed in terms of a parameter type and some affiliated type? A
good example is the distance type for an iterator type.