mjhjmtu

In the GADTs section of the "Language extensions" chapter of the official OCaml docs, refutation cases of the form _ -> . are introduced. However, I thought that pattern-matching was already exhaustive, so I'm not sure when a refutation case is actually necessary.

The example given in the doc is as follows:

type _ t =
 | Int : int t
 | Bool : bool t

let deep : (char t * int) option -> char = function
 | None -> 'c'
 | _ -> .

But even the docs state that this refutation case is redundant. Is there an example where a refutation case is necessary for the code to typecheck?

Refutation cases are useful for exhaustiveness checking, not type checking directly.

Your example is a bit confusing because the compiler automatically adds a simple refutation clause | _ -> . when the patter matching is simple enough. In other words,

let deep : (char t * int) option -> char = function None -> 'c'

is equivalent to

let deep : (char t * int) option -> char = function
| None -> 'c'
| _ -> .

because the typechecker adds a refutation clause by itself. Before the introduction of refutation clause in 4.03, the only way to write deep was

let deep : (char t * int) option -> char = function
 | None -> 'c';;

Warning 8: this pattern-matching is not exhaustive. Here is an example of a value that is not matched:

Some _

At this point in time, there was no way to get rid of this warning (without disabling it) since the remaining cases are syntactically possible but forbidden by some type constraints.

Refutation clause are here to solve this issue, and they are added automatically in those simple cases. But in more complex situation, hand-written refutation clause are necessary. For instance, if I start with this function

let either : (float t, char t) result -> char = ...

there is no way to complete the ellipsis ... with concrete patterns with the right types:

let either : (float t, char t) result -> char = function
| Ok Int -> ... (* no, wrong type: (int t, _ ) result *)
| Ok Bool -> ... (* still no possible (bool t, _) result *)
| Error Int -> ... (* not working either: (_, int t) result *)
| Either Bool -> ... (* yep, impossible (_, bool t) result *)

Refutation clause are a way to indicate to the typechecker that the remaining cases of a pattern are not compatible with the existing type constraints

let either : (float t, char t) result -> char = function
| Ok _ -> .
| _ -> .

More precisely, those refutation clauses tell to the compiler to try expand all any _ pattern in the left-hand side of the clause and check that there is no way for those patterns to typecheck.

In general, there is three kinds of situations where a hand-written refutation clause is needed:

• Pattern matching on an type without any possible values


• No automatic refutation clause has been added


• The default counter-example exploration depth is not enough

First, the simplest toy example happens when there is no possible patterns:

 let f: float t -> _ = function _ -> . 

The second case is when one falls out of the default refutation clause. In particular, a refutation clause is only added when there is one clause in the match:

 type 'a ternary = A | B | C of 'a
 let ternary : float t ternary -> _ = function
 | A -> ()
 | B -> ()

Warning 8: this pattern-matching is not exhaustive.
Here is an example of a case that is not matched:
C _

Thus a hand-written clause is needed

 let ternary : float t ternary -> _ = function
 | A -> ()
 | B -> ()
 | _ -> .

Finally, sometimes the default exploration depth for counter-examples is not enough to prove that there is no counter-examples.
By default, the exploration depth is 1: a pattern _ is exploded once.
For instance, in your example , | _ -> . is transformed into Int | Bool -> ., then the typechecker checks that no cases is valid.

Consequently, a simple way to make the refutation case necessary is to nest two type constructors. For instance:

let either : (float t, char t) result -> char = function
| _ -> .

Error: This match case could not be refuted.
Here is an example of a value that would reach it: _

Here, it is necessary to expand by hand at least one of the Ok or Error cases:

let either : (float t, char t) result -> char = function
| Ok _ -> . 
| _ -> .

Note that there is a special case for types with only one constructor which counts only for 1/5 of a full expansion when expanded. For instance, if you introduce a type

 type 'a delay = A of 'a

then

 let nested : float t delay option -> _ = function
 | None -> ()

is fine because expanding _ to A _ costs 0.2 expansion, and we have still some budget for expanding A _ to A Int | A Float.

Nevertheless, if you nest enough delays, a warning appears

 let nested : float t delay delay delay delay delay delay option -> _ = 
 function
 | None -> ()

Warning 8: this pattern-matching is not exhaustive.
Here is an example of a case that is not matched:
Some (A (A (A (A (A _)))))

The warning may be fixed by adding a refutation clause:

 let nested : float t delay delay delay delay delay delay option -> _ = function
 | None -> ()
 | Some A _ -> .