summaryrefslogtreecommitdiff
path: root/testsuite/tests/typing-gadts/didier.ml
blob: 75062f760893c7a61132ffcf8c292525d3d260d4 (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
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
(* TEST
 expect;
*)

type 'a ty =
  | Int : int ty
  | Bool : bool ty

let fbool (type t) (x : t) (tag : t ty) =
  match tag with
  | Bool -> x
;;
[%%expect{|
type 'a ty = Int : int ty | Bool : bool ty
Lines 6-7, characters 2-13:
6 | ..match tag with
7 |   | Bool -> x
Warning 8 [partial-match]: this pattern-matching is not exhaustive.
Here is an example of a case that is not matched:
Int

val fbool : 't -> 't ty -> 't = <fun>
|}];;
(* val fbool : 'a -> 'a ty -> 'a = <fun> *)
(** OK: the return value is x of type t **)

let fint (type t) (x : t) (tag : t ty) =
  match tag with
  | Int -> x > 0
;;
[%%expect{|
Lines 2-3, characters 2-16:
2 | ..match tag with
3 |   | Int -> x > 0
Warning 8 [partial-match]: this pattern-matching is not exhaustive.
Here is an example of a case that is not matched:
Bool

val fint : 't -> 't ty -> bool = <fun>
|}];;
(* val fint : 'a -> 'a ty -> bool = <fun> *)
(** OK: the return value is x > 0 of type bool;
This has used the equation t = bool, not visible in the return type **)

(* not principal *)
let f (type t) (x : t) (tag : t ty) =
  match tag with
  | Int -> x > 0
  | Bool -> x
;;
[%%expect{|
val f : 't -> 't ty -> bool = <fun>
|}, Principal{|
Line 4, characters 12-13:
4 |   | Bool -> x
                ^
Error: This expression has type t = bool
       but an expression was expected of type bool
       This instance of bool is ambiguous:
       it would escape the scope of its equation
|}];;
(* val f : 'a -> 'a ty -> bool = <fun> *)

(* fail for both *)
let g (type t) (x : t) (tag : t ty) =
  match tag with
  | Bool -> x
  | Int -> x > 0
;;
[%%expect{|
Line 4, characters 11-16:
4 |   | Int -> x > 0
               ^^^^^
Error: This expression has type bool but an expression was expected of type
         t = int
|}, Principal{|
Line 4, characters 11-16:
4 |   | Int -> x > 0
               ^^^^^
Error: This expression has type bool but an expression was expected of type
         t = int
       This instance of int is ambiguous:
       it would escape the scope of its equation
|}];;
(* Error: This expression has type bool but an expression was expected of type
t = int *)

(* OK *)
let g (type t) (x : t) (tag : t ty) : bool =
  match tag with
  | Bool -> x
  | Int -> x > 0
;;
[%%expect{|
val g : 't -> 't ty -> bool = <fun>
|}];;

let id x = x;;
let idb1 = (fun id -> let _ = id true in id) id;;
let idb2 : bool -> bool = id;;
let idb3 ( _ : bool ) = false;;

let g (type t) (x : t) (tag : t ty) =
  match tag with
  | Bool -> idb3 x
  | Int -> x > 0
;;
[%%expect{|
val id : 'a -> 'a = <fun>
val idb1 : bool -> bool = <fun>
val idb2 : bool -> bool = <fun>
val idb3 : bool -> bool = <fun>
val g : 't -> 't ty -> bool = <fun>
|}];;

let g (type t) (x : t) (tag : t ty) =
  match tag with
  | Bool -> idb2 x
  | Int -> x > 0
;;
[%%expect{|
val g : 't -> 't ty -> bool = <fun>
|}];;