From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr 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 EAF9B7F20B for ; Tue, 12 Feb 2013 03:24:25 +0100 (CET) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of garrigue@math.nagoya-u.ac.jp) identity=pra; client-ip=133.6.130.5; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="garrigue@math.nagoya-u.ac.jp"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of garrigue@math.nagoya-u.ac.jp) identity=mailfrom; client-ip=133.6.130.5; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="garrigue@math.nagoya-u.ac.jp"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mailhost.math.nagoya-u.ac.jp) identity=helo; client-ip=133.6.130.5; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="postmaster@mailhost.math.nagoya-u.ac.jp"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Ap4EAACnGVGFBoIF/2dsb2JhbABEwT9zgh8BAQQBJxMJATUCAwsLRiE2BhOIAAMJBa0SgzGBEAKEfA1MiQgHjD+EbWGIZ4tngVmLQIUTgxU X-IPAS-Result: Ap4EAACnGVGFBoIF/2dsb2JhbABEwT9zgh8BAQQBJxMJATUCAwsLRiE2BhOIAAMJBa0SgzGBEAKEfA1MiQgHjD+EbWGIZ4tngVmLQIUTgxU X-IronPort-AV: E=Sophos;i="4.84,646,1355094000"; d="scan'208";a="1863340" Received: from rabbit.math.nagoya-u.ac.jp (HELO mailhost.math.nagoya-u.ac.jp) ([133.6.130.5]) by mail3-smtp-sop.national.inria.fr with ESMTP; 12 Feb 2013 03:13:59 +0100 Received: from mailhost.math.nagoya-u.ac.jp (localhost [127.0.0.1]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id 88030636B; Tue, 12 Feb 2013 11:24:20 +0900 (JST) Received: from mailhost.math.nagoya-u.ac.jp (localhost [127.0.0.1]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id 5DFC7252F; Tue, 12 Feb 2013 11:24:20 +0900 (JST) DomainKey-Signature: h=Received:Content-Type:Mime-Version:Subject:From:In-Reply-To:Date:Cc:Content-Transfer-Encoding:Message-Id:References:To:X-Mailer; b=; c=nofws; d=math.nagoya-u.ac.jp; q=; s=alpha Received: from garrigue-mini.math.nagoya-u.ac.jp (garrigue-mini.math.nagoya-u.ac.jp [172.16.30.37]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id 5706C252E; Tue, 12 Feb 2013 11:24:20 +0900 (JST) Content-Type: text/plain; charset=us-ascii Mime-Version: 1.0 (Mac OS X Mail 6.2 \(1499\)) From: Jacques Garrigue In-Reply-To: Date: Tue, 12 Feb 2013 11:28:39 +0900 Cc: "caml-list@inria.fr" Content-Transfer-Encoding: quoted-printable Message-Id: <0B8A0D3C-CB7E-4B37-8386-F05B81E416C0@math.nagoya-u.ac.jp> References: To: Sebastien Mondet X-Mailer: Apple Mail (2.1499) Subject: Re: [Caml-list] Propagating types to pattern-matching On 2013/02/12, at 0:31, Sebastien Mondet wrote: > Hi Jacques >=20 > I don't know if this directly related, or if it is actually intended, but= this looks like a regression to me: >=20 >=20 > With OCaml version 4.00.1+dev2_2012-08-06 (4.00.1+short-types in Opam): >=20 > # let f =3D function 0 -> `zero | 1 -> `one | _ -> `some;; > val f : int -> [> `one | `some | `zero ] =3D >=20 > # let g x =3D match f x with `one -> 1 | `zero -> 0;; > Error: This pattern matches values of type [< `one | `zero ] > but a pattern was expected which matches values of type > [> `one | `some | `zero ] > The first variant type does not allow tag(s) `some >=20 > which is the nice behavior we were used to, > but with OCaml version 4.01.0+dev10-2012-10-16 (a.k.a. 4.01.0dev+short-= paths), the error has been downgraded to a warning: >=20 > # let f =3D function 0 -> `zero | 1 -> `one | _ -> `some;; > val f : int -> [> `one | `some | `zero ] =3D >=20 > # let g x =3D match f x with `one -> 1 | `zero -> 0;; > Warning 8: this pattern-matching is not exhaustive. > Here is an example of a value that is not matched: > `some > val g : int -> int =3D >=20 This is related, and this is the intended behavior. For polymorphic variants, you get a warning if the type was known early eno= ugh, and a hard error otherwise. Actually, I see it as a progress, since the warning gives you a counter-exa= mple, whereas the error message only gives you a discrepancy between types. For me the only sane handling of partial matching is to see it as an error, so use at least -warn-error P. (Or at least watch for warnings) Jacques Garrigue