Function used in type cannot be found unless imported publicly in declaring module

[msmorgan]

Reporting an issue discovered in #4154.

Steps to Reproduce

Clone this repository, then run:

$ idris --checkpkg export_bug.ipkg

Expected Behavior

Checks successfully.

Observed Behavior

The following error occurs:

Type checking ./Main.idr
Main.idr:6:12:When checking right hand side of testFinite with expected type
        MonadLike True Int

No such variable InfUtil.inf
Main.idr:10:14:When checking right hand side of testInfinite with expected type
        MonadLike True Int

No such variable InfUtil.inf

Changing the import line in MonadLike.idr fixes the issue. There is a branch named import-public which contains this change.

[ahmadsalim]

@msmorgan Thanks for reporting the issue. It would indeed be nice if one got a compile error when something is exported publicly but depends on a privately imported module.

In general the module system of Idris could use a lift w.r.t selective import/export of things.