title: How can this phantom type example possibly be valid?
body: <pre><code>data Expr a
    = C a
    | Add (Int -&gt; a) (Expr Int) (Expr Int)
    | Eq (Bool -&gt; a) (Expr Int) (Expr Int)
  
  add = Add id
  eq  = Eq id
  
  eval :: Expr a -&gt; 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
  </code></pre>
  
  <p>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.</p>
  
  <p>What the above does is emulate a GADT with phantom types, but not in a way I could have imagined it working. <code>Int -&gt; a</code> and <code>Bool -&gt; a</code> 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 <code>bool</code> while the other returns an <code>int</code>.</p>
  
  <p>Can anyone illuminate as to why this example is correct in Haskell?</p>
  
  <p>Edit: Here is a further elaboration of the problem.</p>
  
  <pre><code>data Expr a
    = C a
    | Add (Expr Int) (Expr Int)
    | Eq (Expr Int) (Expr Int)
  
  add = Add
  eq  = Eq
  
  eval :: Expr a -&gt; 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
  </code></pre>
  
  <p>When I remove the <code>Int -&gt; a</code> and <code>Bool -&gt; a</code> parts, the example fails to typecheck.</p>
  
  <p>But in the first example those functions can only be <code>id</code>, that is of type <code>Int -&gt; Int</code> and <code>Bool -&gt; Bool</code> respectively. Applying the proof function the ADTs are carrying around with them should do absolutely nothing to change that fact as they are <code>id</code> in the example and should logically fail to typecheck. Applying them should do absolutely nothing.</p>
  
  <p>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.</p>
  
  <p>Edit2: Here is the F# translation:</p>
  
  <pre><code>type Expr&lt;'a&gt; =
      | C of 'a
      | Add of ((int -&gt; 'a) * Expr&lt;int&gt; * Expr&lt;int&gt;)
      | Eq of ((bool -&gt; 'a) * Expr&lt;int&gt; * Expr&lt;int&gt;)
  
  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&lt;'a&gt;) : 'a = 
      match x with
      | C x -&gt; x
      | Add(f,x,y) -&gt; f (eval x + eval y)
      | Eq(f,x,y) -&gt; f (eval x = eval y)
  
  let expr = add (C 5) (C 1) |&gt; eq (C 7)
  
  let r = eval expr
  </code></pre>
  
  <p>In the above example, in the <code>eval</code> function <code>'a</code> is inferred to be of type <code>int</code> and as a result the last line fails to type check.</p>