Что означает «существует» в системе типов Haskell?

Я изо всех сил пытаюсь понять ключевое слово exists по отношению к Система типов Haskell. Насколько мне известно, по умолчанию в Haskell нет такого ключевого слова, но:

• Есть расширений , которые добавляют их в объявлениях, подобных этим data Accum a = exists s. MkAccum s (a -> s -> s) (s -> a)
• Я видел статью о них, и (если я правильно помню) он заявил, что ключевое слово exists не нужно для системы типов, поскольку оно может быть обобщено с помощью forall

Но я даже не могу понять, что существует означает.

Когда я говорю, forall a. a -> Int , это означает (в моем понимании неправильный, я полагаю) «для каждого (типа) a существует функция типа 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

Когда я говорю, что существует. a -> Int , что это вообще может значить? «Существует хотя бы один тип a , для которого существует функция типа a -> Int »? Зачем писать такое заявление? Какая цель? Семантика? Поведение компилятора?

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

Обратите внимание, что это не настоящий код, который можно компилировать, просто пример того, что я представляю, а потом слышу об этих квантификаторах.

PS Я не совсем новичок в Haskell (может быть, как второклассник), но мне не хватает математических основ этих вещей.