diff --git a/test/AllTests.agda b/test/AllTests.agda index c62f9f24..721e2fd6 100644 --- a/test/AllTests.agda +++ b/test/AllTests.agda @@ -91,6 +91,7 @@ import ErasedPatternLambda import CustomTuples import ProjectionLike import FunCon +import Issue308 {-# FOREIGN AGDA2HS import Issue14 @@ -179,4 +180,5 @@ import ErasedPatternLambda import CustomTuples import ProjectionLike import FunCon +import Issue308 #-} diff --git a/test/Issue308.agda b/test/Issue308.agda new file mode 100644 index 00000000..ddd05f40 --- /dev/null +++ b/test/Issue308.agda @@ -0,0 +1,22 @@ +open import Haskell.Prelude + +record Class (a : Set) : Set where + field + foo : a → a +open Class {{...}} public +{-# COMPILE AGDA2HS Class class #-} + +module M1 (@0 X : Set) where + + instance + ClassInt : Class Int + ClassInt .foo = _+ 1 + {-# COMPILE AGDA2HS ClassInt #-} + +module M2 (@0 X : Set) where + + open M1 X + + tester : Int + tester = foo 41 + {-# COMPILE AGDA2HS tester #-} diff --git a/test/golden/AllTests.hs b/test/golden/AllTests.hs index f970e50c..0f7d8576 100644 --- a/test/golden/AllTests.hs +++ b/test/golden/AllTests.hs @@ -86,4 +86,5 @@ import ErasedPatternLambda import CustomTuples import ProjectionLike import FunCon +import Issue308 diff --git a/test/golden/Issue308.hs b/test/golden/Issue308.hs new file mode 100644 index 00000000..8dd7f11b --- /dev/null +++ b/test/golden/Issue308.hs @@ -0,0 +1,11 @@ +module Issue308 where + +class Class a where + foo :: a -> a + +instance Class Int where + foo = (+ 1) + +tester :: Int +tester = foo 41 +