Description
A small issue came up recently. It's mostly harmless for now, but if we start adding x = y equations when simplifying the then branch of if x == y this could cause problems.
The issue is that the Aliases module expects that there exists a total ordering between elements, and this ordering is given by the binding time.
It's already a bit shaky, as all constants have the same binding time (and the same for symbols), but those are guaranteed to never alias so we still get the property that all elements of a set of aliases have distinct binding times.
This starts to break for imported variables: for now they have a distinguished binding time (Binding_time.imported_variables), and we have access to their aliases in the imported environment, so when we create an alias from a variable in scope to an imported variable, we know that we can find the canonical element for the imported variable and use it as the only imported variable in the set of aliases. However, if we were allowed to discover aliases between existing variables (such as in the if x == y case), then we could easily end up with more than one imported variable in a set of aliases.
I don't have a good solution for this, but I'm wondering if this might not be solvable by making Binding_time.imported_variables later than any other normal binding time. I would expect that we only really need a strict ordering between canonical elements that may alias, so if we can ensure that in the current environment every alias set must contain at least one element valid in the current scope, then we'll know that external variables can never be canonical elements so it's fine if they share the same binding time. But of course this breaks the intuition behind binding time ordering, as one would expect variables from imported units to be bound earlier than those in the current unit.
Anyway, if we have time to solve this properly this would be nice, but I think it's also fine to let this issue open for now.