Thanks for the help previously received, but I still cannot seem to get on top of this. The types for the constructor K will not resolve and I'm at a loss to work out what to do with it. If anyone can offer a further explanation and help I would be very grateful. My code (File Test5.hs): ---------------------------- {-# LANGUAGE ExistentialQuantification #-} class A a where a1 :: a a2 :: a -> a a3 :: (B b) => b -> a class B b where b1 :: Int -> b --data Ainst b = I | J (Ainst b) | K b -- a3 :: (B b, A a) => b -> a -- yet without the constraint on K, K :: b -> Ainst b -- so the above data definition fails. Trying to -- existentially quantify K below seems to make -- sense, but also fails ... data Ainst b = I | J (Ainst b) | (B b) => K b instance (B b) => A (Ainst b) where a1 = I a2 = J a3 = K -- Reported line of the error data Binst = Val Int instance B Binst where b1 = Val ------------------------------- The error from ghci is as follows: Test5.hs:25:9: Couldn't match expected type `b' against inferred type `b1' `b' is a rigid type variable bound by the type signature for `a3' at Test5.hs:7:13 `b1' is a rigid type variable bound by the instance declaration at Test5.hs:16:12 Expected type: b -> Ainst b1 Inferred type: b1 -> Ainst b1 In the expression: K In the definition of `a3': a3 = K Failed, modules loaded: none. Thanks in advance for any help. Apologies if what I am doing is odd or the answer is obvious, I'm still very new to Haskell. Darryn.