Erasure/getArity: definition not found for Data.Tree.Empty

[corazza]

I'm trying to use https://github.com/jfdm/idris-containers (I opened an issue there as well, but I found another similar issue here (#3713) that suggest this might be more related to Idris itself). This package can compile/install on its own, but when I try compiling a simple executable with it, I get the following error:

$ idris --build test.ipkg
Entering directory `.\src'
idris.exe: Erasure/getArity: definition not found for Data.Tree.Empty
CallStack (from HasCallStack):
  error, called at src\Idris\Erasure.hs:605:20 in idris-1.3.2-J5ej6IrsDvx8J6Vzd0MiVR:Idris.Erasure

This is on Idris 1.3.2. I have another machine that's stuck on 1.3.1 because of this, and the error is not present there.

The code I'm trying to compile is (probably irrelevant, happens in another codebase too):

module Main

import Data.AVL.Set

remove : Ord a => a -> Set a -> Set a
remove x = let to_remove = insert x empty
               in flip difference to_remove

example : Set Int
example = fromList [1, 2, 3]

main : IO ()
main = do
  putStrLn $ show $ Set.toList $ remove 3 example

[jamietallingbell]

Did you ever find a fix for this? I am getting the exact same thing. I am also using idris-containers, but as you say it might have nothing to do with that.

Going to try downgrading to Idris 1.3.1 to avoid this, but it would obviously be good to find a fix for 1.3.2

[jfdm]

I’ll have a look at this next time I am at work. The original issue came at a time of great personal change. But local builds of Idris 1.3.2 builds the package fine. Try clobbering the package of ibc and nuking the contents of ‘Idris —libdir’/containers.

[jfdm]

Right, I have had a look. Turns out that the error was most likely a PEBKAC issue. During refactoring, I might have inadvertently made some terms hidden. I have tested the attached example locally.

I do not think this is an issue with Erasure. @ziman would be best to comment if it was.

[ziman]

I agree, this should definitely not happen. We did have some erasure bugs in the past but it's been a long time since I've seen one so reports are welcome.

I can't reproduce the bug with 1.3.2-git:7af67ac42, though. Is it still there?

$ idris --version
1.3.2-git:7af67ac42

$ idris x.idr -p containers -o x
$ ./x
[1, 2]

$ idris --build containers-test.ipkg 
Type checking ./Test/Random/Values.idr
Type checking ./Data/AVL/Test/Dict.idr
Type checking ./Data/AVL/Test/Set.idr
Type checking ./Data/AVL/Test/Graph.idr
Type checking ./Data/Test/Stack.idr
Type checking ./Data/Test/Queue.idr
Type checking ./Data/Test/RedBlack.idr
$ 

[jfdm]

If you use HEAD-2 of containers the issue should manifest.

[ziman]

Yep, reproduced, thanks. This looks strange, I'll dig deeper after work.

[jfdm]

@ziman For what it is worth:

• there was a wrong module name in Data.AVL.Dict, and
• you might want to double check the visibility modifiers on imports.

Essentially, there was a Data.AVL that represented the original core representation of AVL trees that publicly imported (i.e. exported) the collection of core modules to be used in the Data.AVL.* modules. I am thinking either there was a visibility modifier issue (PEBKAC) or there is something about publicly exported modules in a nested setting that was not being picked up by the Erasure code.

[gallais]

Hit the same bug today while working on Idris2. It started occurring after I removed a non-exported function that was used in the body of an exported one. Rebuilt everything from scratch and the error went away.