Clean out the SAWScript type checker - #3334
Open
sauclovian-g wants to merge 27 commits into
Open
Conversation
sauclovian-g
requested review from
RyanGlScott,
brianhuffman and
chathhorn-galois
July 9, 2026 03:48
RyanGlScott
reviewed
Jul 9, 2026
Comment on lines
1
to
-13
| Loading file "err013.saw" | ||
| err013.saw:9:33-9:35: Type mismatch. | ||
| Occurs check failure: cannot unify t.1 with [t.1] because t.1 appears within [t.1] | ||
| <type of concat>:1:2-1:3: The type t.1 arises from a fresh type variable introduced here | ||
| <type of concat>:1:5-1:8: The type [t.1] arises from this type annotation | ||
|
|
||
| Expected: t.1 | ||
| Found: [t.1] | ||
|
|
||
| Expected: [t.1] | ||
| Found: [[t.1]] | ||
|
|
||
| within "paste" (err013.saw:9:5-9:10) |
Contributor
There was a problem hiding this comment.
I'm of two minds on this change. On the one hand, it is nice to condense the amount of positions reported in error messages to avoid information overload. On the other hand, knowing that an error occurs in a particular function name (paste, in this example) is valuable context that can help users quickly locate the cause of a type mismatch. One can figure out the context by squinting at the source positions and figuring out where they correspond to in the SAW script, but that can be a bit more time-consuming of a process.
Do you think there is merit in at least keeping the names of the functions around as a simple form of call stack?
Contributor
Author
There was a problem hiding this comment.
I don't know. I've always seen those names as just excess noise, so now that I'm sure the positions work I just nuked them without thinking twice.
After having chewed on it for a while in the back of my mind today, though, I think probably if we want more context we should do something else. Which top-level declaration the type error appears in is overly broad, especially for routine files that have a couple of Crucible specs and a couple verify calls.
I have never particularly liked the way modern compilers repeat the input line for you, but if we want something along these lines I think it would be a lot more effective, and at this point probably not super expensive to implement.
This is essentially extra positional information we were carrying around as user hints back in the days when the reported positions routinely lied, and no longer serves much use. This removes the addendum at the end of type errors that says "within foo". If there are remaining cases where the position information is wrong or inadequate, such that this extra info actually helps, they should get fixed. Please file a ticket.
It's no longer used since the call-checking improvements associated with implementing optional arguments. NFCI
Always pass in the list of enclosing found/expected type pairs when recursing into types. Use it when generating errors. Remove the old mechanism for adding lines about the enclosing types on error on the way out. This way does slightly more consing, maybe, but if that matters someone's doing something wrong, and on the plus side it's easier to reason about the behavior this way and all the error text is generated in one place. NFCI
For some undetermined reason not worth chasing after, this results in fewer blank lines some of the time (but seemingly not all of the time). Also, there were a few messages (e.g. the message generated for unbound variables) used to repeat the position at the end of the message. This was another leftover from when position tracking didn't work, and has now been removed. On the minus side, this change required some ugly prettyprinter hackery to avoid generating unwanted newlines in some places in some error messages. Roughly speaking, it seems that the prettyprinter library will insert newlines in places where it knows how, if it thinks it should, and you can't stop it. You can only make sure that every print that encloses something that might be multiline has a multiline form. In this case it was insisting on using that multiline form for every type, even ones with as short a string representation as (), so I applied force majeure.
Source files should have - directives - the Haddock header - the module name and export list - imports in a rational order Also remove a directive we aren't using. NFCI
This allows posting errors when they occur instead of returning them out, which simplifies the code some. It also means you can get more errors out, since it doesn't give up on unifying subpieces of types after the first failure. One of the tests does this; it has record types with multiple fields of the same names but different types. It will also let us update the working substitution on the fly instead of returning out maps and then doing more that slightly dodgy merges on them. But not in this commit.
The case at the bottom of "mgus" that had been marked previously as possibly unreachable... is in fact unreachable, at least correctly, so change it to a panic.
It doesn't offer anything over the generic "type mismatch" and the type constructor names it prints are sometimes confusing.
In particular, we can finally stop printing "Type mismatch. Mismatch of types."
These messages now appear as separate prints after each error, instead of in the middle, with their positions handled accordingly, and they say "Note:" instead of "Error:" for greater clarity. I've also hacked a blank line after them so there's a blank line in between one type error's messages and the next. There should probably be a more organized way to do this, but it'll do for now.
Stop flinging around whole substitution maps. Remove the dodgy code for merging substitutions. This is the simplest form of this change (more or less) and doesn't take full advantage of the simpler dataflow. More to come. This change affects one of the test outputs. It was wrong before (not fully resolved) and we hadn't noticed.
Maintain an invariant that when the a unification variable points to another one, it only points to a lower-numbered one. Take appropriate steps when inserting into the substitution / resolution table. We don't have any known way to generate such cycles, but I've never been particularly convinced it was impossible and I don't think anyone's tried particularly hard to trigger it. This change affects a couple of test outputs, because we do have cases where unification variables resolve to other unification variables.
Thus if a resolves to b and b resolves to a real type t, if we start from a we'll get t out. We can do this safely now without going into an infinite loop. As with generating cycles to loop over in the first place, we have no known ways to break the old logic, but I've never been particularly convinced it was impossible and I don't think anybody's ever tried particularly hard.
Apart from the panic on mismatched lengths, which can be moved to the call site it's specific to, it can now just be zipWithM_ mgu.
Instead of updating "encs" (in "mgu") on every entry, do it only when using it to generate an error message. Now that we substitute recursively it's safe to defer all substitute operations until the results are needed; it might not have been before. There are other places in here we could substitute less aggressively, but not just yet.
Let's just have "unify". NFCI
It appears we don't need the descending reference order invariant for unification vars to prevent cycles, and maybe it should be removed. It's also not by itself sufficient to prevent reference cycles that involve references within other types. All the same, I'd rather keep it for safety in the absence of a proof system for Haskell. The occurs check is sufficient for these purposes _provided_ that the types it examines with are fully expanded with all unification var resolutions done so far. If that's the case, then any resolution that completes a cycle will find an occurrence of the remaining unification var somewhere in the expansion and fail the occurs check. (I still not convinced that the code prior to this branch was sound, but haven't yet managed to break it.) Comments only. (no code changes)
sauclovian-g
force-pushed
the
typechecker-cleanout
branch
from
July 17, 2026 19:19
01aee71 to
4a36d68
Compare
Contributor
Author
|
(rebased on head) |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This is not everything one might want yet, but it seems reasonable to merge this much and I suspect it's quite enough to review on its own.
This is probably best read one commit at a time; among other things there's a fairly broad whitespace commit in there...