From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id 771B37EEBF for ; Fri, 24 Jul 2015 16:37:30 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.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=mail2-smtp-roc.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 (mail2-smtp-roc.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=mail2-smtp-roc.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 (mail2-smtp-roc.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=mail2-smtp-roc.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: A0ClAABaTbJVlwWCBoVchFLDRgKCDAEBAQEBARIBAQEBAQgWB0+EJAEBBDoGAwE1AQEOCw4KHBJXBohAtmWFWwKMOYRnAQEBAQEBBAEBAQEBAQEBEwEGi02EVDMHgxiBFI02hzKMPJkkhDJggksBAQE X-IPAS-Result: A0ClAABaTbJVlwWCBoVchFLDRgKCDAEBAQEBARIBAQEBAQgWB0+EJAEBBDoGAwE1AQEOCw4KHBJXBohAtmWFWwKMOYRnAQEBAQEBBAEBAQEBAQEBEwEGi02EVDMHgxiBFI02hzKMPJkkhDJggksBAQE X-IronPort-AV: E=Sophos;i="5.15,538,1432591200"; d="scan'208";a="171525118" Received: from rabbit.math.nagoya-u.ac.jp (HELO mailhost.math.nagoya-u.ac.jp) ([133.6.130.5]) by mail2-smtp-roc.national.inria.fr with ESMTP; 24 Jul 2015 16:37:28 +0200 Received: from mailhost.math.nagoya-u.ac.jp (localhost [127.0.0.1]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id AEF8266F4; Fri, 24 Jul 2015 23:37:25 +0900 (JST) Received: from mailhost.math.nagoya-u.ac.jp (rabbit-172 [172.16.254.254]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id 5D81124EA; Fri, 24 Jul 2015 23:37:25 +0900 (JST) DKIM-Signature: v=1; a=rsa-sha1; c=relaxed; d=math.nagoya-u.ac.jp; h= content-type:mime-version:subject:from:in-reply-to:date:cc :content-transfer-encoding:message-id:references:to; s=alpha; bh=8comj2l/tsab+PTuVDgLYk5SauI=; b=E1rl3+W2FdEUd8OoiFxxJ1e0Ov6c Z+wjScan6qwU/2M10D1l4UogOqlbsxy5fw3wl8quU6tbw2Ru0pzyn6RLuuej3C/f DpFFhFsdt89Yl5+dL37nKfZ//p0vDRop2ycFl/SzV835cg3u4mi9kxrL0+DpTCv2 ZNIwR8cT1DW3eV0= DomainKey-Signature: a=rsa-sha1; h=Received:Content-Type:Mime-Version:Subject:From:In-Reply-To:Date:Cc:Content-Transfer-Encoding:Message-Id:References:To:X-Mailer; b=sf+LIMUsBZ0V2/Cykvr2uRveRRTqS58SiQ6IUYyaX4jo199XlEMN08tusq056KwOqLQZHIvbQeDjo7+McBqD4oSs+VFrY+8mkAWh4Jcoe847fGgjiqKJqfKC9olwp4PWFiINlwj+TCgcRMB+wpOde1YC3wUjvVPJHwnhDGgICLU=; c=nofws; d=math.nagoya-u.ac.jp; q=dns; s=alpha Received: from tet.garrigue.jp (58x158x128x157.ap58.ftth.ucom.ne.jp [58.158.128.157]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTPSA id D47D58060; Fri, 24 Jul 2015 23:38:07 +0900 (JST) Content-Type: text/plain; charset=us-ascii Mime-Version: 1.0 (Mac OS X Mail 8.2 \(2102\)) From: Jacques Garrigue In-Reply-To: Date: Fri, 24 Jul 2015 23:37:24 +0900 Cc: OCaML List Mailing Content-Transfer-Encoding: quoted-printable Message-Id: References: To: Ben Millwood X-Mailer: Apple Mail (2.2102) Subject: Re: [Caml-list] Can we have more flexible destructive type substitution? On 2015/07/24 23:25, Ben Millwood wrote: >=20 > Currently, for [sig ... end with type lhs :=3D rhs] to be valid, rhs need= s to be an application of a type constructor to the same type parameters as= lhs. >=20 > I'd like to do, at a minimum, [sig ... end with type 'a t :=3D 'a], but t= his is currently forbidden. Are there conceptual obstacles to permitting ar= bitrary type expressions on the RHS, or are they simply not implemented yet? I think there is no problem in theory. The reason it is not allowed currently is that substitution relies on the p= ath substitution code, which allows only replacing a path by another path. Would have to think about how much new code this would require to implement= . It might not be that much in practice. Jacques Garrigue