summaryrefslogtreecommitdiff
path: root/testsuite/tests/typing-gadts/nested_equations.ml
blob: 4a9173c0393c5eb681602038e9c387a332cc5440 (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
90
91
92
(* TEST
 expect;
*)

(* Tests for nested equations (bind abstract types from other modules) *)

type _ t = Int : int t;;

let to_int (type a) (w : a t) (x : a) : int = let Int = w in x;;
[%%expect{|
type _ t = Int : int t
val to_int : 'a t -> 'a -> int = <fun>
|}];;

let w_bool : bool t = Obj.magic 0;;
let f_bool (x : bool) : int = let Int = w_bool in x;; (* fail *)
[%%expect{|
val w_bool : bool t = Int
Line 2, characters 34-37:
2 | let f_bool (x : bool) : int = let Int = w_bool in x;; (* fail *)
                                      ^^^
Error: This pattern matches values of type int t
       but a pattern was expected which matches values of type bool t
       Type int is not compatible with type bool
|}];;

let w_buffer : Buffer.t t = Obj.magic 0;;
let f_buffer (x : Buffer.t) : int = let Int = w_buffer in x;; (* ok *)
[%%expect{|
val w_buffer : Buffer.t t = Int
val f_buffer : Buffer.t -> int = <fun>
|}];;

let w_spec : Arg.spec t = Obj.magic 0;;
let f_spec (x : Arg.spec) : int = let Int = w_spec in x;; (* fail *)
[%%expect{|
val w_spec : Arg.spec t = Int
Line 2, characters 38-41:
2 | let f_spec (x : Arg.spec) : int = let Int = w_spec in x;; (* fail *)
                                          ^^^
Error: This pattern matches values of type int t
       but a pattern was expected which matches values of type Arg.spec t
       Type int is not compatible with type Arg.spec
|}];;

module M : sig type u val w : u t val x : u end =
  struct type u = int let w = Int let x = 33 end;;
let m_x : int = let Int = M.w in M.x;;
[%%expect{|
module M : sig type u val w : u t val x : u end
val m_x : int = 33
|}];;

module F (X : sig type u = int val x : u end) = struct let x : int = X.x end;;
let fm_x : int = let Int = M.w in let module FM = F(M) in FM.x;; (* ok *)
[%%expect{|
module F :
  functor (X : sig type u = int val x : u end) -> sig val x : int end
val fm_x : int = 33
|}];;

module M' = struct module M : sig type u val w : u t val x : u end = M end;;
module F' (X : sig module M : sig type u = int val x : u end end) =
  struct let x : int = X.M.x end;;
let fm'_x : int =
  let Int = M'.M.w in let module FM' = F'(M') in FM'.x;; (* ok *)
[%%expect{|
module M' : sig module M : sig type u val w : u t val x : u end end
module F' :
  functor (X : sig module M : sig type u = int val x : u end end) ->
    sig val x : int end
val fm'_x : int = 33
|}];;

(* PR#7233 *)

type (_, _) eq = Refl : ('a, 'a) eq

module type S = sig
  type t
  val eql : (t, int) eq
end

module F (M : S) = struct
  let zero : M.t =
    let Refl = M.eql in 0
end;;
[%%expect{|
type (_, _) eq = Refl : ('a, 'a) eq
module type S = sig type t val eql : (t, int) eq end
module F : functor (M : S) -> sig val zero : M.t end
|}];;