Skip to content

Settle every recursive type digest through one complete reduction - #12658

Merged
rtfeldman merged 7 commits into
mainfrom
issue-12607-recursive-digest-fold
Oct 29, 2026
Merged

rtfeldman merged 7 commits into
mainfrom
issue-12607-recursive-digest-fold

Conversation

@rtfeldman

Copy link
Copy Markdown
Contributor

A package function's procedure identity could differ between two apps even though both computed the same specialization key for it, so after one app's `roc check` filled the object cache, a second app's compile-time evaluation spliced in a cached procedure for the wrong identity (a debug panic, and a segfault or garbage compile-time crash in release). In roc-pg the function was `Parse.parse`, which returns `Try(List(Node), _)`. One app's lambda solving drew the recursive `Node` type as a single knot; the other drew a rolled-out copy whose own knot also referenced a second, separately tied copy. Procedure identity reduced each cyclic component on its own and hashed the reference into the second copy as an opaque digest, so the same infinite type got two identities.

The layout store already handled this shape by pairing such a component against the settled group it refers into, but Monotype type digests, Lambda Mono type digests and procedure identities each had their own copy of the reduction without that step. This replaces all four copies with one reduction in `base.recursive_digest`, which folds rolled-out copies onto settled positions, pairs a cyclic component coinductively against any settled group it refers into, and otherwise reduces by bisimulation as before. Every consumer now only encodes its nodes. This also turns Monotype's pinned "entangled equivalent knots" incompleteness into equality.

Fixes #12607

Monotype type digests, Lambda Mono type digests, procedure identities and
recursive layout keys each carried their own copy of the recursive-type
reduction, and only the layout store's paired a cyclic component against a
settled group it refers into. A program whose solved types tie a copy of a
recursive type whose references lead into a separately tied copy therefore
rendered a different procedure identity than a program drawing a single knot,
under the same specialization key, and a cached procedure from the first
program was spliced into the second for the wrong identity.

base.recursive_digest is now the one reduction every consumer uses: acyclic
copies fold onto settled positions, a cyclic component referring into a
settled group is paired coinductively against its member shapes, and every
other component is reduced by bisimulation as before.
@rtfeldman
rtfeldman marked this pull request as ready for review October 27, 2026 14:14
@rtfeldman
rtfeldman merged commit 089a0b2 into main Oct 29, 2026
32 checks passed
@rtfeldman
rtfeldman deleted the issue-12607-recursive-digest-fold branch October 29, 2026 05:40
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

1 participant