Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Improve type variables name allocation when reporting type errors #1512

Merged
merged 3 commits into from
Aug 9, 2023

Conversation

yannham
Copy link
Member

@yannham yannham commented Aug 8, 2023

The implementation of the conversion from unification type to human-readable types was a bit confused, using two name tables without really making it clear which table corresponds to which. The implementation didn't correctly update correctly the set of variables already in use, and failed to propagate position information for user-written type variables.

This PR simplifies the implementation, moving free-standing functions into NameReg, diminishing the number of arguments and gets rid of the additional table, with the effect of correctly propagating position information for user-written type variables.

This improves the error reporting of the variable level mismatch error. Previously, the offending type variable wasn't pointed at, but after this PR, it is:

let eval : forall a. (forall b. b -> b) -> a -> a =
fun f x => f x
in (let g = fun x => x
in eval g) : _
error: function types mismatch
  ┌─ <unknown> (generated by evaluation):1:1
  │
1 │ b -> b
  │ - this part of the expected type
  │
  ┌─ <unknown> (generated by evaluation):1:1
  │
1 │ _a -> _a
  │ -- does not match this part of the inferred type
  │
  ┌─ repl-input-0:4:9
  │
4 │ in eval g) : _
  │         ^ this expression
  │
  = Expected an expression of type `b -> b`
  = Found an expression of type `_a -> _a`
  = Could not match the two function types

error: while matching function types: invalid polymorphic generalization
  ┌─ repl-input-0:1:30
  │
1 │ let eval : forall a. (forall b. b -> b) -> a -> a =
  │                              - this polymorphic type variable
  │
  = While the type of this expression is still undetermined, it appears indirectly in the type of another expression introduced before the `forall` block.
  = The type of this expression escapes the scope of the corresponding `forall` and can't be generalized to the polymorphic type variable `b`

The implementation of the conversion from unification type to
human-readable types was a bit confused, using two name tables, not
updating correctly the set of already used variables, etc.

This commit simplifies the implementation, move free-standing functions
into `NameReg`, with the effect of correctly propagating position
information for user-written type variables and thus improving the error
reporting for the variable level mismath error.
@github-actions github-actions bot temporarily deployed to pull request August 8, 2023 09:49 Inactive
Comment on lines 115 to 117
pub fn into_typecheck_err(self, state: &mut State, pos_opt: TermPos) -> TypecheckError {
let mut names = reporting::NameReg::new(std::mem::take(state.names));
self.into_typecheck_err_(state, &mut names, pos_opt)
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This function now replaces the NameReg in state by an empty one and calls into_typecheck_err_ with the old, filled one. This might end up being very surprising. I wouldn't expect that into_typecheck_err removes name allocations from the state. Maybe it would make more sense to take ownership of state?

In any case, the doc-comment needs to be updated.

Copy link
Member Author

@yannham yannham Aug 8, 2023

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Good point, but doing that at the caller site might be very annoying, because State is taken by reference everywhere, so we would end up with a lot of std::mem::take (EDIT: because into_typecheck_err is called a lot)

In practice, when you call to into_typecheck_err, you go the error path, so you don't need the state anymore. But you're right that the behavior isn't necessarily natural. Maybe cloning is the path of least resistance. Another solution is to separate the name tables between the one coming from state, that would be immutably borrowed, and the one corresponding to generated names, that is owned, but that also sounds like more boilerplate (lifetimes, wrapper around get, etc.) just to avoid one clone.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'll just clone, it's the simplest.

@github-actions github-actions bot temporarily deployed to pull request August 8, 2023 10:20 Inactive
@yannham yannham enabled auto-merge August 9, 2023 08:32
@github-actions github-actions bot temporarily deployed to pull request August 9, 2023 08:37 Inactive
@yannham yannham added this pull request to the merge queue Aug 9, 2023
Merged via the queue into master with commit dd58ac1 Aug 9, 2023
4 checks passed
@yannham yannham deleted the task/improve-typechecking-reporting branch August 9, 2023 09:38
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants