(* 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
|}]