Re: [Caml-list] type proofs

[Jacques Garrigue <garrigue@kurims.kyoto-u.ac.jp>]

From: Charles Martin <joelisp@yahoo.com>

> 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