From mboxrd@z Thu Jan  1 00:00:00 1970
Received: (from weis@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id KAA25583 for caml-red; Wed, 18 Oct 2000 10:36:18 +0200 (MET DST)
Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id VAA19827 for <caml-list@pauillac.inria.fr>; Tue, 17 Oct 2000 21:11:08 +0200 (MET DST)
Received: from morgon.inria.fr (morgon.inria.fr [128.93.8.33])
	by concorde.inria.fr (8.11.1/8.10.0) with ESMTP id e9HJB7X07601;
	Tue, 17 Oct 2000 21:11:07 +0200 (MET DST)
Received: (from remy@localhost)
	by morgon.inria.fr (8.9.3/8.9.3) id VAA24184;
	Tue, 17 Oct 2000 21:17:58 +0200
Date: Tue, 17 Oct 2000 21:17:58 +0200
From: Didier Remy <Didier.Remy@inria.fr>
To: David Monniaux <David.Monniaux@ens.fr>
Cc: Liste CAML <caml-list@inria.fr>
Subject: Re: generalization in tuples
Message-ID: <20001017211757.A24092@morgon.inria.fr>
Reply-To: Didier.Remy@inria.fr
References: <Pine.GSO.4.03.10010161015350.24630-100000@basilic.ens.fr> <20001017101155.A16955@morgon.inria.fr>
Mime-Version: 1.0
Content-Type: text/plain; charset=us-ascii
X-Mailer: Mutt 1.0pre3us
In-Reply-To: <20001017101155.A16955@morgon.inria.fr>
Organization: INRIA, BP 105, F-78153 Le Chesnay Cedex
Phone: (33) 1 3963 5317 -- Sec: (33) 1 3963 5570 -- Fax: (33) 1 3963 5684
Web: http://cristal.inria.fr/~remy
Sender: weis@pauillac.inria.fr

>         let x = (let y = fun x -> x in ref y, y)
>                  : ('a -> 'a) ref * ('a -> 'a)

Indeed, as Michel Mauny pointed out to me, this expression would have type:

          let x = (let y = fun x -> x in ref y, y)
                   : ('a -> 'a) ref * ('b -> 'b)

thus 'b appearing only in a non-expansive expression could be also
generalized here. (BTW, the context "let x = v in [ ]" is non-expansive
whenever v is)

I meant to create the situation where a type variable appears on both
side of a product, when one side is expansive, this other is not, and the
context of the product is non-expansive. But I can't think of a ``natural''
example of this. The usual trick: 

          let x = (fun (y : 'a) -> ref y, y) (fun x -> x)
                   : ('a -> 'a) ref * ('a -> 'a)

does not work, because the whole expression becomes an application and is
expansive. I can only think of using an artifial typing constraint:

          let x = (let y = fun x -> x in ref (y : 'a), (y : 'a))
                   : ('a -> 'a) ref * ('a -> 'a)

> Here 'a appears both in an outer expansive expansive expression and in a
> non-expansive expressions. Hence it is dangerous can cannot be generalized. 

Funny! it is so difficult to stop type generalization...

        Didier