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

Dirk Ullrich dirk.ullrich at gmail.com
Wed Mar 19 16:08:11 CET 2014


Hello,


2014-03-19 15:51 GMT+01:00 Andreas Abel <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
>
>  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>>:
>>
>>
>>     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
>> 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
> http://www2.tcs.ifi.lmu.de/~abel/
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140319/201dbafa/attachment.html


More information about the Agda mailing list