From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <anders@fugmann.net>
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 42C667F7AF
	for <caml-list@sympa.inria.fr>; Thu,  8 Oct 2015 20:46:52 +0200 (CEST)
IronPort-PHdr: 9a23:2b0pgBD1hctCCA7Sy0XGUyQJP3N1i/DPJgcQr6AfoPdwSP7/osbcNUDSrc9gkEXOFd2CrakU16yJ7uu5AzFIyK3CmU5BWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYsExnyfTB4Ov7yUtaLyZ/ni6btptaKOVgArQH+SI0xBS3+lR/WuMgSjNkqAYcK4TyNnEF1ff9Lz3hjP1OZkkW0zM6x+Jl+73YY4Kp5pIYTGZn9Kq8xSLgdCDU9L0g04tfqvF/NV1ih/HwZB0wQnhdSGED94Q33RN/fryT/v+x7kH2TO8H7V6scVymt6q5tTlnuhTtRZG1xy33elsEl1PETmxmmvREqm4M=
Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=anders@fugmann.net; spf=Pass smtp.mailfrom=anders@fugmann.net; spf=None smtp.helo=postmaster@gw.fugmann.net
Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender
  authenticity information available from domain of
  anders@fugmann.net) identity=pra; client-ip=90.184.182.235;
  receiver=mail3-smtp-sop.national.inria.fr;
  envelope-from="anders@fugmann.net";
  x-sender="anders@fugmann.net"; x-conformance=sidf_compatible
Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of
  anders@fugmann.net designates 90.184.182.235 as permitted
  sender) identity=mailfrom; client-ip=90.184.182.235;
  receiver=mail3-smtp-sop.national.inria.fr;
  envelope-from="anders@fugmann.net";
  x-sender="anders@fugmann.net"; 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@gw.fugmann.net) identity=helo;
  client-ip=90.184.182.235;
  receiver=mail3-smtp-sop.national.inria.fr;
  envelope-from="anders@fugmann.net";
  x-sender="postmaster@gw.fugmann.net";
  x-conformance=sidf_compatible
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: A0BPBgBxuRZW/+u2uFpegnssVG6/MRmCeoIKglQ8EAEBAQEBAQEBgQmCH4IxBBEIAQE2AjQCBRYLAgsDAgECAVgIAogrA64ocYRlAQWPWAaBIo96glKBRZYPhRiKIJlaOCuBSgEKAQEBOR2BVm+HbAEBAQ
X-IPAS-Result: A0BPBgBxuRZW/+u2uFpegnssVG6/MRmCeoIKglQ8EAEBAQEBAQEBgQmCH4IxBBEIAQE2AjQCBRYLAgsDAgECAVgIAogrA64ocYRlAQWPWAaBIo96glKBRZYPhRiKIJlaOCuBSgEKAQEBOR2BVm+HbAEBAQ
X-IronPort-AV: E=Sophos;i="5.17,655,1437429600"; 
   d="scan'208";a="150020393"
Received: from gw.fugmann.net ([90.184.182.235])
  by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/ADH-AES256-GCM-SHA384; 08 Oct 2015 20:46:51 +0200
Received: from [IPv6:2001:470:dc46:1:daa2:5eff:fe95:453e] (zaphod.fugmann.net [IPv6:2001:470:dc46:1:daa2:5eff:fe95:453e])
	(using TLSv1.2 with cipher ECDHE-RSA-AES128-GCM-SHA256 (128/128 bits))
	(No client certificate requested)
	by gw.fugmann.net (Postfix) with ESMTPSA id DF7FB2BAB259
	for <caml-list@inria.fr>; Thu,  8 Oct 2015 20:46:48 +0200 (CEST)
DKIM-Signature: v=1; a=rsa-sha256; c=simple/simple; d=fugmann.net; s=mail;
	t=1444330009; bh=x0SzTUI+1VhYoWJbGV/3cVcHEl5uTC8emlBjdI1ZJnA=;
	h=To:From:Subject:Date:From;
	b=cxKeX7r8a2yFeKoDnvvtVYVXQPL6B9d3AR/xHHHrU9QfPu+Nh3Ar5Hr+qf8/bsy/p
	 Iry9adU+P1tN0vdmu7Y1yfoxsR6Z1qakqSpPEJTNOtAEVG7AjA/LPztBxCUlrKPtL0
	 fVBbS9biOYXC2hHvFu/Grz4BJ9E3NXzDZPiaz7k4=
To: caml-list@inria.fr
From: Anders Peter Fugmann <anders@fugmann.net>
Message-ID: <5616BA18.8000808@fugmann.net>
Date: Thu, 8 Oct 2015 20:46:48 +0200
User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101
 Icedove/38.2.0
MIME-Version: 1.0
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Transfer-Encoding: 7bit
Subject: [Caml-list] Strange Gadt error

Hi,

I the following example (boiled down from a real use case):

type _ elem =
   | Int: int elem

let rec incr: type a. a elem -> a -> int = function
   | Int -> fun i -> add i 1
and add n m = n + m

I get the error (Ocaml 4.02.3):
File "example.ml", line 5, characters 24-25:
Error: This expression has type int but an expression was expected of type
          int
        This instance of int is ambiguous:
        it would escape the scope of its equation

I can get rid of the error by annotating the type of i in line 5 like this:

  | Int -> fun (i : int) -> add i 1
                    ^^^

Or move add above incr like this:

let rec add n m = n + m
and incr: type a. a elem -> a -> int = function
   | Int -> fun i -> add i 1

Is there an explanation to why I need to give the type of i in this 
case? As 'i' _must_ be an int (from the type annotation of incr), 
annotating the function seems ambiguous.

/Anders