From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <jp.deplaix@gmail.com>
Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83])
	by sympa.inria.fr (Postfix) with ESMTPS id 692087EE51
	for <caml-list@sympa.inria.fr>; Tue, 28 May 2013 23:01:28 +0200 (CEST)
Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender
  authenticity information available from domain of
  jp.deplaix@gmail.com) identity=pra; client-ip=74.125.82.179;
  receiver=mail2-smtp-roc.national.inria.fr;
  envelope-from="jp.deplaix@gmail.com";
  x-sender="jp.deplaix@gmail.com";
  x-conformance=sidf_compatible
Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of
  jp.deplaix@gmail.com designates 74.125.82.179 as permitted
  sender) identity=mailfrom; client-ip=74.125.82.179;
  receiver=mail2-smtp-roc.national.inria.fr;
  envelope-from="jp.deplaix@gmail.com";
  x-sender="jp.deplaix@gmail.com";
  x-conformance=sidf_compatible; x-record-type="v=spf1"
Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender
  authenticity information available from domain of
  postmaster@mail-we0-f179.google.com) identity=helo;
  client-ip=74.125.82.179;
  receiver=mail2-smtp-roc.national.inria.fr;
  envelope-from="jp.deplaix@gmail.com";
  x-sender="postmaster@mail-we0-f179.google.com";
  x-conformance=sidf_compatible
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: ArEBALMapVFKfVKzk2dsb2JhbABZDoMrgzqFXrkJgQYWDgEBAQEHCwsJFAQkgiMBAQUjBBkBGxwBAQMMBgUEBwMKCRYLAgIJAwIBAgEREQEFARwGDQEHAQGHdgEDDwSeIYtwT4J9hG4KGScNWId1AQUMjxEHgkGBEwOXO4YeiT0/g3dA
X-IPAS-Result: ArEBALMapVFKfVKzk2dsb2JhbABZDoMrgzqFXrkJgQYWDgEBAQEHCwsJFAQkgiMBAQUjBBkBGxwBAQMMBgUEBwMKCRYLAgIJAwIBAgEREQEFARwGDQEHAQGHdgEDDwSeIYtwT4J9hG4KGScNWId1AQUMjxEHgkGBEwOXO4YeiT0/g3dA
X-IronPort-AV: E=Sophos;i="4.87,759,1363129200"; 
   d="scan'208,217";a="19354365"
Received: from mail-we0-f179.google.com ([74.125.82.179])
  by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 28 May 2013 23:01:28 +0200
Received: by mail-we0-f179.google.com with SMTP id m46so5666160wev.38
        for <caml-list@inria.fr>; Tue, 28 May 2013 14:01:27 -0700 (PDT)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
        d=gmail.com; s=20120113;
        h=message-id:date:from:user-agent:mime-version:to:cc:subject
         :references:in-reply-to:x-enigmail-version:content-type;
        bh=e4VOwk7cGz87OmTYWP02x4tAWE5fvArV7d54cTuzyL8=;
        b=AB7Qqfv0E4cXNK2UfMAmkAtoxyCxg2Z9tCQnGTaJZ2VpVCdntr4ZvXH7e/I7PhPOD3
         JQ3bRJ2cA8NLW+WKTIizFKtkrtf/eA2XhKIzSs18HrLSWcRNlLjJzj87lDIWVAiaUw2Y
         xhwaRsC4TT8ZJXDCdQtRVB5cGTWOs8HRJToeVmmivZRw/cXXxi3vWu5XQgI2uzfY0CM0
         yN7l/96GyvFOYMujUmSnm93//+GMblkzTvm0qbj1uFCehFLMBP4e8Ojma7lZGS7onRoC
         msBddX0sXDZh1YjmziMtwUyxwEC7DUAAfCjwGuIN7WPLiIhDq80dnNI0iR0ykP6bRnFS
         lBGA==
X-Received: by 10.194.216.136 with SMTP id oq8mr6589253wjc.8.1369774887630;
        Tue, 28 May 2013 14:01:27 -0700 (PDT)
Received: from [192.168.1.10] (AMontsouris-652-1-163-222.w92-163.abo.wanadoo.fr. [92.163.58.222])
        by mx.google.com with ESMTPSA id q13sm26964456wie.8.2013.05.28.14.01.25
        for <multiple recipients>
        (version=TLSv1 cipher=ECDHE-RSA-RC4-SHA bits=128/128);
        Tue, 28 May 2013 14:01:26 -0700 (PDT)
