OK, since I didn't give a very good example, let me try to show a better one. Let's imagine you're writing a testing library. You have a series of tests; each one of them takes in an input, a function to run on the input, and an expected output.

    data Test i o = Test String i (i -> o) o

and then say your testing function is something like

    runTest :: Eq o => Test i o -> IO ()
    runTest (Test name input f output) = case f input of
        o | o == output -> putStrLn $ name ++ " passed"
          | otherwise   -> putStrLn $ name ++ " failed"

Then let's say you had a bunch of tests. For example, you want to test that addition works:

    test1 = Test "addition" (1, 2) (\a b -> a + b) 3

And you want to test string concatenation:

    test2 = Test "concat" ("hello", "world") (\a b -> a ++ b) "helloworld"

Then you could write your tests as

    doTests = runTest test1 >> runTest test2

Now if you have a lot of tests, it would be nice to put them in a list:

    doTests tests = forM_ tests runTest

However, this would require that every test have the same inputs and outputs. You couldn't do

    doTests [test1, test2]

Even though the resulting type is known (it will be an IO () regardless), and even though runTest will operate on each one, because test1 and test2 have different types, you can't put them all in a list.

I think that `forall` and similar allow you to get around this restriction somehow, but I don't really know how that works.

I mean, I agree such examples exist. I don't think this is yet a truly good example, though. The real advantage to existential types like this are in creation of multiple variants---again I recommend reading Jeremy Gibbons' paper.

But, for completeness, here's how you could write your type

    {-# LANGUAGE ExistentialQuantification #-}
    data Test = forall i o . Test i (i -> o) (o -> o -> Bool) o

Although, note, this is exactly equivalent to `Bool`, although in two ways—if we knew the comparator function was commutative then there'd be just one way to convert to `Bool`.

    testBool :: Test -> Bool
    testBool (Test i fun cmp o) = cmp (fun i) o

    testBool' :: Test -> Bool
    testBool' (Test i fun cmp o) = cmp o (fun i)

But in either case there are no other ways to "observe" the existentially quantified types since we've forgotten absolutely everything besides `Bool`. More likely we would want to also, say, show the input.

    data Test = forall i o . (Eq o, Show i) =>
                Test i (i -> o) o

and this type is now equal to `(String, Bool)`.

    testOff :: Test -> (String, Bool)
    testOff (Test i fun o) = (show i, fun i == o)

So, in general, if you're using existential types you really want to either be using multiple variants or when you have such a combination of observables that it's not worth expressing them all directly.