7.14. Scoped Type Variables

A pattern type signature can introduce a scoped type variable. For example

f (xs::[a]) = ys ++ ys
              ys :: [a]
              ys = reverse xs

The pattern (xs::[a]) includes a type signature for xs. This brings the type variable a into scope; it scopes over all the patterns and right hand sides for this equation for f. In particular, it is in scope at the type signature for y.

At ordinary type signatures, such as that for ys, any type variables mentioned in the type signature that are not in scope are implicitly universally quantified. (If there are no type variables in scope, all type variables mentioned in the signature are universally quantified, which is just as in Haskell 98.) In this case, since a is in scope, it is not universally quantified, so the type of ys is the same as that of xs. In Haskell 98 it is not possible to declare a type for ys; a major benefit of scoped type variables is that it becomes possible to do so.

Scoped type variables are implemented in both GHC and Hugs. Where the implementations differ from the specification below, those differences are noted.

So much for the basic idea. Here are the details.

7.14.1. Scope and implicit quantification

7.14.2. Polymorphism

7.14.3. Result type signatures

Result type signatures are not yet implemented in Hugs.

7.14.4. Pattern signatures on other constructs

Such degnerate function bindings do not fall under the monomorphism restriction. Thus:

  g :: a -> a -> Bool = \x y. x==y

Here g has type forall a. Eq a => a -> a -> Bool, just as if g had a separate type signature. Lacking a type signature, g would get a monomorphic type.

7.14.5. Existentials