[Caml-list] GADT and locally ADT

[Ivan Gotovchits <ivg@ieee.org>]

I'm trying to get a grasp of GADT with a simple example, in which I use subj as a
phantom type. With the following, purely synthetical types:

    type ro
    type rw

    type ('a,_) access =
        | Read : 'a -> ('a,ro) access
        | ReadWrite : 'a -> ('a,rw) access

next I define function 

    let f1 = function
      | ReadWrite (ch) -> ();;

    val f : ('a, rw) access -> unit = <fun>

That's ok, I understand, by intuition, that the argument of the function
shouldn't have both types at once: ('a,rw) access and ('a,ro) access. So
the matching is exhaustive. In accordance with it, compiler forbids the
following function:

     let f inp  = match inp with
       | ReadWrite (ch) -> ()
       | Read (ch) -> ();;

     Characters 57-66:
       | Read (ch) -> ();;
           ^^^^^^^^^
     Error: This pattern matches values of type ('a, ro) access
            but a pattern was expected which matches values of type
              ('a, rw) access

But, if I add a type annotation I can successfully delude the compiler
and it typechecks what he has recently considered illegal:

     let f (type t)  (inp: ('a,t) access)  = match inp with
       | ReadWrite (ch) -> ()
       | Read (ch) -> ();;
     
    val f : ('a, 'b) access -> unit = <fun>

Are there any logical explanation to this?

Thank in advance!


-- 
         (__) 
         (oo) 
   /------\/ 
  / |    ||   
 *  /\---/\ 
    ~~   ~~   
...."Have you mooed today?"...