Dear Gabriel,
Here's an example of the sort of misbehaviour that the variance
condition on GADTs is intended to prevent. Consider what happens when
we decorate our old friend the equality GADT with a variance
annotation on one of the type parameters (it doesn't matter which):
type (_, +_) eq = Refl : ('a, 'a) eq
Even this fairly harmless looking addition allows us to write the
dreaded 'magic' function of type 'a -> 'b. Here's how (somewhat
untested):
let magic : 'a 'b. 'a -> 'b =
(* Dramatis personae:
* i, the input type
* o, the output type
* x, a value of the input type
*)
fun (type i) (type o) (x : i) ->
(* Step 1. Coerce a (legitimate) proof of <m:t> = <m:t> (any t) to a
* (dodgy) proof of <m:t> = < >.
*)
let bad_proof (type t) = (Refl : (<m:t>, <m:t>) eq :>
(<m:t>, < >) eq) in
(* Step 2. Use GADT pattern matching / type refinement to write a
* (legitimate) function from a proof of t = < > (any t) and a
* value of < > to a value of t.
*)
let downcast_1 : type a. (a, < >) eq -> < > -> a =
fun (type a) (Refl : (a, < >) eq) (s : < >) ->
(s :> a) in
(* Step 3. Apply the (legitimate) function to the (dodgy) proof to
* obtain a (dodgy) conversion from < > to <m:o>.
*)
let downcast_2 : < > -> <m:o> = downcast_1 bad_proof in
(* Step 4. Wrap up x in an object, and hide it behind a (legitimate)
* upcast to < >.
*)
let wrapped_x = ((object method m = x end) :> < >) in
(* Step 5. Apply the (dodgy) conversion to the wrapped x to obtain a
* value of type <m:o>, from which we can extract x at type o.
*)
(downcast_2 wrapped_x) # m
If I understand correctly, constraints 1-3 alone wouldn't be enough to
prevent this sort of thing.
Kind regards,
Jeremy.
--
Caml-list mailing list. Subscription management and archives:
https://sympa-roc.inria.fr/wws/info/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs
