Idris2中的“导入使用”或“导入隐藏”

Question

我想将Control.App导入到一个模块中，该模块通过许多地方的非限定名PrimIO来引用PrimIO.PrimIO。当然，问题是Control.App还导出了一个名为PrimIO的定义。我希望通过只从App导入或从Control.App导入 PrimIO以外的所有东西来最小化损害；也就是说，在Haskell中如何处理import Control.App (App)或import Control.App hiding (PrimIO)。

这样做的Idris2方式是什么？

Answer 1

基于@michaelmesser的评论，我能够使用以下方法完成此工作：

import Control.App
%hide Control.App.PrimIO

但是，当我确实需要引用Control.App.PrimIO时，这并不能给我提供一个显式引用它的好方法。