Hello, To experiment with some of GHC's new features in HEAD, I have started ported part of the Prelude from values and functions to types and constraints. For example: comparing lists. instance Compare '[] '[] EQ instance Compare '[] (x ': xs) LT instance Compare (x ': xs) '[] GT instance (Compare x y o, Case o [ EQ --> Compare xs ys r, o --> o ~ r ]) => Compare (x ': xs) (y ': ys) r Prelude.Type> T :: (Compare '[I 1, I 2] '[I 1, I 3] a) => T a LT Sometimes I get nice error messages. Prelude.Type> T :: If (I 1 == I 2) (a ~ "hello") (a ~ 3) => T a Kind mis-match The left argument of the equality predicate had kind `Symbol', but `3' has kind `Nat' But often GHC refuses to type large constraints when there are too many constraint kinds and free variables. It also gets confused if I pretend to use higher-order kinds. instance ((a >>= Const b) c) => (a >> b) c Kind mis-match The first argument of `>>' should have kind `k0 k1', but `a' has kind `k0 k1' In the instance declaration for `(a >> b) c' I'm not sure yet how this is useful this, but I hope it can at least entertain a few people and stress-test the typechecker. http://code.atnnn.com/projects/type-prelude/repository/entry/Prelude/Type.hs darcs get http://code.atnnn.com/darcs/type-prelude/ Etienne Laurin