[Agda-dev] agda: <<loop>>

Wolfram Kahl kahl at cas.mcmaster.ca
Sat Mar 14 17:08:20 CET 2015


On Thu, Mar 12, 2015 at 07:58:30PM -0500, Andrés Sicard-Ramírez wrote:
> On 12 March 2015 at 17:41, Wolfram Kahl <kahl at cas.mcmaster.ca> wrote:
> > With Agda compiled with -feager-blackholing,
> > while checking the standard library with -N1, I get:
> >
> >      Finished Data.Bool.Base.
> >  50374120   8877328   9098816  0.03  0.03    0.75    1.08    0    0  (Gen:  1)
> > agda: <<loop>>
> >
> >
> > Now this makes me really curious what is going on there!
> 
> Just out of curiosity, I tried to reproduce the issue. These are my results:
> 
> GHC 7.8.4: I could reproduce the issue
> GHC 7.6.3 and GHC 7.10.RC2: I *couldn't* reproduce the issue
> 
> Please report this regression/progression to GHC using this small test case :-)

Well, if it is ``fixed'' in GHC 7.10.RC2, it might not be worth reporting ---
any intuition why such a thing could affect the current development version of Agda
at all? Andreas suggested sharing --- has somebody actually started putting
`par` into places?


And how did you manage to compile with GHC 7.10.RC2?
I am getting:

[  6 of 289] Compiling Agda.Utils.Cluster ( src/full/Agda/Utils/Cluster.hs, dist/build/Agda/Utils/Cluster.o )

src/full/Agda/Utils/Cluster.hs:146:3:
    Exception when trying to run compile-time code:
      Higher-kinded type variables in type: forall (a_0 :: *) . a_0 -> [a_0] -> GHC.Types.Bool
    Code: quickCheckAll
    In the splice: $quickCheckAll



Wolfram



 # ghc-pkg list
/usr/local/packages/Agda-2.4.3.3/lib/ghc-7.10.0.20150123/package.conf.d
   Cabal-1.22.1.0
   QuickCheck-2.7.6
   STMonadTrans-0.3.2
   array-0.5.0.1
   base-4.8.0.0
   bin-package-db-0.0.0.0
   binary-0.7.3.0
   boxes-0.1.4
   bytestring-0.10.6.0
   containers-0.5.6.2
   cpphs-1.18.9
   data-hash-0.2.0.0
   deepseq-1.4.0.0
   directory-1.2.2.0
   equivalence-0.2.5
   filemanip-0.3.6.3
   filepath-1.3.1.0
   geniplate-0.6.0.5
   ghc-7.10.0.20150123
   ghc-prim-0.3.1.0
   hashable-1.2.3.1
   hashtables-1.2.0.2
   haskeline-0.7.1.3
   haskeline-0.7.2.0
   haskell-src-exts-1.16.0.1
   hoopl-3.10.0.2
   hpc-0.6.0.2
   integer-gmp-1.0.0.0
   mtl-2.2.1
   old-locale-1.0.0.7
   old-time-1.1.0.3
   parallel-3.2.0.6
   polyparse-1.11
   pretty-1.1.2.0
   primitive-0.5.4.0
   process-1.2.2.0
   random-1.1
   regex-base-0.93.2
   regex-compat-0.95.1
   regex-posix-0.95.2
   rts-1.0
   split-0.2.2
   strict-0.3.2
   template-haskell-2.10.0.0
   terminfo-0.4.0.1
   text-1.2.0.4
   tf-random-0.5
   time-1.5.0.1
   transformers-0.4.2.0
   unix-2.7.1.0
   unix-compat-0.4.1.4
   unordered-containers-0.2.5.1
   vector-0.10.12.2
   xhtml-3000.2.1
   zlib-0.5.4.2


More information about the Agda-dev mailing list