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 +