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 UAA13387 for caml-redistribution; Sun, 22 Aug 1999 20:17:52 +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 IAA19192 for ; Mon, 16 Aug 1999 08:32:06 +0200 (MET DST) Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35]) by concorde.inria.fr (8.8.7/8.8.7) with ESMTP id IAA18027; Mon, 16 Aug 1999 08:32:00 +0200 (MET DST) Received: (from fpottier@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id IAA19883; Mon, 16 Aug 1999 08:31:58 +0200 (MET DST) Message-ID: <19990816083158.52649@pauillac.inria.fr> Date: Mon, 16 Aug 1999 08:31:58 +0200 From: Francois Pottier To: Jacques GARRIGUE Cc: caml-list@inria.fr Subject: Re: Weird behavior with mutually recursive type definitions References: <19990804155239.50895@pauillac.inria.fr> <19990813104206X.garrigue@kurims.kyoto-u.ac.jp> Mime-Version: 1.0 Content-Type: text/plain; charset=iso-8859-1 Content-Transfer-Encoding: 8bit X-Mailer: Mutt 0.89.1 In-Reply-To: <19990813104206X.garrigue@kurims.kyoto-u.ac.jp>; from Jacques GARRIGUE on Fri, Aug 13, 1999 at 10:42:06AM +0900 Sender: weis > Why is it so? Constraints are required for the object system, and if > there are constraints you must expand abbreviations inside definitions > to check them. If recursion occurs before the abbreviation is > generalized, this means that all occurences of an abbreviation in the > same type definition will be unified, and have the same constraints. I fail to see why type abbreviations should be monomorphic while their declaration is being checked. Is this intended to make the type system safe, or to guarantee the typechecker's termination? By the way, I find O'Caml's error messages on this topic rather strange. If I try: type 'a t = ('a -> 'a) u and 'a u = ('a -> 'a) t then I obtain This type ('a -> 'a) -> 'a -> 'a should be an instance of type 'a which corresponds to the problem discussed so far. This seems to indicate that t and u are understood as mutually recursive type abbreviations. However, if I try: type t = u and u = t then O'Caml answers A type variable is unbound in this type declaration which surprises me. I would rather expect to be warned about cyclic type abbreviations. -- François Pottier Francois.Pottier@inria.fr http://pauillac.inria.fr/~fpottier/