From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: 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 B51867EE25 for ; Fri, 25 Oct 2013 14:26:27 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of gabriel.scherer@gmail.com) identity=pra; client-ip=209.85.215.174; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of gabriel.scherer@gmail.com designates 209.85.215.174 as permitted sender) identity=mailfrom; client-ip=209.85.215.174; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@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-ea0-f174.google.com) identity=helo; client-ip=209.85.215.174; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="postmaster@mail-ea0-f174.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AkkCAAFialLRVdeum2dsb2JhbABZgz9Uq2qKGIhHgRoIFg4BAQEBAQYLCwkUKIIlAQEEAScZARsSCwEDDAYFCxohIgERAQUBChIGExKHYgEDCQYNmx2MVoMKhC0KGScDCmSJAQEFDIxxglIEB4QsA5gKgS+ObBgphFM6 X-IPAS-Result: AkkCAAFialLRVdeum2dsb2JhbABZgz9Uq2qKGIhHgRoIFg4BAQEBAQYLCwkUKIIlAQEEAScZARsSCwEDDAYFCxohIgERAQUBChIGExKHYgEDCQYNmx2MVoMKhC0KGScDCmSJAQEFDIxxglIEB4QsA5gKgS+ObBgphFM6 X-IronPort-AV: E=Sophos;i="4.93,570,1378850400"; d="scan'208";a="31866342" Received: from mail-ea0-f174.google.com ([209.85.215.174]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 25 Oct 2013 14:26:27 +0200 Received: by mail-ea0-f174.google.com with SMTP id z15so573985ead.5 for ; Fri, 25 Oct 2013 05:26:26 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type; bh=u6MKd50qMCQ2M/b1dIM5SDH4Es2EUzwNM/CBQawvGJk=; b=c4Ejy1YkLwaSVgoQpy2Xj+nRS0qSH9g+4BhimBOle1pV5qhhKCRLsqWHZP7jWzHY2c Fj0erwIWw4lCVnXsicXmloOhQPrF0p9AEGlNrEa/DW5xX6PE8Kfe2w0sbPhLrt1ZVbU0 WqY01+nWOAjuooMb3WMErhOwspePYfbZxR6oEATDzRdjZzrrkGHLlJAZITmPOb3KxZa4 LbkJfr3tCxji+7/AYMftUNFd80tzSuzhv1QETyCbnce+4qe3PHZYtxElpTVhIB1+/pxV qNpsPJjZuHoz8PtSkbz8TXDXf/yi0x+xModcbT0QbSShBMxivwzD6gWeNW7wekJROydt Nr/Q== X-Received: by 10.204.226.71 with SMTP id iv7mr13220bkb.32.1382703986669; Fri, 25 Oct 2013 05:26:26 -0700 (PDT) MIME-Version: 1.0 Received: by 10.204.122.72 with HTTP; Fri, 25 Oct 2013 05:25:46 -0700 (PDT) In-Reply-To: <526A5F2A.6060904@labri.fr> References: <526A5F2A.6060904@labri.fr> From: Gabriel Scherer Date: Fri, 25 Oct 2013 14:25:46 +0200 Message-ID: To: David RENAULT Cc: caml users Content-Type: multipart/alternative; boundary=485b3970d160f4a40604e98fdb20 Subject: Re: [Caml-list] GADTs : a type variable cannot be deduced --485b3970d160f4a40604e98fdb20 Content-Type: text/plain; charset=ISO-8859-1 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). On Fri, Oct 25, 2013 at 2:08 PM, David RENAULT wrote: > > 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 > > -- > Caml-list mailing list. Subscription management and archives: > https://sympa.inria.fr/sympa/arc/caml-list > Beginner's list: http://groups.yahoo.com/group/ocaml_beginners > Bug reports: http://caml.inria.fr/bin/caml-bugs > --485b3970d160f4a40604e98fdb20 Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable
The problem is with the assumed injectivity= of the abstract type 'a succ. You should write:

=A0 type = 'a succ =3D Succ

then everything works out.

Injecti= vity was assumed to hold for types *defined* to be abstract, but does not h= old 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 us= e a constructor for that (using a constructor makes your type nominal/gener= ative/fresh, which enforces injectivity).

Remark: I'll let you work out while it would be problematic t= o consider a ('a succ succ nat)-matching branch as dead when matching o= ver a ('a succ nat) value, under the definition (type 'a succ =3D i= nt).


On Fri, Oct 25, 2013 at 2:08 PM, David= RENAULT <renault@labri.fr> wrote:

=A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 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 =3D
=A0 | Zero : zero nat
=A0 | 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
=A0 =A0 =A0 =A0from 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 =3D
=A0 | Zero : zero nat
=A0 | Succ : _ nat -> (_ succ) nat
(* type _ nat =3D Zero : zero nat | Succ : 'b nat -> 'a succ nat= *)

Succ Zero;; (* 'a succ nat =3D 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/testsui= te/tests/typing-gadts/pr5985.ml

Is the code I am writing incorrect ? (for reference, the same code in
Haskell (with ghc) works as expected)

=A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 RENAULT David

--
Caml-list mailing list. =A0Subscription management and archives:
ht= tps://sympa.inria.fr/sympa/arc/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs

--485b3970d160f4a40604e98fdb20--