I have imported a data type, X, defined as
data X a = X a
Locally, I have defined a universally quantified data type, Y
type Y = forall a. X a
Now I need to define two functions, toY and fromY. For fromY, this definition works fine:
fromY :: Y -> X a
fromY a = a
but if I try the same thing for toY, I get an error
Couldn't match type 'a' with 'a0'
'a' is a rigid type variable bound by the type signature for 'toY :: X a -> y'
'a0' is a rigid type variable bound by the type signature for 'toY :: X a -> X a0'
Expected type: X a0
Actual type: X a
If I understand correctly, the type signature for toY is expanding to forall a. X a -> (forall a0. X a0) because Y is defined as a synonym, rather than a newtype, and so the two as in the definitions don't match up.
But if this is the case, then why does fromY type-check successfully? And is there any way around this problem other than using unsafeCoerce?
This is more like a comment but I could not really put it there as it would have been unreadable; please forgive me this one time.
Aside from what dfeuer already told you, you might see (when you use his answer) that toY is now really easy to do but you might have trouble defining fromY – because you basically lose the type-information, so this will not work:
{-# LANGUAGE GADTs #-}
module ExTypes where
data X a = X a
data Y where
Y :: X a -> Y
fromY :: Y -> X a
fromY (Y a) = a
as here you have two different as – one from the constructor Y and one from X a – indeed if you strip the definition and try to compile: fromY (Y a) = a the compiler will tell you that the type a escapes:
Couldn't match expected type `t' with actual type `X a'
because type variable `a' would escape its scope
This (rigid, skolem) type variable is bound by
a pattern with constructor
Y :: forall a. X a -> Y,
in an equation for `fromY'
I think the only thing you will have left now will be something like this:
useY :: (forall a . X a -> b) -> Y -> b
useY f (Y x) = f x
but this might prove not to be too useful.
The thing is that you normally should constrain the forall a there a bit more (with type-classes) to get any meaningful behavior – but of course I cannot help here.
This wiki article might be interesting for you on the details.