Re: [Caml-list] Why is this coercion necessary?

[Martin Jambon <martin.jambon@ens-lyon.org>]

On Wed, 13 Aug 2008, Jacques Carette wrote:

> Here is a much simplified version from a (much) larger problem I have 
> recently encountered:
>
> type 'a a = [`A of 'a b]
> and 'a b  = [`B of 'a a]
> and 'a c  = [`C ]
>
> type 'a d = [ 'a a | 'a b | 'a c]
> type e = e d
>
> # this code gives an error (details below)
> let f1 (x:e) : e = match x with
>   |  `A n -> n
>   |  `B n -> n
>   |  `C   -> `C
>
> # this works
> let f2 (x:e) : e = match x with
>   |  `A n -> (n :> e)
>   |  `B n -> (n :> e)
>   |  `C   -> `C
>
> f1 gives an error  on the "| `B n -> n" line, pointing to the second 'n' with
> This expression has type e a but is used with type e b
> These two variant types have no intersection
>
> Indeed, they have no intersection, but they have a union!  That is what it 
> seems the coercion in f2 'forces' the type-checker to realize, and all works 
> fine.  But of course, such coercions end up polluting my code all over the 
> place (since the actual example is made of 9 types with 20 tags in total, and 
> the 'recursive knot' requires 2 parameters to close properly).
>
> So, is this a bug?  Is there a way to avoid these coercions?


The following works, but I doubt it would make your code shorter:


type 'a a = [`A of 'a b]
and 'a b  = [`B of 'a a]
and 'a c  = [`C ]

type 'a d = [ 'a a | 'a b | 'a c]
type e = e d

type f = [`A of e | `B of e | `C ]

let f3 (x:e) : e = match (x :> f) with
    | `A n -> n
    | `B n -> n
    | `C   -> `C


Martin

--
http://mjambon.com/