Strange error in show for datatype

[Daan Leijen]

Simon Peyton-Jones wrote:
> Consider:
> 
> data T a = T1 Int | T2 a
> 
> It's clear that (T1 Int) has no a's in it, not even bottom.  Mark Shields
> and ruminated in the corridor about a kind system to make this apparent.
> That is, T1 would have type
> 
> T1 :: forall a::Pure .  Int -> T a
> 
> Then if we see (forall a::Pure. Show a => <type>)
> we're justified in fixing a to Empty.   

I think that even with this kind system, we can't fix it 'a' to Empty. 
For example, the empty list constructor would get type:

[] :: forall (a::Pure) . [a]

and as Koen showed, we still can't fix the 'a' to Empty.

-- Daan.