[Agda] Weird constraint on type of a record field

Andreas Abel andreas.abel at ifi.lmu.de
Mon May 14 22:51:55 CEST 2012

Hi, I am not sure this is a bug.  Agda compares

   (IsSemigroup.isEquivalence (IsMonoid.isSemigroup
     (IsRing.*-isMonoid isRing)))


   (IsSemigroup.isEquivalence (IsMonoid.isSemigroup
     (IsGroup.isMonoid (IsAbelianGroup.isGroup (IsRing.+-isAbelianGroup 

and then fails with the error message you cite below.

What you claim is that

   IsRing.*-isMonoid isRing

is the same as

   IsGroup.isMonoid (IsAbelianGroup.isGroup (IsRing.+-isAbelianGroup 

but I doubt it is.  You seem to compare the + with the *-monoid of a Ring.

I have filed your issue as 638, but I won't proceed on it.  If you think 
it is a bug, supply more evidence, please.


On 14.05.12 3:14 PM, Dr. ERDI Gergo wrote:
> 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

Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de

More information about the Agda mailing list