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 DAA31086; Sat, 8 Dec 2001 03:20:40 +0100 (MET) X-Authentication-Warning: pauillac.inria.fr: majordomo set sender to owner-caml-list@pauillac.inria.fr using -f Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id DAA31143 for ; Sat, 8 Dec 2001 03:20:36 +0100 (MET) Received: from favie.faith.gr.jp (favie.faith.gr.jp [61.127.175.250]) by nez-perce.inria.fr (8.11.1/8.11.1) with ESMTP id fB82KY508198 for ; Sat, 8 Dec 2001 03:20:34 +0100 (MET) Received: from localhost (dhcp7.faith.gr.jp [192.168.1.17]) by favie.faith.gr.jp (8.9.3/8.9.3) with ESMTP id LAA09415; Sat, 8 Dec 2001 11:20:28 +0900 To: joelisp@yahoo.com Cc: caml-list@inria.fr Subject: Re: [Caml-list] type proofs In-Reply-To: <20011207212818.27730.qmail@web9207.mail.yahoo.com> References: <20011207212818.27730.qmail@web9207.mail.yahoo.com> X-Mailer: Mew version 1.94.2 on Emacs 20.7 / Mule 4.0 (HANANOEN) Mime-Version: 1.0 Content-Type: Text/Plain; charset=us-ascii Content-Transfer-Encoding: 7bit Message-Id: <20011208112002D.garrigue@kurims.kyoto-u.ac.jp> Date: Sat, 08 Dec 2001 11:20:02 +0900 From: Jacques Garrigue X-Dispatcher: imput version 20000228(IM140) Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk From: Charles Martin > 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 > > Now, this is just the tip of an iceberg that goes very deep. Does > anyone have a tool somewhere that will print out a more complete > type proof? I could check such a proof over to find the true > mistake. You can read your source code in the ocamlbrowser editor, and typecheck it (compiler menu). Then you will be able to check the type of any subexpression, which is equivalent to having a proof of the typing. Not that this works particularly well in your case, since the type error above is at the module level, and your implementation has been checked succesfully. I know of no tool to build a partial proof, which would be needed when type checking is not succesful. Jacques Garrigue ------------------- 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