Re: [Caml-list] GADT and locally ADT

[Ivan Gotovchits <ivg@ieee.org>]

Gabriel Scherer <gabriel.scherer@gmail.com> writes:

> If the function knows (or infer) that the argument type is (ro), then
> there is only one case to handle. But there is also a function that is
> polymorphic over the second argument, and it must be callable with
> both (ro) and (rw) values : this function works "for any access mode".
> This is what the annotated function
>
>>      let f (type t)  (inp: ('a,t) access)  = match inp with
>>        | ReadWrite (ch) -> ()
>>        | Read (ch) -> ();;
>
> does.

Looks reasonable, but can you, please, explain the difference between
function:

    let f (type t)  (inp: ('a,t) access)  = match inp with
      | ReadWrite ch -> ()
      | Read ch -> ()

that have type 

    val f : ('a, 'b) access -> unit

and

    let f (inp: ('a,'b) access)  = match inp with
      | ReadWrite ch -> ()
      | Read ch -> ()

that fails to type check:

Error: This pattern matches values of type ('a, ro) access
       but a pattern was expected which matches values of type
         ('a, rw) access