Issue using StrictData

[Andrés Sicard-Ramírez]

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/a96933017470d03a1c9414c9c90dfd5c0f0903ed

  $ 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