[Caml-list] GADT exhaustiveness check

[Kaspar Rohrer <kaspar.rohrer@gmail.com>]

Hi List

I'm messing around with the new GADT feature in OCaml 4.0, trying to write a (more or less) strongly typed EDSL. And I've run into non-exhaustive pattern-matching warnings (see below for an example). I'm pretty sure that it is just an inherent shortcoming of GADTs, not a bug. The workaround is easy as well, simply add a catch all clause with a runtime error to silence the warning, and prove manually that the offending patterns can not occur.

I tried to find more information on this topic, but without getting all academic, documentation on GADT seems sparse at best. The description of the original implementation at https://sites.google.com/site/ocamlgadt/ seems to be the most comprehensive I've found so far. And I'm not sure the information about exhaustiveness is still up to date.

It would be nice if somebody could maybe shed some more light on this.

Cheers
	Kaspar


Code that illustrates the problem:

module T :
    sig
      type 'a t
      val int : int t
    end
    =
  struct
    type 'a t = ()
    let int = ()
  end

type ('r,_) args =
  | ANil : ('r,'r) args
  | ACons : 'a * ('r,'b) args -> ('r,'a -> 'b) args

let a = ANil
let b = ACons (3, ANil)

type ('r,'a) fun' =
  | FVoid : 'r T.t -> ('r,'r) fun'
  | FLambda : 'a T.t * ('r,'b) fun' -> ('r,'a -> 'b) fun'

let f = FVoid T.int
let g = FLambda (T.int, f)

let rec apply : type r a . (r,a) fun' * (r,a) args -> unit = function
  | FVoid t, ANil -> ()
  | FLambda (t,f), ACons (_,a) -> apply (f,a)
(*
Warning 8: this pattern-matching is not exhaustive.
Here is an example of a value that is not matched:
(FLambda (_, _), ANil)
 *)