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

["Lukasz Stafiniak" <lukstafi@gmail.com>]

There is no way to avoid coercions altogether: OCaml doesn't have
inference for subtyping, using unification with row variables gives
the intersection behavior. But the language could be changed, with a
syntax like

match x return e with
| ... -> ...
| ... -> ...

meaning that all branches should be coerced to e.

On Thu, Aug 14, 2008 at 4:18 AM, Jacques Carette <carette@mcmaster.ca> 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?
>
> Jacques
>
> _______________________________________________
> Caml-list mailing list. Subscription management:
> http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
> Archives: http://caml.inria.fr
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
>