Importing a name from a module Haskell.* should generate import

[HeinrichApfelmus]

I would like to import an external Haskell module, say, Data.ByteString. However, I am unable to generate the corresponding Haskell import statement.

More specifically: After #379 , I can create an Agda wrapper module Haskell.Data.ByteString

-- agda
module Haskell.Data.ByteString where

postulate
  ByteString : Set

However, when using this module, say, as

-- agda
module Test where

open import Haskell.Data.ByteString using (ByteString)

test : ByteString → ByteString
test x = x

{-# COMPILE AGDA2HS test #-}

the transpilation output is

-- Haskell
module Test where

test :: ByteString -> ByteString
test x = x

This is not what I had in mind, though — I was hoping that the transpilation output would include the import statement.

import Data.ByteString (ByteString)

As a workaround, I can add this import manually with FOREIGN AGDA2HS in the module Test, but this module is not the right place — ideally, I should be able to specify in Haskell.Data.ByteString that the postulated ByteString type is a Haskell identifier that comes from the module Data.ByteString.

[HeinrichApfelmus]

Solving this issue would allow me to contribute Haskell functions modules that are outside of the Prelude, such as:

• Additions to Data.List such as foldl', nub, …
• Additions to Data.Maybe such as isJust, catMaybes, …
• Axiomatization of Data.Set
• Axiomatization of Data.Map
• …

Related issue: #377

[jespercockx]

Ah yes this is a rather important omission in my PR. It should be easy to fix, let me take a look!

[HeinrichApfelmus]

Thank you for the quick fix!

The original issue appears to be fixed, but there is a new issue when the imported module contains postulate instance: #394.