Экзистенциальное количественное определение без конструкторов данных

Question

Экзистенциальную количественную оценку легко получить, упаковав словари в конструкторы данных.

{-# LANGUAGE GADTs #-}

data S where
  MkS :: Show a => a -> S

f :: Int -> S
f x = case x of
  0 -> MkS 0
  _ -> MkS "non-zero"

В соответствующем разделе в руководстве по GHC прямо говорится о "экзистенциально количественных конструкторах данных". Можно ли написать тот же код, но без введения дополнительных типов данных и конструкторов, то есть что-то с сигнатурой типа

f :: Int -> (exists a. Show a => a)
f x = case x of
  0 -> 0
  _ -> "non-zero"

Если нет, есть ли документированная причина, по которой существует это ограничение? Как избежать добавления нового квантификатора?

Answer 1

Заимствуя из комментария Колина и глядя на этот ответ , можно написать CPS-версию этого же кода без exists квантификатора.

f' :: Int -> ((forall a. Show a => a -> r) -> r)
f' x = case x of
  0 -> \k -> k 0
  _ -> \k -> k "non-zero"

Хотя это не идеально, оно, безусловно, решает проблему без введения дополнительных типов данных.