lexically-scoped type variables in GHC 6.6

[Brian Hulley]

Brian Hulley wrote:
> Ross Paterson wrote:
>> data T = forall a. MkT [a]
>>
>> k :: T -> T
>> k (forall a. MkT [t]) = MkT t3
>> where
>> t3::[a] = [t,t,t]
>
> What was wrong with the example in the documentation?
>
>  k :: T -> T
>  k (MkT [t::a]) = MkT t3
>                 where
>                   t3::[a] = [t,t,t]
>
> The type of (t) is (a) - what could possibly be simpler?
>
> No doubt I'm missing something because the docs then go on to say "If
> this seems a little odd..." - but it doesn't. It makes perfect sense.
> Why shouldn't a pattern type signature introduce a scoped type
> variable? It also has the advantage that you can see what the type
> variable is supposed to represent without having to track down the
> original data declaration.

If the problem is that pattern type signatures normally have an implicit 
forall (which stops them introducing lexically scoped type variables), 
perhaps the implicit forall could be discarded so that any type variables in 
a pattern signature not in the scope of an *explicit* forall would be 
lexically scoped over the whole of an equation (or the guarded part if they 
occur first in the guard) eg:

    foo (f :: a -> b) (x:: a) = ((f x) :: b)

meaning:

    forall a b. (foo (f :: a -> b) (x :: a) = ((f x) :: b))

and

    foo (f :: forall a. a-> b) x = ((f x) :: b)

meaning:

    forall b. (foo (f :: forall a. a-> b) x = ((f x) :: b))

Apologies if I'm still missing what the real problem is,
Brian.