Re: [Caml-list] GADT exhaustiveness check

[Jeremy Yallop <yallop@gmail.com>]

Dear Kaspar,

On 17 November 2012 12:44, Kaspar Rohrer <kaspar.rohrer@gmail.com> wrote:
> 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.
[...]
> 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)
>  *)

Here's how you know that the offending pattern can never match a value: the
ANil constructor would constrain "r" and "a" to denote the same type, and the
arguments of the FLambda constructor would have types "'a T.t" and "('a -> 'b,
'b) fun'" (for suitable 'a and 'b).  It's then sufficient to show that at
least one of these types is not inhabited.  However, in order to show this you
need to use information about the possible ways of building values of those
types: for example, you need to know that there's no polymorphic value of type
"'a t".  If you add such a value to the T module:

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

then you *can* build values that match the missing patterns:

  # apply (FLambda (T.int, FVoid T.poly), ANil)
  Exception: Match_failure ("//toplevel//", 113, 9).

I don't think that the exhaustiveness checker has any information available
regarding the possible ways of constructing values of an abstract type.

Here's an example without GADTs illustrating the same issue.  Suppose we have
your original definition of the T module:

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

We can define a datatype with two constructors using T.t:

    type s =
      Int of int T.t
    | Float of float T.t

Since there is no value of type "float T.t", patterns involving the Float
constructor are redundant.  However, the exhaustiveness checker doesn't know
that, so you'll still get a warning for omitting the Float case:

    Characters 8-28:
      let f = function Int _ -> ();;
              ^^^^^^^^^^^^^^^^^^^^
    Warning 8: this pattern-matching is not exhaustive.
    Here is an example of a value that is not matched:
    Float _

Hope that helps a bit,

Jeremy.