From 481d885e45a5cc136d818202dc1b6325f55046c3 Mon Sep 17 00:00:00 2001
From: flupe <lucas@escot.me>
Date: Tue, 1 Oct 2024 14:06:25 +0200
Subject: [PATCH] [ fix #373 ] enable existing-class on postulated type formers

---
 src/Agda2Hs/Compile/Utils.hs |  1 +
 test/AllTests.agda           |  2 ++
 test/Issue373.agda           | 21 +++++++++++++++++++++
 test/golden/AllTests.hs      |  1 +
 test/golden/Issue373.hs      |  8 ++++++++
 5 files changed, 33 insertions(+)
 create mode 100644 test/Issue373.agda
 create mode 100644 test/golden/Issue373.hs

diff --git a/src/Agda2Hs/Compile/Utils.hs b/src/Agda2Hs/Compile/Utils.hs
index 9ff54f3f..1cdce461 100644
--- a/src/Agda2Hs/Compile/Utils.hs
+++ b/src/Agda2Hs/Compile/Utils.hs
@@ -173,6 +173,7 @@ isClassName q = getConstInfo' q >>= \case
       ClassPragma _       -> True
       ExistingClassPragma -> True
       _                   -> False
+  Right Defn{defName = r, theDef = Axiom{}} -> processPragma r <&> (ExistingClassPragma ==)
   _                       -> return False
 
 -- | Check if the given type corresponds to a class constraint in Haskell.
diff --git a/test/AllTests.agda b/test/AllTests.agda
index 721e2fd6..e793b94d 100644
--- a/test/AllTests.agda
+++ b/test/AllTests.agda
@@ -92,6 +92,7 @@ import CustomTuples
 import ProjectionLike
 import FunCon
 import Issue308
+import Issue373
 
 {-# FOREIGN AGDA2HS
 import Issue14
@@ -181,4 +182,5 @@ import CustomTuples
 import ProjectionLike
 import FunCon
 import Issue308
+import Issue373
 #-}
diff --git a/test/Issue373.agda b/test/Issue373.agda
new file mode 100644
index 00000000..b3b1545a
--- /dev/null
+++ b/test/Issue373.agda
@@ -0,0 +1,21 @@
+module Issue373 where
+
+open import Haskell.Prelude
+
+{-# FOREIGN AGDA2HS
+
+class MyShow a where
+  myshow :: a -> String
+
+#-}
+
+postulate
+  MyShow : Set → Set
+  myshow : {{ MyShow a }} → a → String
+
+{-# COMPILE AGDA2HS MyShow existing-class #-}
+
+anothershow : {{ MyShow a }} → a → String
+anothershow = myshow
+
+{-# COMPILE AGDA2HS anothershow #-}
diff --git a/test/golden/AllTests.hs b/test/golden/AllTests.hs
index 0f7d8576..2e4ccc81 100644
--- a/test/golden/AllTests.hs
+++ b/test/golden/AllTests.hs
@@ -87,4 +87,5 @@ import CustomTuples
 import ProjectionLike
 import FunCon
 import Issue308
+import Issue373
 
diff --git a/test/golden/Issue373.hs b/test/golden/Issue373.hs
new file mode 100644
index 00000000..0fe773cf
--- /dev/null
+++ b/test/golden/Issue373.hs
@@ -0,0 +1,8 @@
+module Issue373 where
+
+class MyShow a where
+  myshow :: a -> String
+
+anothershow :: MyShow a => a -> String
+anothershow = myshow
+