Scoped type variables

Simon Peyton-Jones simonpj at
Wed Feb 8 12:48:24 EST 2006

| >    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
| What if we want to give signatures for both arguments?  Will the a's
| be the same?


	f (MkT (x::a) (f::a->Int)) = ...

You can imagine that either (a) both bind 'a' to the skolem, but must do
consistently; or (b) that (x::a) binds 'a', and (f::a->Int) is a bound
occurrence.  It doesn't matter which you choose, I think.


More information about the Haskell-prime mailing list