[ #308 ] Already fixed by new canonicity check, adding test case

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

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

test/golden/AllTests.hs

@@ -86,4 +86,5 @@ import ErasedPatternLambda
 import CustomTuples
 import ProjectionLike
 import FunCon
+import Issue308
 

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
+