[Agda] Strange error when trying to install Agda 2.4.0.1 from cabal

Christopher Jenkins cjenkin1 at trinity.edu
Fri Jul 18 18:56:18 CEST 2014


Andres,

Thanks, that fixed it entirely!


On Fri, Jul 18, 2014 at 10:49 AM, Andrés Sicard-Ramírez <asr at eafit.edu.co>
wrote:

>
> On 18 July 2014 10:43, Christopher Jenkins <cjenkin1 at trinity.edu> wrote:
>
>> I recently installed Linux Mint 17 on a new computer and ran the
>> following commands to install Agda:
>>
>> # apt-get update
>> # apt-get install haskell-platform libncurses5-dev
>> # cabal update
>> # cabal install agda
>>
>> Agda gets stuck compiling "src/full/Agda/Syntax/Position.hs" with the
>> following error:
>>     Could not deduce (Num (NonNegative Integer))
>>       arising from a use of `arbitrary'
>>     from the context (Arbitrarlly a)
>>       bound by the instance declaration
>>       at src/full/Agda/Syntax/Position.hs:492:10-47
>>
>> (full text of error in pastebin: http://pastebin.com/8izELMCB)
>>
>> Has anyone seen this before, or is using LM17 and was able to get Agda
>> working? My GHC is v7.6.3.
>>
>
> Agda 2.4.0.1 doesn't compile with QuickCheck 2.7.6 (it is fixed in the
> upstream version). For installing Agda 2.4.0.1 using QuickCheck 2.7.5 you
> can use the following command:
>
>   $ cabal install Agda --constraint=QuickCheck==2.7.5
>
> --
> Andrés
>



-- 
Christopher Jenkins
Computer Science 2013
Trinity University
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140718/926620d2/attachment.html


More information about the Agda mailing list