Merge pull request #5284 from unisonweb/lsp/improved-mismatch-ranges

Author: aryairani

parser-typechecker/src/Unison/PrintError.hs

@@ -535,6 +535,7 @@ renderTypeError e env src = case e of
           src
           [styleAnnotated Type1 foundLeaf]
           [styleAnnotated Type2 expectedLeaf],
+        missingDelayHint,
         unitHint,
         intLiteralSyntaxTip mismatchSite expectedType,
         debugNoteLoc
@@ -555,6 +556,20 @@ renderTypeError e env src = case e of
         debugSummary note
       ]
     where
+      missingDelayHint = case additionalInfo of
+        Nothing -> ""
+        Just MissingDelay ->
+          Pr.lines
+            [ "I expected the expression to be delayed, but it was not.",
+              "Are you missing a `do`?"
+            ]
+        Just SuperfluousDelay ->
+          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)

parser-typechecker/src/Unison/Typechecker.hs

@@ -10,6 +10,7 @@ module Unison.Typechecker
     isEqual,
     isSubtype,
     fitsScheme,
+    isMismatchMissingDelay,
     Env (..),
     Notes (..),
     Resolution (..),
@@ -32,6 +33,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
@@ -43,6 +45,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
@@ -126,6 +129,33 @@ synthesize ppe pmccSwitch env t =
             (TypeVar.liftTerm t)
    in Result.hoist (pure . runIdentity) $ fmap TypeVar.lowerType result
 
+-- | @subtype a b@ is @Right b@ iff @f x@ is well-typed given
+-- @x : a@ and @f : b -> t@. That is, if a value of type `a`
+-- can be passed to a function expecting a `b`, then `subtype a b`
+-- returns `Right b`. This function returns @Left note@ with information
+-- about the reason for subtyping failure otherwise.
+--
+-- Example: @subtype (forall a. a -> a) (Int -> Int)@ returns @Right (Int -> Int)@.
+-- subtype :: Var v => Type v -> Type v -> Either Note (Type v)
+-- subtype t1 t2 = error "todo"
+-- let (t1', t2') = (ABT.vmap TypeVar.Universal t1, ABT.vmap TypeVar.Universal t2)
+-- in case Context.runM (Context.subtype t1' t2')
+--                      (Context.MEnv Context.env0 [] Map.empty True) of
+--   Left e -> Left e
+--   Right _ -> Right t2
+
+-- | Returns true if @subtype t1 t2@ returns @Right@, false otherwise
+-- isSubtype :: Var v => Type v -> Type v -> Bool
+-- isSubtype t1 t2 = case subtype t1 t2 of
+--   Left _ -> False
+--   Right _ -> True
+
+-- | Returns true if the two type are equal, up to alpha equivalence and
+-- order of quantifier introduction. Note that alpha equivalence considers:
+-- `forall b a . a -> b -> a` and
+-- `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
 isSubtype :: (Var v) => Type v loc -> Type v loc -> Bool
 isSubtype t1 t2 =
   handleCompilerBug (Context.isSubtype (tvar $ void t1) (tvar $ void t2))
@@ -450,30 +480,12 @@ wellTyped ppe env term =
     enable =
       Context.PatternMatchCoverageCheckAndKindInferenceSwitch'Enabled
 
--- | @subtype a b@ is @Right b@ iff @f x@ is well-typed given
--- @x : a@ and @f : b -> t@. That is, if a value of type `a`
--- can be passed to a function expecting a `b`, then `subtype a b`
--- returns `Right b`. This function returns @Left note@ with information
--- about the reason for subtyping failure otherwise.
---
--- Example: @subtype (forall a. a -> a) (Int -> Int)@ returns @Right (Int -> Int)@.
--- subtype :: Var v => Type v -> Type v -> Either Note (Type v)
--- subtype t1 t2 = error "todo"
--- let (t1', t2') = (ABT.vmap TypeVar.Universal t1, ABT.vmap TypeVar.Universal t2)
--- in case Context.runM (Context.subtype t1' t2')
---                      (Context.MEnv Context.env0 [] Map.empty True) of
---   Left e -> Left e
---   Right _ -> Right t2
-
--- | Returns true if @subtype t1 t2@ returns @Right@, false otherwise
--- isSubtype :: Var v => Type v -> Type v -> Bool
--- isSubtype t1 t2 = case subtype t1 t2 of
---   Left _ -> False
---   Right _ -> True
-
--- | Returns true if the two type are equal, up to alpha equivalence and
--- order of quantifier introduction. Note that alpha equivalence considers:
--- `forall b a . a -> b -> a` and
--- `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))
+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

