[Agda] Building Agda on GHC 7.9

Mateusz Kowalczyk fuuzetsu at fuuzetsu.co.uk
Sun Mar 30 17:57:24 CEST 2014


Hi,

I'm trying to look into http://trac.haskell.org/haddock/ticket/295 but I
can't build darcs version of Agda with GHC 7.9 so that I can actually
try and fix the issue with current Haddock.

Does anyone have tips on getting Agda to compile? Is there just no
incentive to have Agda compile with 7.9 at all? I am using darcs version
of Agda, the Hackage version would not even begin to compile due to
version bounds.

The error is below:

Preprocessing library template-haskell-2.8.0.0...
[1 of 6] Compiling Language.Haskell.TH.Syntax (
Language/Haskell/TH/Syntax.hs,
dist/dist-sandbox-a07c4207/build/Language/Haskell/TH/Syntax.o )

Language/Haskell/TH/Syntax.hs:721:37:
    Couldn't match expected type ‘Bool’ with actual type ‘Int#’
    In the expression: u1 <# u2
    In a stmt of a pattern guard for
                   an equation for ‘compare’:
      u1 <# u2
    In an equation for ‘compare’:
        (NameU u1) `compare` (NameU u2)
          | u1 <# u2 = LT
          | u1 ==# u2 = EQ
          | otherwise = GT

Language/Haskell/TH/Syntax.hs:722:37:
    Couldn't match expected type ‘Bool’ with actual type ‘Int#’
    In the expression: u1 ==# u2
    In a stmt of a pattern guard for
                   an equation for ‘compare’:
      u1 ==# u2
    In an equation for ‘compare’:
        (NameU u1) `compare` (NameU u2)
          | u1 <# u2 = LT
          | u1 ==# u2 = EQ
          | otherwise = GT

Language/Haskell/TH/Syntax.hs:729:37:
    Couldn't match expected type ‘Bool’ with actual type ‘Int#’
    In the expression: u1 <# u2
    In a stmt of a pattern guard for
                   an equation for ‘compare’:
      u1 <# u2
    In an equation for ‘compare’:
        (NameL u1) `compare` (NameL u2)
          | u1 <# u2 = LT
          | u1 ==# u2 = EQ
          | otherwise = GT

Language/Haskell/TH/Syntax.hs:730:37:
    Couldn't match expected type ‘Bool’ with actual type ‘Int#’
    In the expression: u1 ==# u2
    In a stmt of a pattern guard for
                   an equation for ‘compare’:
      u1 ==# u2
    In an equation for ‘compare’:
        (NameL u1) `compare` (NameL u2)
          | u1 <# u2 = LT
          | u1 ==# u2 = EQ
          | otherwise = GT
Failed to install template-haskell-2.8.0.0

-- 
Mateusz K.


More information about the Agda mailing list