[ fix #210 ] More robust calculation of which arguments to drop via g…

…etDefFreeVars

src/Agda2Hs/Compile/Function.hs

@@ -133,11 +133,18 @@ compileClause' curModule x c@Clause{..} = do
   reportSDoc "agda2hs.compile" 7 $ "compiling clause: " <+> prettyTCM c
   addContext (KeepNames clauseTel) $ do
     ps <- compilePats namedClausePats
-    body <- compileTerm $ fromMaybe __IMPOSSIBLE__ clauseBody
     let isWhereDecl = not . isExtendedLambdaName
           /\ (curModule `isFatherModuleOf`) . qnameModule
     children <- filter isWhereDecl <$> asks locals
     whereDecls <- mapM (getConstInfo >=> compileFun' True) children
+    -- Jesper, 2023-10-30: We should compile the body in the module of the
+    -- `where` declarations (if there are any) in order to drop the arguments
+    -- that correspond to the pattern variables of this clause from the calls to
+    -- the functions defined in the `where` block.
+    let inWhereModule = case children of
+          [] -> id
+          (c:_) -> withCurrentModule $ qnameModule c
+    body <- inWhereModule $ compileTerm $ fromMaybe __IMPOSSIBLE__ clauseBody
     let rhs = Hs.UnGuardedRhs () body
         whereBinds | null whereDecls = Nothing
                    | otherwise       = Just $ Hs.BDecls () (concat whereDecls)

src/Agda2Hs/Compile/Term.hs

@@ -240,12 +240,9 @@ compileTerm v = do
           False -> do
             reportSDoc "agda2hs.compile.term" 12 $ text "Compiling application of regular function"
             -- Drop module parameters of local `where` functions
-            xs <- asks locals
-            reportSDoc "agda2hs.compile.term" 15 $ text "Locals: " <+> (prettyTCM xs)
-            n <- if
-              | f `elem` xs -> size <$> lookupSection (qnameModule f)
-              | otherwise   -> return 0
-            (`app` drop n es) . Hs.Var () =<< compileQName f
+            moduleArgs <- getDefFreeVars f
+            reportSDoc "agda2hs.compile.term" 15 $ text "Module arguments for" <+> (prettyTCM f <> text ":") <+> prettyTCM moduleArgs
+            (`app` drop moduleArgs es) . Hs.Var () =<< compileQName f
     Con h i es
       | Just semantics <- isSpecialCon (conName h) -> semantics h i es
     Con h i es -> isUnboxConstructor (conName h) >>= \case

test/AllTests.agda

@@ -59,6 +59,7 @@ import IOFile
 import IOInput
 import Issue200
 import Issue169
+import Issue210
 
 {-# FOREIGN AGDA2HS
 import Issue14
@@ -118,4 +119,5 @@ import IOFile
 import IOInput
 import Issue200
 import Issue169
+import Issue210
 #-}

test/Issue210.agda

@@ -0,0 +1,35 @@
+open import Haskell.Prelude hiding (f)
+
+record Test (a : Set) : Set₁ where
+  field
+    f : a -> a
+open Test {{...}} public
+{-# COMPILE AGDA2HS Test class #-}
+
+instance
+  testNat : Test Nat
+  Test.f testNat n = h
+    where
+    g : Nat
+    g = 3 + n
+    h : Nat
+    h = n + g
+  {-# COMPILE AGDA2HS testNat #-}
+
+f1 : Nat -> Nat
+f1 n = h1
+  where
+  g1 : Nat
+  g1 = 3 + n
+  h1 : Nat
+  h1 = n + g1
+{-# COMPILE AGDA2HS f1 #-}
+
+f2 : Nat -> Nat
+f2 n = h2 n
+  where
+  g2 : Nat
+  g2 = 3 + n
+  h2 : Nat -> Nat
+  h2 m = n + g2 + m
+{-# COMPILE AGDA2HS f2 #-}

test/golden/AllTests.hs

@@ -57,4 +57,5 @@ import IOFile
 import IOInput
 import Issue200
 import Issue169
+import Issue210
 

test/golden/Issue210.hs

@@ -0,0 +1,31 @@
+module Issue210 where
+
+import Numeric.Natural (Natural)
+
+class Test a where
+    f :: a -> a
+
+instance Test Natural where
+    f n = h
+      where
+        g :: Natural
+        g = 3 + n
+        h :: Natural
+        h = n + g
+
+f1 :: Natural -> Natural
+f1 n = h1
+  where
+    g1 :: Natural
+    g1 = 3 + n
+    h1 :: Natural
+    h1 = n + g1
+
+f2 :: Natural -> Natural
+f2 n = h2 n
+  where
+    g2 :: Natural
+    g2 = 3 + n
+    h2 :: Natural -> Natural
+    h2 m = n + g2 + m
+