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

Follow up to #1559 : have the name of unknown missing tag depend on the row #1564

Merged
merged 4 commits into from Jan 18, 2018

Conversation

Projects
None yet
3 participants
@garrigue
Copy link
Contributor

garrigue commented Jan 10, 2018

GPR #1559 fixed a soundness issue in exhaustiveness, but didn't try much to improve the warning.
This PR goes further by using a different name depending on the cause of non-exhaustiveness.

@garrigue garrigue requested a review from trefis Jan 10, 2018

@trefis
Copy link
Contributor

trefis left a comment

To clarify: I was fine with the state of things after the last PR got merged, the emitted warnings were less pretty, but correct.

The current GPR makes the warnings pretty again in many instances.
I have no idea whether it will confuse some people to see a proper tag in some cases and <some private tag> in others, and if it would be better for the warning to be consistently ugly.
I leave it to someone who has an opinion on the matter to formally approve (or discuss) this PR.

As for the implementation: it seems correct to me.
In particular, the pitfall of selecting a tag already present on the column is avoided by making sure the tag we generate is not among the discriminating constructors of the matrix/column.
The implementation of that last part makes me a bit sad though: at worst, generating a fresh tag is quadratic in the number of discriminating constructors; it should be easy to do better than this, but I'm not sure it's worth the effort.

@gasche

This comment has been minimized.

Copy link
Member

gasche commented Jan 12, 2018

I have no idea whether it will confuse some people to see a proper tag in some cases and in others, and if it would be better for the warning to be consistently ugly.

I prefer occasional clarity to consistent strangeness. (But I would still vote for AnyOtherTag rather than AnyExtraTag.) Furthermore, I think this PR highlights and enables an interesting distinction (private row variables) that suggests an explanation in this specific difficult case (we could have a mention in the manual that "" shows up for private rows and explain why): we can do better thanks to the distinction.

@garrigue

This comment has been minimized.

Copy link
Contributor Author

garrigue commented Jan 18, 2018

Changed the tag name as suggested. Merge as soon as tests pass.

@garrigue

This comment has been minimized.

Copy link
Contributor Author

garrigue commented Jan 18, 2018

Small remark: the algorithm is not quadratic in the number of discriminating constructors, it is just < the number of discriminating constructors > * (< number of `AnyOtherTag among them > + 1). The last one is 0 in 99.99% of cases, and at most one except if you are intentionally trying to fool the algorithm. So this should be good enough.

Concerning documenting the change, where should it go? I'm OK to adding something to the warning section of the manual, but this already relatively self-explenatory.

@garrigue garrigue merged commit 55e6d74 into ocaml:trunk Jan 18, 2018

2 checks passed

continuous-integration/appveyor/pr AppVeyor build succeeded
Details
continuous-integration/travis-ci/pr The Travis CI build passed
Details
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.
You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.