[Agda] Error when compiling Agda from Darcs repository by GHC 7.2

Andreas Abel andreas.abel at ifi.lmu.de
Wed Mar 19 18:37:04 CET 2014


Thanks for the feedback.  I filed a ghc dodcumentation bug

   https://ghc.haskell.org/trac/ghc/ticket/8912#ticket

I will remove that type class and hope it compiles on 7.2 then.

Cheers,
Andreas

P.S.: In the mean time, Ulf has fixed the problem already.

On 19.03.2014 16:08, Dirk Ullrich wrote:
> Hello,
>
>
> 2014-03-19 15:51 GMT+01:00 Andreas Abel <andreas.abel at ifi.lmu.de
> <mailto:andreas.abel at ifi.lmu.de>>:
>
>     I did not introduce this incompatibility by intention, but since I
>     switched to ghc 7.6 a while ago I did not notice.
>
>     If anyone cares for compiling with ghc 7.2 I can easily remove the
>     offending type class instance.
>
> I do care: if it is not to costly I would like to have ghc 7.2 support, too.
>
>     debian stable (wheezy) has now haskell-platform (2012.2.0.0) which
>     is based on ghc 7.4.1.  So maybe it is sufficient to support ghc 7.4
>     as oldest version.
>
>     Funnily, according to the docs of ghc 7.6.3, this should still be an
>     error.
>
>
>     http://www.haskell.org/ghc/__docs/7.6.3/html/users_guide/__other-type-extensions.html#__implicit-parameters
>     <http://www.haskell.org/ghc/docs/7.6.3/html/users_guide/other-type-extensions.html#implicit-parameters>
>
>       You can't have an implicit parameter in the context of a class or
>     instance declaration. For example, both these declarations are illegal:
>
>        class (?x::Int) => C a where ...
>        instance (?x::a) => Foo [a] where ...
>
>     That's a lie, obviously.
>
> When trying to hunt the ghc 7.2 compile bug I've read this, too, and was
> irritated.
>
>
>     How can I find out when this feature entered ghc?  Does Agda compile
>     on 7.4?
>
> Here it does compile on  ghc 7.4.
>
>
>     Cheers,
>     Andreas
>
>
>     On 19.03.2014 13:53, Dirk Ullrich wrote:
>
>         Hello,
>
>
>         2014-03-19 13:15 GMT+01:00 Mateusz Kowalczyk
>         <fuuzetsu at fuuzetsu.co.uk <mailto:fuuzetsu at fuuzetsu.co.uk>
>         <mailto:fuuzetsu at fuuzetsu.co.__uk
>         <mailto:fuuzetsu at fuuzetsu.co.uk>>>:
>
>
>              On 19/03/14 10:54, Dirk Ullrich wrote:
>               > Hello,
>               >
>               > [...]
>               > Is GHC 7.2 not supported any longer?
>               >
>               > Dirk
>               >
>               >
>
>              7.2 is nearly 4 stable releases old, I'd be very surprised
>         if it was
>              still supported. You should really get at least 7.6.3 and
>         7.8 is coming
>              out soon too.
>
>              --
>              Mateusz K.
>
>         Before the last updates I could Agda even compile by GHC 7.0
>         (with some
>         trivial patching).
>         Moreover the current `Agda.cabal' says:
>
>         tested-with:   GHC == 7.2.2
>                               GHC == 7.4.2
>                               GHC == 7.6.3
>
>
>         Dirk
>
>
>
>         _________________________________________________
>         Agda mailing list
>         Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>         https://lists.chalmers.se/__mailman/listinfo/agda
>         <https://lists.chalmers.se/mailman/listinfo/agda>
>
>
>
>     --
>     Andreas Abel  <><      Du bist der geliebte Mensch.
>
>     Department of Computer Science and Engineering
>     Chalmers and Gothenburg University, Sweden
>
>     andreas.abel at gu.se <mailto:andreas.abel at gu.se>
>     http://www2.tcs.ifi.lmu.de/~__abel/ <http://www2.tcs.ifi.lmu.de/~abel/>
>
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/


More information about the Agda mailing list