[Agda] [ANNOUNCE] Agda 2.5.1 release candidate

[Sergei Meshveliani]

On Sat, 2016-02-13 at 13:20 -0500, Andrés Sicard-Ramírez wrote:
> Dear all,
> 
> The Agda Team is very pleased to announce a release candidate of Agda
> 2.5.1 available at
> 
>   http://www1.eafit.edu.co/asr/tmp/Agda-2.5.0.20160213.tar.gz
> [..]
>   $ tar xzf Agda-2.5.0.20160213.tar.gz
>   $ cd Agda-2.5.0.20160213.tar.gz
>   $ cabal install
>
> [..]


It does type-check my (large) project of DoCon-A.

But it fails to compile it to Haskell. After compiling about 5 modules,
it reports

-----------------------------
Compiling Structures1
in /home/mechvel/agda/tosave/bugs/feb14-2016/Structures1.agdai
to /home/mechvel/agda/tosave/bugs/feb14-2016/MAlonzo/Code/Structures1.hs
Unbound name: Structures1.OfMonoidHomo.recCon-NOT-PRINTED
[157]@263218534
An internal error has occurred. Please report this as a bug.
Location of the error: src/full/Agda/TypeChecking/Reduce/Monad.hs:174
-----------------------------

This is for  ghc-7.10.2, MAlonzo, Debian Linux.

Main.agda  is made by  agda -c,  
it is only  

-------------------------------------------- Main.agda ---
open import Foreign.Haskell
open import IO.Primitive
open import Data.String using (toCostring)

open import Structures1 

main : IO Unit
main = putStrLn (toCostring "done")
----------------------------------------------

But if I merge  Main.agda  to  Structures1.agda  then it is compiled
(!).

I am currently trying to minimize the example.

Regards,

------
Sergei