You should include the definitions of the classes before saying
HOrderedList l' just has to prove by induction that for any element in the list, the next element is greater, so the class is simply: class HOrderedList l instance HNil instance HCons a HNil instance (HOrderedList (HCons b l),HLe a b) => HCons a (HCons b l) which is the equivalent type level program to ordered :: [Int] -> Bool ordered [] = True ordered [a] = True ordered (a:(b:l)) = if a<=b then ordered (b:l) else False ordered _ = False It is obvious by observation that the a<=b ensures order. This is a lot simpler than say a heap-sort. I suppose you could contend that there are some classes above I still haven't defined - but you wouldn't expect to see definitions for (<=) which is defined in the prelude. Of course to show statically that order is preserved the 'value' of the elements to be ordered must be visible to the type system - so the values must be reified to types... This can be done for any Haskell type, but for numbers we would use Peano numbers - the HLe class for these is again easily defined by induction: class HLe n n' instance HLe HZero HZero instance HLe x y => HLe (HSucc x) (HSucc y) Keean.