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?
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.