Commit | Line | Data |
---|---|---|
7f918cf1 CE |
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}; |