From 1625b0f8d27d4cbe36f421d659637ee9b3b5e85a Mon Sep 17 00:00:00 2001
From: Ryan Scott <ryan.gl.scott@gmail.com>
Date: Thu, 7 Jul 2022 07:17:35 -0400
Subject: [PATCH] Patch Agda to accommodate ghc/ghc!8529

Agda defines its own `applyWhen` function, so use explicit imports from
`Data.Function` to avoid name clashes.
---
 patches/Agda-2.6.2.2.patch | 65 ++++++++++++++++++++++++++++++++++++++
 1 file changed, 65 insertions(+)
 create mode 100644 patches/Agda-2.6.2.2.patch

diff --git a/patches/Agda-2.6.2.2.patch b/patches/Agda-2.6.2.2.patch
new file mode 100644
index 00000000..14a3280a
--- /dev/null
+++ b/patches/Agda-2.6.2.2.patch
@@ -0,0 +1,65 @@
+diff --git a/src/full/Agda/Interaction/Highlighting/LaTeX/Base.hs b/src/full/Agda/Interaction/Highlighting/LaTeX/Base.hs
+index 6138f7b..f2cc7cb 100644
+--- a/src/full/Agda/Interaction/Highlighting/LaTeX/Base.hs
++++ b/src/full/Agda/Interaction/Highlighting/LaTeX/Base.hs
+@@ -20,7 +20,7 @@ import Prelude hiding (log)
+ import Data.Bifunctor (second)
+ import Data.Char
+ import Data.Maybe
+-import Data.Function
++import Data.Function (on)
+ import Data.Foldable (toList)
+ #if !(MIN_VERSION_base(4,11,0))
+ import Data.Semigroup (Semigroup(..))
+diff --git a/src/full/Agda/Interaction/InteractionTop.hs b/src/full/Agda/Interaction/InteractionTop.hs
+index 3191d4e..1ca94eb 100644
+--- a/src/full/Agda/Interaction/InteractionTop.hs
++++ b/src/full/Agda/Interaction/InteractionTop.hs
+@@ -25,7 +25,7 @@ import Control.Monad.STM
+ import Control.Monad.Trans          ( lift )
+ 
+ import qualified Data.Char as Char
+-import Data.Function
++import Data.Function (on)
+ import qualified Data.List as List
+ import qualified Data.Map as Map
+ import Data.Maybe
+diff --git a/src/full/Agda/Interaction/MakeCase.hs b/src/full/Agda/Interaction/MakeCase.hs
+index b47fad3..aee1fa3 100644
+--- a/src/full/Agda/Interaction/MakeCase.hs
++++ b/src/full/Agda/Interaction/MakeCase.hs
+@@ -7,7 +7,7 @@ import Prelude hiding (null)
+ import Control.Monad
+ 
+ import Data.Either
+-import Data.Function
++import Data.Function (on)
+ import qualified Data.List as List
+ import Data.Maybe
+ import Data.Monoid
+diff --git a/src/full/Agda/TypeChecking/SizedTypes/Solve.hs b/src/full/Agda/TypeChecking/SizedTypes/Solve.hs
+index a3abde7..21ad249 100644
+--- a/src/full/Agda/TypeChecking/SizedTypes/Solve.hs
++++ b/src/full/Agda/TypeChecking/SizedTypes/Solve.hs
+@@ -57,7 +57,7 @@ import Control.Monad.Trans.Maybe
+ import Data.Either
+ import Data.Foldable (forM_)
+ import qualified Data.Foldable as Fold
+-import Data.Function
++import Data.Function (on)
+ import qualified Data.List as List
+ import Data.Monoid
+ import qualified Data.Map as Map
+diff --git a/src/full/Agda/Utils/List.hs b/src/full/Agda/Utils/List.hs
+index 37e37e7..02513aa 100644
+--- a/src/full/Agda/Utils/List.hs
++++ b/src/full/Agda/Utils/List.hs
+@@ -7,7 +7,7 @@ import Control.Monad (filterM)
+ import Data.Array (Array, array, listArray)
+ import qualified Data.Array as Array
+ import Data.Bifunctor
+-import Data.Function
++import Data.Function (on)
+ import qualified Data.List as List
+ import qualified Data.List.NonEmpty as List1
+ import Data.List.NonEmpty (pattern (:|), (<|))
-- 
GitLab