Re: Typing problem

[j h woodyatt <jhw@conjury.org>]

Daniel Bünzli <daniel.buenzli@epfl.ch>
>
> I would like to define the following types.
>
>> type u = [ `U1 | `U2 ]
>> type 'a t = [`A of 'a | `B of ([`U1 ] as 'a) ] constraint 'a = [< u ]
>
> t's parameter is used to statically express constraints in other  
> parts of the code. My problem is that the constraint on 'a is  
> downgraded to [`U1] while I would like to be able to write
>
>> let param : 'a t -> 'a = function (`A v | `B v) -> v
>
> and get the following typing behaviour.
>
>> let v = param (`A `U1) (* should type *)
>> let v = param (`A `U2) (* should type *)
>> let v = param (`B `U1) (* should type *)
>> let v = param (`B `U2) (* should not type *)
>
> Is it possible to express that in ocaml's type system ?

The short answer is no.  The reason is that 'a is not the same type  
in the `A case as in the `B case.  Type t really has two type  
parameters.  (Well, it can have only one if this contrived example is  
fully representative of your code, as I'll describe below).

type ('a, 'b) t = [ `A of 'a | `B of 'b ]
   constraint 'a = [< u ] constraint 'b = [ `U1 ]

However, 'b is concrete in your example, so-- if it's fully  
representative of your code-- you could just do this, and you would  
still have only one type parameter:

type 'a t = [ `A of 'a | `B of [ `U1 ] ]
   constraint 'a = [< u ]

—
j h woodyatt <jhw@conjury.org>