TypeVariableScope

In Standard ML, every type variable is scoped (or bound) at a particular point in the program. A type variable can be either implicitly scoped or explicitly scoped. For example, 'a is implicitly scoped in

val id: 'a -> 'a = fn x => x

and is implicitly scoped in

val id = fn x: 'a => x

On the other hand, 'a is explicitly scoped in

val 'a id: 'a -> 'a = fn x => x

and is explicitly scoped in

val 'a id = fn x: 'a => x

A type variable can be scoped at a val or fun declaration. An SML type checker performs scope inference on each top-level declaration to determine the scope of each implicitly scoped type variable. After scope inference, every type variable is scoped at exactly one enclosing val or fun declaration. Scope inference shows that the first and second example above are equivalent to the third and fourth example, respectively.

Section 4.6 of the Definition specifies precisely the scope of an implicitly scoped type variable. A free occurrence of a type variable 'a in a declaration d is said to be unguarded in d if 'a is not part of a smaller declaration. A type variable 'a is implicitly scoped at d if 'a is unguarded in d and 'a does not occur unguarded in any declaration containing d.

Scope inference examples

In this example,
```
val id: 'a -> 'a = fn x => x
```
'a is unguarded in val id and does not occur unguarded in any containing declaration. Hence, 'a is scoped at val id and the declaration is equivalent to the following.
```
val 'a id: 'a -> 'a = fn x => x
```
In this example,
```
 val f = fn x => let exception E of 'a in E x end
```
'a is unguarded in val f and does not occur unguarded in any containing declaration. Hence, 'a is scoped at val f and the declaration is equivalent to the following.
```
val 'a f = fn x => let exception E of 'a in E x end
```
In this example (taken from the Definition),
```
val x: int -> int = let val id: 'a -> 'a = fn z => z in id id end
```
'a occurs unguarded in val id, but not in val x. Hence, 'a is implicitly scoped at val id, and the declaration is equivalent to the following.
```
val x: int -> int = let val 'a id: 'a -> 'a = fn z => z in id id end
```
In this example,
```
val f = (fn x: 'a => x) (fn y => y)
```
'a occurs unguarded in val f and does not occur unguarded in any containing declaration. Hence, 'a is implicitly scoped at val f, and the declaration is equivalent to the following.
```
val 'a f = (fn x: 'a => x) (fn y => y)
```
This does not type check due to the ValueRestriction.
In this example,
```
fun f x =
  let
    fun g (y: 'a) = if true then x else y
  in
    g x
  end
```
'a occurs unguarded in fun g, not in fun f. Hence, 'a is implicitly scoped at fun g, and the declaration is equivalent to
```
fun f x =
  let
    fun 'a g (y: 'a) = if true then x else y
  in
    g x
  end
```
This fails to type check because x and y must have the same type, but the x occurs outside the scope of the type variable 'a. MLton reports the following error.
```
Error: z.sml 3.21-3.41.
  Then and else branches disagree.
    then: [???]
    else: ['a]
    in: if true then x else y
    note: type would escape its scope: 'a
    escape to: z.sml 1.1-6.5
```
This problem could be fixed either by adding an explicit type constraint, as in fun f (x: 'a), or by explicitly scoping 'a, as in fun 'a f x = ....

Restrictions on type variable scope

It is not allowed to scope a type variable within a declaration in which it is already in scope (see the last restriction listed on page 9 of the Definition). For example, the following program is invalid.

fun 'a f (x: 'a) =
   let
      fun 'a g (y: 'a) = y
   in
      ()
   end

MLton reports the following error.

Error: z.sml 3.11-3.12.
  Type variable scoped at an outer declaration: 'a.
    scoped at: z.sml 1.1-6.6

This is an error even if the scoping is implicit. That is, the following program is invalid as well.

fun f (x: 'a) =
   let
      fun 'a g (y: 'a) = y
   in
      ()
   end