Pavel

Concerning “Another one”, the problem is that with BangPatterns enabled, GHC understands

          vs ! i = ...

to mean

          vs (!i) = ...

with a bang-pattern, thus defining vs rather than (!).  Reason: the common case  of saying

          f !x !y = e

is so convenient that we didn’t want to require parens.  But the cost is that you can’t define (!) in an infix way.  So that’s that one.

For the profiling thing, is this the same as http://hackage.haskell.org/trac/ghc/ticket/4462?  What happens if you say –dcore-lint?    We should look at #4462.

Simon

From: glasgow-haskell-users-bounces@haskell.org [mailto:glasgow-haskell-users-bounces@haskell.org] On Behalf Of Pavel Perikov
Sent: 01 February 2011 15:01
To: GHC users
Subject: Trying to build Agda 2.2.9 with ghc-7.1.20110131

If anyone interested...

Agda-2.2.9 compiled perfectly with 7.0.1 release but with 7.1.20110131 the compiler had a few problems including "impossible happened" when building profiling library.

Another one was in src/full/Agda/TypeChecking/Positivity.hs @ 260: 

instance ComputeOccurrences Term where

  occurrences vars v = case v of

    Var i args ->

      maybe Map.empty here (vars ! fromIntegral i)

  ..........................

    where

         vs ! i

         | i < length vs = vs !! i

         | otherwise     = error $ show vs ++ " ! " ++ show i ++ "  (" ++ show v ++ ")"

Compiler complained about ! in "vars ! fromIntegral" suggesting Map.!

after i changed the code to 

    where

         (!) vs  i

         | i < length vs = vs !! i

         | otherwise     = error $ show vs ++ " ! " ++ show i ++ "  (" ++ show v ++ ")"

everything proceeded as expected.

I also had to give -XFlexibleInstances and -XBangPatterns that was not required previously.

Agda can be got from 

darcs get http://code.haskell.org/Agda/

pavel.