From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <edwin+ml-ocaml@etorok.net>
X-Original-To: caml-list@sympa.inria.fr
Delivered-To: caml-list@sympa.inria.fr
Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105])
	by sympa.inria.fr (Postfix) with ESMTPS id 109A17EE94
	for <caml-list@sympa.inria.fr>; Fri,  4 Jan 2013 17:36:26 +0100 (CET)
Received-SPF: None (mail4-smtp-sop.national.inria.fr: no sender
  authenticity information available from domain of
  edwin+ml-ocaml@etorok.net) identity=pra;
  client-ip=176.9.138.55;
  receiver=mail4-smtp-sop.national.inria.fr;
  envelope-from="edwin+ml-ocaml@etorok.net";
  x-sender="edwin+ml-ocaml@etorok.net";
  x-conformance=sidf_compatible
Received-SPF: Pass (mail4-smtp-sop.national.inria.fr: domain of
  edwin+ml-ocaml@etorok.net designates 176.9.138.55 as
  permitted sender) identity=mailfrom; client-ip=176.9.138.55;
  receiver=mail4-smtp-sop.national.inria.fr;
  envelope-from="edwin+ml-ocaml@etorok.net";
  x-sender="edwin+ml-ocaml@etorok.net";
  x-conformance=sidf_compatible; x-record-type="v=spf1"
Received-SPF: Pass (mail4-smtp-sop.national.inria.fr: domain of
  postmaster@mail.etorok.net designates 176.9.138.55 as
  permitted sender) identity=helo; client-ip=176.9.138.55;
  receiver=mail4-smtp-sop.national.inria.fr;
  envelope-from="edwin+ml-ocaml@etorok.net";
  x-sender="postmaster@mail.etorok.net";
  x-conformance=sidf_compatible; x-record-type="v=spf1"
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: Av0HAH4D51CwCYo3/2dsb2JhbABFg0e6BhZzgkwZAQE2AjsWGAMCAQIBPxkIAogUpFCEOgEFi1gGjWyDKZYOhWuKXoJ2
X-IronPort-AV: E=Sophos;i="4.84,411,1355094000"; 
   d="scan'208";a="167449852"
Received: from mail.etorok.net ([176.9.138.55])
  by mail4-smtp-sop.national.inria.fr with ESMTP; 04 Jan 2013 17:36:25 +0100
Received: from [172.30.42.2] (unknown [79.114.32.5])
	by mail.etorok.net (Postfix) with ESMTPSA id ACCA346B3
	for <caml-list@inria.fr>; Fri,  4 Jan 2013 17:36:22 +0100 (CET)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=etorok.net;
	s=MAILOUT; t=1357317382;
	bh=XWMdHMAi8MeaxMJiGe7LoteLN/euzPkLw5CkqF3IPvA=;
	h=Message-ID:Date:From:MIME-Version:To:Subject:Content-Type:
	 Content-Transfer-Encoding;
	b=RpeIPxT57ogVsmmcV23BWI156BywGOKro0THOr0G5Wc/M6KBdaniadkd7CbkpCFUM
	 rv0PKSkgUeQwCcdcwHu8bRO94xdKH3U3v1n8oQzR4AqAJgfb/vVXYTvu9TP0M/0iR0
	 NUimgm5dGGFiojJVW+oFidoeQa2oq/JRQR7UglSk=
Message-ID: <50E70504.6080502@etorok.net>
Date: Fri, 04 Jan 2013 18:36:20 +0200
From: =?ISO-8859-1?Q?T=F6r=F6k_Edwin?= <edwin+ml-ocaml@etorok.net>
User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:10.0.11) Gecko/20121122 Icedove/10.0.11
MIME-Version: 1.0
To: caml-list@inria.fr
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: 7bit
X-Virus-Scanned: clamav-milter 0.97.6 at mail
X-Virus-Status: Clean
Subject: [Caml-list] strange type inference for polymorphic variants

Hi,

If I use a polymorphic variant in a match case that has a _ branch then I get an "interesting" type inferred,
 for example: [< `A of a | `B of a > `A ], instead of: [< `A of a | `B of a ].
To make it work I have to list all possibilities instead of _, _.

I always use `A with a parameter of type a, it seems strange that OCaml would infer `A without a parameter.
Also the inferred type ([< `A of a | `B of a > `A ]) does actually accept both [`A of a] and [`B of a] as input,
and doesn't accept `A without a parameter, so what is the difference between the inferred type and the one I wrote in the signature
([< `A of a | `B of a])?

Here is some simplified code that fails to compile:

$ ocaml
        OCaml version 4.00.1

# type a = string * string;;
type a = string * string
# module Bad3 : sig
  val copy: [< `A of a | `B of a ] -> [< `A of a | `C of a] -> unit
end = struct
  let generic (a: [< `A of a | `B of a]) (b: [< `A of a | `C of a]) = ()
  let specific a b = false
  let copy a b = match a, b with
  | `A x, `A y ->
      if not (specific (`A x) (`A y)) then
        generic a b
  | _, _ ->
      generic a b
end;;
Error: Signature mismatch:
       ...
       Values do not match:
         val copy :
           [< `A of a | `B of a > `A ] -> [< `A of a | `C of a > `A ] -> unit
       is not included in
         val copy : [< `A of a | `B of a ] -> [< `A of a | `C of a ] -> unit


And here is some code that works:
module OK : sig
  val copy: [< `A of a | `B of a ] -> [< `A of a | `C of a] -> unit
end = struct
  let generic (a: [< `A of a | `B of a]) (b: [< `A of a | `C of a]) = ()
  let specific a b = false
  let copy a b = match a, b with
    | `A x, `A y when specific (`A x) (`A y) -> ()
    | (`A _ | `B _), (`A _ | `C _ ) ->
      generic a b
end;;

Here are a few other ways to write the same code which result in an error:
module Bad1: sig
  val test: [< `A of a | `B of a ] -> [< `A of a | `C of a] -> unit
end = struct
  let generic (a: [< `A of a | `B of a]) (b: [< `A of a | `C of a]) = ()
  let specific (a: [`A of a]) (b:[`A of a]) = false
  let test a b =
    let use_specific = match a, b with
      | `A x, `A y -> specific (`A x) (`A y)
      | _, _ -> false in
    if not use_specific then
      generic a b;;
end;;

module Bad2 : sig
  val copy: [< `A of a | `B of a ] -> [< `A of a | `C of a] -> unit
end = struct
  let generic (a: [< `A of a | `B of a]) (b: [< `A of a | `C of a]) = ()
  let specific (a: [`A of a]) (b:[`A of a]) = false
  let copy a b = match a, b with
    | `A x, `A y when specific (`A x) (`A y) ->
        ()
    | _, _ ->
        generic a b
end;;

Best regards,
--Edwin