Fix #1675.

[athas]

While this fixes a real soundness bug in the type checker, I am somewhat concerned by the amount of code this breaks. A lot of polymorphic module-level code played fast and loose with uniqueness and aliases of abstract types. While I think this is overall the simplest solution, I would like to see if we can make some improvements to alias analysis to limit the scope of the breakage.

[FluxusMagna]

How does this interact with SOACs and other higher order functions, like map?
Will they be polymorphic in the functional argument and transfer uniqueness properties from the function to the arrays they operate on? Can this be annotated with the current type syntax?

[athas]

It does not change anything about SOACs or higher-order functions specifically. This only affects the aliases of top level bindings of values of abstract types (meaning abstract through the module system, as type parameters do not exist at top level).

[Copilot]

Pull request overview

This PR addresses a type-checker soundness issue in uniqueness/alias analysis around closures (especially lambdas/local functions and global alias propagation), and updates affected library interfaces and regression tests accordingly.

Changes:

• Refines alias tracking for function closures and global aliases in Consumption.hs, including a new AliasClosure marker to suppress spurious user-facing errors while preserving conservative compiler assumptions.
• Updates several module-type signatures and implementations in tests (and prelude/math.fut) to reflect stricter uniqueness/alias requirements.
• Adds new regression tests covering closure/global alias propagation and higher-order/pipeline corner cases.

Reviewed changes

Copilot reviewed 11 out of 11 changed files in this pull request and generated 1 comment.

Show a summary per file

File	Description
tests/uniqueness/uniqueness-error69.fut	New regression test for pipeline alias propagation when return is non-unique.
tests/uniqueness/uniqueness-error70.fut	New regression test: escaping lambda that returns a global must be rejected.
tests/uniqueness/uniqueness-error71.fut	New regression test variant where lambda is applied via non-unique-returning function.
tests/modules/local_open5.fut	Updates module type/defs to satisfy new uniqueness expectations (adds * and copy).
tests/issue2209.fut	Tightens vspace interface uniqueness and fixes aliasing via copy where needed.
tests/issue1481.fut	Updates field module type to require unique results for operations.
tests/higher-order-functions/alias4.fut	New regression test ensuring unique-return closures don’t spuriously alias through pipelines.
tests/higher-order-functions/alias6.fut	New regression test ensuring “not consumable” is a proper type error (not ICE).
tests/higher-order-functions/alias7.fut	New regression test: non-escaping lambda returning a global is OK under unique construction.
src/Language/Futhark/TypeChecker/Consumption.hs	Core fix: closure/global alias propagation + AliasClosure + refined alias derivation rules.
prelude/math.fut	Updates numeric module type signatures to return unique results (*t) to match new checking.

Suppressed comments (1)

src/Language/Futhark/TypeChecker/Consumption.hs:1199

• This note refers to 'resultAliases', but there is no such function in this module. It looks like the intended reference is to 'aliases' (which includes closure aliases on arrow types), since that's what 'checkGlobalAliases' actually inspects for named functions.

--     aliases with it. 'checkGlobalAliases' therefore looks through arrows via
--     'resultAliases', and catches the escape there.

---

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.