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
|
(* TEST
* expect
*)
(* Optional binders can be used in value declarations,
and signatures are equivalent with or without them. *)
module type Id1 = sig val id : 'a -> 'a end
module type Id2 = sig val id : 'a . 'a -> 'a end
module F (X : Id1) : Id2 = X
module G (X : Id2) : Id1 = X
module Id : Id2 = struct let id x = x end
[%%expect{|
module type Id1 = sig val id : 'a -> 'a end
module type Id2 = sig val id : 'a -> 'a end
module F : functor (X : Id1) -> Id2
module G : functor (X : Id2) -> Id1
module Id : Id2
|}]
(* If present, the variables must be universally quantified *)
type 'a constrained = string constraint 'a = int
module type Ok_constraint = sig val c : 'a constrained end
[%%expect{|
type 'a constrained = string constraint 'a = int
module type Ok_constraint = sig val c : int constrained end
|}]
module type Bad_constraint = sig val c : 'a . 'a constrained end
[%%expect{|
Line 1, characters 41-60:
1 | module type Bad_constraint = sig val c : 'a . 'a constrained end
^^^^^^^^^^^^^^^^^^^
Error: The universal type variable 'a cannot be generalized: it is bound to
int.
|}]
(* with the usual caveat for row variables *)
module type Row = sig val poly : 'a 'b . ([> `Foo of int] as 'a) * 'b end
module type NotRow = sig val poly : 'a 'b . (int as 'a) * 'b end
[%%expect{|
module type Row = sig val poly : [> `Foo of int ] * 'b end
Line 2, characters 36-60:
2 | module type NotRow = sig val poly : 'a 'b . (int as 'a) * 'b end
^^^^^^^^^^^^^^^^^^^^^^^^
Error: The universal type variable 'a cannot be generalized: it is bound to
int.
|}]
(* If present, the quantifier must quantify all variables *)
module type F1 = sig
val four : 'a 'b 'c 'd . 'a -> 'b -> 'c -> 'd -> 'a * 'b * 'c * 'd
end
[%%expect{|
module type F1 = sig val four : 'a -> 'b -> 'c -> 'd -> 'a * 'b * 'c * 'd end
|}]
;;
module type F2 = sig
val four : 'a 'b 'd . 'a -> 'b -> 'c -> 'd -> 'a * 'b * 'c * 'd
end
[%%expect{|
Line 2, characters 36-38:
2 | val four : 'a 'b 'd . 'a -> 'b -> 'c -> 'd -> 'a * 'b * 'c * 'd
^^
Error: The type variable 'c is unbound in this type declaration.
|}]
(* Explicit quantifiers may also be used in external definitions *)
module Ident : sig
external identity : 'a . 'a -> 'a = "%identity"
end = struct
external identity : 'a . 'a -> 'a = "%identity"
end
[%%expect{|
module Ident : sig external identity : 'a -> 'a = "%identity" end
|}]
(* Explicit quantifiers may also be used in GADTs *)
type g1 = Foo : 'a * ('a -> unit) -> g1
type g2 = g1 = Foo : 'a . 'a * ('a -> unit) -> g2
type g3 = g2 = Foo : 'b 'c 'd . 'd * ('d -> unit) -> g3
let intro = Foo (5, print_int)
let elim (Foo (x, f)) = f x
[%%expect{|
type g1 = Foo : 'a * ('a -> unit) -> g1
type g2 = g1 = Foo : 'a * ('a -> unit) -> g2
type g3 = g2 = Foo : 'd * ('d -> unit) -> g3
val intro : g3 = Foo (<poly>, <fun>)
val elim : g3 -> unit = <fun>
|}]
(* In GADT syntax, all type variables must be bound, even parameters *)
type 'a t =
| Ok1 : 'b 'a . 'a -> 'a t
| Ok2 of 'a
| Bad : 'b . 'a -> 'a t
[%%expect{|
Line 4, characters 15-17:
4 | | Bad : 'b . 'a -> 'a t
^^
Error: The type variable 'a is unbound in this type declaration.
|}]
|
