How can this phantom type example possibly be valid?

data Expr a
  = C a
  | Add (Int -> a) (Expr Int) (Expr Int)
  | Eq (Bool -> a) (Expr Int) (Expr Int)

add = Add id
eq  = Eq id

eval :: Expr a -> a
eval (C x) = x
eval (Add f e1 e2) = f (eval e1 + eval e2)
eval (Eq f e1 e2)  = f (eval e1 == eval e2)

expr1 = (C 5 `add` C 1) `eq` C 6

main = print $ eval expr1

Coming from a different functional language, ever so often I get an inkling that I do not exactly get Haskell's type system and the above is one of those cases.

What the above does is emulate a GADT with phantom types, but not in a way I could have imagined it working. Int -> a and Bool -> a are supposedly proofs of what type is supposed to be here, but when I translated the above example in F# as expected, it did not work because one of the pattern matching branches returns a bool while the other returns an int.

Can anyone illuminate as to why this example is correct in Haskell?

Edit: Here is a further elaboration of the problem.

data Expr a
  = C a
  | Add (Expr Int) (Expr Int)
  | Eq (Expr Int) (Expr Int)

add = Add
eq  = Eq

eval :: Expr a -> a
eval (C x) = x
eval (Add e1 e2) = eval e1 + eval e2
eval (Eq e1 e2)  = eval e1 == eval e2

expr1 = (C 5 `add` C 1) `eq` C 6

main = print $ eval expr1

When I remove the Int -> a and Bool -> a parts, the example fails to typecheck.

But in the first example those functions can only be id, that is of type Int -> Int and Bool -> Bool respectively. Applying the proof function the ADTs are carrying around with them should do absolutely nothing to change that fact as they are id in the example and should logically fail to typecheck. Applying them should do absolutely nothing.

This is what I do not understand; as far as I am concerned this example is pretty much magical to me in terms of how types work.

Edit2: Here is the F# translation:

type Expr<'a> =
    | C of 'a
    | Add of ((int -> 'a) * Expr<int> * Expr<int>)
    | Eq of ((bool -> 'a) * Expr<int> * Expr<int>)

let inline id x = x
let inline add x y = Add(id,x,y)
let inline eq x y = Eq(id,x,y)

let rec eval (x: Expr<'a>) : 'a = 
    match x with
    | C x -> x
    | Add(f,x,y) -> f (eval x + eval y)
    | Eq(f,x,y) -> f (eval x = eval y)

let expr = add (C 5) (C 1) |> eq (C 7)

let r = eval expr

In the above example, in the eval function 'a is inferred to be of type int and as a result the last line fails to type check.

Solution

Take a look at the following type:

eval :: Expr a -> a

This says, "given a value of type Expr a, for any a at all, I can produce an a". Your implementation of eval needs to be a proof of this statement.

Going back to the definition of the Expr type

data Expr a
  = C a
  | Add (Int -> a) (Expr Int) (Expr Int)
  | Eq (Bool -> a) (Expr Int) (Expr Int)

we can see that the constructors Add and Eq, apart from containing two values of type Expr Int, also contain a function from Int or Bool to a. The important part here is that this is the same a as in the type constructor, therefore the type of the value contained in this field will constrain the type of the value as a whole. You can check this in ghci:

λ. :t Add id
Add id :: Expr Int -> Expr Int -> Expr Int
λ. :t Eq id
Eq id :: Expr Int -> Expr Int -> Expr Bool

This also works in the other direction, meaning that if an expression of type Expr Bool is expected in some context, and you try to use the Add constructor to create this expression, the type of its first field must be Int -> Bool. Generalising this leads you to the conclusion: if an expression of type Expr a is expected in that context, and you attempt to create such an expression using the Add or Eq constructors, the function contained inside must be of type Int -> a or Bool -> a, respectively.

Therefore, the functions contained inside those constructors are proof that, no matter which concrete a is in question, you will be able to apply them to either an Int or a Bool to construct an a. This is true by construction since picking out a concrete function chooses which concrete a we are dealing with.

Finally, going back to the implementation of eval:

eval :: Expr a -> a
eval (C x) = x
eval (Add f e1 e2) = f (eval e1 + eval e2)
eval (Eq f e1 e2) = f (eval e1 == eval e2)

Let's examine the three branches to check whether it is indeed a proof of the we set out to prove, which was "given a value of type Expr a, for any a at all, I can produce an a":

For the C branch this is trivially true since x :: a.
For the Add branch, we can determine that the type of eval e1 + eval e2 must be Int. Luckily, we have f :: Int -> a which, by construction, is able to give us an a from an Int so this case is proved.
For the Eq branch, eval e1 == eval e2 clearly has the type Bool (due to (==)). Again, we have f :: Bool -> a which is able to produce an a from this Bool and satisfy the type.

Therefore, given a value of type Expr a constructed via any of its constructors, we are able to produce an a without knowing what concrete a we are talking about.

Also, keep in mind that since eval is polymorphic in a, different calls of eval can return values of different types, but the above should demonstrate that for a single call, all three branches are constrained to return the same type.