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

chore: improve error message for seq type mismatch #2790

Merged
merged 7 commits into from
Sep 30, 2022

Conversation

alex-chew
Copy link
Contributor

@alex-chew alex-chew commented Sep 22, 2022

Fixes #1887.

This adds a wrapper to "lazily" retrieve the string representation of a sequence's element type that is unresolved while the type constraint (and its error message) is being constructed.

For simplicity, instead of the originally proposed message

s[0] has type T instead of the expected char (seq<T> is not compatible with the expected seq<char> aka string)

this PR changes the sequence-type-mismatch error message to

selected element has type T which is incompatible with expected type char (seq<T> is incompatible with seq<char>)

when a type mismatch arises from a single selection (e.g. s[0]).

When a type mismatch arises from a "multi-selection" (e.g. s[0..2]), the expected type is an InferredTypeProxy that may not resolve to a sequence type at all, in which case we can't speak of the expected sequence type's type argument. For that reason the multi-selection type mismatch error message makes no mention of the expected type argument:

multi-selection has type seq<T> which is incompatible with expected type seq<char>

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

cpitclaudel
cpitclaudel previously approved these changes Sep 29, 2022
Copy link
Member

@cpitclaudel cpitclaudel left a comment

Choose a reason for hiding this comment

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

Looks good, but: are you actually using the new overload?

Copy link
Member

@cpitclaudel cpitclaudel left a comment

Choose a reason for hiding this comment

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

One more small thing that I just caught; sorry! IIUC the problem isn't ToString, it's .AsSeqType.Arg, right?

Source/DafnyCore/Resolver.cs Outdated Show resolved Hide resolved
Copy link
Member

@cpitclaudel cpitclaudel left a comment

Choose a reason for hiding this comment

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

🎉

@cpitclaudel cpitclaudel enabled auto-merge (squash) September 29, 2022 23:31
@cpitclaudel cpitclaudel merged commit 3b8a23b into dafny-lang:master Sep 30, 2022
@alex-chew alex-chew deleted the fix/issue-1887 branch September 30, 2022 00:07
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.

Unclear message for sequence type mismatch
2 participants