Is it possible to have forgetful type synonyms in Haskell?

Question

If I have a type with a phantom parameter that I only sometimes care about, like this one:

data Foo p a b = Bar a b

Is there any hack way to write a type synonym Baz such that Baz a b is Foo p a b for some p that I've forgotten?

You can't do:

type Baz a b = Foo p a b

and while you can do (with appropriate extensions):

type Baz a b = forall p.Foo p a b

It doesn't seem like that does what I want, because I can't convert a value of type Foo P1 a b to type Baz a b, with a message about a "rigid type variable".

Do you need another layer of contructors to achieve this effect, as below? Could you briefly explain why?

data Baz' a b = forall p.Baz' (Foo p a b)

Answer 1

There isn't currently a way to do this as a type synonym. However, if you have GHC 7.10, you can turn on the PartialTypeSignatures extension and write Foo _ a b instead. Use -fno-warn-partial-type-signatures to ask GHC not to warn you about each of the holes you leave in this way.

Answer 2

This can't really be done reliably with type synonyms. You need either existential types or rank-n types.

The problem is that Haskell allows type synonyms to be fully intersubstitutable. I.e., when you define type Baz a b = Foo p a b, then in every context where you have Foo p a b, you would be allowed to use Baz a b, and vice-versa. So for example, if you had a function of this type:

f1 :: Foo Something a b -> Whatever Something b a

Then because of substitutability, that'd be the same type as this:

f1 :: Baz a b -> Whatever Something b a

And as this:

f1 :: Foo p a b -> Whatever Something b a

...which then you could specialize to this:

f1 :: Foo SomethingElse a b -> Whatever Something b a

So, what can you do? One is to define an existential wrapper type:

{-# LANGUAGE ExistentialTypes #-}

data Baz a b = forall p. Baz (Foo p a b)

Alternative way of doing the same thing:

{-# LANGUAGE GADTs #-}

data Baz a b where
     Baz :: Foo p a b -> Baz a b

Second way you could go: rank-n types and continuation-passing style:

{-# LANGUAGE RankNTypes #-}

-- To consume one of these, you pass a "callback" function to `runBaz`,
-- which is not allowed to restrict the type variable `p`.
newtype Baz a b = Baz { runBaz :: forall p r. (Foo p a b -> r) -> r }

makeBaz :: Foo p a -> Baz a b
makeBaz foo = Baz ($foo)

Third way, which you've attempted and (I'm told) doesn't work very well: type synonyms + impredicative types (which are required to get forall synonyms to occur as type arguments in many cases).