summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorUlfNorell <>2016-11-25 08:38:00 (GMT)
committerhdiff <hdiff@hdiff.luite.com>2016-11-25 08:38:00 (GMT)
commit943f54b053c0702c851e5508e36adb55ba934444 (patch)
tree351e33f3ac6e4b89a99f5bb8d3b40c3328b30cab
parent8ade7eec7e2e736938610db608d87cd6b8b5122e (diff)
version 2.5.1.22.5.1.2
-rw-r--r--Agda.cabal14
-rw-r--r--CHANGELOG7
-rw-r--r--dist/build/Agda/Syntax/Parser/Lexer.hs934
-rw-r--r--dist/build/Agda/Syntax/Parser/Parser.hs4
-rw-r--r--src/data/emacs-mode/agda2-mode.el2
-rw-r--r--src/full/Agda/Syntax/Abstract/Views.hs6
6 files changed, 954 insertions, 13 deletions
diff --git a/Agda.cabal b/Agda.cabal
index 30b0e5d..3adcfac 100644
--- a/Agda.cabal
+++ b/Agda.cabal
@@ -1,5 +1,5 @@
name: Agda
-version: 2.5.1.1
+version: 2.5.1.2
cabal-version: >= 1.8
build-type: Custom
license: OtherLicense
@@ -77,8 +77,8 @@ source-repository head
source-repository this
type: git
- location: https://github.com/agda/agda/tree/v2.5.1.1
- tag: v2.5.1.1
+ location: https://github.com/agda/agda/tree/v2.5.1.2
+ tag: v2.5.1.2
flag cpphs
default: True
@@ -175,9 +175,9 @@ library
else
build-depends: zlib >= 0.4.0.1 && < 0.7
- build-tools:
- alex >= 3.1.0 && < 3.2
- , happy >= 1.19.4 && < 2
+ -- Agda doesn't build with Alex 3.2.0.
+ build-tools: alex >= 3.1.0 && < 3.2.0 || >= 3.2.1 && < 3.3
+ , happy >= 1.19.4 && < 2
exposed-modules: Agda.Auto.Auto
Agda.Auto.CaseSplit
@@ -536,7 +536,7 @@ executable agda
hs-source-dirs: src/main
main-is: Main.hs
build-depends:
- Agda == 2.5.1.1
+ Agda == 2.5.1.2
-- Nothing is used from the following package, except for the
-- prelude.
, base >= 4.6.0.1 && < 6
diff --git a/CHANGELOG b/CHANGELOG
index 62f2315..3a42d11 100644
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -1,4 +1,11 @@
------------------------------------------------------------------------
+-- Release notes for Agda version 2.5.1.2
+------------------------------------------------------------------------
+
+* Fixed broken type signatures that were incorrectly accepted due to
+ GHC #12784 (https://ghc.haskell.org/trac/ghc/ticket/12784).
+
+------------------------------------------------------------------------
-- Release notes for Agda version 2.5.1.1
------------------------------------------------------------------------
diff --git a/dist/build/Agda/Syntax/Parser/Lexer.hs b/dist/build/Agda/Syntax/Parser/Lexer.hs
index 135bf75..b4dee9d 100644
--- a/dist/build/Agda/Syntax/Parser/Lexer.hs
+++ b/dist/build/Agda/Syntax/Parser/Lexer.hs
@@ -267,6 +267,940 @@ alex_action_117 = identifier
{-# LINE 1 "templates/GenericTemplate.hs" #-}
{-# LINE 1 "<built-in>" #-}
{-# LINE 1 "<command-line>" #-}
+{-# LINE 12 "<command-line>" #-}
+{-# LINE 1 "/usr/local/Cellar/ghc/8.0.1/lib/ghc-8.0.1/include/ghcversion.h" #-}
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+{-# LINE 12 "<command-line>" #-}
+{-# LINE 1 "/var/folders/vh/5xdrm2c941q4v68c8rr_9c5m0000gn/T/ghc93933_0/ghc_2.h" #-}
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+{-# LINE 12 "<command-line>" #-}
{-# LINE 1 "templates/GenericTemplate.hs" #-}
-- -----------------------------------------------------------------------------
-- ALEX TEMPLATE
diff --git a/dist/build/Agda/Syntax/Parser/Parser.hs b/dist/build/Agda/Syntax/Parser/Parser.hs
index 49642f6..d66d4b4 100644
--- a/dist/build/Agda/Syntax/Parser/Parser.hs
+++ b/dist/build/Agda/Syntax/Parser/Parser.hs
@@ -61,9 +61,8 @@ import Agda.Utils.Impossible
import qualified Data.Array as Happy_Data_Array
import qualified GHC.Exts as Happy_GHC_Exts
import Control.Applicative(Applicative(..))
-import Control.Monad (ap)
--- parser produced by Happy Version 1.19.5
+-- parser produced by Happy Version 1.19.4
newtype HappyAbsSyn t13 t14 t15 t37 t40 t43 t44 t45 t53 t54 t83 = HappyAbsSyn HappyAny
#if __GLASGOW_HASKELL__ >= 607
@@ -6322,7 +6321,6 @@ tests = runTests "Agda.Syntax.Parser.Parser"
]
{-# LINE 1 "templates/GenericTemplate.hs" #-}
{-# LINE 1 "templates/GenericTemplate.hs" #-}
-{-# LINE 1 "<built-in>" #-}
{-# LINE 1 "<command-line>" #-}
{-# LINE 1 "templates/GenericTemplate.hs" #-}
-- Id: GenericTemplate.hs,v 1.26 2005/01/14 14:47:22 simonmar Exp
diff --git a/src/data/emacs-mode/agda2-mode.el b/src/data/emacs-mode/agda2-mode.el
index d58eaf9..3b47631 100644
--- a/src/data/emacs-mode/agda2-mode.el
+++ b/src/data/emacs-mode/agda2-mode.el
@@ -10,7 +10,7 @@
;;; Code:
-(defvar agda2-version "2.5.1.1"
+(defvar agda2-version "2.5.1.2"
"The version of the Agda mode.
Note that the same version of the Agda executable must be used.")
diff --git a/src/full/Agda/Syntax/Abstract/Views.hs b/src/full/Agda/Syntax/Abstract/Views.hs
index 03a7f86..ef0957e 100644
--- a/src/full/Agda/Syntax/Abstract/Views.hs
+++ b/src/full/Agda/Syntax/Abstract/Views.hs
@@ -1,5 +1,7 @@
{-# LANGUAGE CPP #-}
{-# LANGUAGE DefaultSignatures #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE NoMonoLocalBinds #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE TupleSections #-}
@@ -90,8 +92,8 @@ deepUnscopeDecl d = [deepUnscope d]
class ExprLike a where
-- | The first expression is pre-traversal, the second one post-traversal.
recurseExpr :: (Applicative m) => (Expr -> m Expr -> m Expr) -> a -> m a
- default recurseExpr :: (Traversable f, Applicative m)
- => (Expr -> m Expr -> m Expr) -> f a -> m (f a)
+ default recurseExpr :: (Traversable f, ExprLike a', a ~ f a', Applicative m)
+ => (Expr -> m Expr -> m Expr) -> a -> m a
recurseExpr = traverse . recurseExpr
foldExpr :: Monoid m => (Expr -> m) -> a -> m