[Caml-list] Exhaustiveness check and GADTs

["Neuhaeusser, Martin" <martin.neuhaeusser@siemens.com>]

[-- Attachment #1: Type: text/plain, Size: 2207 bytes --]

Dear all,

when trying to use some GADTs, I stumbled across a strange behavior of OCaml's exhaustiveness check (4.02.3 and 4.03.0+trunk).
The following piece of code triggers Warning 8 in function get_root_id. Although evaluating get_root always yields a root node, the compiler expects a match for LeafNode:

type instance
type abstract

(** triggers Warning 8: *)
type root = abstract * (instance, int) Hashtbl.t * instance
type leaf = abstract * root * instance

(** any node can either be a root, or a leaf *)
type _ node =
  | RootNode : root -> root node
  | LeafNode : leaf -> leaf node

(** @return the root of any node *)
let get_root : type t. t node -> root node =
  fun some_node ->
    match some_node with
    | RootNode _ -> some_node
    | LeafNode (_, root, _) -> RootNode root

(** @return the id (here just 1) of any node's root *)
let get_root_id : type t. t node -> int =
  fun some_node ->
    let root_node = get_root some_node in
    match root_node with
    | RootNode _ -> 1

If the order of the tuple elements in the definition of leaf is changed,
the exhaustiveness check succeeds:

type instance
type abstract

(** does not trigger Warning 8: *)
type root = abstract * (instance, int) Hashtbl.t * instance
type leaf = root * abstract * instance

(** any node can either be a root, or a leaf *)
type _ node =
  | RootNode : root -> root node
  | LeafNode : leaf -> leaf node

(** @return the root of any node *)
let get_root : type t. t node -> root node =
  fun some_node ->
    match some_node with
    | RootNode _ -> some_node
    | LeafNode (root, _, _) -> RootNode root

(** @return the id (here just 1) of any node's root *)
let get_root_id : type t. t node -> int =
  fun some_node ->
    let root_node = get_root some_node in
    match root_node with
    | RootNode _ -> 1

It seems that the failure of the exhaustiveness check is related to the use of a module (here Hashtbl.t).
If (instance, int) Hashtbl.t is replaced by a different type (e.g. int), the exhaustiveness check succeeds
in both code fragments.

I would be very interested, to see the reason for the difference.

Best regards,
Martin


[-- Attachment #2: Type: text/html, Size: 4263 bytes --]