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 950D6801CD for ; Tue, 29 Aug 2017 21:13:41 +0200 (CEST) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=stecksoft@gmail.com; spf=Pass smtp.mailfrom=stecksoft@gmail.com; spf=None smtp.helo=postmaster@mail-pg0-f53.google.com Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of stecksoft@gmail.com) identity=pra; client-ip=74.125.83.53; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="stecksoft@gmail.com"; x-sender="stecksoft@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of stecksoft@gmail.com designates 74.125.83.53 as permitted sender) identity=mailfrom; client-ip=74.125.83.53; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="stecksoft@gmail.com"; x-sender="stecksoft@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-pg0-f53.google.com) identity=helo; client-ip=74.125.83.53; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="stecksoft@gmail.com"; x-sender="postmaster@mail-pg0-f53.google.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3AcrJFDhzDbK8xmMrXCy+O+j09IxM/srCxBDY+r6Qd?= =?us-ascii?q?0uwUIJqq85mqBkHD//Il1AaPBtqLra8cw8Pt8IneGkU4qa6bt34DdJEeHzQksu?= =?us-ascii?q?4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2NBXupSi55DsWXxH+LhZd?= =?us-ascii?q?J+LvG4eUgd7k+fq1/siZWwxVgHKUJ/tJMBi9rgHcrINe1ZB+J60y4gDVr3BLYO?= =?us-ascii?q?NY2SVjIlfFzEW03du54JM2q3cYgPkm7cMVCag=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0DIBACXu6VZhjVTfUpdHRgHDBgHg0g/g?= =?us-ascii?q?RUHg3CaNzgJBoEmmGmJLAdCFQEBAQEBAQEBAQEBEgEBAQgLCwgoL4IzIoJtBBk?= =?us-ascii?q?BOQMNBRAPAiYCJBIBBQGKTgMIDRCeZoNFQIwLgW06gwkFhAMnDYRFAgYSe4Idg?= =?us-ascii?q?gKBB4Ujg1WCG4JHgmEFoGgCgWmFboxzkmuUeRUfgRU1gS93FWMGgx6BCgELAUM?= =?us-ascii?q?cggMkNgGLUwEBAQ?= X-IPAS-Result: =?us-ascii?q?A0DIBACXu6VZhjVTfUpdHRgHDBgHg0g/gRUHg3CaNzgJBoE?= =?us-ascii?q?mmGmJLAdCFQEBAQEBAQEBAQEBEgEBAQgLCwgoL4IzIoJtBBkBOQMNBRAPAiYCJ?= =?us-ascii?q?BIBBQGKTgMIDRCeZoNFQIwLgW06gwkFhAMnDYRFAgYSe4IdggKBB4Ujg1WCG4J?= =?us-ascii?q?HgmEFoGgCgWmFboxzkmuUeRUfgRU1gS93FWMGgx6BCgELAUMcggMkNgGLUwEBA?= =?us-ascii?q?Q?= X-IronPort-AV: E=Sophos;i="5.41,445,1498514400"; d="scan'208";a="235660608" Received: from mail-pg0-f53.google.com ([74.125.83.53]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 29 Aug 2017 21:13:40 +0200 Received: by mail-pg0-f53.google.com with SMTP id 63so13368764pgc.2 for ; Tue, 29 Aug 2017 12:13:40 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:sender:from:date:message-id:subject:to; bh=6nrrUL/GRXeLHZCfIjvpFWxQ7R/4F0fill8rp36eq6s=; b=APwtrlNV68Li9t3y8CiP5LUdI6BwjVn3aiNDMYnkm0c2NwQLxWrgRYj53sXQLQnsLw tykKbI6WrNQHLU8O/YziZ+iBQRpsgZAqTo/+vPhBm25fijMT/EK7h4WQ+/KMthzvw/UI QA8DzOYvOpbva9Ualwz3LNe05REN5231VMbAC3A+Ynzzc9Gwxa3I1j+B5op9v+BsZuJe wWrQwoY9Om2OHmxulkPSArqtiEt5VZd+1JKY/bgubbyb6zCeVWw3YOVsf17Xhps+1o8T euI9mCFmrO0hyodt+eQzluFPj8lv3BAj9kPBVusX9f6T98l/8YVPwDm8OHVtZpoxp/f6 981A== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:mime-version:sender:from:date:message-id:subject :to; bh=6nrrUL/GRXeLHZCfIjvpFWxQ7R/4F0fill8rp36eq6s=; b=IpwXNXNv+QCway7xm0iJeiO7MTPgh+eowXzonPRwT26AvKF2mXliz7z31CbFiieNpI 6z/N2gI/lJNG42y/eUUZirTNOGvZ1v5NrMWUdGQbg8Gd2u6+WHwkDw2ywnMbGmc1YjKl TdS29LRtBm7z0SsuIiqVaNKq4+rOY18BVWRceyTBCEp3VYMY+q1UyTy0lgmugcICxb0q tLGxE6C6pxoQ4mXXeiSTW5dwiYMXX9dkY267gdu/aLm5Q7lhFg2L/G7+Yiz3TI2wat6E 3OLy2q7XT5sE2FwHDspy7NhSlq7xYn5ltuIebLWMpXY2OlIj0iiJMfsxjwnECFxG95qi ISDQ== X-Gm-Message-State: AHYfb5j4++YqDUDL8XuOdbz591WlAqJle1DHIebrqcnYUIoNM4idZuv9 yTxJqDH9GMByDi21yb/IL0nM9vHxJAWR X-Received: by 10.99.109.202 with SMTP id i193mr1314500pgc.355.1504034018528; Tue, 29 Aug 2017 12:13:38 -0700 (PDT) MIME-Version: 1.0 Sender: stecksoft@gmail.com Received: by 10.100.148.100 with HTTP; Tue, 29 Aug 2017 12:13:08 -0700 (PDT) From: "Paul A. Steckler" Date: Tue, 29 Aug 2017 15:13:08 -0400 X-Google-Sender-Auth: Yj8_ntpALOat_VCT4sE2Tbe55zs Message-ID: To: caml-list@inria.fr Content-Type: text/plain; charset="UTF-8" Subject: [Caml-list] Typing issue in explicit module Here's some code that compiles successfully with 4.05.0 ocamlc. The .ml file is: .ml file: -- type t let id x = x let idid = id id -- .mli file: -- type t val id: 'a -> 'a val idid : t -> t -- If I wrap the code in an explicit module, I get a type error: .ml file: -- module Foo = struct end -- .mli file: -- module Foo : sig end -- With this change made, ocamlc complains: -- Error: The implementation Foo.ml does not match the interface Foo.cmi: In module Foo: Modules do not match: sig type t = Foo.t val id : 'a -> 'a val idid : '_a -> '_a end is not included in sig type t val id : 'a -> 'a val idid : t -> t end In module Foo: Values do not match: val idid : '_a -> '_a is not included in val idid : t -> t -- Adding a type annotation t -> t to the definition of "idid" gets rid of the error. With OCaml 4.04.0, no error occurs, and the type annotation is unnecessary. Is this change expected? The code I've shown is a simplified version of OCaml code extracted from a Coq script, reported as a bug in Coq: https://coq.inria.fr/bugs/show_bug.cgi?id=5705. -- Paul