summaryrefslogtreecommitdiff
path: root/testsuite/tests/typing-gadts/pr7421.ml
blob: 79acaceb7da2a771289734cfe6dff8ee282c21a5 (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
*)

type (_, _) eq = Refl : ('a, 'a) eq;;
type empty = (int, unit) eq;;
[%%expect{|
type (_, _) eq = Refl : ('a, 'a) eq
type empty = (int, unit) eq
|}]
let f (x : ('a, empty Lazy.t) result) =
  match x with
  | Ok x -> x
  | Error (lazy _) -> .;;
[%%expect{|
Line 4, characters 4-18:
4 |   | Error (lazy _) -> .;;
        ^^^^^^^^^^^^^^
Error: This match case could not be refuted.
       Here is an example of a value that would reach it: Error lazy _
|}]
let f (x : ('a, empty Lazy.t) result) =
  match x with
  | Ok x -> x
  | Error (lazy Refl) -> .;;
[%%expect{|
Line 4, characters 16-20:
4 |   | Error (lazy Refl) -> .;;
                    ^^^^
Error: This pattern matches values of type (int, int) eq
       but a pattern was expected which matches values of type
         empty = (int, unit) eq
       Type int is not compatible with type unit
|}]