Calling between functions in (multiple) anonymous modules causes arguments to disappear

[anka-213]

This Agda code

open import Haskell.Prelude

module MultipleAnonModules where

module _ (a : Bool) (b : Int) where
    foo : Bool
    foo = not a
{-# COMPILE AGDA2HS neg #-}

module _ (b : Int) where
    bar : Bool
    bar = foo True 2 -- Note that foo is called with two arguments

{-# COMPILE AGDA2HS bar #-}

generates this Haskell code

module MultipleAnonModules where

foo :: Bool -> Int -> Bool
foo a b = not a

bar :: Int -> Bool
bar b = foo 2 -- Here the first argument disappeared

For each parameter in the second anonymous module, one argument in the call into the first module disappears. It doesn't matter what the parameters are or if they are used or not.

---

The same issue appears if both functions are in the same module:

open import Haskell.Prelude
module OneAnonModule where

module _ (a : Bool) (b : Int) where
    foo : Bool
    foo = not a

    bar : Bool
    bar = foo

    {-# COMPILE AGDA2HS bar #-}
    {-# COMPILE AGDA2HS neg #-}

This generates

module OneAnonModule where

foo :: Bool -> Int -> Bool
foo a b = not a

bar :: Bool -> Int -> Bool
bar a b = foo

But this instance of the bug feels slightly less surprising, since now the generated code looks like the original.

[anka-213]

I also encountered a different mysterious related bug that I don't currently have a good MWE for. If I have anonymous modules in a file, then in some cases, a completely unrelated function later in the file (not in an anonymous module) can lose bindings from its where-clause when I move things out of that anonymous module.

[jespercockx]

The problem seems to be caused by this piece of code, which looks like it's a leftover from the time when all module parameters would be erased by agda2hs:

https://github.com/agda/agda2hs/blob/0467b2675dbfb7454bee830fbd904ae30c89a5f0/src/Agda2Hs/Compile/Term.hs#L174-L184

Unfortunately, removing these lines messes with the way we compile minimal class instances. Here is a minimal example that gets compiled wrongly without it:

record C (a : Set) : Set where
  field
    fld : Maybe a
    fld2 : Maybe a

record MinC (a : Set) : Set where
  fld2 : Maybe a
  fld2 = Nothing

  fld : Maybe a
  fld = fld2

open C {{...}} public

{-# COMPILE AGDA2HS C class MinC #-}

Gets compiled to:

class C a where
    fld :: Maybe a
    fld2 :: Maybe a
    {-# MINIMAL #-}
    fld = fld2 r
    fld2 = Nothing

where the call to fld2 has a spurious argument r. So before we can remove the old code, we should properly handle calls to default method implementations defined in a record module.

[anka-213]

I have been trying to make a minimal example of the where-clause bug, but was unable to do so, since almost any change I make in the file affects if the bug happens or not. If I add any dependent function here, then the last function in the file loses its last where-clause definitions. However, if I do it a few lines earlier, the bug does not trigger.

I don't know if this is a separate bug or not, but it seems to be affected by anonymous modules, so it might be caused by the same thing.

[anka-213]

From what I can tell, at least part of the issue with the line of code that you linked is that the definition of "same module" is "has the same name", which will be true for all anonymous modules in the same module.

Replacing that line with

if mnameToList currentMod `isPrefixOf` mnameToList defMod then do

resolves the first issue with different anonymous modules, since now different anonymous modules are treated as actually being different. But there is still the issue that the argument disappears within the same module.

Edit: This should also resolve potential bugs from one module name being the prefix of another module name.

[anka-213]

I can confirm that changing this line to be more precise also fixes the where-clause issue I had.

Looking at debug-logs, it seems like where-clauses are treated as anonymous modules internally by Agda and also have the module name _. So I guess where-clauses are also a case where the arguments need to be removed when calling functions within a module. If I remove those lines, where-clauses also get spurious extra-arguments.