1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
|
(* TEST
expect;
*)
type t = < x : 'a. int as 'a >
[%%expect {|
Line 1, characters 15-28:
1 | type t = < x : 'a. int as 'a >
^^^^^^^^^^^^^
Error: The universal type variable "'a" cannot be generalized: it is bound to
"int".
|}]
type u = < x : 'a 'b. 'a as 'b >
[%%expect {|
Line 1, characters 15-30:
1 | type u = < x : 'a 'b. 'a as 'b >
^^^^^^^^^^^^^^^
Error: The universal type variable "'b" cannot be generalized:
it is already bound to another variable.
|}]
type v = 'b -> < x : 'a. 'b as 'a >
[%%expect {|
Line 1, characters 21-33:
1 | type v = 'b -> < x : 'a. 'b as 'a >
^^^^^^^^^^^^
Error: The universal type variable "'a" cannot be generalized:
it escapes its scope.
|}]
(** Check that renaming universal type variable is properly tracked
in printtyp *)
let f (x:<a:'a; b:'a. 'a>) (y:<a:'a;b:'a>) = x = y
[%%expect {|
Line 4, characters 49-50:
4 | let f (x:<a:'a; b:'a. 'a>) (y:<a:'a;b:'a>) = x = y
^
Error: The value "y" has type "< a : 'a; b : 'a >"
but an expression was expected of type "< a : 'a; b : 'a0. 'a0 >"
The method "b" has type "'a", but the expected method type was "'a0. 'a0"
The universal variable "'a0" would escape its scope
|}]
(** MPR 7565 *)
class type t_a = object
method f: 'a. 'a -> int
end
let f (o:t_a) = o # f 0
let _ = f (object
method f _ = 0
end);;
[%%expect {|
class type t_a = object method f : 'a -> int end
val f : t_a -> int = <fun>
Lines 5-7, characters 10-5:
5 | ..........(object
6 | method f _ = 0
7 | end)..
Error: This expression has type "< f : 'a -> int >"
but an expression was expected of type "t_a"
The method "f" has type "'a -> int", but the expected method type was
"'a0. 'a0 -> int"
The universal variable "'a0" would escape its scope
|}
]
type uv = [ `A of <f: 'a. 'a -> int > ]
type 'a v = [ `A of <f: 'a -> int > ]
let f (`A o:uv) = o # f 0
let () = f ( `A (object method f _ = 0 end): _ v);;
[%%expect {|
type uv = [ `A of < f : 'a. 'a -> int > ]
type 'a v = [ `A of < f : 'a -> int > ]
val f : uv -> int = <fun>
Line 4, characters 11-49:
4 | let () = f ( `A (object method f _ = 0 end): _ v);;
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: This expression has type "'a v" but an expression was expected of type
"uv"
The method "f" has type "'a -> int", but the expected method type was
"'a0. 'a0 -> int"
The universal variable "'a0" would escape its scope
|}]
(* Issue #8702: row types unified with universally quantified types*)
let f: 'a. ([> `A ] as 'a) -> [ `A ] = fun x -> x
[%%expect {|
Line 1, characters 48-49:
1 | let f: 'a. ([> `A ] as 'a) -> [ `A ] = fun x -> x
^
Error: The value "x" has type "[> `A ]" but an expression was expected of type
"[ `A ]"
The first variant type is bound to the universal type variable "'a",
it cannot be closed
|}]
let f: 'a. [ `A ] -> ([> `A ] as 'a) = fun x -> x
[%%expect {|
Line 1, characters 48-49:
1 | let f: 'a. [ `A ] -> ([> `A ] as 'a) = fun x -> x
^
Error: The value "x" has type "[ `A ]" but an expression was expected of type
"[> `A ]"
The second variant type is bound to the universal type variable "'a",
it cannot be closed
|}]
let f: 'a. [ `A | `B ] -> ([> `A ] as 'a) = fun x -> x
[%%expect {|
Line 1, characters 53-54:
1 | let f: 'a. [ `A | `B ] -> ([> `A ] as 'a) = fun x -> x
^
Error: The value "x" has type "[ `A | `B ]"
but an expression was expected of type "[> `A ]"
The second variant type is bound to the universal type variable "'a",
it cannot be closed
|}]
let f: 'a. [> `A | `B | `C ] -> ([> `A ] as 'a) = fun x -> x
[%%expect {|
Line 1, characters 59-60:
1 | let f: 'a. [> `A | `B | `C ] -> ([> `A ] as 'a) = fun x -> x
^
Error: The value "x" has type "[> `A | `B | `C ]"
but an expression was expected of type "[> `A ]"
The second variant type is bound to the universal type variable "'a",
it may not allow the tag(s) "`B", "`C"
|}]
|
