MAlonzo: name conflicts with private definition

[omelkonian]

MAlonzo: name conflicts with private definition

[nad]

I put this in the icebox for now, but contributions are welcome.

[nad]

Maybe I misunderstood something, but isn't the problem in your own Haskell code? There is no guarantee that every symbol exported from every Haskell file generated by Agda will have a globally unique name.

[omelkonian]

In M2, I have private Value = ... which I would expect would be respected by MAlonzo. Instead, an artifact of the internals d_Value leaks to the exported identifiers and also happens to conflict with an existing name.

So, I believe there are two related issues with MAlonzo here:

1. When compiling an Agda module Ag to a Haskell module Hs, the following invariant is not respected:
   Ag.exports == Hs.exports.
2. If (1) is impossible, MAlonzo could at least make sure the internal ids that leak to the public namespace not to reuse names from imported modules.

[nad]

1. When compiling an Agda module Ag to a Haskell module Hs, the following invariant is not respected:
   Ag.exports == Hs.exports.

Private names can appear implicitly in importing Agda modules (due to reduction and unification), and can thus also appear in importing Haskell modules.

2. If (1) is impossible, MAlonzo could at least make sure the internal ids that leak to the public namespace not to reuse names from imported modules.

A different approach might be to have two sets of generated Haskell modules:

• The current one. It currently has the prefix MAlonzo, that could be changed to something like Agda_GHC_backend.Internal (perhaps with different prefixes for the non-strict and strict backends).
• A set of modules that reexports exactly those definitions that are exported from the Agda modules. These modules could have a prefix like Agda_GHC_backend.Exported.