List of existentially quantified values in Haskell

Question

I'm wondering why this piece of code doesn't type-check:

{-# LANGUAGE ScopedTypeVariables, Rank2Types, RankNTypes #-}
{-# OPTIONS -fglasgow-exts #-}

module Main where

foo :: [forall a. a]
foo = [1]

ghc complains:

Could not deduce (Num a) from the context ()
  arising from the literal `1' at exist5.hs:7:7

Given that:

Prelude> :t 1
1 :: (Num t) => t
Prelude> 

it seems that the (Num t) context can't match the () context of arg. The point I can't understand is that since () is more general than (Num t), the latter should and inclusion of the former. Has this anything to do with lack of Haskell support for sub-typing?

Thank you for any comment on this.

Answer 1

You're not using existential quantification here. You're using rank N types.

Here [forall a. a] means that every element must have every possible type (not any, every). So [undefined, undefined] would be a valid list of that type and that's basically it.

To expand on that a bit: if a list has type [forall a. a] that means that all the elements have type forall a. a. That means that any function that takes any kind of argument, can take an element of that list as argument. This is no longer true if you put in an element which has a more specific type than forall a. a, so you can't.

To get a list which can contain any type, you need to define your own list type with existential quantification. Like so:

data MyList = Nil | forall a. Cons a MyList
foo :: MyList
foo = Cons 1 Nil

Of course unless you restrain element types to at least instantiate Show, you can't do anything with a list of that type.