Improve error messages involving skolem variables #2102
Assignees
Labels
C-Moderate Effort
Should take a moderate amount of time to address.
L-Error reporting
Reporting language or runtime errors to the player.
L-Type inference
The process of inferring the type of a Swarm expression.
S-Nice to have
The bug fix or feature would be nice but doesn't currently have much negative impact.
Z-User Experience
This issue seeks to make the game more enjoyable to play.
Comments
mergify bot
pushed a commit
that referenced
this issue
Mar 10, 2025
…2340) Each type variable now carries two variable names: one, the original, user-supplied name of the type variable, and another, the (potentially different) current freshly generated name. These can diverge specifically in the case that we skolemize a user-supplied polymorphic type. We use the second name for all comparisons, but the first name when pretty-printing. For example, `def f : a -> a = \x. 3 end` used to generate an error message saying something like "expected `3` to have type `s1` ; it now says "expected `3` to have type `a`". Closes #2102. That issue also talks about improving the error message that says "skolem variable would escape its scope", but at the moment I can't even find a way to get that error message to be generated at all, so I propose to not worry about it for now. There is one specific situation where this can be confusing, when one type variable is shadowed by another with the same name. For example: ``` > def f : a -> (a * Int) = \\x. let g : forall a. a * Int = (x, 3) in g end 1:59: Type mismatch:\n From context, expected `x` to have type `a`,\n but it actually has type `a` ``` Not sure whether it's worth doing anything about this; open to suggestions.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
There are two kinds of error messages we could get involving skolem variables.
We can simply get a type mismatch when we try to unify a skolem variable with something else. However, the current error is confusing since it references a made-up variable. For example:
It would be better if the error said something about polymorphism and mentioned the type variable
a. This might require keeping track of a mapping between generated skolem variables and type variables in the polymorphic type.When a skolem variable escapes, the error message is even worse since the error explicitly mentions the word "skolem":
This case is more obscure and probably won't happen very much (especially once we fix Strange type checking error "Skolem variable would escape its scope" #2101), but it would still be nice to come up with a better error message that at least hints at what the problem might be.
The text was updated successfully, but these errors were encountered: