From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <rathereasy@gmail.com>
Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82])
	by yquem.inria.fr (Postfix) with ESMTP id D4A04BC57
	for <caml-list@yquem.inria.fr>; Sat,  4 Dec 2010 21:54:20 +0100 (CET)
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: AqYAAL44+kxKfVK0k2dsb2JhbACjJggVAQEBAQkJCgkRBB6lNYlpghmEBy6IVgEBAwWFRASEX4YPhgU
X-IronPort-AV: E=Sophos;i="4.59,299,1288566000"; 
   d="scan'208";a="91294428"
Received: from mail-wy0-f180.google.com ([74.125.82.180])
  by mail1-smtp-roc.national.inria.fr with ESMTP; 04 Dec 2010 21:54:20 +0100
Received: by wyb29 with SMTP id 29so5930166wyb.39
        for <caml-list@yquem.inria.fr>; Sat, 04 Dec 2010 12:54:20 -0800 (PST)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
        d=gmail.com; s=gamma;
        h=domainkey-signature:mime-version:received:received:in-reply-to
         :references:date:message-id:subject:from:to:cc:content-type;
        bh=zHM37X+VCQ535PNP56k4IaGhl6BXXU0yFRKd+bGWO2c=;
        b=AM6aKky9vSyIL2POkbR2XFbidOfyLINXItla/TxNW4tLbegGWW53lCl6UwTTJ/Fpz3
         Kg9g7Qz5wfoEjIcU6z9Ws1cVnujX4Co3ibVmu1ze6ABQGbN2at5VWeRjfmRHxKxkOqrR
         YRIHMaqXMgWBfVBNqvIWPZ4iivaXPMKll0syc=
DomainKey-Signature: a=rsa-sha1; c=nofws;
        d=gmail.com; s=gamma;
        h=mime-version:in-reply-to:references:date:message-id:subject:from:to
         :cc:content-type;
        b=JWJNppNGtCk81oGtqE1sCPxT4U4wp69FmIErbZf7XmKFRmxBpHXjGuhPBGY49SLv6y
         3e+X5iLCYlRfB33eblSZ4MSRofJrYHi9gZM/eowlC8Z/jMUCo505ymzf0g4NavbTThk0
         4XuPrHXJ6OQHCVCI1YstxNrr4vvsg+ukCe5EY=
MIME-Version: 1.0
Received: by 10.227.141.137 with SMTP id m9mr3640005wbu.115.1291496060182;
 Sat, 04 Dec 2010 12:54:20 -0800 (PST)
Received: by 10.227.11.71 with HTTP; Sat, 4 Dec 2010 12:54:20 -0800 (PST)
In-Reply-To: <AANLkTi=brs65VkfeM0qt+fLFVd=Vc7PMm809VstVN=Q-@mail.gmail.com>
References: <AANLkTimVTv7J_b6AY1gKKT9hdQx83a+4FBM7pqvHpAHM@mail.gmail.com>
	<AANLkTimmAMG_1+UhNh+Q8bR22XsDtoF44gDd7YEwx5v+@mail.gmail.com>
	<AANLkTim5uyeAXwSzvsVtDyQi28kqdKfE2hDOeCnRW+4Z@mail.gmail.com>
	<AANLkTi=brs65VkfeM0qt+fLFVd=Vc7PMm809VstVN=Q-@mail.gmail.com>
Date: Sat, 4 Dec 2010 15:54:20 -0500
Message-ID: <AANLkTin9Bdea8CZjx3OR1NsFFawSu7G8KGD_ZiTvGr1S@mail.gmail.com>
Subject: Re: [Caml-list] GADT constructor syntax
From: Jacques Le Normand <rathereasy@gmail.com>
To: Lukasz Stafiniak <lukstafi@gmail.com>
Cc: caml-list caml-list <caml-list@yquem.inria.fr>
Content-Type: text/plain; charset=ISO-8859-1
X-Spam: no; 0.00; syntax:01 constructors:01 constructors:01 unifying:01 lukasz:01 foo:01 forall:01 foo:01 wrote:01 wrote:01 caml-list:01 constructor:01 constructor:01 int:01 explicitly:02 

you may want to name your type parameters because you can mix GADT
constructors with normal constructors. consider:

type 'a term =
     | Ignore of 'a term : int term
     | Embed of 'a

I don't think propagating type parameters is a good idea. The current
rule is: ignore type parameters in GADT constructors. This is simpler
than unifying the type parameters with the arguments of the return
type of the constructor.

On Sat, Dec 4, 2010 at 3:22 PM, Lukasz Stafiniak <lukstafi@gmail.com> wrote:
> On Sat, Dec 4, 2010 at 9:14 PM, Jacques Le Normand <rathereasy@gmail.com> wrote:
>>
>> having
>>
>> type 'a t = Foo of 'a : 'b t
>>
>> creating a constructor of type forall 'a. 'a -> 'a t is really
>> confusing since the user explicitly gave the return type of the
>> constructor as 'b t.
>
> But why would the user have named 'a in the first place then. In the
> context of Foo, it should be assumed that
>
> 'a t = 'b t
>