diff --git a/Agda.cabal b/Agda.cabal
--- 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 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 @@
   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 @@
   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
--- 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
--- a/dist/build/Agda/Syntax/Parser/Lexer.hs
+++ b/dist/build/Agda/Syntax/Parser/Lexer.hs
@@ -267,6 +267,940 @@
 {-# 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
--- a/dist/build/Agda/Syntax/Parser/Parser.hs
+++ b/dist/build/Agda/Syntax/Parser/Parser.hs
@@ -61,9 +61,8 @@
 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 @@
   ]
 {-# 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
--- 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
--- 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 @@
 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