I apologize if this question has been asked before... It seems to me the following code should be legal: type Thing m = m () type Const a b = a f :: Thing m -> Thing m f x = x test :: Thing (Const Int) -> Thing (Const Int) test = f However, GHC gives the following error: Couldn't match `Thing m' against `Thing (Const Int)' Expected type: Thing m Inferred type: Thing (Const Int) Expected type: Thing (Const Int) -> Thing (Const Int) Inferred type: Thing m -> Thing m But if you change the definition of Const newtype Const a b = MakeConst a the code compiles fine. Is this the desired behavior? Is it the case that when you have quantification of a type variable of kind * -> * (in this case, m), that variable may only become bound to a type constructor? Sam Moelius