[Caml-list] small GADT problem

[Caml-list] small GADT problem

[Pietro Abate]

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

Re: [Caml-list] small GADT problem

[Jeremy Yallop]

On 19 May 2016 at 10:51, Pietro Abate <pietro.abate@inria.fr> wrote:
> 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

The types 'a', 'b' and 'c' are abstract, so the type checker doesn't
know that they are not equal.  If you give them representations, like
this

  type a = A
  type b = B
  type c = C

 then the fact that they are distinct will become visible to the type
checker and you'll no longer see the warning.