[Haskell-cafe] Rigid type variable error

[Jason Dagit]

On Sat, Jun 27, 2009 at 10:45 PM, Darryn <djreid at aapt.net.au> 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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20090628/b9ca6171/attachment.html