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

[Ulf Norell]

I fixed this, so now Agda compiles with 7.2.2 again.

/ Ulf


On Wed, Mar 19, 2014 at 4:08 PM, Dirk Ullrich <dirk.ullrich at gmail.com>wrote:

> 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/
>>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140319/ed30b9e4/attachment-0001.html