Scoped type variables

[Ross Paterson]

On Wed, Feb 08, 2006 at 11:19:41AM -0000, Simon Peyton-Jones wrote:
> I agree with the "simplest thing" plan.  But if HPrime is to include
> existentials, we MUST have a way to name the type variables they bind,
> otherwise we can't write signatures that involve them.  Stephanie and
> Dimitrios and I are working on this scheme:
> [...]
>    b) A pattern type signature may bring into scope a skolem bound
> 	in the same pattern:
> 		data T where
> 		  MkT :: a -> (a->Int) -> T
> 		f (MkT (x::a) f) = ...
> 
> 	The skolem bound by MkT can be bound *only* in the patterns that
> 	are the arguments to MkT (i.e. pretty much right away).

I see -- my scheme was overly simple.  But this too feels unsatisfactory.
What if we want to give signatures for both arguments?  Will the a's
be the same?