[Agda] Weird constraint on type of a record field

[Dr. ERDI Gergo]

Hi,

I'm getting a really weird typing error that I believe may point to a bug. 
I've removed all the unnecessary code and uploaded what remains here:
http://hpaste.org/68497

The problem comes from line 27. The error message is:
IsRing.*-isMonoid /= IsRing.+-isAbelianGroup

which is true, but I don't see why it should matter... if I replace the 
reference to *-monoid to a hole and look at all its constraints, I see 
that it explicitly mentions +-isAbelianGroup in the isEquivalence witness 
field. Where does this constraint come from?

Interestingly, if instead of the reference to *-monoid, I create a new 
IsMonoid record, and fill in all the leaves with the appropriate leaves of 
*-monoid, it passes the typechecker.

Any idea what's going on here?

Thanks,
 	Gergo

-- 

   .--= ULLA! =-----------------.
    \     http://gergo.erdi.hu   \
     `---= gergo at erdi.hu =-------'
Why experiment on animals when there are so many lawyers?