When are refutation cases necessary in OCaml?

Question

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?

Ada

Answer 1

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 case | _ -> . when the pattern 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 case by itself. Before the introduction of refutation cases 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 that 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 cases are here to solve this issue, and they are added automatically in those simple cases. But in a more complex situation, hand-written refutation cases 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 ... using 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 *)
  | Error Bool -> ... (* yep, impossible (_, bool t) result *)

Refutation cases 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 cases tell the compiler to try to expand all _ patterns in the left-hand side of the case and check that there is no way for those patterns to typecheck.

In general, there are three kinds of situations where a handwritten refutation case is needed:

• Pattern matching on a type without any possible values
• No automatic refutation case 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 case. In particular, a refutation case is only added when there is one case 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 handwritten case 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 are 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 are 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 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 case:

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

Tertius

Thank you for the incredibly detailed answer! I didn't know that OCaml had an exploration depth. Is the default depth of 1 and the special-case depth of 0.2 documented anywhere? – Ada

The exploration depth for splitting wild card pattern and the reason behind this heuristic is detailed in Jacques Garrigue's article: math.nagoya-u.ac.jp/~garrigue/papers/gadtspm-long.pdf . The special casing of variant with one constructor and tuples is also explained, but their specific cost is more of an implementation detail. – Tertius