You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
ohad@ohad-coml-laptop:~$ cd dev/
ohad@ohad-coml-laptop:~/dev$ git clone https://github.com/ohad/module-bug-report.git
Cloning into 'module-bug-report'...
remote: Enumerating objects: 16, done.
remote: Counting objects: 100% (16/16), done.
remote: Compressing objects: 100% (14/14), done.
remote: Total 16 (delta 0), reused 16 (delta 0), pack-reused 0
Unpacking objects: 100% (16/16), done.
ohad@ohad-coml-laptop:~/dev$ cd module-bug-report/
ohad@ohad-coml-laptop:~/dev/module-bug-report$ cd a
ohad@ohad-coml-laptop:~/dev/module-bug-report/a$ idris2 --build a.ipkg
1/2: Building Data.Structure (Data/Structure.idr)
2/2: Building ModuleA (ModuleA.idr)
ohad@ohad-coml-laptop:~/dev/module-bug-report/a$ cd ../b
ohad@ohad-coml-laptop:~/dev/module-bug-report/b$ idris2 --build b.ipkg
1/2: Building Data.Structure (Data/Structure.idr)
2/2: Building ModuleB (ModuleB.idr)
ohad@ohad-coml-laptop:~/dev/module-bug-report/b$ cd ../c/
ohad@ohad-coml-laptop:~/dev/module-bug-report/c$ mkdir depends
ohad@ohad-coml-laptop:~/dev/module-bug-report/c$ mkdir depends/a-0
ohad@ohad-coml-laptop:~/dev/module-bug-report/c$ mkdir depends/b-0
ohad@ohad-coml-laptop:~/dev/module-bug-report/c$ cp -r ../a/build/ttc/* depends/a-0/
ohad@ohad-coml-laptop:~/dev/module-bug-report/c$ cp -r ../b/build/ttc/* depends/b-0/
ohad@ohad-coml-laptop:~/dev/module-bug-report/c$ idris2 --build c.ipkg
Expected Behavior
Both client modules type-check
Observed Behavior
Neither client module typechecks:
1/2: Building IndirectClient (IndirectClient.idr)
Error: While processing right hand side of prf. When
unifying B = B and fromInteger 1 + ConstantA = ConstantB.
Undefined name Data.Structure.B.
IndirectClient:7:7--7:11
3 | import ModuleA
4 | import ModuleB
5 |
6 | prf : 1 + ConstantA === ConstantB
7 | prf = Refl
^^^^
Because both packages have the same module Data.Structure, idris doesn't seem to find the module from package b.
The text was updated successfully, but these errors were encountered:
Anything module related is a bit verbose, sorry!
I'm using this scratch repo: https://github.com/ohad/module-bug-report
Steps to Reproduce
Expected Behavior
Both client modules type-check
Observed Behavior
Neither client module typechecks:
Because both packages have the same module
Data.Structure
, idris doesn't seem to find the module from packageb
.The text was updated successfully, but these errors were encountered: