[Agda] Re: [ANNOUNCE] Agda 2.5.1 release candidate

[darais at cs.umd.edu]

Hi Andrés and the Agda team,

I have a small use of typeclasses that no longer typechecks with Agda
2.5.0.20160213.

It appears typeclass instances as record parameters are no longer in scope for
definitions local to the record. In the example below, the `ADD` instance is
not found by typeclass resolution in the definition of `neg`. This example
typchecks just fine with Agda 2.4.2.5.

Thanks,
David Darais

record Additive {ℓ} (A : Set ℓ) : Set ℓ where
  field
    zero : A
    _+_ : A → A → A
open Additive {{...}} public

record Subtractive {ℓ} (A : Set ℓ) {{ADD : Additive A}} : Set ℓ where
  field
    _-_ : A → A → A
  neg : A → A
  neg x = zero - x
open Subtractive {{...}} public

> Date: Sat, 13 Feb 2016 13:20:41 -0500
> From: Andrés Sicard-Ramírez <asr at eafit.edu.co>
> 
> 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
> 
> 
> GHC supported versions
> ===============
> 
> This RC has been tested with GHC 7.6.3, 7.8.4 and 7.10.3.
> 
> 
> Installation
> =======
> 
> This RC can be installed using the following instructions:
> 
>  $ tar xzf Agda-2.5.0.20160213.tar.gz
>  $ cd Agda-2.5.0.20160213.tar.gz
>  $ cabal install
> 
> 
> Standard library
> ==========
> 
> For the time being, a version (the master branch) of the standard
> library compatible with this RC is available via
> 
>  $ git clone https://github.com/agda/agda-stdlib.git
> 
> 
> What is new?
> ========
> 
> The RC includes various new features and changes:
> 
> * A new library management
> 
> * The reflection framework has received a massive overhaul.
> 
> * Instance search performance has been improved.
> 
> * A new backend targeting the Utrecht Haskell Compiler (UHC) is available.
> 
> * The new agda-ghc-names tool for handling profiling files generate
> from MAlonzo-compiled code.
> 
> There also are new options, pragmas and built-ins, and changes related
> to modules, records, operators syntax, literals, instance search, type
> checking, compiler/LaTeX/HTML backends and the Emacs mode. More
> information about the changes included in this RC can be found in
> 
>  https://raw.githubusercontent.com/agda/agda/2.5.0.20160213/CHANGELOG
> 
> 
> Incompatibilities
> ==========
> 
> This RC is not full compatible with Agda 2.4.2.5. The main
> incompatibilities are:
> 
> * A long-standing operator fixity bug has been fixed. As a consequence
> some programs that used to parse no longer do.
> 
> * Emacs mode: Removed the agda-include-dirs customization parameter.
> 
> * Removed pragma {-# ETA R #-}
> 
> More information about the incompatibilities included in this RC can
> be found in the above CHANGELOG.
> 
> 
> Fixed issues
> =======
> 
> Approximately 90 bugs/enhancements were fixed/closed, some of them
> long-standing ones:
> 
> * https://github.com/agda/agda/issues/480
> 
> * https://github.com/agda/agda/issues/520
> 
> * https://github.com/agda/agda/issues/576
> 
> * https://github.com/agda/agda/issues/727
> 
> * https://github.com/agda/agda/issues/896
> 
> 
> Know regressions
> ===========
> 
> * https://github.com/agda/agda/issues/1605
> 
> * https://github.com/agda/agda/issues/1770
> 
> * https://github.com/agda/agda/issues/1775
> 
> * https://github.com/agda/agda/issues/1821
> 
> 
> Know issues
> ========
> 
>  https://github.com/agda/agda/issues?utf8=%E2%9C%93&q=is%3Aopen+milestone%3A2.5.1+label%3Abug+
> 
> 
> Enjoy this RC and please test as much as possible.
> 
> -- 
> Andrés, on behalf of the Agda Team