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?