Adrian Hey wrote: I think all occurences of [] have type forall a. [a] The case expression.. case a of (a':as) -> <expr1> [] -> <expr2> Should be typed as if written.. case a of (a':as) -> let a=(a':as) in <expr1> [] -> let a=[] in <expr2> ---------------------------------------------------- Well, we will have to agree to disagree, I find the current system makes perfect sense, and is easy to reason with. If I want a let binding I can write one. The difference is really this: case a of (a:as) -> <expr1> e -> e In this case e represent 'the same []' as on the left hand side. in the let binding this is a new and fresh '[]'... When I pattern match a variable in a case extression I really expect it to get the type of the case... There are circunstances when I go on to use e, and if it is not grounded by the case expression I will get hit by the monomorphoism restriction, and have to add non haskell98 type annotation to ground 'e'... for example If I pass e to a polymorphic function, it won't know what type e has... case a of (a':as) -> let a=(a':as) in <expr1> [] -> let a=[] in (polyfn a) where polyfn a has a type like polyfna :: Ord a -> [a] -> String Now the above won't work and you will have to do: [] -> let a=[] in (polyfn (a :: [SomeListType])) and of course if you are using generics then how can polyfn get the original type of 'a' in the case expression... for example: polyfn :: Typable a -> [a] -> ShowS polyfn a = shows (typeOf a) then: case a of (a:as) -> <expr1> e -> polyfn e is correct, but: case a of (a':as) -> let a=(a':as) in <expr1> [] -> let a=[] in (polyfn a) does what? Keean.