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/
_______________________________________________
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
