Add better source positions to kind errors - #3495
Conversation
| let sa = case getAnnForKind k2' of | ||
| NullSourceAnn -> getAnnForKind k1' | ||
| ann -> ann | ||
| throwError . errorMessage' (fst sa) $ KindsDoNotUnify k1' k2' |
There was a problem hiding this comment.
I guess since PositionedError takes a NEL, I could put both in there.
|
Christmas is a little early this year 🎉 ❤️ 🎄 |
| errorMessage'' sss err = MultipleErrors [ErrorMessage [PositionedError sss] err] | ||
|
|
||
| -- | Create an error from multiple (possibly empty) source spans, reversed sorted. | ||
| errorMessage''' :: [SourceSpan] -> SimpleErrorMessage -> MultipleErrors |
There was a problem hiding this comment.
Keeping the tradition alive.
I think a potential future improvement (to JSON error reporting in general) is to add an additional source position, the LSP has a concept of |
kritzcreek
left a comment
There was a problem hiding this comment.
This is great, I tested it out on a few work things and it already helped me so much.
| -> m ([SourceKind], [SourceKind]) | ||
| kindsOfAll moduleName syns tys = fmap tidyUp . withFreshSubstitution . captureSubstitution $ do | ||
| synVars <- replicateM (length syns) freshKind | ||
| synVars <- replicateM (length syns) freshKind' |
There was a problem hiding this comment.
Should we traverse these syns instead and use their spans to initialize the fresh kinds here? (Also goes for all the other instances of replicateM (length x) y in here)
Something like:
synVars <- traverse (\(_, _, sourceTy) -> freshKind (getAnnForType sourceTy)) synsThere was a problem hiding this comment.
Potentially, but I think we need to change the signature of this function to take source positions directly. The SourceType here refers to the rhs constructors, however I think when kind-checking a group like this we would want the source position to point to the lhs name.
| quantify ty = foldr (\arg t -> ForAll ann arg t Nothing) ty $ freeTypeVariables ty | ||
| where | ||
| ann = annotationForType ty | ||
| ann = getAnnForType ty |
There was a problem hiding this comment.
I don't think this name is any more helpful than just inlining its definition.
| forM_ ks $ \k -> unifyKinds k kindType | ||
| unless isData $ | ||
| unifyKinds tyCon (foldr (FunKind nullSourceAnn) (head ks) kargs) | ||
| unless isData $ do |
There was a problem hiding this comment.
Don't need that do, unless you're doing it for consistency with the line above?
| unless isData $ do | |
| unless isData $ |
|
I've addressed the feedback. |
* Add lenses for annotations * Add better source positions to kind errors * Throw possibly multiple source spans * Extract to error utility * Remove unused imports * Revert unnecessary rethrowWithPosition * Add positions to kindsForAll vars
This implements https://www.youtube.com/watch?v=rdVqQUOvxSU for the kind checker. The kinds in kind unification errors now have exact positions for the terms in the source they are derived from. Since unification doesn't really have a canonical source for the error (could be either one), and we don't have a way of reporting multiple positions (I guess we could throw two errors?), it just has a bias when reporting the source position. This seems to be a huge improvement in all the testing I've done.