From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id q0O1Lqgi029077 for ; Tue, 24 Jan 2012 02:21:52 +0100 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Ap8EAOUGHk+FBoIF/2dsb2JhbABCFoRzqiaBcgEBBAEjBBkDATUBAQMLCxoCGA4CAlcGiA8IpiJqgz2OCAEGgS+JYTNjiD2MYJJd X-IronPort-AV: E=Sophos;i="4.71,559,1320620400"; d="scan'208";a="128595959" Received: from rabbit.math.nagoya-u.ac.jp (HELO mailhost.math.nagoya-u.ac.jp) ([133.6.130.5]) by mail4-smtp-sop.national.inria.fr with ESMTP; 24 Jan 2012 02:21:46 +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 AB83062B8; Tue, 24 Jan 2012 10:21:43 +0900 (JST) Received: from mailhost.math.nagoya-u.ac.jp (camel-172.math.nagoya-u.ac.jp [172.16.254.4]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id 758BF24E1; Tue, 24 Jan 2012 10:21:43 +0900 (JST) DKIM-Signature: v=1; a=rsa-sha1; c=relaxed; d=math.nagoya-u.ac.jp; h= subject:mime-version:content-type:from:in-reply-to:date:cc :content-transfer-encoding:message-id:references:to; s=alpha; bh=1y1O8uFYWWBGpvwwnYkUFCMULXI=; b=kD7VcxgAEmzsy5CTw2283a5ou9c/ rMWzifdXtKA+QtgPFFoM7z8YK7K7hhTUFY7QqgGMdxNPMq/HRal6zqzZyobxS1UO vL9senW6YkpUya2VXoyzwissWmV19OUHmoHMfq2mm3eNm26DeyLDdGylMrKvOy05 kvs1WJPFeZz+rJs= DomainKey-Signature: a=rsa-sha1; h=Received:Subject:Mime-Version:Content-Type:From:In-Reply-To:Date:Cc:Content-Transfer-Encoding:Message-Id:References:To:X-Mailer; b=mKEUQC2QlQwUQ2WvJGQdMl2fZQ4kerPCypJik+41p0agT4BdbXXJE69KeHh5noGTJNIovIgdRNl4FEVtVd4YaITRMiZGxxciuVcU7VqklsLzLkLPYGtAqRautCs7G82f7rMnRJ7dk+tiemzEsWIDZ+P19uUHVVAJlYew/VdsWqA=; c=nofws; d=math.nagoya-u.ac.jp; q=dns; s=alpha Received: from tet.garrigue.jp (58x158x128x157.ap58.ftth.ucom.ne.jp [58.158.128.157]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTPSA id 4328224D3; Tue, 24 Jan 2012 10:21:43 +0900 (JST) Mime-Version: 1.0 (Apple Message framework v1084) Content-Type: text/plain; charset=utf-8 From: Jacques Garrigue In-Reply-To: Date: Tue, 24 Jan 2012 10:21:43 +0900 Cc: caml-list@inria.fr Message-Id: <2FA31185-B4C7-48D3-8C3C-771756CB26AA@math.nagoya-u.ac.jp> References: To: =?utf-8?Q?Milan_Stanojevi=C4=87?= X-Mailer: Apple Mail (2.1084) Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from quoted-printable to 8bit by walapai.inria.fr id q0O1Lqgi029077 Subject: Re: [Caml-list] polymorphic variants in match statements On 2012/01/24, at 9:53, Milan Stanojević wrote: > Hi, we're trying to understand the type inference with polymorphic > variants in match statements. This is a simplification of an actual > case that happened in practice. > > 1) > let f i a = > match i, a with > | true, `A -> `B > | false, x -> x > > fails with > File "foo.ml", line 4, characters 16-17: > Error: This expression has type [< `A ] > but an expression was expected of type [> `B ] > The first variant type does not allow tag(s) `B > > 2) changing false to _ > let f i a = > match i, a with > | true, `A -> `B > | _, x -> x > > this succeeds with > val f : bool -> ([> `A | `B ] as 'a) -> 'a > > 3) changing x in (1) to _ , and using a on the right side > let f i a = > match i, a with > | true, `A -> `B > | false, _ -> a > > this fails in the same way as (1) > > 4) finally adding another case to match statement > let f i a = > match i, a with > | true, `A -> `B > | false, x -> x > | true, x -> x > > this succeeds with the same type as (2) > > > So it seems there is some interaction between type inference and > exhaustivnest of the match statements. > > Can someone shed some light on what is going on here? Indeed. The basic idea is to close variant types when leaving them open would make the pattern matching non-exhaustive. Here, if we assume that a has type [`A | `B], then the pattern-matching becomes non-exhaustive, so the type inferred is just [`A] (i.e. the list of all constructors appearing inside the patterns at this position). Actually, the theory is a bit more complicated, and the full details are in the following paper, but you should just expect the above behavior in practice. Typing deep pattern-matching in presence of polymorphic variants. http://www.math.nagoya-u.ac.jp/~garrigue/papers/index.html Note that there is also another way to make (1) type, without adding new cases let f i a = match i, a with | true, `A -> `B | false, (`A as x) -> x;; val f : bool -> [< `A ] -> [> `A | `B ] = Here we have removed the connection between a and the output, allowing `A to be combine with `B without changing the type of a. Hope this helps. Jacques Garrigue