"-> ." in pattern matching


The OCaml grammar for patterns includes a case for -> . as the right hand side. I could not find it in the OCaml manual but it seems to be intended for unreachable patterns. Where is this documented and what is the idiomatic use case?

    pattern MINUSGREATER seq_expr
      { Exp.case $1 $3 }
  | pattern WHEN seq_expr MINUSGREATER seq_expr
      { Exp.case $1 ~guard:$3 $5 }
      { Exp.case $1 (Exp.unreachable ~loc:(make_loc $loc($3)) ()) }

Addendum: The reason I did not find it in the manual is that is a language extension that is described in the GADT section and doesn’t have an entry in the table of contents by itself.


Refutation cases are documented here .
Briefly, they are useful when fiddling with GADTs to express that a clause is impossible.
For instance if I have a heterogeneous list defined as

type empty = |
type 'a hlist = []: empty hlist | (::): 'a * 'b hlist -> ('a->'b) hlist 

then if I have a list with type ('a -> 'b) hlist, I know that the list is non-empty.

let hd (type a b) : (a -> b) hlist -> a = function
  | a :: _ -> a
  | _ -> .

Here | _ -> . express the fact that the remaining case, [], is impossible and that the typechecker should be able to prove it.

However, in this case, the typechecker automatically adds a refutation clause _ -> . if there is only one clause in a pattern matching. Thus, I could have written the previous example as

let hd (type a b): (a -> b) hlist -> a = fun (a :: _) -> a

but handwritten refutation clause are necessary in more complex cases.