From mboxrd@z Thu Jan  1 00:00:00 1970
Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82])
	by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id q0O0rnZ1028294
	for <caml-list@sympa-roc.inria.fr>; Tue, 24 Jan 2012 01:53:49 +0100
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: AnwCACIAHk/RVdK2kWdsb2JhbABChQmpGQgiAQEBAQkJDQcSJ4ILAg8EGQEbHgMSEA8CJgIkAREBBQEWQaBigl8KiyJIgm+EXz+IcQIFC4Ekh1uCBoEWBIg7jF6OEj2EHQ
X-IronPort-AV: E=Sophos;i="4.71,559,1320620400"; 
   d="scan'208";a="141143420"
Received: from mail-iy0-f182.google.com ([209.85.210.182])
  by mail1-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 24 Jan 2012 01:53:43 +0100
Received: by iagz16 with SMTP id z16so8893644iag.27
        for <caml-list@inria.fr>; Mon, 23 Jan 2012 16:53:42 -0800 (PST)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
        d=gmail.com; s=gamma;
        h=mime-version:date:message-id:subject:from:to:content-type;
        bh=F+MAeyGMdmrFeCQe4RGn36DW3pqcKxtlhAUpuHRWRZA=;
        b=seqI3rfgtyM9aTPMF//2g/1ixK96N6J3BPq8gcZsml54jTBoB58//CP+uPDIm6N+VF
         osonwJyhPSgLd7sZrgd5P+NhXLKtgv3EcaAIGfWaNBtxXoGmT2HMatyDvIyi8qr8Umvx
         DfbG9fLfp8cXQ7k6b5F+6bxhI2440AjD04z7o=
MIME-Version: 1.0
Received: by 10.50.160.234 with SMTP id xn10mr46068igb.30.1327366422397; Mon,
 23 Jan 2012 16:53:42 -0800 (PST)
Received: by 10.42.134.3 with HTTP; Mon, 23 Jan 2012 16:53:42 -0800 (PST)
Date: Mon, 23 Jan 2012 19:53:42 -0500
Message-ID: <CAKR7PS95d1vL3smxojbMoGj=tXgm8Xu52PUKmfodDyFSRH+QzA@mail.gmail.com>
From: =?UTF-8?Q?Milan_Stanojevi=C4=87?= <milanst@gmail.com>
To: caml-list@inria.fr
Content-Type: text/plain; charset=UTF-8
Subject: [Caml-list] polymorphic variants in match statements

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?