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 mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id CF3E4801CD for ; Fri, 18 Aug 2017 16:36:50 +0200 (CEST) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=gabriel.scherer@gmail.com; spf=Pass smtp.mailfrom=gabriel.scherer@gmail.com; spf=None smtp.helo=postmaster@mail-qk0-f169.google.com Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of gabriel.scherer@gmail.com) identity=pra; client-ip=209.85.220.169; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of gabriel.scherer@gmail.com designates 209.85.220.169 as permitted sender) identity=mailfrom; client-ip=209.85.220.169; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-qk0-f169.google.com) identity=helo; client-ip=209.85.220.169; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="postmaster@mail-qk0-f169.google.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3ASoaXExehKE/VsSGaThRsVOPdlGMj4u6mDksu8pMi?= =?us-ascii?q?zoh2WeGdxc66YB7h7PlgxGXEQZ/co6odzbGJ4+a9ASQp2tWojjMrSNR0TRgLiM?= =?us-ascii?q?EbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpQgpBw7nOAFp?= =?us-ascii?q?CuPwE4/Ux4TrhqHhs6HUNixMiSqwcPtfIxKsqhuZ4sASjJskLaA1213FinRNcu?= =?us-ascii?q?VSg2hvIATAsQz745Kf9ZR58ilU88kq98NaXL+yK6sxR6ZZATBgKGs16dfmrzHM?= =?us-ascii?q?SAKO4j0XVWBAwUkAOBTM8ByvBsS5iSD9rOcohHiX?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0BGAgCL+pZZh6ncVdFcHAEBBAEBCgEBF?= =?us-ascii?q?gEBAQMBAQEJAQEBg1Q/gQITB4UmmHiBboJGk1aCEiyFGwKDZQdBFgEBAQEBAQE?= =?us-ascii?q?BAQEBEgEBAQgNCQgoL4IzBQMEHoI8AQICASMdARsSCwEDAQsGAwILAxcdAgIhA?= =?us-ascii?q?QERAQUBChIGExKKBQEDDQgQjk2RGz+MC4IEBQEcgwkFg2EKGScDClaDSgEBAQE?= =?us-ascii?q?BAQEDAQEBAQEBAQEYAgYSgxaCAoFMgWODJ4JXgkmCZoJhBYgZDIFgjhiHdDyCK?= =?us-ascii?q?IUsh3iEdoIQWYESh3GGcow3iB4VH4EVDxcIgTMyISReGoREKh+BdT42AQGIdoE?= =?us-ascii?q?/AQEB?= X-IPAS-Result: =?us-ascii?q?A0BGAgCL+pZZh6ncVdFcHAEBBAEBCgEBFgEBAQMBAQEJAQE?= =?us-ascii?q?Bg1Q/gQITB4UmmHiBboJGk1aCEiyFGwKDZQdBFgEBAQEBAQEBAQEBEgEBAQgNC?= =?us-ascii?q?QgoL4IzBQMEHoI8AQICASMdARsSCwEDAQsGAwILAxcdAgIhAQERAQUBChIGExK?= =?us-ascii?q?KBQEDDQgQjk2RGz+MC4IEBQEcgwkFg2EKGScDClaDSgEBAQEBAQEDAQEBAQEBA?= =?us-ascii?q?QEYAgYSgxaCAoFMgWODJ4JXgkmCZoJhBYgZDIFgjhiHdDyCKIUsh3iEdoIQWYE?= =?us-ascii?q?Sh3GGcow3iB4VH4EVDxcIgTMyISReGoREKh+BdT42AQGIdoE/AQEB?= X-IronPort-AV: E=Sophos;i="5.41,393,1498514400"; d="scan'208,217";a="234754505" Received: from mail-qk0-f169.google.com ([209.85.220.169]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 18 Aug 2017 16:36:49 +0200 Received: by mail-qk0-f169.google.com with SMTP id 130so19077554qkg.2 for ; Fri, 18 Aug 2017 07:36:49 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc; bh=M9EeOlF7IGaXrWsVwb2NvD4U8T5RILzVMWf429UwfZ0=; b=A53s0ZUG2cwlkYF+5YB0pVKGRe0CJ/zg6ZVKK/BLDDdCLAY0my7R14leCUpgJg+ND3 qfI599MxDncLUSRx7qX3LcrdOkh/8iGjAsFAOa/x/vwjAfOkl96Intl+8PQFB7AfYikj UGPVtmRDSaPSrhBFzEYPx/iGeQ8T83xjBHvVh0FTO+ItmAIBISjwwdq290m1CCuPdEEP twqULwZhBo3SXeOitCWvYNvoOiv8vURBCFVwMfbDQSMeUQ34UWOH0nIq1LKRaxpgn1HO mNUZf1hARjs7TNYLlYUIwg9nEcG9Az0BHH79gdmsoIcoOv+ihRvMsBOhZYKj40w8gKm2 X95Q== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:mime-version:in-reply-to:references:from:date :message-id:subject:to:cc; bh=M9EeOlF7IGaXrWsVwb2NvD4U8T5RILzVMWf429UwfZ0=; b=KYnDBuzQKAvpF2lGJu3Y9w0F6DEs7d9oJ8AUuv33ytx11GWJ37cocjZeu1SiNu3o2Q GYanWKMVwwFKDjOS6B8N9BIIEm3RFTlUwMMwOr/6p8YV2FFDFRn1WQxV8ls3roON6sVT y+vJFe1fnaesxFLh0R02vcho15QnBfNaEF3lC6jutftXWLSlQ/KprdvI6b4ChcE8Qe4V COwE2q0Cm2z15F+lgrl0j9N2s+t2wT7u9Oyt+RgnBxZOaZ0gxm96SQE6xuT5OnpM6eHC Z5EIEtDI1k2ozUNHIULAoRM+2+wVBaBSlAOxFn5Z9xQOZ1KBqb1j/zCLhnMtKC11nju+ 1u2Q== X-Gm-Message-State: AHYfb5hoCIiRFpyqjn7P2O9ne4jAjGZ4qLMGmBcRb/goUxSXxi9t9Xr9 62cPZ44FCBO8Gu4Kb342TYGF/oAI6w== X-Received: by 10.55.161.131 with SMTP id k125mr5299042qke.321.1503067008267; Fri, 18 Aug 2017 07:36:48 -0700 (PDT) MIME-Version: 1.0 Received: by 10.12.184.148 with HTTP; Fri, 18 Aug 2017 07:36:07 -0700 (PDT) In-Reply-To: References: From: Gabriel Scherer Date: Fri, 18 Aug 2017 16:36:07 +0200 Message-ID: To: Alexey Egorov Cc: caml users Content-Type: multipart/alternative; boundary="94eb2c07710c19fad80557080fb0" Subject: Re: [Caml-list] strange type error with -principal --94eb2c07710c19fad80557080fb0 Content-Type: text/plain; charset="UTF-8" These errors on "ambiguous" types come from GADT type checking, which requires annotations in certain places (-principal is more picky about requiring more annotations; instead sometimes the type-checker makes guesses). Currently the syntactic forms let : = in and let : = in are not desugared in the same way. The first is turned into let = ( : ) in and the second into let ( : ) = in In the first case (let ), the body of the definition gets the annotation. This is required, in your code, for this body to compile under -principal. In the second case (let ), the body does not get the annotation, so type-checking fails (under -principal). You can fix it yourself by adding the annotation on the right-hand-side directly let (op, idx) = (begin match ... end : int op * int) in fact it suffices to write (op : int op), 2 in the second clause's right-hand-side. I don't know whether (let : = in ) could instead be desugared into (let ( : : ) in ), which would also fix the issue. The specifics of how type information is propagated in the type-checker is a delicate design aspect of the type-checker which may still evolve in the future. If you wonder what the error message means, you should read the GADT section in the Reference Manual, and in particular the "type inference" subsection (but it depends on the text before it): http://caml.inria.fr/pub/docs/manual-ocaml-4.05/extn.html#sec236 The problem is that within the Op clause, we know the type equality (a = int), but this is not true outside the clause; so when a value that has both types (a op) and (int op) is returned by the clause, the type-checker cannot know which type to give to the outside (a op, or int op?), and it needs an explicit annotation to not make an arbitrary (non-principal) choice. On Fri, Aug 18, 2017 at 4:09 PM, Alexey Egorov wrote: > Hello, > > I'm getting very confusing error when compiling with -principal: > > > Error: This expression has type int op > > but an expression was expected of type 'a > > This instance of int is ambiguous: > > it would escape the scope of its equation > > What is the "instance of int"? > > Here is the code - https://pastebin.com/T74haahx > I'm mostly confused by the fact that changing pattern from (op, idx) > to simple value binding eliminates this error. > > Thanks! > > -- > 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 > --94eb2c07710c19fad80557080fb0 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
These errors on "ambiguous" = types come from GADT type checking, which requires annotations in certain p= laces (-principal is more picky about requiring more annotations; instead s= ometimes the type-checker makes guesses).

