Какова теоретическая основа экзистенциальных типов?

В Haskell Wikiхорошо объясняется, как использовать экзистенциальные типы, но я не совсем понимаю лежащую в их основе теорию.

Рассмотрим этот пример экзистенциального типа:

data S = forall a. Show a => S a      -- (1)

чтобы определить оболочку типа для вещей, которые мы можем преобразовать в String. В вики упоминается, что то, что мы на самом делехотим определить, является типом, подобным

data S = S (exists a. Show a => a)    -- (2)

, то есть истинным «экзистенциальным» типом — в общих чертах я думаю об этом как о том, что «конструктор данных Sпринимает любой тип, для которого Showэкземпляр существует и является его оболочкой». На самом деле, вы, вероятно, могли бы написать GADT следующим образом:

data S where                          -- (3)
    S :: Show a => a -> S

Я не пробовал его компилировать, но кажется, что он должен работать. Для меня GADT, очевидно, эквивалентен коду (2), который мы хотели бы написать.

Однако мне совершенно не очевидно, почему (1) эквивалентно (2). Почему перемещение конструктора данных наружу превращает forallв exists?

Самое близкое, что я могу придумать, это законы Де Морганав логике, где изменение порядка отрицания и квантора превращает кванторы существования в кванторы всеобщности и наоборот:

¬(∀x. px) ⇔ ∃x. ¬(px)

но данные конструкторы кажутся совершенно другим зверем по сравнению с оператором отрицания.

Какая теория лежит в основе возможности определять экзистенциальные типы, используя forallвместо несуществующего exists?