[Caml-list] Serious typechecking error involving new polymorphism (crash)

[John Prevost <j.prevost@cs.cmu.edu>]

I've discovered a fairly serious typechecking bug in 3.05.  I'm
reporting it on the webpage, but also want to mention it here so that
people are aware.

You can do the following:

# type bad = { x : 'a . 'a option ref };;
type bad = { x : 'a. 'a option ref; } 
# let bv = { x = ref None };;
val bv : bad = {x = {contents = None}}
# bv.x := Some 5;;
- : unit = ()
# let extra_bad = !(bv.x);;
val extra_bad : '_a option = Some <poly>
# f extra_bad;;

***CRASH***

It looks like mutable fields are handled correctly and catch that the
value is not, in fact, general enough.  But when the mutable field is
part of the value (in this case, part of the ref), the check is not
done.


To be safe, I recommend being very wary of using field types like:

'a . <type expression involving 'a>

In which values of the type involve mutable portions of type 'a.  As
long as any mutable portion is not also polymorphic, things are fine.

Mutable fields are fine as well, as long as you are careful as
described above.

As an example, Using

mutable x : 'a . 'a option

instead of

x : 'a . 'a option ref

in the above example prevents any poorly typed expressions from
appearing.  No value may be put in the "good" example except None,
since None is the only fully polymorphic option value.

John.
-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners