Johan Nordlander and I have been looking at these interesting examples, and would like to offer another entertaining variation to the collection: class C t where op :: t -> Bool instance C [t] where op x = True p y = (let f :: c -> Bool; f x = op (y >> return x) in f, y ++ []) q y = (y ++ [], let f :: c -> Bool; f x = op (y >> return x) in f) The definitions of p and q differ only in the order of the components in the pair on their right-hand sides. And yet: ghc and "Typing Haskell in Haskell" reject p, but accept q; Hugs rejects q, but accepts p; hbc rejects both p and q; nhc98 ... (Malcolm, can you fill in the blank for us!). The type signature for f forces context reduction to take place, and the results of this depend on whether or not the type of y is known, which in turn depends on which component of the pair the type checker analyzes first. I'm sure we will all continue to ponder this for some time to come ... All the best, Mark & Johan