| 1 | (* This example is interesting because at the time of generalization of f, the |
| 2 | * tyvar 'a is in scope, but does not appear in type types of any of the |
| 3 | * variables in the environment (x's type has not yet been determined to be 'a). |
| 4 | * Nevertheless, it is essential to not generalize 'a at g |
| 5 | *) |
| 6 | val 'a f = fn x => |
| 7 | let |
| 8 | exception E of 'a |
| 9 | fun g (E y) = y |
| 10 | | g _ = raise Fail "bug" |
| 11 | in |
| 12 | E x |
| 13 | end |
| 14 | |
| 15 | (* This example is interesting because it binds a type variable at a scope where |
| 16 | * the type variable does not appear in the type. Nevertheless, it is essential |
| 17 | * to keep the type variable there, because it occurs in an inner scope. |
| 18 | *) |
| 19 | fun 'a f () = |
| 20 | let |
| 21 | val x: 'a = raise Fail "bug" |
| 22 | in |
| 23 | () |
| 24 | end |
| 25 | |
| 26 | (* This example shows that type variables can be rebound in nested datatype |
| 27 | * declarations, unlike the situation for nested value declarations. |
| 28 | *) |
| 29 | val 'a x = |
| 30 | fn () => |
| 31 | let |
| 32 | datatype 'a t = T of 'a |
| 33 | in |
| 34 | () |
| 35 | end |
| 36 | |
| 37 | (* This example verifies that datatype replication is allowed, even when the |
| 38 | * right-hand side isn't a datatype. |
| 39 | *) |
| 40 | type 'a t = 'a * 'a |
| 41 | datatype u = datatype t |
| 42 | val _: int u = (13, 14); |
| 43 | |
| 44 | (* The following examples demonstrate acceptable forms of type variable scoping. |
| 45 | *) |
| 46 | fun f (x: 'a) = |
| 47 | let |
| 48 | fun g (y: 'a) = y |
| 49 | in |
| 50 | () |
| 51 | end |
| 52 | |
| 53 | fun f (x: 'a) = |
| 54 | let |
| 55 | fun 'b g (y: 'b) = y |
| 56 | in |
| 57 | () |
| 58 | end |
| 59 | |
| 60 | fun 'a f (x: 'a) = |
| 61 | let |
| 62 | fun g (y: 'a) = y |
| 63 | in |
| 64 | () |
| 65 | end |
| 66 | |
| 67 | fun 'a f (x: 'a) = |
| 68 | let |
| 69 | fun 'b g (y: 'b) = y |
| 70 | in |
| 71 | () |
| 72 | end |
| 73 | |
| 74 | val 'a x = |
| 75 | fn () => |
| 76 | let |
| 77 | datatype 'a t = T of 'a |
| 78 | in |
| 79 | () |
| 80 | end |
| 81 | |
| 82 | (* This example confirms that bools can be used as labels. *) |
| 83 | val {false = x, ...} = {false = 13}; |