parser-typechecker/src/Unison/Typechecker/TypeError.hs

@@ -9,6 +9,7 @@ import Unison.Pattern (Pattern)
 import Unison.Prelude hiding (whenM)
 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.Extractor qualified as Ex
 import Unison.Typechecker.TypeVar (lowerType)
@@ -22,14 +23,21 @@ data BooleanMismatch = CondMismatch | AndMismatch | OrMismatch | GuardMismatch
 data ExistentialMismatch = IfBody | ListBody | CaseBody
   deriving (Show)
 
+-- | Additional mismatch info, which can be useful for providing hints in error messages.
+data MismatchInfo
+  = MissingDelay
+  | SuperfluousDelay
+  deriving (Show, Eq, Ord)
+
 data TypeError v loc
   = Mismatch
       { foundType :: C.Type v loc, -- overallType1
         expectedType :: C.Type v loc, -- overallType2
         foundLeaf :: C.Type v loc, -- leaf1
         expectedLeaf :: C.Type v loc, -- leaf2
         mismatchSite :: C.Term v loc,
-        note :: C.ErrorNote v loc
+        note :: C.ErrorNote v loc,
+        additionalInfo :: Maybe MismatchInfo
       }
   | BooleanMismatch
       { getBooleanMismatch :: BooleanMismatch,
@@ -322,12 +330,14 @@ generalMismatch = do
   -- it's likely we're missing some arguments from a function.
 
   case Type.cleanups [sub foundType, sub expectedType, sub foundLeaf, sub expectedLeaf] of
-    [ft, et, fl, el] ->
-      case mayNeedArgs of
-        Just needArgs ->
-          pure $ FunctionUnderApplied ft et fl el mismatchSite n (lowerType <$> needArgs)
-        Nothing ->
-          pure $ Mismatch ft et fl el mismatchSite n
+    [ft, et, fl, el] -> do
+      let delayMismatch = Typechecker.isMismatchMissingDelay foundType expectedType
+      case (mayNeedArgs, delayMismatch) of
+        (_, Just (Left {})) -> pure $ Mismatch ft et fl el mismatchSite n (Just MissingDelay)
+        (_, Just (Right {})) -> pure $ Mismatch ft et fl el mismatchSite n (Just SuperfluousDelay)
+        (Just needArgs, _) -> pure $ FunctionUnderApplied ft et fl el mismatchSite n (lowerType <$> needArgs)
+        _ -> do
+          pure $ Mismatch ft et fl el mismatchSite n Nothing
     _ -> error "generalMismatch: Mismatched type binding"
   where
     findUnderApplication found expected

unison-cli/src/Unison/LSP/FileAnalysis.hs

@@ -10,6 +10,7 @@ module Unison.LSP.FileAnalysis
     fileAnalysisWorker,
     getFileDefLocations,
     getFileNames,
+    analyseNotes,
   )
 where
 
@@ -74,6 +75,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
@@ -224,7 +226,8 @@ fileAnalysisWorker = forever do
 analyseFile :: (Lspish m) => (Foldable f) => Uri -> Text -> PPED.PrettyPrintEnvDecl -> f (Note Symbol Ann) -> m ([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
@@ -272,18 +275,31 @@ getTokenMap tokens =
       )
     & fold
 
-analyseNotes :: forall m f. (Lspish m, Foldable f) => Uri -> PrettyPrintEnv -> String -> f (Note Symbol Ann) -> m ([Diagnostic], [RangedCodeAction])
-analyseNotes fileUri ppe src notes = do
+analyseNotes ::
+  forall f m.
+  (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
   foldMapM go notes
   where
     go :: Note Symbol Ann -> m ([Diagnostic], [RangedCodeAction])
     go 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.FunctionUnderApplied {mismatchSite} -> singleRange $ ABT.annotation mismatchSite
               TypeError.FunctionApplication {f} -> singleRange $ ABT.annotation f
               TypeError.NotFunctionApplication {f} -> singleRange $ ABT.annotation f
@@ -381,6 +397,10 @@ analyseNotes fileUri ppe src notes = do
                 Context.OtherBug _s -> todoAnnotation
         pure (noteDiagnostic note ranges, [])
 
+    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])]
@@ -432,7 +452,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
@@ -586,3 +605,38 @@ mkDocumentSymbols parsedFile typecheckedFile =
       name <- maybeToList $ Name.parseText (Var.name sym)
       range <- maybeToList $ annToRange ann
       pure $ UDocumentSymbol name (Just typ) TermSymbol range []
+
+-- | 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]