Wrapping / Unwrapping Universally Quantified Types

Question

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?

Answer 1

You claim to define an existential type, but you do not.

type Y = forall a. X a

defines a universally quantified type. For something to have type Y, it must have type X a for every a. To make an existentially quantified type, you always need to use data, and I find the GADT syntax easier to understand than the traditional existential one.

data Y where
  Y :: forall a . X a -> Y

The forall there is actually optional, but I think clarifies things.

I'm too sleepy right now to work out your other questions, but I'll try again tomorrow if no one else does.