[Agda] Bug in Development Jan-9 ?

[Sergei Meshveliani]

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.

The example is large, and I am going to reduce it.
Meanwhile, I do not know, may be you can guess what is the matter here.

Regards,

------
Sergei