Disallow compilation of symbols from local modules

[jespercockx]

Haskell does not have local modules, so they should not be allowed by agda2hs. We could make an exception if the local module is open publiced at the top-level.

[jespercockx]

In agda2hs 1.3, local definitions are allowed and just treated as top-level definitions (with the module parameters as additional arguments). However, this is actually problematic:

module _ where

open import Haskell.Prelude

module M1 where

  foo : Int
  foo = 21

  {-# COMPILE AGDA2HS foo #-}

module M2 where

  foo : Int
  foo = 21

  {-# COMPILE AGDA2HS foo #-}

bar : Int
bar = M1.foo + M2.foo

{-# COMPILE AGDA2HS bar #-}

produces

foo :: Int
foo = 21

foo :: Int
foo = 21

bar :: Int
bar = foo + foo

with a duplicate definition of foo.

[anka-213]

The solution would probably be to explicitly check for duplicate names and give an error message explaining the issue