Type constraints

[Jim Farrand <jim@farrand.net>]

Hi,

I am writing a camlp4 extension to implement dynamic types in O'Caml[1].
I am doing this by generating run-time type representations of values.
When a value is "made dynamic" I tag it with type information.  Then
when it is later "made static" I check the tagged type information
against the type the value is being cast to.

(* x is a dynamic value with type Dynamic.t *)
value x = (10 => dynamic int) ; 

(* y has type int. *)
value y = (x => static int) ;

(* y has type string *)
value z = (x => static string) ;
(* (But as x doesn't have an int, this raises a Type_error exception) *)

When generating the code for the first example, I have to check that x
really has type int, so that the run-time type information I output
matches the actual type..  I do this by introducing a type constraint.

(x : int)

This works fine for monomorphic value, but I now want to extend to
polymorphic values.  The idea is that if you have a value, which has a
polymorphic type, eg.

value x = ((fun x -> x) => dynamic 'a -> 'a) ;

The problem is that the type constraint generated,

((fun x -> x) : 'a -> 'a)

does not reject values with a less general type.  This is fine when the
type given matches the function, as it does above, but causes me
problems if the type given is less general.

For example,

value x = ((fun x -> x) => dynamic 'a -> int) ;

yields

((fun x -> x) : 'a -> int)

which is happily compiled by ocaml (I want to reject it).

(To understand why this is a problem, consider the code

value y = (x => static 'a -> int) ;

My extension will accept this as the type matches the type given when
the value was made dynamic.  I can now do

value z = y "foo" ; (** Ooops! Just cast a string to an int!! *)

How can I achieve this?

It occurs to me that if I declared a record with a polymorphic type

{ foo : ! 'a . 'a -> 'a }

then values with the intended type are accepted

value t = { foo = id } 

wherease values with a less general type are not

value t = { foo = (id : 'a -> int) } ; (** Type error *)

It seems logical to me that I should be able to use similar syntax in
type constraints, eg. (id : ! 'a . 'a -> 'a), and I think that if I
could, I could use this to solve my problems.

        Objective Caml version 3.09+dev3 (2004-10-06)

# #load "camlp4r.cma" ;;

        Camlp4 Parsing version 3.09+dev3 (2004-10-06)

# value id x = x ;
value id : 'a -> 'a = <fun>
# (id : ! 'a . 'a -> 'a) ;
This expression has type 'a -> 'a but is here used with type 'b. 'b ->
'b

Why is this?

Thanks in advance, and sorry for such a long post.
Jim

[1] I know that there are all sorts of reasons why I shouldn't be doing
this.  I'm not arguing that it's a good idea, but it's certainly
interesting.
-- 
Jim Farrand