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 0470D7FCE8 for ; Thu, 14 Jan 2016 14:24:40 +0100 (CET) IronPort-PHdr: 9a23:WQG8ahzNqHsP0ADXCy+O+j09IxM/srCxBDY+r6Qd0e0fIJqq85mqBkHD//Il1AaPBtWFraIVwLaJ+4nbGkU+or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6anHS+4HYoFwnlMkItf6KuStCU35X8i7/60qaQSjsLrQL1Wal1IhSyoFeZnegtqqwmFJwMzADUqGBDYeVcyDAgD1uSmxHh+pX4p8Y7oGwD884mooRLWKD+OqA5VqBwDTI8Mmlz6teh/U3IRA6Lo38dSXk+kxxSAgGD4gusDbnrtS6v/MxwxSmTMNDtVr0uHXyH5r13SRmiwHMCPiQl8WeRjMFtjKtWvQm6qgZX2I/ZZYyTL7x1eaaLLoBSfnZIQssED38JOYi7dYZaV+c= Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=martin.neuhaeusser@siemens.com; spf=None smtp.mailfrom=martin.neuhaeusser@siemens.com; spf=None smtp.helo=postmaster@david.siemens.de Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of martin.neuhaeusser@siemens.com) identity=pra; client-ip=192.35.17.14; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="martin.neuhaeusser@siemens.com"; x-sender="martin.neuhaeusser@siemens.com"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of martin.neuhaeusser@siemens.com) identity=mailfrom; client-ip=192.35.17.14; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="martin.neuhaeusser@siemens.com"; x-sender="martin.neuhaeusser@siemens.com"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@david.siemens.de) identity=helo; client-ip=192.35.17.14; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="martin.neuhaeusser@siemens.com"; x-sender="postmaster@david.siemens.de"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0BcAQDDoJdWnA4RI8Begm6CEYhVtQaGDwKBPDwQAQEBAQEBAQEQAQEBAQEGDQkJISMLgi2CCQUnBjMrASpWJgEEG4gmBZ9+oDYhhliJVINLgRsFkxOEAwGIN45JhVuOWTmCUYFkhhsBgQcBAQE X-IPAS-Result: A0BcAQDDoJdWnA4RI8Begm6CEYhVtQaGDwKBPDwQAQEBAQEBAQEQAQEBAQEGDQkJISMLgi2CCQUnBjMrASpWJgEEG4gmBZ9+oDYhhliJVINLgRsFkxOEAwGIN45JhVuOWTmCUYFkhhsBgQcBAQE X-IronPort-AV: E=Sophos;i="5.22,294,1449529200"; d="scan'208,217";a="160385856" Received: from david.siemens.de ([192.35.17.14]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-GCM-SHA384; 14 Jan 2016 14:24:38 +0100 Received: from mail1.sbs.de (mail1.sbs.de [192.129.41.35]) by david.siemens.de (8.15.2/8.15.2) with ESMTPS id u0EDOaB3028425 (version=TLSv1.2 cipher=DHE-RSA-AES256-GCM-SHA384 bits=256 verify=OK) for ; Thu, 14 Jan 2016 14:24:37 +0100 Received: from DEFTHW99ERJMSX.ww902.siemens.net (defthw99erjmsx.ww902.siemens.net [139.22.70.135]) by mail1.sbs.de (8.15.1/8.15.1) with ESMTPS id u0EDOas8025594 (version=TLSv1 cipher=AES256-SHA bits=256 verify=FAIL) for ; Thu, 14 Jan 2016 14:24:36 +0100 Received: from DEFTHW99ERPMSX.ww902.siemens.net (139.22.70.202) by DEFTHW99ERJMSX.ww902.siemens.net (139.22.70.135) with Microsoft SMTP Server (TLS) id 14.3.266.1; Thu, 14 Jan 2016 14:24:36 +0100 Received: from DENBGAT9EK5MSX.ww902.siemens.net ([169.254.12.138]) by DEFTHW99ERPMSX.ww902.siemens.net ([139.22.70.202]) with mapi id 14.03.0266.001; Thu, 14 Jan 2016 14:24:35 +0100 From: "Neuhaeusser, Martin" To: "caml-list@inria.fr" Thread-Topic: Exhaustiveness check and GADTs Thread-Index: AdFOzTcAqO6vGSKASGKKuhzS2Cp84Q== Date: Thu, 14 Jan 2016 13:24:34 +0000 Message-ID: <965631B03C670145ABB9F693E51622530D0D8DCF@DENBGAT9EK5MSX.ww902.siemens.net> Accept-Language: de-DE, en-US Content-Language: de-DE X-MS-Has-Attach: X-MS-TNEF-Correlator: x-originating-ip: [139.22.70.36] Content-Type: multipart/alternative; boundary="_000_965631B03C670145ABB9F693E51622530D0D8DCFDENBGAT9EK5MSXw_" MIME-Version: 1.0 Subject: [Caml-list] Exhaustiveness check and GADTs --_000_965631B03C670145ABB9F693E51622530D0D8DCFDENBGAT9EK5MSXw_ Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: quoted-printable Dear all, when trying to use some GADTs, I stumbled across a strange behavior of OCam= l's exhaustiveness check (4.02.3 and 4.03.0+trunk). The following piece of code triggers Warning 8 in function get_root_id. Alt= hough evaluating get_root always yields a root node, the compiler expects a= match for LeafNode: type instance type abstract (** triggers Warning 8: *) type root =3D abstract * (instance, int) Hashtbl.t * instance type leaf =3D abstract * root * instance (** any node can either be a root, or a leaf *) type _ node =3D | RootNode : root -> root node | LeafNode : leaf -> leaf node (** @return the root of any node *) let get_root : type t. t node -> root node =3D 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 =3D fun some_node -> let root_node =3D 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 =3D abstract * (instance, int) Hashtbl.t * instance type leaf =3D root * abstract * instance (** any node can either be a root, or a leaf *) type _ node =3D | RootNode : root -> root node | LeafNode : leaf -> leaf node (** @return the root of any node *) let get_root : type t. t node -> root node =3D 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 =3D fun some_node -> let root_node =3D 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), th= e exhaustiveness check succeeds in both code fragments. I would be very interested, to see the reason for the difference. Best regards, Martin --_000_965631B03C670145ABB9F693E51622530D0D8DCFDENBGAT9EK5MSXw_ Content-Type: text/html; charset="us-ascii" Content-Transfer-Encoding: quoted-printable
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 expe= cts a match for LeafNode:
&nbs= p;
type instance
type abstract
 
