[ fix agda#373 ] enable existing-class on postulated type formers

Author: flupe

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.

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
 #-}

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 #-}

test/golden/AllTests.hs

@@ -87,4 +87,5 @@ import CustomTuples
 import ProjectionLike
 import FunCon
 import Issue308
+import Issue373
 

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
+