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 37E347EF10 for ; Tue, 24 Feb 2015 06:54:43 +0100 (CET) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of garrigue@math.nagoya-u.ac.jp) identity=pra; client-ip=133.6.130.5; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="garrigue@math.nagoya-u.ac.jp"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of garrigue@math.nagoya-u.ac.jp) identity=mailfrom; client-ip=133.6.130.5; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="garrigue@math.nagoya-u.ac.jp"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mailhost.math.nagoya-u.ac.jp) identity=helo; client-ip=133.6.130.5; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="postmaster@mailhost.math.nagoya-u.ac.jp"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0AsAQAVEexUlwWCBoVbhDKDCMYFAoFrAQEBAQEBEAEBAQEBCBYHQoQQAQQBIx0DATUBAQMLCQIaAiYCAlcGE4gnB50qm3xwhGgCjn2EcQEBAQEBAQEDAQEBAQEBAQEBEgEGgSGJcoQ7MweCaC+BFIVnhGeOTIZejFWEHy8xgkMBAQE X-IPAS-Result: A0AsAQAVEexUlwWCBoVbhDKDCMYFAoFrAQEBAQEBEAEBAQEBCBYHQoQQAQQBIx0DATUBAQMLCQIaAiYCAlcGE4gnB50qm3xwhGgCjn2EcQEBAQEBAQEDAQEBAQEBAQEBEgEGgSGJcoQ7MweCaC+BFIVnhGeOTIZejFWEHy8xgkMBAQE X-IronPort-AV: E=Sophos;i="5.09,637,1418079600"; d="scan'208";a="123090530" Received: from rabbit.math.nagoya-u.ac.jp (HELO mailhost.math.nagoya-u.ac.jp) ([133.6.130.5]) by mail2-smtp-roc.national.inria.fr with ESMTP; 24 Feb 2015 06:54:40 +0100 Received: from mailhost.math.nagoya-u.ac.jp (localhost [127.0.0.1]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id 3788A63DE; Tue, 24 Feb 2015 14:54:37 +0900 (JST) Received: from mailhost.math.nagoya-u.ac.jp (localhost [127.0.0.1]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id BFD23395D; Tue, 24 Feb 2015 14:54:36 +0900 (JST) DKIM-Signature: v=1; a=rsa-sha1; c=relaxed; d=math.nagoya-u.ac.jp; h= subject:mime-version:content-type:from:in-reply-to:date:cc :content-transfer-encoding:message-id:references:to; s=alpha; bh=53F6x5yv8/BSqbmv7Udvz0SaECI=; b=Otkow5OnNc5YVDV9jcJ2dTKYd6cU m26B/1qpDCwaNj/0bEUFiGF4QlwgN+EbkSGAtxZxxhMVJO58up0Vf9U7j2ZhZn8J AYkJYZcstunmpR7VRXXf5HBfCNdCC1JavIh0mZyWjqrdwsmrmZI7zM1KY6INsw1f P1sTTS9zR5wupD4= DomainKey-Signature: a=rsa-sha1; h=Received:Subject:Mime-Version:Content-Type:From:In-Reply-To:Date:Cc:Content-Transfer-Encoding:Message-Id:References:To:X-Mailer; b=S7WFvNbHza92xGm4K6mJZ7wjtseWaeQj8eandW7jdJNsi9nLqLzrdwAmzt2OzxPKcjfpxwvNgX4lVtSbxqzVbIuq2Q9ShlZtAi0RjU1khTeuekxytSzJ1ORWUHSl0fUyzeuPYz3Qaqvp0XgX3frdyyhUNLpocXJ8Bhf5EilA2Ng=; c=nofws; d=math.nagoya-u.ac.jp; q=dns; s=alpha Received: from [192.168.1.212] (bsdserver10-alias1.math.nagoya-u.ac.jp [172.16.62.1]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTPSA id 721BF2532; Tue, 24 Feb 2015 14:54:36 +0900 (JST) Mime-Version: 1.0 (Mac OS X Mail 8.2 \(2070.6\)) Content-Type: text/plain; charset=utf-8 From: Jacques Garrigue In-Reply-To: Date: Tue, 24 Feb 2015 14:54:39 +0900 Cc: Carl Eastlund , OCaml Mailing List Content-Transfer-Encoding: quoted-printable Message-Id: <7F37BBAA-D80E-4EE1-BFEE-1136E10A9BB5@math.nagoya-u.ac.jp> References: To: Gabriel Scherer X-Mailer: Apple Mail (2.2070.6) Subject: Re: [Caml-list] Weird type error involving 'include' and applicative functors On 2015/02/24 13:38, Jacques Garrigue wrote: > While logically the T inside C and C.T are the same module, > the typing rule in Leroy's paper do not say anything like that. >=20 > =CF=83 : {1,...,m} =F4=8F=B0=80=E2=86=92 {1,...,n} for all i =E2=88=88 {1= ,...,m}, E;D1;...;Dn =E2=8A=A2 D=CF=83(i) <: Di=E2=80=B2 > -------------------------------------------------------------------------= -------------- > E =E2=8A=A2 sig D1;=E2=80=A6;Dn end <: sig D1=E2=80=B2 ;...;Dm= =E2=80=B2 end >=20 > The definition in the premise must match without extra equations. > Here module aliases do not help. > What could help would be to strengthen the definitions in the premise, so > that T would be converted to C.T. But I don't know whether this is sound > or not, since this is not part of the current theory. More precisely, OCaml actually does a bit more than this rule, as it strengthens abstract types. However there is no such thing as strengthening for module aliases, as this would require having both a signature and an alias for the same module. Allowing that could help solve this problem, but this is not fixing a bug, rather extending the theory. Jacques Garrigue