match v with _ -> .
This is a GADT refutation case.
This comes up with elaborate GADT code, and the point is to suppress a false exhaustiveness warning while maintaining the usefulness of the exhaustiveness warning (i.e., the warning should still arise if the code's changed to actually not be exhaustive, which doesn't happen if you disable the warning or add a _ -> assert false case). I found a use of a refutation case in Dependent typing, where it also serves as a hint that more than Peano numbers are involved since Peano numbers could continue into other cases.
Curious OCaml has this fun example:
type void = |
let absurd (v: void) : 'a = match v with _ -> .
type t = |
This is an empty variant, a type without any type constructors.
Consider:
type void = |
type security =
[ `Plaintext of void
| `Hashed of string ]
let save_password : security -> unit = function
| `Hashed _ -> ()
| `Plaintext _ -> .
let () =
save_password (`Hashed "1234");
save_password (`Plaintext "1234") (* Error *)
Perhaps a library at one point allowed users to save passwords in plaintext, and then decided that this was a very bad idea.
Even so, I don't really get why it would be resolved in this direction, rather than with removing `Plaintext altogether.
{ weekday = Sat | Sun; _ }
This is a familiar "Or" pattern, but it might be surprising that it can happen at deeper than the top level of a match expression. Also adapted from Curious OCaml:
type weekday = | Sun | Mon | Tue | Wed | Thu | Fri | Sat
type date = year:int * month:int * day:int * weekday:weekday
let on_workday : date -> [`Weekend | `Workday] = function
| ~weekday:Sun, .. | ~weekday:Sat, .. -> `Weekend
| _ -> `Workday
(* this works too *)
let on_workday : date -> [`Weekend | `Workday] = function
| ~weekday:(Sun | Sat), .. -> `Weekend
| _ -> `Workday