[Caml-list] small GADT problem

[Pietro Abate <pietro.abate@inria.fr>]

Bonjour,

I fail to understand why in this simple example below I get a warning.
Why the type annotations are not enough to convince the compiler that
the method vartoint cannot accept anything else then UID.a ?

module UID = struct

  type a
  type b
  type c

  type _ value =
    | A : int -> a value
    | B : int -> b value
    | C : int -> c value

  let toa v : a value = A v
  let tob v : b value = B v
  let toc v : c value = C v

end

class type ['a,'b] projection =
  object
    method add : 'a UID.value -> unit
    method inttovar : 'b UID.value -> 'a UID.value
    method vartoint : 'a UID.value -> 'b UID.value
  end

class identity : [UID.a, UID.b] projection = object
  method add v = ()
  method inttovar (UID.B v) = UID.toa v
  method vartoint (UID.A v) = UID.tob v
end

Warning 8: this pattern-matching is not exhaustive.
Here is an example of a value that is not matched:
A _
Warning 8: this pattern-matching is not exhaustive.
Here is an example of a value that is not matched:
B _
class identity : [UID.a, UID.b] projection

The class is correctly typed and the compiler correctly
identifies typing errors : 

# let map = new identity ;;
val map : identity = <obj>
# map#vartoint (UID.toc 1) ;;
Error: This expression has type UID.c UID.value
       but an expression was expected of type UID.a UID.value
       Type UID.c is not compatible with type UID.a 
# map#vartoint (UID.toa 1) ;;
- : UID.b UID.value = UID.B 1
# 
 
(The OCaml compiler, version 4.02.3)

p