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 error LSP ranges on type mismatches #5284

Open
wants to merge 8 commits into
base: trunk
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
18 changes: 17 additions & 1 deletion parser-typechecker/src/Unison/PrintError.hs
Original file line number Diff line number Diff line change
Expand Up @@ -64,6 +64,7 @@ import Unison.Syntax.TermPrinter qualified as TermPrinter
import Unison.Term qualified as Term
import Unison.Type (Type)
import Unison.Type qualified as Type
import Unison.Typechecker qualified as Typechecker
import Unison.Typechecker.Context qualified as C
import Unison.Typechecker.TypeError
import Unison.Typechecker.TypeVar qualified as TypeVar
Expand Down Expand Up @@ -369,7 +370,7 @@ renderTypeError e env src = case e of
Mismatch {..} ->
mconcat
[ Pr.lines
[ "I found a value of type: " <> style Type1 (renderType' env foundLeaf),
Copy link
Contributor

Choose a reason for hiding this comment

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

I think this extra space may have been intentional to allow the types and the :s to line up. I would move the space after the : to preserve that the types line up, or just revert this line altogether.

Copy link
Contributor Author

@ChrisPenner ChrisPenner Aug 30, 2024

Choose a reason for hiding this comment

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

I think this has caught me like 3 times now, I admit I don't find it very intuitive 🙃
I'll move it to after the : so I don't do this again in 3 weeks haha.

[ "I found a value of type: " <> style Type1 (renderType' env foundLeaf),
"where I expected to find: " <> style Type2 (renderType' env expectedLeaf)
],
"\n\n",
Expand All @@ -387,6 +388,7 @@ renderTypeError e env src = case e of
src
[styleAnnotated Type1 foundLeaf]
[styleAnnotated Type2 expectedLeaf],
missingDelayHint,
unitHint,
intLiteralSyntaxTip mismatchSite expectedType,
debugNoteLoc
Expand All @@ -407,6 +409,20 @@ renderTypeError e env src = case e of
debugSummary note
]
where
missingDelayHint = case Typechecker.isMismatchMissingDelay foundType expectedType of
Nothing -> ""
Just (Left _) ->
Pr.lines
[ "I expected the expression to be delayed, but it was not.",
"Are you missing a `do`?"
]
Just (Right _) ->
Pr.lines
[ "",
"I didn't expect this expression to be delayed, but it was.",
"Are you using a `do` where you don't need one,",
"or are you missing a `()` to force an expression?"
]
unitHintMsg =
"\nHint: Actions within a block must have type "
<> style Type2 (renderType' env expectedLeaf)
Expand Down
13 changes: 13 additions & 0 deletions parser-typechecker/src/Unison/Typechecker.hs
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,7 @@ module Unison.Typechecker
isEqual,
isSubtype,
fitsScheme,
isMismatchMissingDelay,
Env (..),
Notes (..),
Resolution (..),
Expand Down Expand Up @@ -38,6 +39,7 @@ import Data.Text qualified as Text
import Data.Tuple qualified as Tuple
import Unison.ABT qualified as ABT
import Unison.Blank qualified as B
import Unison.Builtin.Decls qualified as BuiltinDecls
import Unison.Codebase.BuiltinAnnotation (BuiltinAnnotation)
import Unison.Name qualified as Name
import Unison.Prelude
Expand All @@ -48,6 +50,7 @@ import Unison.Syntax.Name qualified as Name (unsafeParseText, unsafeParseVar)
import Unison.Term (Term)
import Unison.Term qualified as Term
import Unison.Type (Type)
import Unison.Type qualified as Type
import Unison.Typechecker.Context qualified as Context
import Unison.Typechecker.TypeLookup qualified as TL
import Unison.Typechecker.TypeVar qualified as TypeVar
Expand Down Expand Up @@ -405,3 +408,13 @@ wellTyped ppe env term = go <$> runResultT (synthesize ppe Context.PatternMatchC
-- `forall a b . a -> b -> a` to be different types
-- equals :: Var v => Type v -> Type v -> Bool
-- equals t1 t2 = isSubtype t1 t2 && isSubtype t2 t1

-- | Checks if the mismatch between two types is due to a missing delay, if so returns a tag for which type is
-- missing the delay
isMismatchMissingDelay :: (Var v) => Type v loc -> Type v loc -> Maybe (Either (Type v loc) (Type v loc))
Copy link
Contributor Author

@ChrisPenner ChrisPenner Aug 30, 2024

Choose a reason for hiding this comment

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

@pchiusano is this a reasonable way to do this? I suppose ideally this would be done inside the typechecker itself, but it seems like a pretty simple type to check against 🤔

It works in simple cases; but unsurprisingly doesn't seem to work with polymorphic types; e.g. this doesn't trip the hint:

y : '(e -> Nat)
y =
  _ = 1
  _ = "one two three"
  (_a -> 2)

If adding it correctly to the typechecker is difficult it's still beneficial to get the hint sometimes rather than not at all; but would be nice if it worked in all cases :)

Copy link
Contributor Author

Choose a reason for hiding this comment

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

cc @dolio

Copy link
Contributor

Choose a reason for hiding this comment

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

So, here's a possible idea for how to make the typechecker facilitate some of this. Up to you if you want to try out implementing it.

So, we can detect do in the typechecker because it turns into Lam body where Var.typeOf (ABT.variable body) = Delay. We can try to detect 't in the typechecker by looking for a check against () -> t. So, you can try to partition the checking problem into three cases:

  1. Checking λDelay -> ... against () -> t: this looks fine, so just continue as normal
  2. Checking λDelay -> ... against something else: this might be a bad do, so put something in the error scope that indicates this.
  3. Checking something else against () -> t: this might be a missing do, so again put something in the error scope.

Then you can try to parse the improved error information in some situations. Like, if you got a leaf mismatch with an arrow vs. something else, you could look to see if one of these do indicators is upstream, and report something about that instead.

I think with this approach, you might be able to identify the example you mentioned above. I'm not 100% sure that it wouldn't cause some other weird corner cases, though.

isMismatchMissingDelay typeA typeB
| isSubtype (Type.arrow () (Type.ref () BuiltinDecls.unitRef) (typeA $> ())) (typeB $> ()) =
Just (Left typeA)
| isSubtype (ABT.tm (ABT.tm (Type.Ref BuiltinDecls.unitRef) `Type.Arrow` (typeB $> ()))) (typeA $> ()) =
Just (Right typeB)
| otherwise = Nothing
66 changes: 59 additions & 7 deletions unison-cli/src/Unison/LSP/FileAnalysis.hs
Original file line number Diff line number Diff line change
Expand Up @@ -62,6 +62,7 @@ import Unison.Syntax.Name qualified as Name
import Unison.Syntax.Parser qualified as Parser
import Unison.Syntax.TypePrinter qualified as TypePrinter
import Unison.Term qualified as Term
import Unison.Typechecker qualified as Typechecker
import Unison.Typechecker.Context qualified as Context
import Unison.Typechecker.TypeError qualified as TypeError
import Unison.UnisonFile qualified as UF
Expand Down Expand Up @@ -162,7 +163,8 @@ fileAnalysisWorker = forever do
analyseFile :: (Foldable f) => Uri -> Text -> PPED.PrettyPrintEnvDecl -> f (Note Symbol Ann) -> Lsp ([Diagnostic], [RangedCodeAction])
analyseFile fileUri srcText pped notes = do
let ppe = PPED.suffixifiedPPE pped
(noteDiags, noteActions) <- analyseNotes fileUri ppe (Text.unpack srcText) notes
Env {codebase} <- ask
(noteDiags, noteActions) <- analyseNotes codebase fileUri ppe (Text.unpack srcText) notes
pure (noteDiags, noteActions)

-- | Returns diagnostics which show a warning diagnostic when editing a term that's conflicted in the
Expand Down Expand Up @@ -210,15 +212,27 @@ getTokenMap tokens =
)
& fold

analyseNotes :: (Foldable f) => Uri -> PrettyPrintEnv -> String -> f (Note Symbol Ann) -> Lsp ([Diagnostic], [RangedCodeAction])
analyseNotes fileUri ppe src notes = do
analyseNotes ::
(Foldable f, MonadIO m) =>
(Codebase.Codebase IO Symbol Ann) ->
Uri ->
PrettyPrintEnv ->
String ->
f (Note Symbol Ann) ->
m ([Diagnostic], [RangedCodeAction])
analyseNotes codebase fileUri ppe src notes = do
flip foldMapM notes \note -> case note of
Result.TypeError errNote@(Context.ErrorNote {cause}) -> do
let typeErr = TypeError.typeErrorFromNote errNote
ranges = case typeErr of
TypeError.Mismatch {mismatchSite} -> singleRange $ ABT.annotation mismatchSite
TypeError.BooleanMismatch {mismatchSite} -> singleRange $ ABT.annotation mismatchSite
TypeError.ExistentialMismatch {mismatchSite} -> singleRange $ ABT.annotation mismatchSite
TypeError.Mismatch {mismatchSite, foundType, expectedType}
| -- If it's a delay mismatch, the error is likely with the block definition (e.g. missing 'do') so we highlight the whole block.
Just _ <- Typechecker.isMismatchMissingDelay foundType expectedType ->
singleRange $ ABT.annotation mismatchSite
-- Otherwise we highlight the leafe nodes of the block
| otherwise -> leafNodeRanges "mismatch" mismatchSite
TypeError.BooleanMismatch {mismatchSite} -> leafNodeRanges "mismatch" mismatchSite
TypeError.ExistentialMismatch {mismatchSite} -> leafNodeRanges "mismatch" mismatchSite
TypeError.FunctionApplication {f} -> singleRange $ ABT.annotation f
TypeError.NotFunctionApplication {f} -> singleRange $ ABT.annotation f
TypeError.AbilityCheckFailure {abilityCheckFailureSite} -> singleRange abilityCheckFailureSite
Expand Down Expand Up @@ -312,6 +326,10 @@ analyseNotes fileUri ppe src notes = do
Context.OtherBug _s -> todoAnnotation
pure (noteDiagnostic note ranges, [])
where
leafNodeRanges label mismatchSite = do
let locs = ABT.annotation <$> expressionLeafNodes mismatchSite
(r, rs) <- withNeighbours (locs >>= aToR)
pure (r, (label,) <$> rs)
-- Diagnostics with this return value haven't been properly configured yet.
todoAnnotation = []
singleRange :: Ann -> [(Range, [a])]
Expand Down Expand Up @@ -361,7 +379,6 @@ analyseNotes fileUri ppe src notes = do
typeHoleReplacementCodeActions diags v typ
| not (isUserBlank v) = pure []
| otherwise = do
Env {codebase} <- ask
let cleanedTyp = Context.generalizeAndUnTypeVar typ -- TODO: is this right?
refs <- liftIO . Codebase.runTransaction codebase $ Codebase.termsOfType codebase cleanedTyp
forMaybe (toList refs) $ \ref -> runMaybeT $ do
Expand Down Expand Up @@ -471,3 +488,38 @@ mkTypeSignatureHints parsedFile typecheckedFile = do
pure $ TypeSignatureHint name (Referent.fromTermReferenceId ref) newRange typ
)
in typeHints

-- | Crawl a term and find the nodes which actually influence its return type. This is useful for narrowing down a giant
-- "This let/do block has the wrong type" into "This specific line returns the wrong type"
-- This is just a heuristic.
expressionLeafNodes :: Term.Term2 vt at ap v a -> [Term.Term2 vt at ap v a]
expressionLeafNodes abt =
case ABT.out abt of
ABT.Var {} -> [abt]
ABT.Cycle r -> expressionLeafNodes r
ABT.Abs _ r -> expressionLeafNodes r
ABT.Tm f -> case f of
Term.Int {} -> [abt]
Term.Nat {} -> [abt]
Term.Float {} -> [abt]
Term.Boolean {} -> [abt]
Term.Text {} -> [abt]
Term.Char {} -> [abt]
Term.Blank {} -> [abt]
Term.Ref {} -> [abt]
Term.Constructor {} -> [abt]
Term.Request {} -> [abt]
-- Not 100% sure whether the error should appear on the handler or action, maybe both?
Term.Handle handler _action -> expressionLeafNodes handler
Term.App _a _b -> [abt]
Term.Ann a _ -> expressionLeafNodes a
Term.List {} -> [abt]
Term.If _cond a b -> expressionLeafNodes a <> expressionLeafNodes b
Term.And {} -> [abt]
Term.Or {} -> [abt]
Term.Lam a -> expressionLeafNodes a
Term.LetRec _isTop _bindings body -> expressionLeafNodes body
Term.Let _isTop _bindings body -> expressionLeafNodes body
Term.Match _a cases -> cases & foldMap \(Term.MatchCase {matchBody}) -> expressionLeafNodes matchBody
Term.TermLink {} -> [abt]
Term.TypeLink {} -> [abt]
144 changes: 109 additions & 35 deletions unison-cli/tests/Unison/Test/LSP.hs
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,7 @@ import Unison.Codebase.SqliteCodebase qualified as SC
import Unison.ConstructorReference (GConstructorReference (..))
import Unison.FileParsers qualified as FileParsers
import Unison.LSP.Conversions qualified as Cv
import Unison.LSP.FileAnalysis qualified as FileAnalysis
import Unison.LSP.FileAnalysis.UnusedBindings qualified as UnusedBindings
import Unison.LSP.Queries qualified as LSPQ
import Unison.Lexer.Pos qualified as Lexer
Expand All @@ -31,6 +32,7 @@ import Unison.Parser.Ann qualified as Ann
import Unison.Parsers qualified as Parsers
import Unison.Pattern qualified as Pattern
import Unison.Prelude
import Unison.PrettyPrintEnv qualified as PPE
import Unison.Reference qualified as Reference
import Unison.Result qualified as Result
import Unison.Symbol (Symbol)
Expand All @@ -49,7 +51,8 @@ test = do
]
scope "diagnostics" $
tests
[ unusedBindingLocations
[ unusedBindingLocations,
typeMismatchLocations
]

trm :: Term.F Symbol () () (ABT.Term (Term.F Symbol () ()) Symbol ()) -> LSPQ.SourceNode ()
Expand Down Expand Up @@ -251,35 +254,44 @@ term = let
extractCursor :: Text -> Test (Lexer.Pos, Text)
extractCursor txt =
case splitOnDelimiter '^' txt of
Nothing -> crash "expected exactly one cursor"
Just (before, pos, after) -> pure (pos, before <> after)
_ -> crash "expected exactly one cursor"

-- | Splits a text on a delimiter, returning the text before and after the delimiter, along with the position of the delimiter.
--
-- >>> splitOnDelimiter '^' "foo b^ar baz"
-- Just ("foo b",Pos {line = 0, column = 5},"ar baz")
-- Just ("foo b",Pos {line = 1, column = 5},"ar baz")
splitOnDelimiter :: Char -> Text -> Maybe (Text, Lexer.Pos, Text)
splitOnDelimiter sym txt =
case Text.splitOn (Text.singleton sym) txt of
[before, after] ->
let col = (Text.length $ Text.takeWhileEnd (/= '\n') before) + 1
case second Text.uncons $ Text.breakOn (Text.singleton sym) txt of
(_before, Nothing) -> Nothing
(before, Just (_delim, after)) ->
let col = (Text.length $ Text.takeWhileEnd (/= '\n') before)
line = Text.count "\n" before + 1
in Just $ (before, Lexer.Pos line col, after)
_ -> Nothing
in Just (before, Lexer.Pos line col, after)

-- | Test helper which lets you specify a cursor position inline with source text as a '^'.
-- | Test helper which lets you specify a relevant block of source inline using specified delimiters
--
-- >>> extractDelimitedBlocks ('{', '}') "foo {bar} baz"
-- Just ("foo bar baz",[(Ann {start = Pos {line = 1, column = 5}, end = Pos {line = 1, column = 8}},"bar")])
--
-- >>> extractDelimitedBlock ('{', '}') "foo {bar} baz"
-- Just (Ann {start = Pos {line = 1, column = 4}, end = Pos {line = 1, column = 7}},"bar","foo bar baz")
-- >>> extractDelimitedBlocks ('{', '}') "term =\n {foo} = 12345"
-- Just ("term =\n foo = 12345",[(Ann {start = Pos {line = 2, column = 3}, end = Pos {line = 2, column = 6}},"foo")])
--
-- >>> extractDelimitedBlock ('{', '}') "term =\n {foo} = 12345"
-- Just (Ann {start = Pos {line = 2, column = 2}, end = Pos {line = 2, column = 5}},"foo","term =\n foo = 12345")
extractDelimitedBlock :: (Char, Char) -> Text -> Maybe (Ann {- ann spanning the inside of the delimiters -}, Text {- Text within the delimiters -}, Text {- entire source text with the delimiters stripped -})
extractDelimitedBlock (startDelim, endDelim) txt = do
(beforeStart, startPos, afterStart) <- splitOnDelimiter startDelim txt
(beforeEnd, endPos, afterEnd) <- splitOnDelimiter endDelim (beforeStart <> afterStart)
let ann = Ann startPos endPos
pure (ann, Text.takeWhile (/= endDelim) afterStart, beforeEnd <> afterEnd)
-- >>> extractDelimitedBlocks ('{', '}') "term =\n {foo} = {12345} + 10"
-- Just ("term =\n foo = 12345 + 10",[(Ann {start = Pos {line = 2, column = 3}, end = Pos {line = 2, column = 6}},"foo"),(Ann {start = Pos {line = 3, column = 4}, end = Pos {line = 3, column = 9}},"12345")])
extractDelimitedBlocks :: (Char, Char) -> Text -> Maybe (Text {- entire source text with the delimiters stripped -}, [(Ann {- ann spanning the inside of the delimiters -}, Text {- Text within the delimiters -})])
extractDelimitedBlocks (startDelim, endDelim) txt =
extractDelimitedBlocksHelper mempty txt
where
extractDelimitedBlocksHelper :: Lexer.Pos -> Text -> Maybe (Text, [(Ann, Text)])
extractDelimitedBlocksHelper offset txt = do
(beforeStart, startPos, afterStart) <- splitOnDelimiter startDelim txt
(beforeEnd, endPos, afterEnd) <- splitOnDelimiter endDelim (beforeStart <> afterStart)
let ann = Ann (offset <> startPos) (offset <> endPos)
case extractDelimitedBlocksHelper endPos afterEnd of
Nothing -> pure (beforeEnd <> afterEnd, [(ann, Text.takeWhile (/= endDelim) afterStart)])
Just (cleanSrc, splits) -> pure $ (beforeEnd <> cleanSrc, (ann, Text.takeWhile (/= endDelim) afterStart) : splits)

makeNodeSelectionTest :: (String, Text, Bool, LSPQ.SourceNode ()) -> Test ()
makeNodeSelectionTest (name, testSrc, testTypechecked, expected) = scope name $ do
Expand Down Expand Up @@ -416,31 +428,59 @@ withTestCodebase action = do
Codebase.Init.withCreatedCodebase SC.init "lsp-test" tmpDir SC.DontLock action
either (crash . show) pure r

makeDiagnosticRangeTest :: (String, Text) -> Test ()
makeDiagnosticRangeTest (testName, testSrc) = scope testName $ do
let (cleanSrc, mayExpectedDiagnostic) = case extractDelimitedBlock ('«', '»') testSrc of
Nothing -> (testSrc, Nothing)
Just (ann, block, clean) -> (clean, Just (ann, block))
makeUnusedBindingRangeTest :: (String, Text) -> Test ()
makeUnusedBindingRangeTest (testName, testSrc) = scope testName $ do
(cleanSrc, ranges) <- case extractDelimitedBlocks ('«', '»') testSrc of
Nothing -> pure (testSrc, [])
Just (cleanSrc, ranges) -> pure (cleanSrc, ranges)
(pf, _mayTypecheckedFile) <- typecheckSrc testName cleanSrc
UF.terms pf
& Map.elems
& \case
[(_a, trm)] -> do
case (mayExpectedDiagnostic, UnusedBindings.analyseTerm (LSP.Uri "test") trm) of
(Just (ann, _block), [diag]) -> do
let expectedRange = Cv.annToRange ann
let actualRange = Just (diag ^. LSP.range)
when (expectedRange /= actualRange) do
crash $ "Expected diagnostic at range: " <> show expectedRange <> ", got: " <> show actualRange
(Nothing, []) -> pure ()
(expected, actual) -> case expected of
Nothing -> crash $ "Expected no diagnostics, got: " <> show actual
Just _ -> crash $ "Expected exactly one diagnostic, but got " <> show actual
let diags = UnusedBindings.analyseTerm (LSP.Uri "test") trm
matchDiagnostics ranges diags
_ -> crash "Expected exactly one term"

makeTypecheckerDiagnosticRangeTest :: (String, Text) -> Test ()
makeTypecheckerDiagnosticRangeTest (testName, testSrc) = scope testName $ do
(cleanSrc, ranges) <- case extractDelimitedBlocks ('«', '»') testSrc of
Nothing -> pure (testSrc, [])
Just (cleanSrc, ranges) -> pure (cleanSrc, ranges)
(_pf, tf) <- typecheckSrc testName cleanSrc
case tf of
Left notes -> do
let codebase = error "unexpected use of codebase"
let ppe = PPE.empty
(diags, _codeActions) <- FileAnalysis.analyseNotes codebase (LSP.Uri "test") ppe "test" notes
matchDiagnostics ranges diags
Right _ -> crash "Expected typechecking to fail"

matchDiagnostics :: [(Ann, Text)] -> [LSP.Diagnostic] -> Test ()
matchDiagnostics ranges diags = case (ranges, diags) of
([], []) -> pure ()
([], _ : _) -> crash $ "Got diagnostics that weren't matched: " <> show diags
(_ : _, []) -> crash $ "Expected diagnostics that weren't provided" <> show ranges
(range@(ann, _src) : rest, diags) ->
diags
& popFind
( \diag ->
let expectedRange = Cv.annToRange ann
actualRange = Just (diag ^. LSP.range)
in (expectedRange /= actualRange)
)
& \case
Nothing -> crash $ "Expected diagnostic not found" <> show range <> ", remaining diagnostics: " <> show diags
Just (_, diags) -> matchDiagnostics rest diags
where
popFind :: (a -> Bool) -> [a] -> Maybe (a, [a])
popFind p = \case
[] -> Nothing
x : xs -> if p x then Just (x, xs) else second (x :) <$> popFind p xs

unusedBindingLocations :: Test ()
unusedBindingLocations =
scope "unused bindings" . tests . fmap makeDiagnosticRangeTest $
scope "unused bindings" . tests . fmap makeUnusedBindingRangeTest $
[ ( "Unused binding in let block",
[here|term =
usedOne = true
Expand All @@ -466,3 +506,37 @@ unusedBindingLocations =
|]
)
]

typeMismatchLocations :: Test ()
typeMismatchLocations =
scope "type mismatch locations" . tests . fmap makeTypecheckerDiagnosticRangeTest $
[ ( "Should highlight the actual incorrect terminal expression in a let block",
[here|
type Foo = Foo
term : Foo
term =
_blah = true
_foo = true
_baz = true
«"incorrect"»
|]
),
( "Should highlight the actual incorrect terminal expression in an if-block",
[here|
type Foo = Foo
term : Foo
term = if true
then «"wrong"»
else «"also wrong"»
|]
),
( "Should highlight the handler of handle expressions",
[here|
type Foo = Foo
term : Foo
term =
const a b = a
handle "" with const «"wrong"»
|]
)
]
Loading
Loading