[ fix #359 ] Do not reapply clauses of projection-like functions to t…

…heir parameters

src/Agda2Hs/Compile/Function.hs

@@ -131,7 +131,14 @@ compileFun' withSig def@Defn{..} = inTopContext $ withCurrentModule m $ do
       -- module parameters (see https://github.com/agda/agda2hs/issues/305).
       liftTCM $ setModuleCheckpoint m
 
-      pars <- getContextArgs
+      -- We apply the function clause to the module parameters from the context.
+      -- In case of a projection-like function, the clause is already
+      -- (partially or fully) applied so we should not apply again
+      -- (see https://github.com/agda/agda2hs/issues/359)
+      let droppedPars = case funProjection of
+            Left{} -> 0
+            Right proj -> size $ getProjLams $ projLams proj
+      pars <- drop droppedPars <$> getContextArgs
       reportSDoc "agda2hs.compile.type" 8 $ "Function module parameters: " <+> prettyTCM pars
 
       reportSDoc "agda2hs.compile.type" 8 $ "Function type (before instantiation): " <+> inTopContext (prettyTCM defType)

test/AllTests.agda

@@ -87,6 +87,7 @@ import Issue309
 import Issue317
 import ErasedPatternLambda
 import CustomTuples
+import ProjectionLike
 
 {-# FOREIGN AGDA2HS
 import Issue14
@@ -171,4 +172,5 @@ import Issue309
 import Issue317
 import ErasedPatternLambda
 import CustomTuples
+import ProjectionLike
 #-}

test/ProjectionLike.agda

@@ -0,0 +1,16 @@
+
+open import Haskell.Prelude
+
+module _ (@0 n : Bool) where
+
+record R : Set where
+  field
+    fld : Int
+open R public
+
+{-# COMPILE AGDA2HS R #-}
+
+foo : R → Int
+foo x = fld x
+
+{-# COMPILE AGDA2HS foo #-}

test/golden/AllTests.hs

@@ -82,4 +82,5 @@ import Issue309
 import Issue317
 import ErasedPatternLambda
 import CustomTuples
+import ProjectionLike