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 604B67EE25 for ; Fri, 25 Oct 2013 14:08:10 +0200 (CEST) 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: Au8BAEdealKT0giPnGdsb2JhbABZgz+DZ7s2gSIWDgEBAQEBCBQJPIJPBBkBATYCNAIFFgsCCwMCAQIBDUsIAogDDaYadoNdAQWOYwaBKYtUgjkENoJUgUKOVok3gS+FDI50 X-IPAS-Result: Au8BAEdealKT0giPnGdsb2JhbABZgz+DZ7s2gSIWDgEBAQEBCBQJPIJPBBkBATYCNAIFFgsCCwMCAQIBDUsIAogDDaYadoNdAQWOYwaBKYtUgjkENoJUgUKOVok3gS+FDI50 X-IronPort-AV: E=Sophos;i="4.93,570,1378850400"; d="scan'208";a="38769863" Received: from iona.labri.fr ([147.210.8.143]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 25 Oct 2013 14:08:12 +0200 Received: from localhost (localhost [127.0.0.1]) by iona.labri.fr (Postfix) with ESMTP id E42D6551E; Fri, 25 Oct 2013 14:08:09 +0200 (CEST) Authentication-Results: iona.labri.fr (amavisd-new); dkim=pass (1024-bit key) reason="pass (just generated, assumed good)" header.d=labri.fr DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=labri.fr; h= content-transfer-encoding:content-type:content-type:subject :subject:mime-version:user-agent:from:from:date:date:message-id :received:received; s=mail; t=1382702889; x=1384517290; bh=1Xz5p iaUSFfUsu2hcmeW7x8jKyLwBIpVic9Dwmqa94E=; b=rPhtHjAeqSDB377omLJeo eK0zEeJuhU8oNvn3Yni65eDXw37Yx+xtSfrVMiW2S2AEPVMXcj+yoE2AXIWPSzjc f7EcCFyyrG9X4nwR+40L3NN5n9QZBE38myyLyuD5oS5wp/6Ob5/8ZyG6eYweLd2o zzrFpUkBbWkD6r4GJlb2uM= 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 MDE-PdTMD6P2; Fri, 25 Oct 2013 14:08:09 +0200 (CEST) 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 C259D509C; Fri, 25 Oct 2013 14:08:09 +0200 (CEST) Message-ID: <526A5F2A.6060904@labri.fr> Date: Fri, 25 Oct 2013 14:08:10 +0200 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: caml-list@inria.fr X-Enigmail-Version: 1.5.2 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 7bit Subject: [Caml-list] GADTs : a type variable cannot be deduced Hi, I was experimenting on GADTs and phantom types and was using the usual encoding for naturals, as well as a classic implementation of the associated singleton type : type zero type 'a succ type _ nat = | Zero : zero nat | Succ : 'a nat -> ('a succ) nat With ocamlc 4.01.0, this fails to compile with the following error message : Error: In this definition, a type variable cannot be deduced from the type parameters. This is strange, because this code compiled pretty well with ocamlc 4.00.1. Of course, it is possible to modify the code to make it compile by replacing the type variables by underscores, but the resulting type is incorrect : type _ nat = | Zero : zero nat | Succ : _ nat -> (_ succ) nat (* type _ nat = Zero : zero nat | Succ : 'b nat -> 'a succ nat *) Succ Zero;; (* 'a succ nat = Succ Zero, should be "zero succ nat" *) I failed to find in the Changelog the modification that led to this behavior, and nothing really simple about the error message showed up. The following file seems to prove that the problem appears in various other cases : http://caml.inria.fr/svn/ocaml/trunk/testsuite/tests/typing-gadts/pr5985.ml Is the code I am writing incorrect ? (for reference, the same code in Haskell (with ghc) works as expected) RENAULT David