В моем (возможно неправильном) понимании следующие два списка должны быть эквивалентными:
[1, "a"] :: [forall a. Show a => a]
data V = forall a. Show a => V a
[V 1, V "a"] :: [V]
Однако первый из них не принят, но второй работает отлично (с ExistentialQuantification).
Если первый список не существует, каков будет тип в пробеле map V :: ??? -> [V]? Какой тип механизма обеспечивает наличие оболочки?
Ваше понимание неверно. Большая часть проблемы заключается в том, что традиционный синтаксис экзистенциального квантификации, который вы использовали, довольно запутан для всех, кто не знаком с ним. Поэтому я настоятельно рекомендую использовать вместо этого синтаксис GADT, который также имеет преимущество быть более сильным. Легкая вещь - просто включить {-# LANGUAGE GADTs #-}. Пока мы это делаем, включите {-# LANGUAGE ScopedTypeVariables #-}, потому что мне не интересно, что означает forall в любом месте. Ваше определение V означает то же самое, что и
data V where
V :: forall a . Show a => a -> V
Мы можем фактически отказаться от явного forall, если хотите:
data V where
V :: Show a => a -> V
Итак, конструктор данных V - это функция, которая берет что-то из любого видимого типа и создает что-то типа V. Тип map довольно ограничительный:
map :: (a -> b) -> [a] -> [b]
Все элементы списка, переданные в map, должны иметь один и тот же тип. Таким образом, тип map V - это просто
map V :: Show a => [a] -> [V]
Теперь вернемся к вашему первому выражению:
[1, "a"] :: [forall a. Show a => a]
Теперь, что на самом деле говорит, что [1, "a"] - это список, каждый из элементов которого имеет тип forall a . Show a => a. То есть, если я предоставляю любой a экземпляр Show, каждый элемент списка должен иметь этот тип. Это просто неправда. "a", например, не имеет типа Bool. Здесь еще одна проблема; тип [forall a . Show a => a] является "нецелесообразным". Я не понимаю детали того, что это значит, но, как вы говорите, вы застряли forall в аргументе конструктора типа, отличного от ->, и это недопустимо. GHC может предложить вам включить расширение ImpredicativeTypes, но это действительно не работает правильно, поэтому вам не следует. Если вам нужен список существительно сугубо квантифицированных вещей, вам необходимо сначала их обернуть в экзистенциальные типы данных или использовать специализированный тип экзистенциального списка. Если вам нужен список предметов с квантованием по всему миру, сначала их нужно обернуть (возможно, в newtypes).