Why is this coercion necessary?

Jacques Carette
 Lukasz Stafiniak
 Martin Jambon
[
Home
]
[ Index:
by date

by threads
]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
Date:   (:) 
From:  Martin Jambon <martin.jambon@e...> 
Subject:  Re: [Camllist] Why is this coercion necessary? 
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 typechecker 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/