[Agda] Weird constraint on type of a record field

Dr. ERDI Gergo gergo at erdi.hu
Mon May 14 15:14:13 CEST 2012


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:

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?



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

More information about the Agda mailing list