idris-lang / Idris2

A purely functional programming language with first class types
https://idris-lang.org/
Other
2.52k stars 373 forks source link

Unbound identifier involving multiple modules #2561

Open ysangkok opened 2 years ago

ysangkok commented 2 years ago

Steps to Reproduce

package aio

authors    = "bob malcolm <a@example.com>"
version    = "0.0.1"
readme     = "README.md"

modules = Main

sourcedir = "src"

depends = base, contrib
module Main

import Data.SortedMap

e : SortedMap Unit Int
e = empty

public export
main : IO ()
main = print e

Expected Behavior

idris --repl aio.ipkg with :exec main should print fromList []

Observed Behavior

:exec main prints Exception: attempt to reference unbound identifier DataC-45SortedMapC-45Dependent-toList at line 640, char 140 of build/exec/_tmpchez_app/_tmpchez.ss

Curiously idris2 --find-ipkg src/Main.idr with :exec main works fine. The ipkg looks fine to me though.

phischu commented 8 months ago

I can confirm this in v0.7.0 and came here to report it.