Type binds are incorrectly added to the functions ASTs as 'use' terms on import

[nicolas-abril]

Reproducing the behavior

The error was initially reported by @NoamDev here #725 (comment)

Considering this program

# a.bend
from b import *

type MyType:
  A {data: u24}
  B {data: u24}

# b.bend
from a import *

Foo: MyType -> MyType
(Foo (MyType/A a)) = (MyType/A a)
(Foo (MyType/B b)) = (MyType/B b)

# main.bend
from a import *
main = "hello world"

> bend run main.bend
Errors:
In b :
In definition 'b/Foo':
  Unbound variable 'a/MyType'.
  Unbound variable 'a/MyType'.

Investigating this a little bit, it seems that the rebind use MyType = a/MyType in import files that import types.

This happens because all imported binds are considered the same for the import system instead of differentiating between functions and types. The logic for renaming type binds only checks local functions and not imported ones.

I think the way to fix this is to change imports::book::apply_import_binds, specifically to consider the correct sources in the loop that inserts binds in the variable adt_imports, but it seems that it'll require a considerable rework of the import bind logic.

System Settings

Bend commit: 9da1f49

Additional context

No response

[nicolas-abril]

Since a and b are mutually recursive, one of them needs to be loaded first, in this case a. It then calls b recursively, but a's own local definitions are only added to the loaded set after it's dependencies are loaded.

Therefore, when b uses a type defined by a, it's not yet marked as an imported ADT and therefore it's not correctly added to the imported adts set, resulting in the use term being incorrectly added.

If we fix the problem with the use by using subst instead or by calling desugar_use before checking for unbounds, we actually hit a different error related to this import situation.

[nicolas-abril]

@NoamDev the way we're handling mutually recursive imports is really convoluted here and I think that instead of figuring out how I can fix this, I'll just reimplement the import system in a simpler way in the Agda version of Bend.

[NoamDev]

Makes sense, what I currently do is I have a file bend.py that finds all imports and resolves them without any renaming.
(Note that actually without renaming imports can be extremely straightforward.)