From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr 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 452017F60B for ; Fri, 24 Mar 2017 11:13:19 +0100 (CET) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=grumpy@drno.eu; spf=Pass smtp.mailfrom=grumpy@drno.eu; spf=None smtp.helo=postmaster@smtp.drno.eu Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of grumpy@drno.eu) identity=pra; client-ip=5.196.89.207; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="grumpy@drno.eu"; x-sender="grumpy@drno.eu"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of grumpy@drno.eu designates 5.196.89.207 as permitted sender) identity=mailfrom; client-ip=5.196.89.207; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="grumpy@drno.eu"; x-sender="grumpy@drno.eu"; 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@smtp.drno.eu) identity=helo; client-ip=5.196.89.207; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="grumpy@drno.eu"; x-sender="postmaster@smtp.drno.eu"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3AC8amyRcWCExCcQVKKIGRYtuClGMj4u6mDksu8pMi?= =?us-ascii?q?zoh2WeGdxcS5Yx7h7PlgxGXEQZ/co6odzbGH7+a4ASQp2tWoiDg6aptCVhsI24?= =?us-ascii?q?09vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7?= =?us-ascii?q?Ovr6GpLIj8Swyuu+54Dfbx9GiTe5br5+Ngm6oRnMvcQKnIVuLbo8xAHUqXVSYe?= =?us-ascii?q?RWwm1oJVOXnxni48q74YBu/SdNtf8/7sBMSar1cbg2QrxeFzQmLns65Nb3uhnZ?= =?us-ascii?q?TAuA/WUTX2MLmRdVGQfF7RX6XpDssivms+d2xSeXMdHqQb0yRD+v9LlgRgP2hy?= =?us-ascii?q?gbNj456GDXhdJ2jKJHuxKquhhzz5fJbI2JKPZye6XQctQHS2pcRcZRTzJODZ+g?= =?us-ascii?q?b4UBCOoBOPxXr4j7p1ATqRezCg2hCObpxzRVhHH5wLc63vw8Hw/Y0gwuH9EAvn?= =?us-ascii?q?rbo9r3KKgcXvu4zLXLwDjZc/9axSvx5YrOfxs8of+MR7Vwcc/JxEcuDQPFk1CQ?= =?us-ascii?q?qZTlPjiI0ekNvHKb7/dlVeK3i28qsBx+oiKpxscrkIXGmJ8Vx0nC+C5kzog1It?= =?us-ascii?q?i4R1R6Yd6iCJZQtieaN5F3Qsw4WW1otjw6xqUGuJGhfCgKz5MnywTDZPyAdoiF?= =?us-ascii?q?5A/oWuWJITpghH9pYq+zihKz/ES6yeDxUtO43EhWoidHlNTHq2oD2AbJ6sedT/?= =?us-ascii?q?tw5keh1iiL1wDU8uxEOkU0lbbDK5I737EwjJwTsUPZEiDohUX6lK6WdkM69ei0?= =?us-ascii?q?8+nqYq/qqoKYOoJ1kA3zMaAjltahDegkMAUCR22b9v691L3n8035WrJKjvgun6?= =?us-ascii?q?nWqpDaOMEbpra5AgJOz4kj8RC/DzC83NsGgHkLNEhFdw6fj4j1J1HOJ+j1Auul?= =?us-ascii?q?jFSplDdn3vTGPrz6ApXRNXXDi7fgfbNl60FG0gYzzNZf54hVCr4bOv7zVFXx55?= =?us-ascii?q?TlCAQkOVm03/r/E4c6kZgPXHqGRK6fKqLb91GSofk+JvGFI4YPs3H2Iv0hovrv?= =?us-ascii?q?lmNqpVhIW6ii2p+ec0efHPlqKnKz7WCk1tEAGmAOtxF4S+7nhFTEWzdJT3K/T6?= =?us-ascii?q?My53cwD4fwXqnZQYX4r6ac2T+qVslZfH1DEkGkHW3ucMOJRqFfO2qpPsZ9n2lc?= =?us-ascii?q?BvCaQIg72ETr6Vb3?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0CBCQBR8NRY/89ZxAVdHAEBBAEBCgEBF?= =?us-ascii?q?wEBBAEBCgEBhAqBCwGDYYsCkFuCOpUdKoV4AgiDWxUBAQEBAQEBAQEBAWoogjM?= =?us-ascii?q?EAgMZBYI8AQUjBAsBDQEBLAsBDwsYAgIJGgMCAkUBEQYTEoldAxkKqEtogWw6g?= =?us-ascii?q?wgBAQWEJgODDAEBAQEBBQEBAQEBGwiBC4VCggaCaoRUgwaCX4dHDJULgl6EHYt?= =?us-ascii?q?QglCBBo1ak2U1IoEEOiISQYRJghA/NQGIBoFnAQEB?= X-IPAS-Result: =?us-ascii?q?A0CBCQBR8NRY/89ZxAVdHAEBBAEBCgEBFwEBBAEBCgEBhAq?= =?us-ascii?q?BCwGDYYsCkFuCOpUdKoV4AgiDWxUBAQEBAQEBAQEBAWoogjMEAgMZBYI8AQUjB?= =?us-ascii?q?AsBDQEBLAsBDwsYAgIJGgMCAkUBEQYTEoldAxkKqEtogWw6gwgBAQWEJgODDAE?= =?us-ascii?q?BAQEBBQEBAQEBGwiBC4VCggaCaoRUgwaCX4dHDJULgl6EHYtQglCBBo1ak2U1I?= =?us-ascii?q?oEEOiISQYRJghA/NQGIBoFnAQEB?= X-IronPort-AV: E=Sophos;i="5.36,214,1486422000"; d="scan'208";a="266025295" Received: from dns.drno.eu (HELO smtp.drno.eu) ([5.196.89.207]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-GCM-SHA384; 24 Mar 2017 11:13:18 +0100 DKIM-Signature: v=1; a=rsa-sha256; c=simple/simple; d=drno.eu; s=default; t=1490350396; bh=hDyGWENVhDjmKbg9uC2gylNM48/gZKJYPZSOtyd1ztk=; h=Subject:To:References:Cc:From:Date:In-Reply-To; b=tuTfjATvcDfiEUw/4K0zdgtZsWvcyO4cPJ3UhAjUyK3xA+C5UNukUvEx/B+KqUX+9 jbX0hg+AdJw/dhBxpDMduXm4uBvIDZEwkid3cyPih9AejBcIf/pcGTv/c5OL8Fke4+ K3dxun1c2SitvKNAG4jh1S8/mQE+xcqV2k1bWT6H2R2DFxXArSD/MM9r/J8qG2+p0t blIvsCujyVLpdT6f87gWO3wF/vJ2BKASRKX2fVl9leOYY9hoopZA8WxhbPOKmc4s+g YXlASBoEflhFPqWd3OLslKbXLqdys7Nxf0IqPwztCx2yl/QfPgc60ZfzLXAbrp4To5 dGekD0FSsw94erOxIwxCcqmv71jlAq5zcCOao+D9L8wSKifRKBXmbOQOcnXxh5SApU lrtv6BN7v5mXOq010rzkpqu39+Ybcy9G5JkBYGk+e71raKY4vGvUYwR8lKrXwN1hgw p5mGkbZ62Brs6x0YymDnyLrpcqRk8gr8LywkQJdBlbRcXmTXOeNesJ9M1exzCEBaA7 ZyGuro9xx5GRXhTL2VOszDbznr/n02akY5dlLWZpeAdplSjExvXa6RaYw94JTTa4q3 CxQrRK77cupVNvtl1eevMHLpOSJnDBVmt7ARPKBftgbvgg1s3mCqZWnbbNj7YYLR2j ZsR51VEbG7ai9JE5m3l2YuMw= To: =?UTF-8?Q?Nicol=c3=a1s_Ojeda_B=c3=a4r?= References: <167e229f-2ffc-14ab-8725-5d1af71c167b@drno.eu> Cc: OCaml Mailing List From: Grumpy Message-ID: <317e04aa-de79-bf61-e1fd-f4d467b5a484@drno.eu> Date: Fri, 24 Mar 2017 11:13:16 +0100 Mime-Version: 1.0 In-Reply-To: Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: 8bit X-Validation-by: grumpy@drno.eu Subject: Re: [Caml-list] Type inference curiosity This does not explain why the compiler accepts as well typed the function eval2, after inferring a = int from the first branch. Do I miss something ? Le 24/03/2017 à 10:55, Nicolás Ojeda Bär a écrit : > Hello, > > Recursive definitions need to be explicitly annotated to be > polymorphic. The (type a) annotation > introduces an abstract type a in the body of the function but does not > make it polymorphic. > The annotation type a. on the other hand, does both. > > See http://caml.inria.fr/pub/docs/manual-ocaml/extn.html#sec227 > for the > details. > > Cheers, > Nicolas > > > On Fri, Mar 24, 2017 at 10:20 AM, Grumpy > wrote: > > Hello, > > I think there is an incoherency or a bug somewhere in the type inference > engine with the following code with version 4.02.3 (I have not tested in > previous versions). Both functions eval and eval2 are identical but the > inferred types are different, and the type inferred for eval2 is > actually wrong. > > The function eval is typed correcly ('a exp -> 'a) while the type > inferred for funcion function eval2 is (int exp -> int), which is wrong > because of the Inc case returning ('a exp -> 'a). > > It seems the syntax (type a) leads to this incorrect behaviour... > > > type _ exp = > | Stop : int exp > | Inc : (int exp -> int) exp > > let rec eval : type a. a exp -> a = function > | Stop -> 0 > | Inc -> (fun (p : int exp) -> 1 + eval p) > > let rec eval2 (type a) (p : a exp) : a = > match p with > | Stop -> 0 > | Inc -> (fun (p : int exp) -> 1 + eval2 p) > > -- > Caml-list mailing list. Subscription management and archives: > https://sympa.inria.fr/sympa/arc/caml-list > > Beginner's list: http://groups.yahoo.com/group/ocaml_beginners > > Bug reports: http://caml.inria.fr/bin/caml-bugs > > >