Implement Occurs Check

[jaredramirez]

Overview

This PR implements the occurs check for type variables. This means, for a given type variable:

• Resolve it to its type (ie follow redirects until we get a concrete type)
• Recursively unwrap all subtype variables for the type (ie all tags in tag unions, record fields in records, etc)
• Check if we run into a variable we've seen already before

This is the 1st step in the larger project of supporting recursive types in the type system, but only for nominal types – as outlined here. This check is not yet used anywhere, that will come in a follow-up PR.

There has been some discussion in Zulip recently around if it's possible to allow non-nominal-recursion. Depending on how that shakes out, this implementation may change in the future.

Memory Management

During the occurs check, there are things we need to write down:

• What variables we've seen so far (pushed & popped for each recursive branch)
• All the variables we've visited and confirmed are not recursive (to avoid redundant work)
• In the case of an error, what the chain of recursive types was (for error messages)

To capture this, we use a Scratch struct that allocates some array lists that can be re-used across many occurs check. This is the same pattern that unify uses to hold intermediate data.

Differences from the Rust Compiler

This implementation has not significant difference from the Rust compiler version. Originally, I did things slightly differently, but ultimately decided that it probably made the most sense to match the semantics of the Rust version. That said, if those reviewing like the original approach, we can easily revert.

Original "Differences from the Rust Compiler"

The Rust implementation of occurs takes a different approach to avoiding redundant work

• It uses each variable’s Mark field to track visited state during the check
• After the traversal, it resets all visited marks

This requires:

• Mutably updating Mark values on each visited descriptor
• Tracking visited variables separately in order to reset them

The Zig version does not use Mark at all. Instead:

• It tracks visited variables explicitly in an array
• Redundancy is avoided by checking this array during traversal

This results in the same number of allocations, but with two key differences:

1. No need to mutate or reset Mark fields on descriptors
2. Possibly slightly worse per-step performance due to linear O(n) check of the already visited array
   • Note that both the Zig and Rust versions do a linear scan of seen variables, though the total number of seen vars for any given recursive branch would be less than the total visited nodes.

That said, I'm unsure what the average number of variables in a type is, but this approach assumes it would be relatively small. (We could also use a Map to check for seen/visited vars, which may perform better than an array)

[rtfeldman]

I believe so! I think calling .items(.mark) on the MultiArrayList should get you a slice of just the marks, which would mean you could:

• continue to take types_store: *Store
• pass a *const Store and then a mutable slice of just the Marks to a helper function
• now we know the helper only mutates the Marks

[rtfeldman]

Box, List

😍 😍 😍

[rtfeldman]

In working on unify I've actually personally been liking having things do std.mem.Allocation.Error!void and actually use try (instead of the exit on oom thing) - what do you think of doing more of that?

[jaredramirez]

I'm into that, imo the more explicit the points of failure are the better. And tracking the error in the type sigs would make it easier to understand what's allocating and what's not, at a glance

[rtfeldman]

Should this be removed now? 😄

[jaredramirez]

Since this module isn't yet used in any codepath, it'll be DCE'd. But i'll remove in a subsequent PR that hooks occurs up into unify!

[rtfeldman]

@jaredramirez this looks SWEET!!! 🤩

I left a few suggestions, but nothing blocking!