[Haskell-cafe] Non-existing types in existential quantification?

[Christopher Done]

On 1 October 2010 15:27, Henning Thielemann
<lemming at henning-thielemann.de> wrote:
>
> Given the following code, that is accepted by GHC:
>
>> data Exist = forall a. Exist a
>>
>> exist :: Exist
>> exist = Exist undefined
>
> What type has the 'undefined' ?

I think its type is `a'.
>
> So far I assumed that at runtime all objects have a concrete type. This
> seems not to be true.

Consider the following program:

main = putStrLn $ show $ length [undefined :: a,undefined :: b]

A concrete type of the element in list doesn't need to be determined
at runtime, or any time. a unifies with b, and that unifies with x in
length :: [x] -> Int.