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 q0OHgpjG032532 for ; Tue, 24 Jan 2012 18:42:51 +0100 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AoMBAMbsHk/RVaC2kGdsb2JhbABCDgiEc6kgCCIBAQEBCQkNBxQEIYFyAQEBBBICDwQZARsdAQMMBgMCCw0CAiYCAiIBEQEFARwGEwgah2KbEgqLIkiCb4RRP4hxAgULgSSHYgMHBQUBAgEug2kUBoIfgRYEiD+MXo4SPYNIVQ X-IronPort-AV: E=Sophos;i="4.71,563,1320620400"; d="scan'208";a="128710529" Received: from mail-gy0-f182.google.com ([209.85.160.182]) by mail4-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 24 Jan 2012 18:42:45 +0100 Received: by ghbg15 with SMTP id g15so733810ghb.27 for ; Tue, 24 Jan 2012 09:42:45 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :cc:content-type:content-transfer-encoding; bh=uJpALgZlERGRJHDU5TIPOKjV5FGJA+nEcRYxga75v+k=; b=ToaDV4DMCvhfvu3bOBIPgFDbrks7ZWhQeqqdsjGe0BLlYSRjHAZRdEnCaktOurpYzK RkMupiy7S4Sf4C/OeJc39gGc0E35oaK6zpTH/xRn2QPWX/0mf6euinOfFRycQgH35h6G RX+9mJQtZfBu8N1QvpShwVIAXTUgteYRkZNmk= MIME-Version: 1.0 Received: by 10.50.153.198 with SMTP id vi6mr4972088igb.30.1327426964966; Tue, 24 Jan 2012 09:42:44 -0800 (PST) Received: by 10.42.134.3 with HTTP; Tue, 24 Jan 2012 09:42:44 -0800 (PST) In-Reply-To: <2FA31185-B4C7-48D3-8C3C-771756CB26AA@math.nagoya-u.ac.jp> References: <2FA31185-B4C7-48D3-8C3C-771756CB26AA@math.nagoya-u.ac.jp> Date: Tue, 24 Jan 2012 12:42:44 -0500 Message-ID: From: =?UTF-8?Q?Milan_Stanojevi=C4=87?= To: Jacques Garrigue Cc: caml-list@inria.fr Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from quoted-printable to 8bit by walapai.inria.fr id q0OHgpjG032532 Subject: Re: [Caml-list] polymorphic variants in match statements Thanks a lot, Jacques! This helped my understanding a lot. I only wonder if maybe this (and other type checking issues) could be documented in a better way. For example I couldn't find any links to your papers on OCaml website 2012/1/23 Jacques Garrigue : > 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 >