[Haskell-cafe] Rigid type variable error

[Daniel Fischer]

Am Sonntag 28 Juni 2009 07:45:33 schrieb Darryn:
> 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

This means a3 has the type

forall c. (B c) => c -> 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

Tis means K can only take an argument of type b, so

K :: (B b) => b -> Ainst b

>
> instance (B b) => A (Ainst b) where
>     a1 = I
>     a2 = J
>     a3 = K -- Reported line of the error

a3 must have type

forall c. (B b, B c) => c -> Ainst b

which is more general than K's type.

Depending on what you want to do, you could
a) change Ainst,
data Ainst = I | J Ainst | (B b) => K b

instance (B b) => A Ainst where
    a1 = I
    a2 = J
    a3 = K

but then you don't know what type b has been used to construct J (K x), so you can't do 
much with it.

b) make A a multiparameter type class with functional dependencies

class A a b | a -> b where
    a1 :: a
    a2 :: a -> a
    a3 :: b -> a

instance (B b) => A (Ainst b) b where
    a1 = I
    a2 = J
    a3 = K

c) use type families:

class A a where
    type S a
    a1 :: a
    a2 :: a -> a
    a3 :: S a -> a

instance (B b) => A (Ainst b) where
    type S (Ainst b) = b
    a1 = I
    a2 = J
    a3 = K

b) and c) are more or less equivalent and restrict the type of a3 to K's type

>
> 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.
>