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

#labels false;;
type (_,_) eql = Refl : ('a, 'a) eql
type s = x:int -> y:float -> unit
type t = y:int -> x:float -> unit
type silly = {silly: 'a.'a};;
let eql : (s, t) eql = Refl;;
[%%expect{|
type (_, _) eql = Refl : ('a, 'a) eql
type s = x:int -> y:float -> unit
type t = y:int -> x:float -> unit
type silly = { silly : 'a. 'a; }
val eql : (s, t) eql = Refl
|}]

#labels true;;
let f : [`L of (s, t) eql | `R of silly] -> 'a =
  function `R {silly} -> silly
;;
[%%expect{|
Line 2, characters 2-30:
2 |   function `R {silly} -> silly
      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Warning 8 [partial-match]: this pattern-matching is not exhaustive.
Here is an example of a case that is not matched:
`L Refl

val f : [ `L of (s, t) eql | `R of silly ] -> 'a = <fun>
|}]

(* Segfault: let () = print_endline (f (`L eql)) *)