blob: 4bffe1224e69064b63a018c464c4a5a1b87235e8 (
plain)
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
|
(* Report from Jeremy Yallop *)
module F (S : sig type 'a s end) = struct
include S
type _ t = T : 'a -> 'a s t
end;; (* fail *)
(*
module M = F (struct type 'a s = int end) ;;
let M.T x = M.T 3 in x = true;;
*)
(* Fix it using #-annotations *)
module F (S : sig type #'a s end) = struct
include S
type _ t = T : 'a -> 'a s t
end;; (* syntax error *)
(*
module M = F (struct type 'a s = int end) ;; (* fail *)
module M = F (struct type 'a s = new int end) ;; (* ok *)
let M.T x = M.T 3 in x = true;; (* fail *)
let M.T x = M.T 3 in x = 3;; (* ok *)
*)
(* Another version using OCaml 2.00 objects *)
module F(T:sig type 'a t end) = struct
class ['a] c x =
object constraint 'a = 'b T.t val x' : 'b = x method x = x' end
end;; (* fail *)
(* It is not OK to allow modules exported by other compilation units *)
type (_,_) eq = Eq : ('a,'a) eq;;
let eq = Obj.magic Eq;;
(* pretend that Queue.t is not injective *)
let eq : ('a Queue.t, 'b Queue.t) eq = eq;;
type _ t = T : 'a -> 'a Queue.t t;; (* fail *)
(*
let castT (type a) (type b) (x : a t) (e: (a, b) eq) : b t =
let Eq = e in (x : b t);;
let T (x : bool) = castT (T 3) eq;; (* we found a contradiction *)
*)
(* The following signature should not be accepted *)
module type S = sig
type 'a s
type _ t = T : 'a -> 'a s t
end;; (* fail *)
(* Otherwise we can write the following *)
module rec M : (S with type 'a s = unit) = M;;
(* For the above reason, we cannot allow the abstract declaration
of s and the definition of t to be in the same module, as
we could create the signature using [module type of ...] *)
(* Another problem with variance *)
module M = struct type 'a t = 'a -> unit end;;
module F(X:sig type #'a t end) =
struct type +'a s = S of 'b constraint 'a = 'b X.t end;; (* fail *)
(*
module N = F(M);;
let o = N.S (object end);;
let N.S o' = (o :> <m : int> M.t N.s);; (* unsound! *)
*)
(* And yet another *)
type 'a q = Q;;
type +'a t = 'b constraint 'a = 'b q;;
(* shoud fail: we do not know for sure the variance of Queue.t *)
type +'a t = T of 'a;;
type +'a s = 'b constraint 'a = 'b t;; (* ok *)
type -'a s = 'b constraint 'a = 'b t;; (* fail *)
type +'a u = 'a t;;
type 'a t = T of ('a -> 'a);;
type -'a s = 'b constraint 'a = 'b t;; (* ok *)
type +'a s = 'b constraint 'a = 'b q t;; (* ok *)
type +'a s = 'b constraint 'a = 'b t q;; (* fail *)
(* the problem from lablgtk2 *)
module Gobject = struct
type -'a obj
end
open Gobject;;
class virtual ['a] item_container =
object
constraint 'a = < as_item : [>`widget] obj; .. >
method virtual add : 'a -> unit
end;;
|
