[Caml-list] Exhaustiveness check and GADTs

[Caml-list] Exhaustiveness check and GADTs

[Neuhaeusser, Martin]

[-- 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 --]

Re: [Caml-list] Exhaustiveness check and GADTs

[Drup]

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

This is due to the fact that the type checker here believes that root 
and leaf could be the same.
Hashtbl.t is abstract in another module, hence it could potentially be 
equal to root, which means root and leaf could be the same type.

If you reorder the fields, the ambiguity disappear. You can also solve 
it by declaring root and leaf as records with distinct fields.


Le 14/01/2016 14:24, Neuhaeusser, Martin a écrit :
> 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: 5689 bytes --]