[Agda] Bug in Development Jan-9 ?

[Sergei Meshveliani]

On Sat, 2016-01-09 at 22:48 +0400, Sergei Meshveliani wrote:
> Dear Agda developers,
> 
> I compare  Development Agda of December 18, 2015   (A-I)
> to         Development Agda of January   9, 2016   (A-II)
> 
> (both on ghc-7.10.2 and Debian Linux)
> 
> on the current DoCon-A application.
> 
> 
> A-I type-checks it almost to end.
> 
> And A-II breaks in the middle:
> 
>  ...
>  /home/mechvel/doconA/0.04/source/OfIsoMonoids.agda:86,52-64
> (MagmaIsomorphismPair upMagma upMagma') !=<
> (.Structures0.UpMagma (_α_142 upMonoid upMonoid' monIsoPair)
>  (_α=_143 upMonoid upMonoid' monIsoPair))
> of type
> (Set
>  (β= .Agda.Primitive.⊔
>   (β .Agda.Primitive.⊔ (α= .Agda.Primitive.⊔ α))))
> when checking that the expression magmaIsoPair has type
> .Structures0.UpMagma (_α_142 upMonoid upMonoid' monIsoPair)
> (_α=_143 upMonoid upMonoid' monIsoPair)
> 
> The resposible lines are 
> 
>  ...
>  injective-f  = MgIsoPair.injective-f magmaIsoPair              -- 85
>  surjective-f = MagmaIsomorphismPair.surjective-f magmaIsoPair  -- 86 **
> 
> 
> A-I and A-II  differ on the line 86 in  OfIsoMonoids.agda.
> 
> A-II is a certain improvement for A-I
> (the bug tracker wrote  "Closed #1759 via 9c64919",
> and I observe the A-II type-checks the example at which A-I failed).
> 
> But I suspect that A-II is wrong at the module OfIsoMonoids.agda.
> [..]


I think now that  A-II  is more correct.
The situation is as follows.

1) The record  MagmaIsomorphismPair  is imported from a module
   parameterized by
                 upMagma1 upMagma1 : UpMagma,

and `surjective' is implemented in the body of this record.


2)  module MgIsoPair = MagmaIsomorphismPair upMagma upMagma'

is introduced to be used as abbreviation.


3) Further, for

  surjective-f : To.Surjective f
  surjective-f =
    -- MgIsoPair.surjective-f magmaIsoPair                     -- I
    -- MagmaIsomorphismPair.surjective-f upMagma upMagma' magmaIsoPair
                                                               -- II 
    MagmaIsomorphismPair.surjective-f magmaIsoPair             -- III


A-I   type-checks all the three variants, while
A-II  reports of III as of erroneous.

I think that A-II is correct at this point.
Right?

I suspect that this bug in A-I has the same origin as  #1759 and
9c64919.

And I hope further for this latest A-II.

Regards,

------
Sergei