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