1type (_, _) eq = Refl : ('a, 'a) eq;;
2type empty = (int, unit) eq;;
3[%%expect{|
4type (_, _) eq = Refl : ('a, 'a) eq
5type empty = (int, unit) eq
6|}]
7let f (x : ('a, empty Lazy.t) result) =
8  match x with
9  | Ok x -> x
10  | Error (lazy _) -> .;;
11[%%expect{|
12Line _, characters 4-18:
13Error: This match case could not be refuted.
14       Here is an example of a value that would reach it: Error lazy _
15|}]
16let f (x : ('a, empty Lazy.t) result) =
17  match x with
18  | Ok x -> x
19  | Error (lazy Refl) -> .;;
20[%%expect{|
21Line _, characters 16-20:
22Error: This pattern matches values of type (int, int) eq
23       but a pattern was expected which matches values of type
24         empty = (int, unit) eq
25       Type int is not compatible with type unit
26|}]
27