Why is this coercion necessary?
 Jacques Carette
[
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:  Jacques Carette <carette@m...> 
Subject:  Why is this coercion necessary? 
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? Jacques