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.