Message-ID: <51A51B24.4070206@gmail.com>
Date: Tue, 28 May 2013 23:01:24 +0200
From: Jacques-Pascal Deplaix <jp.deplaix@gmail.com>
User-Agent: Mozilla/5.0 (X11; Linux i686; rv:17.0) Gecko/20130514 Thunderbird/17.0.6
MIME-Version: 1.0
To: Leo White <lpw25@cam.ac.uk>
CC: OCaml mailing list <caml-list@inria.fr>
References: <51A38A23.9000402@gmail.com> <86ip23frnx.fsf@cam.ac.uk>
In-Reply-To: <86ip23frnx.fsf@cam.ac.uk>
X-Enigmail-Version: 1.5.1
Content-Type: multipart/alternative;
 boundary="------------050001050207030509000509"
Subject: Re: [Caml-list] Recursive fixed polymorphic variants

This is a multi-part message in MIME format.
--------------050001050207030509000509
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Mmmh I see. Thanks for your answer.

I spent hours to understand how ([< `A | `B of 'a ] 'a) was transformed
into ([< `B of 'a ] as 'a) and I did not saw the influence of the
polymorphism in the type-checking.

Thanks again.

On 05/28/2013 10:13 AM, Leo White wrote:
>> The thing is, if we define M.a and M.b with « unit -> [> a ] » and « 'a -> [> 'a b ] », it does compile but I don't
>> know why the previous code doesn't.
>>
>> Does somebody have any hints ?
> Your f function expects an argument of type:
>
>   ([< `A | `B of 'a ] as 'a)
>
> whilst (M.b (M.a ())) has type:
>
>   [`B of [`A]]
>
> If you try to unify these two types, you have to unify 'a with both [`A]
> and [`B of [`A]]. These types can't be unified since they are both
> closed and are not equal.
>
> If you change the definitions of M.a and M.b as you described, then (M.b
> (M.a ())) has type:
>
>   [> `B of [> `A]]
>
> If you try to unify this with the type of f's argument, you unify 'a
> with [> `A] and [> `B of [> `A]]. These types can be unified because
> they are both open and are not incompatible.
>
> Note that you can use subtyping to give the original (M.b (M.a ())) the
> type:
>
>   ([`A | `B of 'a] as 'a)
>
> which *is* unifiable with the argument type of f:
>
>   f (M.b (M.a ()) :> [`A | `B of 'a] as 'a)
>
> Regards,
>
> Leo


--------------050001050207030509000509
Content-Type: text/html; charset=UTF-8
Content-Transfer-Encoding: 8bit

<html>
  <head>
    <meta content="text/html; charset=UTF-8" http-equiv="Content-Type">
  </head>
  <body bgcolor="#FFFFFF" text="#000000">
    <div class="moz-cite-prefix">Mmmh I see. Thanks for your answer.<br>
      <br>
      I spent hours to understand how <font face="monospace">([&lt; `A
        | `B of 'a ] 'a)</font> was transformed into <font
        face="monospace">([&lt; `B of 'a ] as 'a)</font> and I did not
      saw the influence of the polymorphism in the type-checking.<br>
      <br>
      Thanks again.<br>
      <br>
      On 05/28/2013 10:13 AM, Leo White wrote:<br>
    </div>
    <blockquote cite="mid:86ip23frnx.fsf@cam.ac.uk" type="cite">
      <blockquote type="cite">
        <pre wrap="">
The thing is, if we define M.a and M.b with « unit -&gt; [&gt; a ] » and « 'a -&gt; [&gt; 'a b ] », it does compile but I don't
know why the previous code doesn't.

Does somebody have any hints ?
</pre>
      </blockquote>
      <pre wrap="">
Your f function expects an argument of type:

  ([&lt; `A | `B of 'a ] as 'a)

whilst (M.b (M.a ())) has type:

  [`B of [`A]]

If you try to unify these two types, you have to unify 'a with both [`A]
and [`B of [`A]]. These types can't be unified since they are both
closed and are not equal.

If you change the definitions of M.a and M.b as you described, then (M.b
(M.a ())) has type:

  [&gt; `B of [&gt; `A]]

If you try to unify this with the type of f's argument, you unify 'a
with [&gt; `A] and [&gt; `B of [&gt; `A]]. These types can be unified because
they are both open and are not incompatible.

Note that you can use subtyping to give the original (M.b (M.a ())) the
type:

  ([`A | `B of 'a] as 'a)

which *is* unifiable with the argument type of f:

  f (M.b (M.a ()) :&gt; [`A | `B of 'a] as 'a)

Regards,

Leo
</pre>
    </blockquote>
    <br>
  </body>
</html>

--------------050001050207030509000509--