Why is `[1, "a"] :: [forall a. Show a => a]` not allowed?

Question

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?

Answer 1

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).