Currently the syntac= tic forms
=C2=A0 let <variable> : <type> =3D <expr> in= <expr>
and
=C2=A0 let <pattern> : <type&g= t; =3D <expr> in <expr>
are not desugared in the = same way. The first is turned into
=C2=A0 let <variable>= ; =3D (<expr> : <type>) in <expr>
and the s= econd into
=C2=A0 let (<pattern> : <type>) =3D &l= t;expr> in <expr>

In the first case (let <var= iable>), the body of the definition gets the annotation. This is require= d, in your code, for this body to compile under -principal. In the second c= ase (let <pattern>), the body does not get the annotation, so type-ch= ecking fails (under -principal).

You can fix it yourself = by adding the annotation on the right-hand-side directly

=C2=A0 let = (op, idx) =3D (begin match ... end : int op * int)

in fac= t it suffices to write (op : int op), 2 in the second clause's right-ha= nd-side.

I don't know whether (let <pattern> : = <type> =3D <expr> in <expr>) could instead be desugared i= nto
(let (<pattern> : <type) =3D (<expr> : <= ;type>) in <expr>), which would also fix the issue. The specifics = of how type information is propagated in the type-checker is a delicate des= ign aspect of the type-checker which may still evolve in the future.
If you wonder what the error message means, you should read the= GADT section in the Reference Manual, and in particular the "type inf= erence" subsection (but it depends on the text before it):
=C2=A0 <= a href=3D"http://caml.inria.fr/pub/docs/manual-ocaml-4.05/extn.html#sec236"= >http://caml.inria.fr/pub/docs/manual-ocaml-4.05/extn.html#sec236
The problem is that within the Op clause, we know the type equ= ality (a =3D int), but this is not true outside the clause; so when a value= that has both types (a op) and (int op) is returned by the clause, the typ= e-checker cannot know which type to give to the outside (a op, or int op?),= and it needs an explicit annotation to not make an arbitrary (non-principa= l) choice.

On Fri, Aug 18, 2017 at 4:09 PM, Alexey Egorov &= lt;alex.only.d@g= mail.com> wrote:
Hello,
I'm getting very confusing error when compiling with -principal:

> Error: This expression has type int op
>=C2=A0 =C2=A0 =C2=A0 =C2=A0but an expression was expected of type '= a
>=C2=A0 =C2=A0 =C2=A0 =C2=A0This instance of int is ambiguous:
>=C2=A0 =C2=A0 =C2=A0 =C2=A0it would escape the scope of its equation

What is the "instance of int"?

Here is the code - https://pastebin.com/T74haahx
I'm mostly confused by the fact that changing pattern from (op, idx)
to simple value binding eliminates this error.

Thanks!

--
Caml-list mailing list.=C2=A0 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

--94eb2c07710c19fad80557080fb0--