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.

On Tue, Feb 01, 2011 at 06:01:04PM +0300, Pavel Perikov wrote:
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.
Possibly related: http://hackage.haskell.org/trac/ghc/ticket/4462 Therefore: does the problem change if you pass --ghc-options="-dcore-lint" to ./Setup configure -p ? Wolfram

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.
participants (3)
-
kahl@cas.mcmaster.ca
-
Pavel Perikov
-
Simon Peyton-Jones