Errors caused by incorrect dependence on declared objects (e.g. Modules depending on declared types or operators, or types depending on declared modules) currently only mention the name of the two endpoints of the dependency chain. This information is not always going to be enough to make a fix, which could require breaking the dependency chain somewhere in the middle.
This is especially bad when parts of the dependency chain (or even the non-declared endpoint) are obscured by a clone.
Ideally we'd show the entire dependency chain and highlight the connection that was made by the command that emitted the error.
Example:
The following code should emit an error like "The dependency between T3 and T2 introduces a dependency between declared type T1 and module M: T1 -> T2 -> T3 -> T4 -> f -> M"
theory Thy.
type T3.
type T4 = T3.
op f: T4.
module M = {proc main() = {return f;}}.
end Thy.
section.
declare type T1.
type T2 = T1.
clone include Thy with
type T3 <- T2.
Ref: #749