From mboxrd@z Thu Jan 1 00:00:00 1970 Received: (from majordomo@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id JAA27568; Mon, 10 Dec 2001 09:06:16 +0100 (MET) X-Authentication-Warning: pauillac.inria.fr: majordomo set sender to owner-caml-list@pauillac.inria.fr using -f 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 JAA27754 for ; Mon, 10 Dec 2001 09:06:15 +0100 (MET) Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35]) by concorde.inria.fr (8.11.1/8.11.1) with ESMTP id fBA86DT12364; Mon, 10 Dec 2001 09:06:13 +0100 (MET) Received: (from fpottier@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id JAA27486; Mon, 10 Dec 2001 09:06:12 +0100 (MET) Date: Mon, 10 Dec 2001 09:06:12 +0100 From: Francois Pottier To: Charles Martin Cc: caml-list@inria.fr Subject: Re: [Caml-list] type proofs Message-ID: <20011210090612.A2025@pauillac.inria.fr> Reply-To: Francois.Pottier@inria.fr References: <20011207212818.27730.qmail@web9207.mail.yahoo.com> Mime-Version: 1.0 Content-Type: text/plain; charset=iso-8859-1 Content-Transfer-Encoding: 8bit X-Mailer: Mutt 1.0i In-Reply-To: <20011207212818.27730.qmail@web9207.mail.yahoo.com>; from joelisp@yahoo.com on Fri, Dec 07, 2001 at 01:28:18PM -0800 Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk On Fri, Dec 07, 2001 at 01:28:18PM -0800, Charles Martin wrote: > I have the usual kind of type error: > > Values do not match: > val send : ('a, int, 'b) t -> 'a -> int > is not included in > val send : ('a, 'b, 'c) t -> 'a -> int Your implementation is well-typed, but less general than what's declared in your interface. The right thing to do is to add type annotations to your code to help pinpoint the error location. One would like to write: let send (x : ('a, 'b, 'c) t) (y : 'a) = ... Unfortunately, this will not help, because O'Caml interprets these type variables as existentially bound, i.e. it thinks it is OK to instantiate 'b with int. There is no way, as far as I know, to require them to be intepreted as universally bound. One work-around here is to write: let send (x : ('a, bool, 'c) t) (y : 'a) = ... Here, if your code were general enough, your implementation would still typecheck. However, because the inferred type mentions int and you have required bool, a type error will arise somewhere, and that should help you locate the error. (Here, I have used bool, but any concrete or abstract type other than int would do.) Of course, you'll need to remove the annotation when done. I hope this helps, -- François Pottier Francois.Pottier@inria.fr http://pauillac.inria.fr/~fpottier/ ------------------- Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/ To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr