On Sat, Jun 27, 2009 at 10:45 PM, Darryn wrote:

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.

The actual problem is not that easy to understand until you really get to know the intricacies of Haskell's type checking. Do you think you could explain your problem is less abstract terms? That is, sometimes if you tell people here what you want to do and why they can suggest a better approach. One thing to understand about your type class `A' is that it does not give a relationship between `b' and `a'. As far as the definition of `A' is concerned, `b' is totally arbitrary, so long as it is an instance of `B'. In particular, no relationship with `a' is implied. Additionally, I'm nearly certain that existential types are not needed or even wanted here. K :: b -> Ainst b In particular, the `b' that `K' takes becomes part of the type that `K' returns. This is different than the type of `a3'. In the type of `a3', the `b' that it takes doesn't necessarily become part of the return type. In a way, that means that `K' is less polymorphic than `a3'. This may not seem like a problem, but it is what prevents `K' from having the same type as `a3', and thus you get your error message. The type of `a3' is more general than the type of `K' due to the possible ranges of the type variables involved. I have played with it a bit and found that this does compile: \begin{code} {-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, FlexibleContexts #-} class A a b | b -> 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 instance (B b) => A (Ainst b) b where a1 = I a2 = J a3 = K -- Reported line of the error data Binst = Val Int instance B Binst where b1 = Val \end{code} If you remove all the type class constraints you won't need the FlexibleContexts, but it's also not hurting anything. Here I am using the functional dependency between `a' and `b' that says, once you fix the type of `b', you also fix the type of `a'. You'll notice that, that is exactly what `K' does. Given a `b', it gives you `Ainst a', where `a = b', and therefore the type depends on, or is fixed by, `b'. Multi parameter type classes are needed just so we can give the functional dependency and the flexible things are in there just to work around Haskell 98 restrictions. I hope this sheds more light on the problem. I bet you could be using type families here as well, but I have yet to take the time to understand them. I hope that helps, Jason