In my (might incorrect) understanding, following two lists should be equivalent:
[1, "a"] :: [forall a. Show a => a]
data V = forall a. Show a => V a
[V 1, V "a"] :: [V]
However, the first one is not accepted but the second one works fine (with ExistentialQuantification).
If the first list doesn't exist, what would be the type in the blank of map V :: ??? -> [V]? What type mechanism enforces the existence of the wrapper?
Your understanding is not right. A big part of the problem is that the traditional existential quantification syntax you've used is pretty confusing to anyone who isn't thoroughly familiar with it. I therefore strongly recommend that you use GADT syntax instead, which also has the benefit of being strictly more powerful. The easy thing to do is just to enable {-# LANGUAGE GADTs #-}. While we're at it, let's turn on {-# LANGUAGE ScopedTypeVariables #-}, because I hate wondering what forall means in any given spot. Your V definition means exactly the same thing as
data V where
V :: forall a . Show a => a -> V
We can actually drop the explicit forall if we like:
data V where
V :: Show a => a -> V
So the V data constructor is a function that takes something of any showable type and produces something of type V. The type of map is pretty restrictive:
map :: (a -> b) -> [a] -> [b]
All the elements of the list passed to map have to have the same type. So the type of map V is just
map V :: Show a => [a] -> [V]
Let's get back to your first expression now:
[1, "a"] :: [forall a. Show a => a]
Now what this actually says is that [1, "a"] is a list, each of whose elements has type forall a . Show a => a. That is, if I provide any a that's an instance of Show, each element of the list should have that type. This is simply not true. "a" does not, for example, have type Bool. There's yet another problem here; the type [forall a . Show a => a] is "impredicative". I don't understand the details of what that means, but loosely speaking you've stuck a forall in the argument of a type constructor other than ->, and that's not allowed. GHC might suggest that you enable the ImpredicativeTypes extension, but this really doesn't work right, so you shouldn't. If you want a list of existentially quantified things, you need to wrap them up first in existential datatypes or use a specialized existential list type. If you want a list of universally quantified things, you need to wrap them up first (probably in newtypes).