From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id D72F67FCE8 for ; Thu, 14 Jan 2016 14:34:37 +0100 (CET) IronPort-PHdr: 9a23:jT/13BMiPMZsAQYC1dwl6mtUPXoX/o7sNwtQ0KIMzox0Kf/6rarrMEGX3/hxlliBBdydsKIazbqH+P24EUU7or+/81k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i760zceF13FOBZvIaytQ8iJ35rxh7H5psWbSj4LrQT+SIs6FA+xowTVu5teqqpZAYF19CH0pGBVcf9d32JiKAHbtR/94sCt4MwrqHwI6LoJvvRNWqTifqk+UacQTHF/azh0t4XXskyJawaS5nIRT34NnwAMSy3M9g37WN255i7zrPZ83m+cMND2RL0pQi+v9Y9wSRLthSEccTU+9TeTwoZ7hadf5RagvABXwojOYYjTOuA0NvfWdNYeAG5ARdp5VipbA4r6YZFZXMQbOuMNg5PgvxNaoQGjHRirC6DkwzpMrm3x3ap82OMkR1KVlDc8Fs4D5SyH5O7+M70fBKXslPHF Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=drupyog+caml@zoho.com; spf=Pass smtp.mailfrom=drupyog+caml@zoho.com; spf=None smtp.helo=postmaster@sender153-mail.zoho.com Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of drupyog+caml@zoho.com) identity=pra; client-ip=74.201.84.153; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="drupyog+caml@zoho.com"; x-sender="drupyog+caml@zoho.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of drupyog+caml@zoho.com designates 74.201.84.153 as permitted sender) identity=mailfrom; client-ip=74.201.84.153; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="drupyog+caml@zoho.com"; x-sender="drupyog+caml@zoho.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@sender153-mail.zoho.com) identity=helo; client-ip=74.201.84.153; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="drupyog+caml@zoho.com"; x-sender="postmaster@sender153-mail.zoho.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0AgBADvopdWm5lUyUpegm6CC4hbsxYBAYFuhg8CgT09DwEBAQEBAQEBEAEBAQEBBgsLCSEugi2CCAEBBCcGFgE0Aw4LIRYPCQMCAQIBRQYBDAgBAYgUAQMBBA2vCoVaAodjIiglgn4BCgEBARgHi1WJPZMYhAOBcoZGhSODHoYMhVeOWToBAQGCTYFlcYYxAQEB X-IPAS-Result: A0AgBADvopdWm5lUyUpegm6CC4hbsxYBAYFuhg8CgT09DwEBAQEBAQEBEAEBAQEBBgsLCSEugi2CCAEBBCcGFgE0Aw4LIRYPCQMCAQIBRQYBDAgBAYgUAQMBBA2vCoVaAodjIiglgn4BCgEBARgHi1WJPZMYhAOBcoZGhSODHoYMhVeOWToBAQGCTYFlcYYxAQEB X-IronPort-AV: E=Sophos;i="5.22,294,1449529200"; d="scan'208,217";a="160387399" Received: from sender153-mail.zoho.com ([74.201.84.153]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/AES128-SHA; 14 Jan 2016 14:34:36 +0100 DomainKey-Signature: a=rsa-sha1; q=dns; c=nofws; s=zapps768; d=zoho.com; h=subject:to:references:from:message-id:date:user-agent:mime-version:in-reply-to:content-type; b=h6nMiiU0N3VT7aQ/KBME1FlQsIMKQ9E/7KE+AVuzdbQdvxGNQz9SNcW2YrKIoV0czpaXZFt1kD+d Kl5ppwXu7ZCBaBeZn3v670cTybqnYN7BsF2Ny3z0npzrDY3q+kMu Received: from [134.157.22.141] (134.157.22.141 [134.157.22.141]) by mx.zohomail.com with SMTPS id 1452778468428228.44261715063692; Thu, 14 Jan 2016 05:34:28 -0800 (PST) To: "Neuhaeusser, Martin" , "caml-list@inria.fr" References: <965631B03C670145ABB9F693E51622530D0D8DCF@DENBGAT9EK5MSX.ww902.siemens.net> From: Drup Message-ID: <5697A3E1.6000202@zoho.com> Date: Thu, 14 Jan 2016 14:34:25 +0100 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.5.1 MIME-Version: 1.0 In-Reply-To: <965631B03C670145ABB9F693E51622530D0D8DCF@DENBGAT9EK5MSX.ww902.siemens.net> Content-Type: multipart/alternative; boundary="------------040907020201030102050806" X-Zoho-Virus-Status: 1 Subject: Re: [Caml-list] Exhaustiveness check and GADTs This is a multi-part message in MIME format. --------------040907020201030102050806 Content-Type: text/plain; charset=windows-1252; format=flowed Content-Transfer-Encoding: 8bit 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 --------------040907020201030102050806 Content-Type: text/html; charset=windows-1252 Content-Transfer-Encoding: 8bit
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
 

--------------040907020201030102050806--