From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <alain@frisch.fr>
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 492A07EE51
	for <caml-list@sympa.inria.fr>; Mon, 29 Apr 2013 13:23:06 +0200 (CEST)
Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender
  authenticity information available from domain of
  alain@frisch.fr) identity=pra; client-ip=193.252.23.212;
  receiver=mail3-smtp-sop.national.inria.fr;
  envelope-from="alain@frisch.fr"; x-sender="alain@frisch.fr";
  x-conformance=sidf_compatible
Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender
  authenticity information available from domain of
  alain@frisch.fr) identity=mailfrom; client-ip=193.252.23.212;
  receiver=mail3-smtp-sop.national.inria.fr;
  envelope-from="alain@frisch.fr"; x-sender="alain@frisch.fr";
  x-conformance=sidf_compatible
Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender
  authenticity information available from domain of
  postmaster@msa.smtpout.orange.fr) identity=helo;
  client-ip=193.252.23.212;
  receiver=mail3-smtp-sop.national.inria.fr;
  envelope-from="alain@frisch.fr";
  x-sender="postmaster@msa.smtpout.orange.fr";
  x-conformance=sidf_compatible
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: Ao4CANhWflHB/BfUcmdsb2JhbABTDoMwu2KCZYEZDgEKCgwJFAMlgh8BAQU4UQsYCSUPAkYGAQwIAQGIFrwCjyGDTwOXHoYTjWlB
X-IPAS-Result: Ao4CANhWflHB/BfUcmdsb2JhbABTDoMwu2KCZYEZDgEKCgwJFAMlgh8BAQU4UQsYCSUPAkYGAQwIAQGIFrwCjyGDTwOXHoYTjWlB
X-IronPort-AV: E=Sophos;i="4.87,572,1363129200"; 
   d="scan'208";a="12583629"
Received: from msa03.smtpout.orange.fr (HELO msa.smtpout.orange.fr) ([193.252.23.212])
  by mail3-smtp-sop.national.inria.fr with ESMTP; 29 Apr 2013 13:23:05 +0200
Received: from [192.168.1.106] ([86.195.153.11])
	by mwinf5d61 with ME
	id VnP41l0030F12tA03nP4Rq; Mon, 29 Apr 2013 13:23:05 +0200
Message-ID: <517E581A.20506@frisch.fr>
Date: Mon, 29 Apr 2013 13:23:06 +0200
From: Alain Frisch <alain@frisch.fr>
User-Agent: Mozilla/5.0 (X11; Linux i686 on x86_64; rv:21.0) Gecko/20100101 Thunderbird/21.0
MIME-Version: 1.0
To: Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>, 
 OCaML List Mailing <caml-list@inria.fr>
References: <00C57DF0-C6F0-4EDE-8607-2155F3A17146@math.nagoya-u.ac.jp> <CAK0y-36uPAAXGanrhZKQOQAPsELjTFxM1Av820da-mU4kqTVfg@mail.gmail.com> <517E2818.5040506@frisch.fr> <1EA5B7CE-C0C3-4113-9F8F-C4C3BC888D49@math.nagoya-u.ac.jp>
In-Reply-To: <1EA5B7CE-C0C3-4113-9F8F-C4C3BC888D49@math.nagoya-u.ac.jp>
Content-Type: text/plain; charset=windows-1252; format=flowed
Content-Transfer-Encoding: 7bit
Subject: Re: [Caml-list] Request for feedback: A problem with injectivity
 and GADTs

On 04/29/2013 12:52 PM, Jacques Garrigue wrote:
> What I want to know is whether anybody is using GADTs in a way that
> would be broken if we disallow type variables under abstract types
> (other  than the predefined ones) in the return type of GADTs.
> I.e., for instance defining a type witness type involving such abstract types.

The only abstract types in the return type of GADTs in LexiFi's code 
base code are currently either non-parametrized ones or built-in types 
(array, lazy).  So we'd be fine with the proposed fix (assuming that 
abstract types are not injective).

-- Alain