feat: add a 'highInferredUniverse' error explanation #722
Conversation
robsimmons
changed the title
robsimmons
changed the title
kmill
left a comment
kmill
left a comment
There was a problem hiding this comment.
Here are some possibilities to clarify some of the explanations. They're not meant to be edits, just some additional draft material.
| In this case, the error message is a false positive, but the issue can be easily fixed with | ||
| clarifying annotations. After annotating Foo with a universe `u`, the overall type can be assigned | ||
| type that the error message suggests, which silences the error. |
There was a problem hiding this comment.
I'm thinking of modifying the universe level inference algorithm to use a different error here, a simple universe level metavariable error localized to the binder. I think we talked a bit about how it's weird that it creates universe level parameters for constructor fields — this isn't something that should be done automatically.
There was a problem hiding this comment.
I think that's great — error explanation pages can be valuable even or especially if the error message sometimes appears in wonky places. If you change the error message in this kind of example, then it'll make sense to just remove the example from the manual page.
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
|
Preview for this PR is ready! 🎉 (also as a proofreading version). built with commit 3b93aa9. |
This PR introduces a new error explanation for possibly-too-high inferred universes, with the goal of shortening a long but important error explanation. (The theory is that an example is worth several dozen words.)