[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