This is the message that Marcin referred to, proposing a change in the semantics of scoped type variables. I may just go ahead and implement it in GHC. (The implementation is easy: delete a couple of lines; and I guess the same is so for Hugs. The question is whether it's a desirable change.) Simon -----Original Message----- From: Simon Peyton-Jones Sent: 08 February 2001 02:32 Cc: Simon Peyton-Jones; qrczak@knm.org.pl Subject: Scoped type variables Dear Huggy people | But for pattern and result type signatures changing the rules makes | sense. | f (x::a) = ... | does not mean that x has type "forall a. a" anyway. It should actually | only give the type a name, no matter what it is. | | Similarly, | f (x :: (a,b)) = ... | should unify the appropriate type variable with (,), and give names to | monomorphic arguments of (,) used in the call we are in. I must say that I agree with Marcin's point. When we write f x = e we mean that x is a name for whatever argument f is given. Marcin argues that the same should apply for f (x :: (a,b)) = e Namely, that x is a name for the argument, a is a name for the type of the fst of x, and slly b. Arguments in favour: - It's more like term-variable pattern matching - In the present system, saying (x::a) doesn't mean x's type is really universally quantified -- it may have a type constraint. And there's really a continuum between saying forall a. C a => t[a] and t[Int] because the Int amounts to a rather strong constraint on a. Indeed, when we have functional dependencies, forall a. C Int a => t[a] may indeed be the same as C Int Int => t[Int] - It's simpler; less to explain to the programmer (quite a bit of the GHC documentation on this stuff is to explain what about the universal quantification) Arguments against - It's not what GHC and Hugs do now. It would be an easy change to make, but I'd prefer it if GHC and Hugs stayed in sync over this (modulo release schedules), so I'd be interested in your views. Simon Someone (Jeff?) wrote: | Could you clarify what you are proposing? Is it | something like "let me name that type `a' even tho I know | it's really something more specific"? (i.e. similar to the | current hugs extension, but without the "can't be more | specific than inferred" restriction) Exactly so. For example f (x::a) = let y::a = x+1 in h x y would be legal even if h :: Int -> Int -> Int The point is that 'a' simply names the type of x, even if that type isn't a type variable.