Re: [Caml-list] How to use GADTs across modules in OCaml without raising warnings?

[Jeremy Yallop <yallop@gmail.com>]

On 13 October 2015 at 07:15, Ben Millwood <bmillwood@janestreet.com> wrote:
> I'll advance on others' advice by pointing out that if you say:
>
> type never = private [`never]
>
> then you neither "use up" a constructor name nor is it possible to write an
> expression with type never.

A nit: there are lots of *expressions* of type 'never', such as
'(assert false: never)'.  However, there are no (closed) *values* of
type 'never'.

> Unfortunately, the compiler still doesn't realise that, so it
> doesn't help you for pattern-matching.

The gadt-warnings branch, which is described here:

   GADTs and exhaustiveness: looking for the impossible
   Jacques Garrigue's and Jacques Le Normand
   ACM SIGPLAN Workshop on ML, September 2015
   http://www.mlworkshop.org/gadts-and-exhaustiveness-looking-for-the-impossible.pdf

includes better supports for "empty" types.  For example, here's a
definition of an empty type 'wrong':

   type 'a is_true = T: [`True] is_true
   type wrong = [`False] is_true

and here's a function definition which omits a case that you can
deduce is unmatchable when you know that 'wrong' is empty:

   let f : wrong option -> unit = fun None -> ()

The current OCaml compiler (4.02.3) issues a warning for 'f':

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

In contrast, the compiler in the gadt-warnings branch compiles 'f'
without complaint (and generates more efficient code, since there's no
need to inspect the argument).

Jeremy.