<div dir="ltr">Thanks for spotting this. I've filed <a href="https://github.com/agda/agda/issues/1847">https://github.com/agda/agda/issues/1847</a>. The problem is that record parameters are turned into hidden parameters inside the record definition. This is the right thing to do for explicit arguments, but instance arguments should stay instance.<div><br></div><div>/ Ulf</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Tue, Feb 16, 2016 at 3:18 AM, <span dir="ltr"><<a href="mailto:darais@cs.umd.edu" target="_blank">darais@cs.umd.edu</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi Andrés and the Agda team,<br>
<br>
I have a small use of typeclasses that no longer typechecks with Agda<br>
2.5.0.20160213.<br>
<br>
It appears typeclass instances as record parameters are no longer in scope for<br>
definitions local to the record. In the example below, the `ADD` instance is<br>
not found by typeclass resolution in the definition of `neg`. This example<br>
typchecks just fine with Agda 2.4.2.5.<br>
<br>
Thanks,<br>
David Darais<br>
<br>
record Additive {ℓ} (A : Set ℓ) : Set ℓ where<br>
field<br>
zero : A<br>
_+_ : A → A → A<br>
open Additive {{...}} public<br>
<br>
record Subtractive {ℓ} (A : Set ℓ) {{ADD : Additive A}} : Set ℓ where<br>
field<br>
_-_ : A → A → A<br>
neg : A → A<br>
neg x = zero - x<br>
open Subtractive {{...}} public<br>
<br>
> Date: Sat, 13 Feb 2016 13:20:41 -0500<br>
> From: Andrés Sicard-Ramírez <<a href="mailto:asr@eafit.edu.co">asr@eafit.edu.co</a>><br>
<span class="im HOEnZb">><br>
> Dear all,<br>
><br>
> The Agda Team is very pleased to announce a release candidate of Agda<br>
> 2.5.1 available at<br>
><br>
> <a href="http://www1.eafit.edu.co/asr/tmp/Agda-2.5.0.20160213.tar.gz" rel="noreferrer" target="_blank">http://www1.eafit.edu.co/asr/tmp/Agda-2.5.0.20160213.tar.gz</a><br>
><br>
><br>
</span><span class="im HOEnZb">> GHC supported versions<br>
> ===============<br>
><br>
> This RC has been tested with GHC 7.6.3, 7.8.4 and 7.10.3.<br>
><br>
><br>
> Installation<br>
> =======<br>
><br>
> This RC can be installed using the following instructions:<br>
><br>
</span><span class="im HOEnZb">> $ tar xzf Agda-2.5.0.20160213.tar.gz<br>
> $ cd Agda-2.5.0.20160213.tar.gz<br>
> $ cabal install<br>
><br>
><br>
</span><div class="HOEnZb"><div class="h5">> Standard library<br>
> ==========<br>
><br>
> For the time being, a version (the master branch) of the standard<br>
> library compatible with this RC is available via<br>
><br>
> $ git clone <a href="https://github.com/agda/agda-stdlib.git" rel="noreferrer" target="_blank">https://github.com/agda/agda-stdlib.git</a><br>
><br>
><br>
> What is new?<br>
> ========<br>
><br>
> The RC includes various new features and changes:<br>
><br>
> * A new library management<br>
><br>
> * The reflection framework has received a massive overhaul.<br>
><br>
> * Instance search performance has been improved.<br>
><br>
> * A new backend targeting the Utrecht Haskell Compiler (UHC) is available.<br>
><br>
> * The new agda-ghc-names tool for handling profiling files generate<br>
> from MAlonzo-compiled code.<br>
><br>
> There also are new options, pragmas and built-ins, and changes related<br>
> to modules, records, operators syntax, literals, instance search, type<br>
> checking, compiler/LaTeX/HTML backends and the Emacs mode. More<br>
> information about the changes included in this RC can be found in<br>
><br>
> <a href="https://raw.githubusercontent.com/agda/agda/2.5.0.20160213/CHANGELOG" rel="noreferrer" target="_blank">https://raw.githubusercontent.com/agda/agda/2.5.0.20160213/CHANGELOG</a><br>
><br>
><br>
> Incompatibilities<br>
> ==========<br>
><br>
> This RC is not full compatible with Agda 2.4.2.5. The main<br>
> incompatibilities are:<br>
><br>
> * A long-standing operator fixity bug has been fixed. As a consequence<br>
> some programs that used to parse no longer do.<br>
><br>
> * Emacs mode: Removed the agda-include-dirs customization parameter.<br>
><br>
> * Removed pragma {-# ETA R #-}<br>
><br>
> More information about the incompatibilities included in this RC can<br>
> be found in the above CHANGELOG.<br>
><br>
><br>
> Fixed issues<br>
> =======<br>
><br>
> Approximately 90 bugs/enhancements were fixed/closed, some of them<br>
> long-standing ones:<br>
><br>
> * <a href="https://github.com/agda/agda/issues/480" rel="noreferrer" target="_blank">https://github.com/agda/agda/issues/480</a><br>
><br>
> * <a href="https://github.com/agda/agda/issues/520" rel="noreferrer" target="_blank">https://github.com/agda/agda/issues/520</a><br>
><br>
> * <a href="https://github.com/agda/agda/issues/576" rel="noreferrer" target="_blank">https://github.com/agda/agda/issues/576</a><br>
><br>
> * <a href="https://github.com/agda/agda/issues/727" rel="noreferrer" target="_blank">https://github.com/agda/agda/issues/727</a><br>
><br>
> * <a href="https://github.com/agda/agda/issues/896" rel="noreferrer" target="_blank">https://github.com/agda/agda/issues/896</a><br>
><br>
><br>
> Know regressions<br>
> ===========<br>
><br>
> * <a href="https://github.com/agda/agda/issues/1605" rel="noreferrer" target="_blank">https://github.com/agda/agda/issues/1605</a><br>
><br>
> * <a href="https://github.com/agda/agda/issues/1770" rel="noreferrer" target="_blank">https://github.com/agda/agda/issues/1770</a><br>
><br>
> * <a href="https://github.com/agda/agda/issues/1775" rel="noreferrer" target="_blank">https://github.com/agda/agda/issues/1775</a><br>
><br>
> * <a href="https://github.com/agda/agda/issues/1821" rel="noreferrer" target="_blank">https://github.com/agda/agda/issues/1821</a><br>
><br>
><br>
> Know issues<br>
> ========<br>
><br>
> <a href="https://github.com/agda/agda/issues?utf8=%E2%9C%93&q=is%3Aopen+milestone%3A2.5.1+label%3Abug+" rel="noreferrer" target="_blank">https://github.com/agda/agda/issues?utf8=%E2%9C%93&q=is%3Aopen+milestone%3A2.5.1+label%3Abug+</a><br>
><br>
><br>
> Enjoy this RC and please test as much as possible.<br>
><br>
> --<br>
> Andrés, on behalf of the Agda Team<br>
<br>
</div></div><div class="HOEnZb"><div class="h5">_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</div></div></blockquote></div><br></div>