From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: 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 605A47EE51 for ; Tue, 28 May 2013 10:12:09 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of lpw25@cam.ac.uk) identity=pra; client-ip=131.111.8.152; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="lpw25@cam.ac.uk"; x-sender="lpw25@cam.ac.uk"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of lpw25@cam.ac.uk) identity=mailfrom; client-ip=131.111.8.152; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="lpw25@cam.ac.uk"; x-sender="lpw25@cam.ac.uk"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@ppsw-52.csi.cam.ac.uk) identity=helo; client-ip=131.111.8.152; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="lpw25@cam.ac.uk"; x-sender="postmaster@ppsw-52.csi.cam.ac.uk"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AoABAK9lpFGDbwiYnGdsb2JhbABZhnO+V4EEFg4BAQEBAQgLCQkUKIIjAQEEASMEUhALGgIFIQICDwEESYgaBgSrE4k1h08WgRCNRDMHgkGBEwOsCw X-IPAS-Result: AoABAK9lpFGDbwiYnGdsb2JhbABZhnO+V4EEFg4BAQEBAQgLCQkUKIIjAQEEASMEUhALGgIFIQICDwEESYgaBgSrE4k1h08WgRCNRDMHgkGBEwOsCw X-IronPort-AV: E=Sophos;i="4.87,756,1363129200"; d="scan'208";a="19247105" Received: from ppsw-52.csi.cam.ac.uk ([131.111.8.152]) by mail2-smtp-roc.national.inria.fr with ESMTP; 28 May 2013 10:12:08 +0200 X-Cam-AntiVirus: no malware found X-Cam-ScannerInfo: http://www.cam.ac.uk/cs/email/scanner/ Received: from cpc2-cmbg14-2-0-cust33.5-4.cable.virginmedia.com ([86.26.0.34]:59360 helo=netbook) by ppsw-52.csi.cam.ac.uk (smtp.hermes.cam.ac.uk [131.111.8.158]:587) with esmtpsa (PLAIN:lpw25) (TLSv1.2:DHE-RSA-AES128-SHA:128) id 1UhF0q-0005Fb-FE (Exim 4.80_167-5a66dd3) (return-path ); Tue, 28 May 2013 09:12:08 +0100 From: Leo White To: Jacques-Pascal Deplaix Cc: OCaml mailing list References: <51A38A23.9000402@gmail.com> Date: Tue, 28 May 2013 09:13:38 +0100 In-Reply-To: <51A38A23.9000402@gmail.com> (Jacques-Pascal Deplaix's message of "Mon, 27 May 2013 18:30:27 +0200") Message-ID: <86ip23frnx.fsf@cam.ac.uk> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/23.4 (gnu/linux) MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable Subject: Re: [Caml-list] Recursive fixed polymorphic variants > > The thing is, if we define M.a and M.b with =C2=AB unit -> [> a ] =C2=BB = and =C2=AB 'a -> [> 'a b ] =C2=BB, 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