Re: [Caml-list] Closed variants, type constraints and module signature

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

From: Philippe Veber <philippe.veber@googlemail.com>

> I'd like to define a type with a variable that is constrained to accept only
> polymorphic variant types included in a given set of tags. That is how I
> believed one should do :
> 
>         Objective Caml version 3.11.2
> 
> # type 'a t = 'a constraint 'a = [< `a | `b ];;
> type 'a t = 'a constraint 'a = [< `a | `b ]
>
> But I stumbled upon the following problem, when trying to use this
> definition
> 
> 
> # module type S = sig
>   val v : 'a t
> end;;
> module type S = sig val v : [< `a | `b ] t end
> 
> # module I : S = struct
>     let v = `a
>   end;;
> 
>   Error: Signature mismatch:
>        Modules do not match: sig val v : [> `a ] end is not included in S
>        Values do not match:
>          val v : [> `a ]
>        is not included in
>          val v : [< `a | `b ] t
> 
> Does anyone know why the definition of module I is rejected ? And if this is
> the intended behavior, why does the following work ?
> 
> # let v : 'a t = `a
>   ;;
> val v : [< `a | `b > `a ] t = `a

But it doesn't really work!
More precisely, the type [< `a | `b > `a ] t is an instance of 'a t,
not 'a t itself, an a module interface should give a type at most as
general as the implementation.

In your case, you should simply write

  type t = [`a | `b]

since you don't know what v may be.

Jacques Garrigue