Defining Phantom Types - can't compile examples

Question

I'm trying to learn more about Phantom Types. I'm trying to read through Fun with Phantom Types by Ralf Hinze. He's using a keyword with I haven't seen before and that I can't get to compile. I get a parse error on = when I try this.

data Type t = RInt                    with t = Int
            | RChar                   with t = Char
            | RList (Type a)          with t = [a ]
            | RPair (Type a) (Type b) with t = (a, b)

Earlier in the paper, he says that the "with" statements aren't strictly necessary, that you can set a = t instead, but I can't figure out how to define this data type without them. The following errors with: Not in scope: type variable 'a'

data Type t = RInt
            | RChar
            | RList (Type a)
            | RPair (Type a) (Type b)

What am I missing?

Answer 1

Although ugly, the following will work and might be considered slightly closer to that notation in spirit. This is essentially desugaring a GADT into type equalities (which seem not to have their own extension so you need either GADTs or TypeFamilies enabled to use them) and existentials.

{-# LANGUAGE ExistentialQuantification, TypeFamilies #-}

data Type t = t ~ Int => RInt
            | t ~ Char => RChar
            | forall a. t ~ [a] => RList (Type a)
            | forall a b. t ~ (a, b) => RPair (Type a) (Type b)

Answer 2

My guess is that the definition sans-with suggested in the paper is

data Type t = RInt
            | RChar
            | RList (Type t)
            | RPair (Type t) (Type t)

Above, the parameter t is never used. It is, indeed, phantom.

This implies that, e.g.

RInt :: Type a

for any type a. By contrast, if the with constraints were followed, it would be impossible to have RInt :: Type t for any t but for t ~ Int.

The with syntax is not present in GHC, but GADTs play essentially the same role.

{-# LANGUAGE GADTs #-}
data Type t where
   RInt  :: t ~ Int   => Type t
   RChar :: t ~ Char  => Type t
   RList :: t ~ [a]   => Type a -> Type t
   RPair :: t ~ (a,b) => Type a -> Type b -> Type t

Note how with is replaced by an equality constraint in each constructor. It's basically the same thing, written differently.

More compactly, we can rewrite the above into

data Type t where
   RInt  :: Type Int
   RChar :: Type Char
   RList :: Type a -> Type [a]
   RPair :: Type a -> Type b -> Type (a,b)

where the constraints have been "inlined" in the final type.