Properly differentiate between multiple anonymous modules

[anka-213]

Partial fix for issue Fixes #353.

Instead of checking if the prettyprinted qualified module name is a prefix to determine if a module is contained within another, we check if the actual list of Name is a prefix, which uses the internal hashes.

With this fix, calling another function within the same local module will still cause an issue, but at least calling other modules won't cause arguments to magically disappear.

I am also not completely sure if the direction of the check is correct? Wouldn't we want to skip arguments only if calling a function from a surrounding module, rather than only when calling into a submodule? The current version is mostly equivalent to an equality check, since you can't call into a where-clause from outside of it

[anka-213]

I tested calling a function from an outer where-clause from a nested where-clause and it did indeed have the expected issue. In addition to flipping the order of the arguments, since we need to get the number of arguments from the module where the function is defined instead of the current module.

nested : Bool → Nat
nested b = inner1
  where
    outer : Nat
    outer = 5

    inner1 : Nat
    inner1 = 2 + inner2
      where
        inner2 : Nat
        inner2 = outer

generates

nested :: Bool -> Natural
nested b = inner1
  where
    outer :: Natural
    outer = 5
    inner1 :: Natural
    inner1 = 2 + inner2
      where
        inner2 :: Natural
        inner2 = outer b -- Notice the extra b argument here

with the current version.

I have also fixed and added a test case for this issue.

[jespercockx]

Thank you for the PR, this is great! For the remaining issue, I wonder if we could throw an error when compiling a call to a function from the current module (or a nested one), that module is anonymous and parametrized, and it is not the where module we are currently compiling. But perhaps getting access to all the information for those checks is tricky.

[anka-213]

my guess is that it is no more difficult to solve the remaining issue than it is to show that error, since that's exactly the info we need to make it behave correctly.

edit: it is easy to detect the "in a class" case you mentioned in the issue. the information is already there and just a call to isClassModule is needed. we do however need some way to detect when we're calling a function from a were-clause, which is probably best solved by adding the info to the CompileEnv. Which I guess could be removed again when the comment

-- TODO: simplify this when Agda exposes where-provenance in 'Internal' syntax

that's scattered over the codebase gets resolved. In that case we wouldn't even need the submodule check, since you can never call into a where-clause unless you're already in the same context.

[anka-213]

this version of the code covers almost all cases, including calling between functions in the same module.

    -- TODO: simplify this when Agda exposes where-provenance in 'Internal' syntax
    defIsClass <- isClassModule defMod -- If we're compiling a minimal class
    isLocal <- asks compilingLocal -- or if we're calling from a where-clause
    localDefs <- asks locals -- or if we're calling into a where-clause

    (ty', args') <- 
      -- and we're calling into a module that we're currently in, then we drop the module parameters.
      if (f `elem` localDefs || isLocal || defIsClass) && (mnameToList defMod `isPrefixOf` mnameToList currentMod) then do

the only issue that remains is if you call a function in the same local module, from within a where-clause, we currently have no easy way to distinguish it from a binding in an outer where-clause (until Agda exposes where-provenance in 'Internal' syntax), so that call still loses arguments. if we remove the isLocal check, the bottom example instead breaks

module _ (b : Bool) where

    foo : Bool
    foo = True
    {-# COMPILE AGDA2HS foo #-}

    -- Works fine now
    bar : Bool
    bar = foo
    {-# COMPILE AGDA2HS bar #-}

    -- The call to foo won't get the necessary Bool argument here
    callFromNested : Bool
    callFromNested = nested
      where nested = foo
    {-# COMPILE AGDA2HS callFromNested #-}

-- We can't fix the above case without breaking this case (unless we add more info to env)
nestedWhere : Bool -> Bool
nestedWhere b = a2
  where
    a1 = True
    a2 = b1
      where b1 = a1
{-# COMPILE AGDA2HS callFromNested #-}

edit: though, I guess, since we can detect if we are in one of those two cases, just not which one, it would be a reasonable thing to add an error message for, since both are relatively rare cases. and especially, since calling the outer where-clause from an inner where-clause was already broken before this patch

[anka-213]

Now I've added code that keeps track of which where-clauses are currently in scope, so we can use that to determine if the arguments should be removed or not. This change replaced the compilation of the body in the module of the where-declaration, since we keep track of it in a different way now.

agda2hs/src/Agda2Hs/Compile/Function.hs

Lines 227 to 230 in 078622c

	-- 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.

This should fix the last issues. All test cases succeed now!

[jespercockx]

Awesome! Thanks again.