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 4BE917EE25 for ; Tue, 29 Oct 2013 15:17:31 +0100 (CET) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of renault@labri.fr) identity=pra; client-ip=147.210.8.143; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="renault@labri.fr"; x-sender="renault@labri.fr"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of renault@labri.fr designates 147.210.8.143 as permitted sender) identity=mailfrom; client-ip=147.210.8.143; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="renault@labri.fr"; x-sender="renault@labri.fr"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of postmaster@iona.labri.fr designates 147.210.8.143 as permitted sender) identity=helo; client-ip=147.210.8.143; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="renault@labri.fr"; x-sender="postmaster@iona.labri.fr"; x-conformance=sidf_compatible; x-record-type="v=spf1" X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: ArIBACHDb1KT0giPnGdsb2JhbABZw0iBKRYOAQEBAQEIFAk8giUBAQUnGQEBNwEPCxgJJQ8CDjgGDQEHAogDphqEUwEFjwYGjxQzB4QsjlaJN4Y8jnM X-IPAS-Result: ArIBACHDb1KT0giPnGdsb2JhbABZw0iBKRYOAQEBAQEIFAk8giUBAQUnGQEBNwEPCxgJJQ8CDjgGDQEHAogDphqEUwEFjwYGjxQzB4QsjlaJN4Y8jnM X-IronPort-AV: E=Sophos;i="4.93,593,1378850400"; d="scan'208";a="39448313" Received: from iona.labri.fr ([147.210.8.143]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 29 Oct 2013 15:17:17 +0100 Received: from localhost (localhost [127.0.0.1]) by iona.labri.fr (Postfix) with ESMTP id C7CE5718D; Tue, 29 Oct 2013 15:17:27 +0100 (CET) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=labri.fr; h= content-transfer-encoding:content-type:content-type:in-reply-to :references:subject:subject:mime-version:user-agent:from:from :date:date:message-id:received:received; s=mail; t=1383056247; x=1384870648; bh=3V0kDruq3xPlgoCVYRYpf/Dg/OAIeRhCDMdrlmr/Qwk=; b= rvavRGI6KTYhx7zPCXkGFSXbk+7F/oGx2xQO058HTH6uH/w4yu6d8tkp3IHP78d/ gUTvYcievy325Y2DGzgL2qXeAEvos7rzt85LFPIO9zdEwFe0RM5dk9EJWn7NBzN2 MPYVw7mEBxmnDblf5ntv2RsyuVAoerps6UImODUupw0= X-Virus-Scanned: amavisd-new at labri.fr Received: from iona.labri.fr ([127.0.0.1]) by localhost (iona.labri.fr [127.0.0.1]) (amavisd-new, port 10027) with LMTP id cWsRrqcoi2dM; Tue, 29 Oct 2013 15:17:27 +0100 (CET) Received: from [147.210.8.54] (aigrette.labri.fr [147.210.8.54]) (using TLSv1 with cipher DHE-RSA-CAMELLIA256-SHA (256/256 bits)) (Client did not present a certificate) by iona.labri.fr (Postfix) with ESMTPSA id A588938FF; Tue, 29 Oct 2013 15:17:27 +0100 (CET) Message-ID: <526FC379.30506@labri.fr> Date: Tue, 29 Oct 2013 15:17:29 +0100 From: David RENAULT User-Agent: Mozilla/5.0 (X11; Linux i686; rv:24.0) Gecko/20100101 Firefox/24.0 SeaMonkey/2.21 MIME-Version: 1.0 To: Gabriel Scherer CC: caml users References: <526A5F2A.6060904@labri.fr> In-Reply-To: X-Enigmail-Version: 1.5.2 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit Subject: Re: [Caml-list] GADTs : a type variable cannot be deduced Gabriel Scherer wrote: > The problem is with the assumed injectivity of the abstract type 'a > succ. You should write: > > type 'a succ = Succ > > then everything works out. > > Injectivity was assumed to hold for types *defined* to be abstract, but > does not hold for types *declared* as abstract (That may have been > defined concretely as just "int" in their implementation). For > consistency, defined-abstract type are no more assumed to be injective, > so you should always use a constructor for that (using a constructor > makes your type nominal/generative/fresh, which enforces injectivity). > > Remark: I'll let you work out while it would be problematic to consider > a ('a succ succ nat)-matching branch as dead when matching over a ('a > succ nat) value, under the definition (type 'a succ = int). OK, thank you for your answer, I have taken some time to dive into the question of injectivity of types, and I believe that there is something I am missing. With your help, the following code compiles : ==================================================================== type 'a succ = Succ type _ nat = NS : 'a nat -> ('a succ) nat ==================================================================== If we leave the type abstract, then the type function NS may not be injective. But if we give a concrete implementation with a constructor, it works out. To me, the concrete implementation is not injective (it maps everything on "Succ nat"), but you proclaim that it becomes automatically injective. Why does mapping everything onto a new type enforce injectivity ? RENAULT David