Hi, I know this isn't a convenient issue report because the "test case" isn't easily reproducible. Since I don't understand the issue, I don't know how to create a smaller test case, sorry. My OS is Ubuntu 12-04 (64 bits) and I'm using the following programs: Agda master branch on commit https://github.com/agda/agda/commit/181a954a40b137c8deb1df801a8ee55fdbc19116 GHC ghc-8.0 branch on commit https://git.haskell.org/ghc.git/commit/a96933017470d03a1c9414c9c90dfd5c0f090... $ cabal --version cabal-install version 1.23.0.0 compiled using version 1.23.1.0 of the Cabal library (compiled with GHC 7.10.3) $ alex --version Alex version 3.1.7, (c) 2003 Chris Dornan and Simon Marlow $ happy --version Happy Version 1.19.5 Copyright (c) 1993-1996 Andy Gill, Simon Marlow (c) 1997-2005 Simon Marlow After adding `extensions: StrictData` to Agda.cabal, I'm getting the following errors: $ cabal install ... Installing library in /home/asr/.cabal/lib/x86_64-linux-ghc-8.0.0.20160316/Agda-2.5.0-8eDdWzYvIFd4CKBTUUP6kU Installing executable(s) in /home/asr/.cabal/bin Generating Agda library interface files... agda: Internal Happy error CallStack (from HasCallStack): error, called at templates/GenericTemplate.hs:288:17 in Agda-2.5.0-8eDdWzYvIFd4CKBTUUP6kU:Agda.Syntax.Parser.Parser WARNING: Failed to typecheck Agda.Primitive! agda: Internal Happy error CallStack (from HasCallStack): error, called at templates/GenericTemplate.hs:288:17 in Agda-2.5.0-8eDdWzYvIFd4CKBTUUP6kU:Agda.Syntax.Parser.Parser WARNING: Failed to typecheck Agda.Builtin.Bool! agda: Internal Happy error CallStack (from HasCallStack): error, called at templates/GenericTemplate.hs:288:17 in Agda-2.5.0-8eDdWzYvIFd4CKBTUUP6kU:Agda.Syntax.Parser.Parser WARNING: Failed to typecheck Agda.Builtin.Char! agda: Internal Happy error CallStack (from HasCallStack): error, called at templates/GenericTemplate.hs:288:17 in Agda-2.5.0-8eDdWzYvIFd4CKBTUUP6kU:Agda.Syntax.Parser.Parser WARNING: Failed to typecheck Agda.Builtin.Coinduction! agda: Internal Happy error CallStack (from HasCallStack): error, called at templates/GenericTemplate.hs:288:17 in Agda-2.5.0-8eDdWzYvIFd4CKBTUUP6kU:Agda.Syntax.Parser.Parser WARNING: Failed to typecheck Agda.Builtin.Equality! agda: Internal Happy error CallStack (from HasCallStack): error, called at templates/GenericTemplate.hs:288:17 in Agda-2.5.0-8eDdWzYvIFd4CKBTUUP6kU:Agda.Syntax.Parser.Parser WARNING: Failed to typecheck Agda.Builtin.Float! agda: Internal Happy error CallStack (from HasCallStack): error, called at templates/GenericTemplate.hs:288:17 in Agda-2.5.0-8eDdWzYvIFd4CKBTUUP6kU:Agda.Syntax.Parser.Parser WARNING: Failed to typecheck Agda.Builtin.FromNat! agda: Internal Happy error CallStack (from HasCallStack): error, called at templates/GenericTemplate.hs:288:17 in Agda-2.5.0-8eDdWzYvIFd4CKBTUUP6kU:Agda.Syntax.Parser.Parser WARNING: Failed to typecheck Agda.Builtin.FromNeg! agda: Internal Happy error CallStack (from HasCallStack): error, called at templates/GenericTemplate.hs:288:17 in Agda-2.5.0-8eDdWzYvIFd4CKBTUUP6kU:Agda.Syntax.Parser.Parser WARNING: Failed to typecheck Agda.Builtin.FromString! agda: Internal Happy error CallStack (from HasCallStack): error, called at templates/GenericTemplate.hs:288:17 in Agda-2.5.0-8eDdWzYvIFd4CKBTUUP6kU:Agda.Syntax.Parser.Parser WARNING: Failed to typecheck Agda.Builtin.IO! agda: Internal Happy error CallStack (from HasCallStack): error, called at templates/GenericTemplate.hs:288:17 in Agda-2.5.0-8eDdWzYvIFd4CKBTUUP6kU:Agda.Syntax.Parser.Parser WARNING: Failed to typecheck Agda.Builtin.Int! agda: Internal Happy error CallStack (from HasCallStack): error, called at templates/GenericTemplate.hs:288:17 in Agda-2.5.0-8eDdWzYvIFd4CKBTUUP6kU:Agda.Syntax.Parser.Parser WARNING: Failed to typecheck Agda.Builtin.List! agda: Internal Happy error CallStack (from HasCallStack): error, called at templates/GenericTemplate.hs:288:17 in Agda-2.5.0-8eDdWzYvIFd4CKBTUUP6kU:Agda.Syntax.Parser.Parser WARNING: Failed to typecheck Agda.Builtin.Nat! agda: Internal Happy error CallStack (from HasCallStack): error, called at templates/GenericTemplate.hs:288:17 in Agda-2.5.0-8eDdWzYvIFd4CKBTUUP6kU:Agda.Syntax.Parser.Parser WARNING: Failed to typecheck Agda.Builtin.Reflection! agda: Internal Happy error CallStack (from HasCallStack): error, called at templates/GenericTemplate.hs:288:17 in Agda-2.5.0-8eDdWzYvIFd4CKBTUUP6kU:Agda.Syntax.Parser.Parser WARNING: Failed to typecheck Agda.Builtin.Size! agda: Internal Happy error CallStack (from HasCallStack): error, called at templates/GenericTemplate.hs:288:17 in Agda-2.5.0-8eDdWzYvIFd4CKBTUUP6kU:Agda.Syntax.Parser.Parser WARNING: Failed to typecheck Agda.Builtin.Strict! agda: Internal Happy error CallStack (from HasCallStack): error, called at templates/GenericTemplate.hs:288:17 in Agda-2.5.0-8eDdWzYvIFd4CKBTUUP6kU:Agda.Syntax.Parser.Parser WARNING: Failed to typecheck Agda.Builtin.String! agda: Internal Happy error CallStack (from HasCallStack): error, called at templates/GenericTemplate.hs:288:17 in Agda-2.5.0-8eDdWzYvIFd4CKBTUUP6kU:Agda.Syntax.Parser.Parser WARNING: Failed to typecheck Agda.Builtin.TrustMe! agda: Internal Happy error CallStack (from HasCallStack): error, called at templates/GenericTemplate.hs:288:17 in Agda-2.5.0-8eDdWzYvIFd4CKBTUUP6kU:Agda.Syntax.Parser.Parser WARNING: Failed to typecheck Agda.Builtin.Unit! Registering Agda-2.5.0... cabal: Leaving directory '.' Installed Agda-2.5.0 Best, -- Andrés