Properly differentiate between multiple anonymous modules

src/Agda2Hs/Compile.hs

@@ -37,6 +37,7 @@ initCompileEnv tlm rewrites = CompileEnv
   , minRecordName     = Nothing
   , locals            = []
   , compilingLocal    = False
+  , whereModules      = []
   , copatternsEnabled = False
   , rewrites          = rewrites
   }

src/Agda2Hs/Compile/Function.hs

@@ -222,20 +222,16 @@ compileClause' curModule projName x ty c@Clause{..} = do
           /\ (curModule `isFatherModuleOf`) . qnameModule
 
     children   <- filter isWhereDecl <$> asks locals
-    whereDecls <- compileLocal $ 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
+    -- TODO: remove this when Agda exposes where-provenance in 'Internal' syntax
+    let withWhereModule = case children of
           []    -> id
-          (c:_) -> withCurrentModule $ qnameModule c
+          (c:_) -> addWhereModule $ qnameModule c
+    whereDecls <- withWhereModule $ compileLocal $ mapM (getConstInfo >=> compileFun' True) children
 
     let Just body            = clauseBody
         Just (unArg -> typ)  = clauseType
 
-    hsBody <- inWhereModule $ compileTerm typ body
+    hsBody <- withWhereModule $ compileTerm typ body
 
     let rhs = Hs.UnGuardedRhs () hsBody
         whereBinds | null whereDecls = Nothing

src/Agda2Hs/Compile/Term.hs

@@ -168,16 +168,19 @@ compileDef f ty args =
   ifM (isInlinedFunction f) (compileInlineFunctionApp f ty args) $ do
     reportSDoc "agda2hs.compile.term" 12 $ text "Compiling application of regular function:" <+> prettyTCM f
 
-    currentMod <- currentModule
     let defMod = qnameModule f
 
+    minRecord <- asks minRecordName
+    -- TODO: simplify this when Agda exposes where-provenance in 'Internal' syntax
+    outerWhereModules <- asks whereModules
+
     (ty', args') <-
 
-      -- if the function is called from the same module it's defined in,
+      -- if the function comes from a where-clause
+      -- or is a class-method for the class we are currently defining,
       -- we drop the module parameters
-      -- NOTE(flupe): in the future we're not always gonna be erasing module parameters
-      if prettyShow currentMod `isPrefixOf` prettyShow defMod then do
-        npars <- size <$> (lookupSection =<< currentModule)
+      if defMod `elem` outerWhereModules || Just defMod == minRecord then do
+        npars <- size <$> lookupSection defMod
         let (pars, rest) = splitAt npars args
         ty' <- piApplyM ty pars
         pure (ty', rest)

src/Agda2Hs/Compile/Types.hs

@@ -82,6 +82,8 @@ data CompileEnv = CompileEnv
   -- ^ keeps track of the current clause's where declarations
   , compilingLocal :: Bool
   -- ^ whether we are currently compiling a where clause or pattern-matching lambda
+  , whereModules :: [ModuleName]
+  -- ^ the where-blocks currently in scope. Hack until Agda adds where-prominence
   , copatternsEnabled :: Bool
   -- ^ whether copatterns should be allowed when compiling patterns
   , rewrites :: SpecialRules

src/Agda2Hs/Compile/Utils.hs

@@ -272,6 +272,9 @@ checkInstance u = do
 compileLocal :: C a -> C a
 compileLocal = local $ \e -> e { compilingLocal = True }
 
+addWhereModule :: ModuleName  -> C a -> C a
+addWhereModule mName = local $ \e -> e { whereModules = mName : whereModules e }
+
 modifyLCase :: (Int -> Int) -> CompileState -> CompileState
 modifyLCase f (CompileState {lcaseUsed = n}) = CompileState {lcaseUsed = f n}
 

test/AllTests.agda

@@ -85,6 +85,7 @@ import Issue305
 import Issue302
 import Issue309
 import Issue317
+import Issue353
 import ErasedPatternLambda
 import CustomTuples
 import ProjectionLike
@@ -170,6 +171,7 @@ import Issue305
 import Issue302
 import Issue309
 import Issue317
+import Issue353
 import ErasedPatternLambda
 import CustomTuples
 import ProjectionLike

test/BangPatterns.agda

@@ -13,11 +13,11 @@ myFoldl f x0 (x ∷ xs) = myFoldl f (f x0 x) xs
 
 {-# COMPILE AGDA2HS myFoldl #-}
 
-foldl' : (b -> a -> b) -> Strict b -> List a -> b
-foldl' f (! x0) [] = x0
-foldl' f (! x0) (x ∷ xs) = foldl' f (! f x0 x) xs
+foldl'' : (b -> a -> b) -> Strict b -> List a -> b
+foldl'' f (! x0) [] = x0
+foldl'' f (! x0) (x ∷ xs) = foldl'' f (! f x0 x) xs
 
-{-# COMPILE AGDA2HS foldl' #-}
+{-# COMPILE AGDA2HS foldl'' #-}
 
 data LazyMaybe (a : Set ℓ) : Set ℓ where
   LazyNothing : LazyMaybe a

test/Issue353.agda

@@ -0,0 +1,43 @@
+open import Haskell.Prelude
+
+module Issue353 where
+-- Calling functions between local anonymous modules removed arguments
+
+module FooBar (a : Bool) where
+    hello : Bool
+    hello = a
+    {-# COMPILE AGDA2HS hello #-}
+
+module Foo (a : Bool) where
+    -- If the name of the current module is a prefix of the called module
+    -- they would be interpreted as the same module
+    world : Bool
+    world = FooBar.hello a
+    {-# COMPILE AGDA2HS world #-}
+
+    open FooBar a
+    world2 : Bool
+    world2 = hello
+    {-# COMPILE AGDA2HS world2 #-}
+
+module _ (a : Bool) (b : Int) where
+    foo : Bool
+    foo = not a
+    {-# COMPILE AGDA2HS foo #-}
+
+module _ (b : Bool) where
+
+    bar : Bool
+    bar = foo True 0
+    {-# COMPILE AGDA2HS bar #-}
+
+    baz : Bool
+    baz = bar
+    {-# COMPILE AGDA2HS baz #-}
+
+    callFromNested : Bool
+    callFromNested = nested
+      where nested = bar
+    {-# COMPILE AGDA2HS callFromNested #-}
+
+-- The check is needed both for instance declarations and where-clauses

test/Where.agda

@@ -51,14 +51,16 @@ ex4 b = mult 42
 ex4' : Bool → Nat
 ex4' b = mult (bool2nat b)
   where
+    extra : Nat
+    extra = 14
     mult : Nat → Nat
     mult n = bump n (bool2nat b)
       where
         bump : Nat → Nat → Nat
         bump x y = go (x * y) (n - bool2nat b)
           where
             go : Nat → Nat → Nat
-            go z w = z + x + w + y + n + bool2nat b
+            go z w = z + x + w + y + n + bool2nat b + extra
 
 -- with pattern matching and multiple clauses
 ex5 : List Nat → Nat

test/golden/AllTests.hs

@@ -80,6 +80,7 @@ import Issue305
 import Issue302
 import Issue309
 import Issue317
+import Issue353
 import ErasedPatternLambda
 import CustomTuples
 import ProjectionLike

test/golden/BangPatterns.hs

@@ -8,9 +8,9 @@ myFoldl :: (b -> a -> b) -> b -> [a] -> b
 myFoldl f x0 [] = x0
 myFoldl f x0 (x : xs) = myFoldl f (f x0 x) xs
 
-foldl' :: (b -> a -> b) -> b -> [a] -> b
-foldl' f !x0 [] = x0
-foldl' f !x0 (x : xs) = foldl' f (f x0 x) xs
+foldl'' :: (b -> a -> b) -> b -> [a] -> b
+foldl'' f !x0 [] = x0
+foldl'' f !x0 (x : xs) = foldl'' f (f x0 x) xs
 
 data LazyMaybe a = LazyNothing
                  | LazyJust a

test/golden/Issue353.hs

@@ -0,0 +1,26 @@
+module Issue353 where
+
+hello :: Bool -> Bool
+hello a = a
+
+world :: Bool -> Bool
+world a = hello a
+
+world2 :: Bool -> Bool
+world2 a = hello a
+
+foo :: Bool -> Int -> Bool
+foo a b = not a
+
+bar :: Bool -> Bool
+bar b = foo True 0
+
+baz :: Bool -> Bool
+baz b = bar b
+
+callFromNested :: Bool -> Bool
+callFromNested b = nested
+  where
+    nested :: Bool
+    nested = bar b
+

test/golden/Where.hs

@@ -44,14 +44,16 @@ ex4 b = mult 42
 ex4' :: Bool -> Natural
 ex4' b = mult (bool2nat b)
   where
+    extra :: Natural
+    extra = 14
     mult :: Natural -> Natural
     mult n = bump n (bool2nat b)
       where
         bump :: Natural -> Natural -> Natural
         bump x y = go (x * y) (n - bool2nat b)
           where
             go :: Natural -> Natural -> Natural
-            go z w = z + x + w + y + n + bool2nat b
+            go z w = z + x + w + y + n + bool2nat b + extra
 
 ex5 :: [Natural] -> Natural
 ex5 [] = zro