[Caml-list] Re: OCaml typechecking bug? (PR#3104) [about phantom types]

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

From: bpr@artisan.com
> Version: 3.08.1
> 
> As mentioned on the mailing list, simple use of phantom types leads to a 
> situation where it appears that built in types and user defined types are
> handled 
> differently. Here's a simple example from the command line. The same behavior is
> 
> observed when I replace int in "type 'p t = int" with int64 and int array, or
> when 
> I change from sum type to record in PHANTOM_INT'  

Not surprising: the distinction is not between built-in and
user-defined, but between abbreviation types and datatypes (which
share the same syntax in ocaml, but have different syntax in most
other dialects)

> bpr@boreal[bpr]$ ocaml
>         Objective Caml version 3.08.1
> 
> # module type PHANTOM_INT = sig
>   type 'p t =  int
[...]
>   val add_even_even : even t -> even t -> even t
> end;;
[...]
> # PhantomInt.add_even_even two three;;
> val three : PhantomInt.odd PhantomInt.t = 3

This behaviour is perfectly normal.
In the above signature, the type t is not phantom at all.
It will be expanded to int before checking equality, so the type
argument will be completely ignored altogether.

> #   module type PHANTOM_INT' = sig
>   type 'p t =  Int of int
[...]
>   val add_even_even : even t -> even t -> even t
> end;;
> # PhantomInt'.add_even_even two' three';;
> This expression has type PhantomInt'.odd PhantomInt'.t
> but is here used with type PhantomInt'.even PhantomInt'.t

Actually this one is not much better.
You indeed get an error if you try to unify [even t] with [odd t],
but you still can cheat by building a value by hand (eg (Int 1 : even
t) is perfectly legal), or by using subtyping ((two' :> odd t) shall
work).
A real phantom type must be abstract, and nothing else will.
That is, in your signature, you must have:
  module type PHANTOM_INT = sig
    type 'p t
    ...
  end

Jacques Garrigue

-------------------
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