Importing class instances from a module Haskell.* should generate valid import

[HeinrichApfelmus]

I would like to import an external Haskell module, say, Data.ByteString. However, when this module contains postulate instance, the transpiled code contains an invalid import Haskell.Data.ByteString () statement that attempts to import class instances.

Specifically, after #392, the input files

-- Haskell/Data/ByteString.agda
module Haskell.Data.ByteString where

open import Haskell.Prelude

postulate
  ByteString : Set

  instance
    iEqByteString : Eq ByteString

-- Test.agda
module Test where

open import Haskell.Prelude
open import Haskell.Data.ByteString using (ByteString)

test : ByteString → ByteString → Bool
test x y = x == y

{-# COMPILE AGDA2HS test #-}

will produce the output

module Test where

import Data.ByteString (ByteString)
import Haskell.Data.ByteString ()
import Prelude hiding (null, subtract)

test :: ByteString -> ByteString -> Bool
test x y = x == y

The line import Haskell.Data.ByteString () should not be present.

I'd be happy with a hacky fix, but in the long run, I think that Agda2hs would benefit from being more systematic about module provenance information. 😅

[jespercockx]

I've made a fix and even made the module resolution of agda2hs a bit more robust in the process! When compiling a module name, it is now also classified in one of three categories:

• a primitive module, corresponding to Prelude in Haskell
• a Haskell module, corresponding to an existing module in Haskell (other than Prelude)
• an Agda module, corresponding to a module generated by agda2hs