+
+-- HLength
+class IntegerT (HLengthOf l) => HLength l where
+ type HLengthOf l
+ hLength :: Integral n => l -> n
+
+instance HLength HNil where
+ type HLengthOf HNil = D0
+ hLength _ = 0
+
+instance ( HLength l
+ , IntegerT (Succ (HLengthOf l))
+ ) => HLength (HCons e l) where
+ type HLengthOf (HCons e l) = Succ (HLengthOf l)
+ hLength (HCons _ l) = 1 + hLength l