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