(** triggers Warning 8: *)
type root =3D abstract * (instance, int) Hashtbl.t * instance
type leaf =3D abstract * root * instance
 
(** any node can either be a root, or a leaf *)
type _ node =3D
  | RootNode : root -> root node
  | LeafNode : leaf -> leaf node
 
(** @return the root of any node *)
let get_root : type t. t node -> root node =3D
  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 =3D
  fun some_node ->
    let root_node =3D get_root some_node in
    match root_node with
    | RootNode _ -> 1
&nbs= p;
If the order of the tuple elements in the definition of leaf is change= d,
the exhaustiveness check succeeds:
&nbs= p;
type instance
type abstract
 
(** does not trigger Warning 8: *)
type root =3D abstract * (instance, int) Hashtbl.t * instance
type leaf =3D root * abstract * instance
 
(** any node can either be a root, or a leaf *)
type _ node =3D
  | RootNode : root -> root node
  | LeafNode : leaf -> leaf node
 
(** @return the root of any node *)
let get_root : type t. t node -> root node =3D
  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 =3D
  fun some_node ->
    let root_node =3D get_root some_node in
    match root_node with
    | RootNode _ -> 1
&nbs= p;
It seems that the failure of the exhaustiveness check is related to th= e 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.
&nbs= p;
I would be very interested, to see the reason for the difference.
&nbs= p;
Best regards,
Martin
&nbs= p;
 --_000_965631B03C670145ABB9F693E51622530D0D8DCFDENBGAT9EK5MSXw_--