From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: weis
Received: (from weis@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id OAA19349 for caml-redistribution; Mon, 2 Jun 1997 14:22:28 +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 MAA29905 for <caml-list@pauillac.inria.fr>; Fri, 30 May 1997 12:11:22 +0200 (MET DST)
Received: from firewall.hd.ibm.de (firewall.hd.ibm.de [192.101.197.10]) by concorde.inria.fr (8.8.5/8.7.3) with SMTP id MAA12700 for <caml-list@pauillac.inria.fr>; Fri, 30 May 1997 12:11:18 +0200 (MET DST)
Received: from kaa.heidelbg.ibm.com by firewall.hd.ibm.de (AIX 4.1/UCB 5.64/4.03/chkV1.0)
          id AA54148; Fri, 30 May 1997 12:10:54 +0200
Received: from idse.heidelbg.ibm.com by kaa.heidelbg.ibm.com (AIX 3.2/UCB 5.64/4.03)
          id AA29509; Fri, 30 May 1997 12:09:48 +0200
Received: by idse.heidelbg.ibm.com (AIX 3.2/UCB 5.64/4.03)
          id AA49225; Fri, 30 May 1997 12:09:35 +0200
Message-Id: <9705301009.AA49225@idse.heidelbg.ibm.com>
X-Mailer: exmh version 1.6.4p2 10/10/95 (wish4.1)
To: mposada@impsat.net.co
Cc: Caml List <caml-list@pauillac.inria.fr>
Subject: Re: Type constraints 
In-Reply-To: (Your message of Thu, 29 May 97 13:56:59 EST.)
             <338DD17B.62C6@impsat.net.co> 
Mime-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Date: Fri, 30 May 97 12:09:35 +0100
From: Wolfgang Lux <lux@heidelbg.ibm.com>
Sender: weis

> Hello. I have the folowing problem. I need to define some interrelated
> types as follows:
> 
> type 'a node = {x: 'a; y: t1}
> and t1 = A | B of t1*t1
> and t2 = C | D of (string * t2) node
> 
> The interpreter prints the inferred type:
> 
> type 'a node = { x: 'a; y: t1 } constraint 'a = string * t2
> type t1 = | A | B of t1 * t1
> type t2 = | C | D of (string * t2) node
> 

A simple solution to get rid of the type constraint in this case, is to 
reorder the type definitions as follows:

type t1 = A | B of t1*t1
type 'a node = {x: 'a; y: t1}
type t2 = C | D of (string * t2) node

> Now, if I add another constructor:
> 
> type 'a node = {x: 'a; y: t1}
> and t1 = A | B of t1*t1
> and t2 = C | D of (string * t2) node | E of bool node
> 
> I obtain this message:
> 
> Characters 98-102:
> This type parameter bool should be an instance of type string * t2
> 
> A solution to this would be something like:
> 
> type ('a,'b) node = {x: 'a; y: 'b}
> and t1 = A | B of t1*t1
> and t2 = C | D of (string * t2, t1) node | E of (bool, t1) node
> 
> This works, but I am not sure to understand the type clash in the former
> example. Why did the type synthetizer infer that constraint?

I'm not absolutely sure on this, but it looks just like another case of 
the monomorphic recursion restriction of the Hindley-Milner type system.
 
> 
> Thank you for any insights on this.
> 

Hope this helps.

Regards
Wolfgang

----
Wolfgang Lux                     WZH Heidelberg, IBM Germany
Phone: +49-6221-59-4546                Fax: +49-6221-59-3500
Internet: lux@heidelbg.ibm.com          Office: mazvm01(lux)