[Agda] Weird constraint on type of a record field

[Andreas Abel]

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

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

to

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

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 
isRing))

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.

Cheers,
Andreas

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
http://www2.tcs.ifi.lmu.de/~abel/