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
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
|
# module Exp :
sig
type _ t =
IntLit : int -> int t
| BoolLit : bool -> bool t
| Pair : 'a t * 'b t -> ('a * 'b) t
| App : ('a -> 'b) t * 'a t -> 'b t
| Abs : ('a -> 'b) -> ('a -> 'b) t
val eval : 's t -> 's
val discern : 'a t -> int
end
# module List :
sig
type zero
type _ t = Nil : zero t | Cons : 'a * 'b t -> ('a * 'b) t
val head : ('a * 'b) t -> 'a
val tail : ('a * 'b) t -> 'b t
val length : 'a t -> int
end
# Characters 206-227:
......function
| C2 x -> x
Warning 8: this pattern-matching is not exhaustive.
Here is an example of a value that is not matched:
C1 _
Characters 469-526:
......function
| Foo _ , Foo _ -> true
| Bar _, Bar _ -> true
Warning 8: this pattern-matching is not exhaustive.
Here is an example of a value that is not matched:
(Bar _, Foo _)
module Nonexhaustive :
sig
type 'a u = C1 : int -> int u | C2 : bool -> bool u
type 'a v = C1 : int -> int v
val unexhaustive : 's u -> 's
module M : sig type t type u end
type 'a t = Foo : M.t -> M.t t | Bar : M.u -> M.u t
val same_type : 's t * 's t -> bool
end
# module Exhaustive :
sig
type t = int
type u = bool
type 'a v = Foo : t -> t v | Bar : u -> u v
val same_type : 's v * 's v -> bool
end
# Characters 119-120:
let eval (D x) = x
^
Error: This expression has type ex#16 t
but an expression was expected of type ex#16 t
The type constructor ex#16 would escape its scope
# Characters 157-158:
C ->
^
Error: Recursive local constraint when unifying (s, s) t with (s, s * s) t
# Characters 174-182:
| (IntLit _ | BoolLit _) -> ()
^^^^^^^^
Error: This pattern matches values of type int t
but a pattern was expected which matches values of type s t
# Characters 213-226:
| `A, BoolLit _ -> ()
^^^^^^^^^^^^^
Error: This pattern matches values of type ([? `A ] as 'a) * bool t
but a pattern was expected which matches values of type 'a * int t
# module Propagation :
sig
type _ t = IntLit : int -> int t | BoolLit : bool -> bool t
val check : 's t -> 's
end
# Characters 87-88:
let f = function A -> 1 | B -> 2
^
Error: This pattern matches values of type b
but a pattern was expected which matches values of type a
# type _ t = Int : int t
# val ky : 'a -> 'a -> 'a = <fun>
# val test : 'a t -> 'a = <fun>
# val test : 'a t -> int = <fun>
# Characters 49-61:
function Int -> ky (1 : a) 1 (* fails *)
^^^^^^^^^^^^
Error: This expression has type a = int
but an expression was expected of type a = int
This instance of int is ambiguous:
it would escape the scope of its equation
# Characters 70-82:
let r = match x with Int -> ky (1 : a) 1 (* fails *)
^^^^^^^^^^^^
Error: This expression has type a = int
but an expression was expected of type a = int
This instance of int is ambiguous:
it would escape the scope of its equation
# Characters 69-81:
let r = match x with Int -> ky 1 (1 : a) (* fails *)
^^^^^^^^^^^^
Error: This expression has type a = int
but an expression was expected of type a = int
This instance of int is ambiguous:
it would escape the scope of its equation
# val test : 'a t -> int = <fun>
# val test : 'a t -> 'a = <fun>
# val test : 'a t -> int = <fun>
# val test : 'a t -> 'a = <fun>
# val test2 : 'a t -> 'a option = <fun>
# val test2 : 'a t -> 'a option = <fun>
# val test2 : 'a t -> 'a option = <fun>
# Characters 152-154:
begin match x with Int -> u := Some 1; r := !u end;
^^
Error: This expression has type int option
but an expression was expected of type a option
Type int is not compatible with type a = int
This instance of int is ambiguous:
it would escape the scope of its equation
# val test2 : 'a t -> 'a option = <fun>
# val test2 : 'a t -> 'a option = <fun>
# Characters 100-101:
match v with Int -> let y = either 1 x in y
^
Error: This expression has type a = int
but an expression was expected of type a = int
This instance of int is ambiguous:
it would escape the scope of its equation
# val f : 'a t -> 'a -> 'a = <fun>
# val f : 'a t -> 'a -> 'a = <fun>
# val f : 'a t -> 'a -> 'a = <fun>
# val f : 'a t -> 'a -> 'a = <fun>
# val f : 'a t -> 'a -> 'a = <fun>
# Characters 136-137:
let module M = struct type b = a let z = (y : b) end
^
Error: This expression has type a = int
but an expression was expected of type b = int
This instance of int is ambiguous:
it would escape the scope of its equation
# val f : 'a t -> int -> int = <fun>
# type _ h = Has_m : < m : int > h | Has_b : < b : bool > h
val f : 'a h -> 'a = <fun>
# type _ j = Has_A : [ `A of int ] j | Has_B : [ `B of bool ] j
val f : 'a j -> 'a = <fun>
# type (_, _) eq = Eq : ('a, 'a) eq
# Characters 5-91:
....f : type a b. (a,b) eq -> (<m : a; ..> as 'c) -> (<m : b; ..> as 'c) =
fun Eq o -> o
Error: The universal type variable 'b cannot be generalized:
it is already bound to another variable.
# Characters 74-75:
fun Eq o -> o
^
Error: This expression has type < m : a; .. >
but an expression was expected of type < m : b; .. >
Type a is not compatible with type b = a
This instance of a is ambiguous:
it would escape the scope of its equation
# Characters 97-98:
match eq with Eq -> o ;; (* should fail *)
^
Error: This expression has type < m : a; .. >
but an expression was expected of type < m : b; .. >
Type a is not compatible with type b = a
This instance of a is ambiguous:
it would escape the scope of its equation
# val f : ('a, 'b) eq -> < m : 'a > -> < m : 'b > = <fun>
# val int_of_bool : (bool, int) eq = Eq
# val x : < m : bool > = <obj>
# val y : < m : bool > * < m : int > = (<obj>, <obj>)
# val f : ('a, int) eq -> < m : 'a > -> bool = <fun>
# val f : ('a, 'b) eq -> < m : 'a > -> < m : 'b > = <fun>
# Characters 118-119:
let r : < m : b > = match eq with Eq -> o in (* fail *)
^
Error: This expression has type < m : a; .. >
but an expression was expected of type < m : b >
Type a is not compatible with type b = a
This instance of a is ambiguous:
it would escape the scope of its equation
# Characters 74-75:
fun Eq o -> o ;; (* fail *)
^
Error: This expression has type [> `A of a ]
but an expression was expected of type [> `A of b ]
Type a is not compatible with type b = a
This instance of a is ambiguous:
it would escape the scope of its equation
# Characters 97-98:
match eq with Eq -> v ;; (* should fail *)
^
Error: This expression has type [> `A of a ]
but an expression was expected of type [> `A of b ]
Type a is not compatible with type b = a
This instance of a is ambiguous:
it would escape the scope of its equation
# Characters 5-85:
....f : type a b. (a,b) eq -> [< `A of a | `B] -> [< `A of b | `B] =
fun Eq o -> o..............
Error: This definition has type
('a, 'b) eq -> ([< `A of 'b & 'a | `B ] as 'c) -> 'c
which is less general than 'a0 'b0. ('a0, 'b0) eq -> 'c -> 'c
# val f : ('a, 'b) eq -> [ `A of 'a | `B ] -> [ `A of 'b | `B ] = <fun>
# val f : ('a, int) eq -> [ `A of 'a ] -> bool = <fun>
# val f : ('a, 'b) eq -> [ `A of 'a | `B ] -> [ `A of 'b | `B ] = <fun>
# Characters 131-132:
let r : [`A of b | `B] = match eq with Eq -> o in (* fail *)
^
Error: This expression has type [> `A of a | `B ]
but an expression was expected of type [ `A of b | `B ]
Type a is not compatible with type b = a
This instance of a is ambiguous:
it would escape the scope of its equation
# type 'a t = A of int | B of bool | C of float | D of 'a
type _ ty =
TE : 'a ty -> 'a array ty
| TA : int ty
| TB : bool ty
| TC : float ty
| TD : string -> bool ty
val f : 'a ty -> 'a t -> int = <fun>
# Characters 51-202:
..match x, y with
| _, A z -> z
| _, B z -> if z then 1 else 2
| _, C z -> truncate z
| TE TC, D [|1.0|] -> 14
| TA, D 0 -> -1
| TA, D z -> z
Warning 8: this pattern-matching is not exhaustive.
Here is an example of a value that is not matched:
(TE TC, D [| |])
val f : 'a ty -> 'a t -> int = <fun>
# Characters 147-154:
| D [|1.0|], TE TC -> 14
^^^^^^^
Error: This pattern matches values of type 'a array
but a pattern was expected which matches values of type a
# Characters 259-266:
| {left=TE TC; right=D [|1.0|]} -> 14
^^^^^^^
Error: This pattern matches values of type 'a array
but a pattern was expected which matches values of type a
# Characters 92-334:
..match {left=x; right=y} with
| {left=_; right=A z} -> z
| {left=_; right=B z} -> if z then 1 else 2
| {left=_; right=C z} -> truncate z
| {left=TE TC; right=D [|1.0|]} -> 14
| {left=TA; right=D 0} -> -1
| {left=TA; right=D z} -> z
Warning 8: this pattern-matching is not exhaustive.
Here is an example of a value that is not matched:
{left=TE TC; right=D [| |]}
type ('a, 'b) pair = { left : 'a; right : 'b; }
val f : 'a ty -> 'a t -> int = <fun>
# module M : sig type 'a t val eq : ('a t, 'b t) eq end
# Characters 69-71:
function Eq -> Eq (* fail *)
^^
Error: This expression has type (a, a) eq
but an expression was expected of type (a, b) eq
# val f : ('a M.t * 'a, 'b M.t * 'b) eq -> ('a, 'b) eq = <fun>
# val f : ('a * 'a M.t, 'b * 'b M.t) eq -> ('a, 'b) eq = <fun>
# type _ t = V1 : [ `A | `B ] t | V2 : [ `C | `D ] t
val f : 'a t -> 'a = <fun>
# - : [ `A | `B ] = `A
# type _ int_foo = IF_constr : < foo : int; .. > int_foo
type _ int_bar = IB_constr : < bar : int; .. > int_bar
# Characters 98-99:
(x:<foo:int>)
^
Error: This expression has type t = < foo : int; .. >
but an expression was expected of type < foo : int >
Type ex#20 = < bar : int; .. > is not compatible with type < >
The second object type has no method bar
# Characters 98-99:
(x:<foo:int;bar:int>)
^
Error: This expression has type t = < foo : int; .. >
but an expression was expected of type < bar : int; foo : int >
Type ex#22 = < bar : int; .. > is not compatible with type
< bar : int >
# Characters 98-99:
(x:<foo:int;bar:int;..>)
^
Error: This expression has type < bar : int; foo : int; .. > as 'a
but an expression was expected of type 'a
The type constructor ex#25 would escape its scope
# val g : 'a -> 'a int_foo -> 'a int_bar -> 'a = <fun>
# val g : 'a -> 'a int_foo -> 'a int_bar -> 'a * int * int = <fun>
# type 'a ty = Int : int -> int ty
# val f : 'a ty -> 'a = <fun>
# val g : 'a ty -> 'a = <fun>
#
|
