Skip to content

Conversation

@strub
Copy link
Member

@strub strub commented Jan 12, 2026

No description provided.

@strub strub requested a review from oskgo January 12, 2026 10:48
@strub strub self-assigned this Jan 12, 2026
@strub strub added the bug label Jan 12, 2026
@strub strub linked an issue Jan 12, 2026 that may be closed by this pull request
@strub strub enabled auto-merge (rebase) January 12, 2026 10:48
@oskgo
Copy link
Contributor

oskgo commented Jan 12, 2026

I think the error message for the cloning case could be improved. The error message tells the user the underlying problem, but is unhelpful in explaining why the clone caused it.

At least for modules we know that they cannot be given as parameters to a clone, so if this happens during a clone it must be solely because a declared parameter was fed as an argument to the clone where a declared parameter wasn't allowed.

Would it be feasible to get an error message like " _f cannot be instantiated by an operator depending on the declared operator _h because a module (M) in T0 depends on it" for the following example?:

theory TO.

type _T.
type T = _T.
op _f: T.
op f: T = _f.

module M = {proc main() = {return f;}}.

end TO.

theory Thy.
section.

declare type _T.
type T = _T.
declare op _h: T.

op _g = _h.

clone include TO with
type _T <- _T,
type T <- T,
op _f <- _g.

This also doesn't fix the example shown by @MM45, but I suppose those can be fixed in another PR since they're caused by declared modules rather than declared operators. Should I open an additional issue for this one? I also found a related example using globals myself:

theory Thy.
module type MT = {}. 
section.

declare module M <: MT.

op f: glob M.

end section.
end Thy.

print Thy.

@strub
Copy link
Member Author

strub commented Jan 12, 2026

@oskgo

The error messages for clones are bad because they often comes from low-level mechanisms without any effort to recast them. They should be reworked entirely, but this is out of scope of this PR.

Yes, you can open a new issue for the module issue.

Copy link
Contributor

@oskgo oskgo left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'll open those issues. Looks good to me.

@strub strub merged commit 2a9d76e into main Jan 12, 2026
15 checks passed
@strub strub deleted the fix-749 branch January 12, 2026 13:34
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Declared operators can indirectly leak into modules

3 participants