I sometimes come across a situation when I only want to provide a _partial_ type annotation, perhaps because the full type has some variable unified with some variable in some other type annotation, or something. For instance: f :: forall a. [a] -> [a] -> [a] f x y = g x where g [] = y g (_:_) = x ...there doesn't seem to be a way of giving a type annotation for 'g'. Theoretically it's '[a] -> [a]', but where 'a' is the same as the 'a' in the type signature for 'f'. Under this proposal, unqualified type variables would be considered to be 'free' rather than implicitly forall-qualified. So for instance, any function could be given the partial type annotation 'a -> b'. For instance, all these annotations would be the same given this function: k :: a k :: a -> ba k :: a -> b -> a k :: forall b. a -> b -> a k :: forall a b. a -> b -> a k x y = x ...and these would both be the same, but different from the previous: k' :: Int -> ba k' :: forall b. Int -> b -> Int k' x y = x And so we could write this: f :: forall a. [a] -> [a] -> [a] f x y = g x where g :: [a] -> [a] -- partial annotation may be sufficient g [] = y g (_:_) = x I admit that's a bit of a change, and might break programs... In addition, it doesn't address the occasional need to tie type annotations together, something that has often made me add ugly dummy arguments used just for their type. -- Ashley Yakeley, Seattle WA