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 4EC41801CD for ; Fri, 18 Aug 2017 17:24:01 +0200 (CEST) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=alex.only.d@gmail.com; spf=Pass smtp.mailfrom=alex.only.d@gmail.com; spf=None smtp.helo=postmaster@mail-io0-f178.google.com Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of alex.only.d@gmail.com) identity=pra; client-ip=209.85.223.178; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="alex.only.d@gmail.com"; x-sender="alex.only.d@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of alex.only.d@gmail.com designates 209.85.223.178 as permitted sender) identity=mailfrom; client-ip=209.85.223.178; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="alex.only.d@gmail.com"; x-sender="alex.only.d@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-io0-f178.google.com) identity=helo; client-ip=209.85.223.178; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="alex.only.d@gmail.com"; x-sender="postmaster@mail-io0-f178.google.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3Ak7yXchKY+sgVih1VGNmcpTZWNBhigK39O0sv0rFi?= =?us-ascii?q?tYgUKPnxwZ3uMQTl6Ol3ixeRBMOAtKIC1rKempujcFJDyK7JiGoFfp1IWk1Nou?= =?us-ascii?q?QttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBX660e/5j8KGxj5KRE9?= =?us-ascii?q?ZqGsQtaT3PKMyvuq9pbPTwJNjTu7KfMufVTl5TnW4+Yfi5FjJ6J58RDJr2FFYa?= =?us-ascii?q?wCympiP1Oem1Dn7ce95pN52ytVsvMlscVHVPOpUb4/SOlxCDk2PnF9ycLsrx7d?= =?us-ascii?q?BV+G4nYMFGIQlgsODyDK6Rj7WtH6tS6s5bk14zWTIcCjFeN8Yj+l9ao+DUKxhQ?= =?us-ascii?q?=3D=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0AsAQARBpdZhrLfVdFdGgEBAQECAQEBA?= =?us-ascii?q?QgBAQEBFQEBAQECAQEBAQgBAQEBg1Q0C4ECEweeHoFugkaVaCyFFwICAoNlB0I?= =?us-ascii?q?VAQEBAQEBAQEBAQESAQEBCAsLCCgvgjMFAR4GgjwBAgMjHQEbEgsBAwwGBQsNA?= =?us-ascii?q?gIJHQICIQEBEQEFAQoSBhMSigUBAwgNEKAKP4wLggQFARyDCQWDYQoZJwMKVoN?= =?us-ascii?q?KAQEBAQEBAQMBAQEBAQEBGQIGEnmCHYICM4J8gyeCV4UvgmEFiBkMigCNbDyHV?= =?us-ascii?q?Id4hHaCEFmJA4ZyjDeIHhUfgRU1gSwyISReGoRuH4F6OTYBAYhigVMBAQE?= X-IPAS-Result: =?us-ascii?q?A0AsAQARBpdZhrLfVdFdGgEBAQECAQEBAQgBAQEBFQEBAQE?= =?us-ascii?q?CAQEBAQgBAQEBg1Q0C4ECEweeHoFugkaVaCyFFwICAoNlB0IVAQEBAQEBAQEBA?= =?us-ascii?q?QESAQEBCAsLCCgvgjMFAR4GgjwBAgMjHQEbEgsBAwwGBQsNAgIJHQICIQEBEQE?= =?us-ascii?q?FAQoSBhMSigUBAwgNEKAKP4wLggQFARyDCQWDYQoZJwMKVoNKAQEBAQEBAQMBA?= =?us-ascii?q?QEBAQEBGQIGEnmCHYICM4J8gyeCV4UvgmEFiBkMigCNbDyHVId4hHaCEFmJA4Z?= =?us-ascii?q?yjDeIHhUfgRU1gSwyISReGoRuH4F6OTYBAYhigVMBAQE?= X-IronPort-AV: E=Sophos;i="5.41,393,1498514400"; d="scan'208";a="287525311" Received: from mail-io0-f178.google.com ([209.85.223.178]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 18 Aug 2017 17:23:59 +0200 Received: by mail-io0-f178.google.com with SMTP id m88so33861053iod.2 for ; Fri, 18 Aug 2017 08:23:59 -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=dYwVBVdhwX9Gvjr0A87JO1/o6MSPa48OwWipV9t/VUI=; b=nwpo19FLtGb4wTGEQwb+VoMePb5MsHJ19u7QuTOZColplxVN2Qv0V+Q91PBBzfUbic XPVkKYmo69C9x9ML/RRGK0GMoM8H4T4Qopo1Hu9ODtOp/DzKklqbLYkv0bVKBqCXBkQE A161IWKeiN/D1oChzyE/AgzA2t0J+d5vBNS9j4Y9iCfo82Y9EpzYkUbU6B/iPU0DWbUh Y+kfUYiImlORtppEel+tvF2ihxirHg03AA8E8/xbBRSl+vMjYbuwcK7Y1D+Sxvtt6KOA 9V4UgsAlaZQrdkw4NMOSmVTLUJS/lKTodDLulnkueuVJw9Uf96iw4drwSuA7pfTg1ZU6 M7VA== 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=dYwVBVdhwX9Gvjr0A87JO1/o6MSPa48OwWipV9t/VUI=; b=pe2eXLOJ9tMHKqVCCwS+iKBAtfHmEkuTTnKmgYWkXfCv2D4yHGwEKF92ksEWrqpUDV iEVS+pLnqVjdIfAWHNqloTrnELM9SXpkIeB8AH6sqDvE2VB9AtVbknjbxk11/q5tLsdD y1EIn98JqmeYsxgaSSysHn/DRu0ORz22NwJSTxBJ0E9sGVL+adjf6in4u7giwY44ol08 jY39niSRejBYE2KuF0MfProTSN1MgFlH65jzZ5PFDTY00WSYK7zdX1GPXLOPNrHPRWTO ICv8uLCWw/8aS9RDnPA3mJgXLTfRpkClwba7+2aRcdDXZHJnDsige8Lu4a/pnk65XxHK a0ww== X-Gm-Message-State: AHYfb5i4XWLciZsbB7YXlZQ/abhcyI9KaiDdT0/uSNDgnuxjKSP7VJ5N TW9QbFFtJTq0vruYb0isrymOnL/qNA== X-Received: by 10.107.179.135 with SMTP id c129mr8704668iof.106.1503069837955; Fri, 18 Aug 2017 08:23:57 -0700 (PDT) MIME-Version: 1.0 Received: by 10.2.77.84 with HTTP; Fri, 18 Aug 2017 08:23:57 -0700 (PDT) In-Reply-To: References: From: Alexey Egorov Date: Fri, 18 Aug 2017 20:23:57 +0500 Message-ID: To: Gabriel Scherer Cc: caml users Content-Type: text/plain; charset="UTF-8" Subject: Re: [Caml-list] strange type error with -principal Thanks for explanation! Every problem I've had with GADTs was solved placing an annotation in the right place... 2017-08-18 19:36 GMT+05:00 Gabriel Scherer : > 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 > >