What does "exists" mean in Haskell type system?

I'm struggling to understand the exists keyword in relation to Haskell type system. As far as I know, there is no such keyword in Haskell by default, but:

There are extensions which add them, in declarations like these data Accum a = exists s. MkAccum s (a -> s -> s) (s -> a)
I've seen a paper about them, and (if I recall correctly) it stated that exists keyword is unnecessary for type system since it can be generalized by forall

But I can't even understand what exists means.

When I say, forall a . a -> Int, it means (in my understanding, the incorrect one, I guess) "for every (type) a, there is a function of a type a -> Int":

myF1 :: forall a . a -> Int
myF1 _ = 123
-- okay, that function (`a -> Int`) does exist for any `a`
-- because we have just defined it

When I say exists a . a -> Int, what can it even mean? "There is at least one type a for which there is a function of a type a -> Int"? Why one would write a statement like that? What the purpose? Semantics? Compiler behavior?

myF2 :: exists a . a -> Int
myF2 _ = 123
-- okay, there is at least one type `a` for which there is such function
-- because, in fact, we have just defined it for any type
-- and there is at least one type...
-- so these two lines are equivalent to the two lines above

Please note it's not intended to be a real code which can compile, just an example of what I'm imagining then I hear about these quantifiers.

P.S. I'm not exactly a total newbie in Haskell (maybe like a second grader), but my Math foundations of these things are lacking.

Solution

A use of existential types that I've run into is with my code for mediating a game of Clue.

My mediation code sort of acts like a dealer. It doesn't care what the types of the players are - all it cares about is that all the players implement the hooks given in the Player typeclass.

class Player p m where
  -- deal them in to a particular game
  dealIn :: TotalPlayers -> PlayerPosition -> [Card] -> StateT p m ()

  -- let them know what another player does
  notify :: Event -> StateT p m ()

  -- ask them to make a suggestion
  suggest :: StateT p m (Maybe Scenario)

  -- ask them to make an accusation
  accuse :: StateT p m (Maybe Scenario)

  -- ask them to reveal a card to invalidate a suggestion
  reveal :: (PlayerPosition, Scenario) -> StateT p m Card

Now, the dealer could keep a list of players of type Player p m => [p], but that would constrict all the players to be of the same type.

That's overly constrictive. What if I want to have different kinds of players, each implemented differently, and run them against each other?

So I use ExistentialTypes to create a wrapper for players:

-- wrapper for storing a player within a given monad
data WpPlayer m = forall p. Player p m => WpPlayer p

Now I can easily keep a heterogenous list of players. The dealer can still easily interact with the players using the interface specified by the Player typeclass.

Consider the type of the constructor WpPlayer.

    WpPlayer :: forall p. Player p m  => p -> WpPlayer m

Other than the forall at the front, this is pretty standard haskell. For all types p that satisfy the contract Player p m, the constructor WpPlayer maps a value of type p to a value of type WpPlayer m.

The interesting bit comes with a deconstructor:

    unWpPlayer (WpPlayer p) = p

What's the type of unWpPlayer? Does this work?

    unWpPlayer :: forall p. Player p m => WpPlayer m -> p

No, not really. A bunch of different types p could satisfy the Player p m contract with a particular type m. And we gave the WpPlayer constructor a particular type p, so it should return that same type. So we can't use forall.

All we can really say is that there exists some type p, which satisfies the Player p m contract with the type m.

    unWpPlayer :: exists p. Player p m => WpPlayer m -> p