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 CF7947F84F for ; Sun, 23 Feb 2014 10:18:27 +0100 (CET) Received-SPF: None (mail3-smtp-sop.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=mail3-smtp-sop.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 (mail3-smtp-sop.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=mail3-smtp-sop.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 (mail3-smtp-sop.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=mail3-smtp-sop.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: AlsCAO+7CVOFBoIFdGdsb2JhbABZxGyBGw4BDBUIPIIlAQEEAToJATUCAwsLNAcLVwYuh2IHpiqEXQKWRIZbEAeOMTMHgySBFIlKjm6UFoFN X-IPAS-Result: AlsCAO+7CVOFBoIFdGdsb2JhbABZxGyBGw4BDBUIPIIlAQEEAToJATUCAwsLNAcLVwYuh2IHpiqEXQKWRIZbEAeOMTMHgySBFIlKjm6UFoFN X-IronPort-AV: E=Sophos;i="4.97,528,1389740400"; d="scan'208";a="50120627" Received: from rabbit.math.nagoya-u.ac.jp (HELO mailhost.math.nagoya-u.ac.jp) ([133.6.130.5]) by mail3-smtp-sop.national.inria.fr with ESMTP; 23 Feb 2014 10:18:25 +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 66D4F63B8; Sun, 23 Feb 2014 18:18:21 +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 C6A52410F; Sun, 23 Feb 2014 18:18:20 +0900 (JST) DomainKey-Signature: h=Received:Subject:Mime-Version:Content-Type:From:In-Reply-To:Date:Cc:Content-Transfer-Encoding:Message-Id:References:To:X-Mailer; b=; c=nofws; d=math.nagoya-u.ac.jp; q=; s=alpha Received: from tanpopo.garrigue.jp (58x158x128x157.ap58.ftth.ucom.ne.jp [58.158.128.157]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTPSA id 327F04109; Sun, 23 Feb 2014 18:18:20 +0900 (JST) Mime-Version: 1.0 (Mac OS X Mail 7.1 \(1827\)) Content-Type: text/plain; charset=us-ascii From: Jacques Garrigue In-Reply-To: <20140222175435.GA21007@frosties> Date: Sun, 23 Feb 2014 18:18:19 +0900 Cc: OCaml Mailing List Content-Transfer-Encoding: quoted-printable Message-Id: References: <20140222175435.GA21007@frosties> To: Goswin von Brederlow X-Mailer: Apple Mail (2.1827) Subject: Re: [Caml-list] Error: In this definition, a type variable cannot be deduced from the type parameters On 2014/02/23 02:54, Goswin von Brederlow wrote: > Hi, >=20 > I'm stuck trying to solve this error: >=20 > Error: In this definition, a type variable cannot be deduced > from the type parameters. >=20 > The error happens when I use the "type 'a node =3D InnerNode.t" from the > comment and disapears when I box it in a constructor as shown below. >=20 > Can anyone explain what is missing that makes the extra constructor > necessary? >=20 > MfG > Goswin >=20 > PS: needs and must work with ocaml 4.01. Actually it seems that you have already found the solution: if a type variable appears in the return type of a gadt, and is used in the body, injectivity under invariance must be guaranteed for this retur= n type. This is the famous PR#5985. Injectivity is broken if the type variable can disappear by expanding any abbreviation in the type, such as node in your case. By making node a nominal type, you prevented that. Note that using a private abbreviation would not be sufficient here, as a private abbreviation can be used to hide a normal abbreviation. If you dislike the change in internal representation for node, you can also define a separate type for the gadt parameter. Except in very specific cases, there is no strong reason for the gadt parameter type and the concrete type to coincide. Jacques=