Search code examples
importsyntaxmodulenamespacesidris

`import using` or `import hiding` in Idris2

I'd like to import Control.App into a module that refers to PrimIO.PrimIO via the unqualified name PrimIO in a lot of places. The problem, of course, is that Control.App also exports a definition named PrimIO. I would like to minimize the damage by importing either only App or everything but PrimIO from Control.App; i.e. what one would do with import Control.App (App) or import Control.App hiding (PrimIO) in Haskell.

What is the Idris2 way of doing this?

Solution

  • Based on @michaelmesser's comment, I was able to get this working with the following:

    import Control.App
%hide Control.App.PrimIO

    However, this doesn't give me a good way of explicitly referring to Control.App.PrimIO when I do need to refer to it.