From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <abate@pps.univ-paris-diderot.fr>
X-Original-To: caml-list@sympa.inria.fr
Delivered-To: caml-list@sympa.inria.fr
Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104])
	by sympa.inria.fr (Postfix) with ESMTPS id 05A997F919
	for <caml-list@sympa.inria.fr>; Thu, 19 May 2016 11:51:36 +0200 (CEST)
X-IronPort-AV: E=Sophos;i="5.26,334,1459807200"; 
   d="scan'208";a="178300269"
Received: from 126.18.31.93.rev.sfr.net (HELO pps.univ-paris-diderot.fr) ([93.31.18.126])
  by mail3-relais-sop.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 19 May 2016 11:51:35 +0200
Received: (nullmailer pid 20028 invoked by uid 1000);
	Thu, 19 May 2016 09:51:35 -0000
Date: Thu, 19 May 2016 11:51:35 +0200
From: Pietro Abate <pietro.abate@inria.fr>
To: caml-list@inria.fr
Message-ID: <20160519095135.GA18204@pps.univ-paris-diderot.fr>
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline
X-Operating-System: GNU/Linux
X-Organization: INRIA / IRILL
User-Agent: Mutt/1.6.0 (2016-04-01)
X-Validation-by: pietro.abate@inria.fr
Subject: [Caml-list] small GADT problem

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