Attempt to improve function under-application and over-application errors

parser-typechecker/src/Unison/PrintError.hs

@@ -75,6 +75,7 @@ import Unison.Util.AnnotatedText qualified as AT
 import Unison.Util.ColorText (Color)
 import Unison.Util.ColorText qualified as Color
 import Unison.Util.Monoid (intercalateMap)
+import Unison.Util.Monoid qualified as Monoid
 import Unison.Util.Pretty (ColorText, Pretty)
 import Unison.Util.Pretty qualified as Pr
 import Unison.Util.Range (Range (..), startingLine)
@@ -332,14 +333,6 @@ renderTypeError e env src = case e of
               " expression ",
               "need to have the same type."
             ]
-  NotFunctionApplication {..} ->
-    mconcat
-      [ "This looks like a function call, but with a ",
-        style Type1 (renderType' env ft),
-        " where the function should be.  Are you missing an operator?\n\n",
-        annotatedAsStyle Type1 src f,
-        debugSummary note
-      ]
   ActionRestrictionFailure {..} ->
     mconcat
       [ Pr.lines
@@ -361,6 +354,87 @@ renderTypeError e env src = case e of
           ],
         debugSummary note
       ]
+  FunctionUnderApplied {..} ->
+    let expectedTypeStr = style Type2 (renderType' env expectedLeaf)
+        actualTypeStr = style ErrorSite (renderType' env foundLeaf)
+     in mconcat
+          [ "This call-site has type " <> actualTypeStr <> ":\n",
+            showSourceMaybes src [styleAnnotated ErrorSite foundLeaf],
+            "\n\n",
+            "But I expected the type " <> expectedTypeStr <> " because of:\n",
+            showSourceMaybes
+              src
+              [ (,Type1) . startingLine <$> (rangeForAnnotated mismatchSite),
+                (,Type2) <$> rangeForAnnotated expectedLeaf
+              ],
+            "\n\n",
+            Pr.lines
+              [ "It looks like the function application is missing these arguments:\n",
+                Pr.indentN 2 $ Monoid.intercalateMap ", " (style Type2 . renderType' env) needArgs
+              ],
+            unitHint,
+            intLiteralSyntaxTip mismatchSite expectedType,
+            debugNoteLoc
+              . mconcat
+              $ [ "\nloc debug:",
+                  "\n  mismatchSite: ",
+                  annotatedToEnglish mismatchSite,
+                  "\n     foundType: ",
+                  annotatedToEnglish foundType,
+                  "\n     foundLeaf: ",
+                  annotatedToEnglish foundLeaf,
+                  "\n  expectedType: ",
+                  annotatedToEnglish expectedType,
+                  "\n  expectedLeaf: ",
+                  annotatedToEnglish expectedLeaf,
+                  "\n"
+                ],
+            debugSummary note
+          ]
+    where
+      unitHintMsg =
+        "\nHint: Actions within a block must have type "
+          <> style Type2 (renderType' env expectedLeaf)
+          <> ".\n"
+          <> "      Use "
+          <> style Type1 "_ = <expr>"
+          <> " to ignore a result."
+      unitHint = if giveUnitHint then unitHintMsg else ""
+      giveUnitHint = case expectedType of
+        Type.Ref' u | u == unitRef -> case mismatchSite of
+          Term.Let1Named' v _ _ -> Var.isAction v
+          _ -> False
+        _ -> False
+  NotFunctionApplication {..} ->
+    case Type.arityIgnoringEffects ft of
+      0 ->
+        mconcat
+          [ "It looks like" <> style ErrorSite " this " <> "expression is being called like a function:\n\n",
+            annotatedAsStyle ErrorSite src f,
+            "\n\nbut the thing being applied has the type:\n\n",
+            style Type2 (renderType' env ft),
+            "\n\nWhich doesn't expect any arguments.",
+            "\n\n",
+            debugSummary note
+          ]
+      arity ->
+        mconcat
+          [ "It looks like" <> style ErrorSite " this " <> "function call:\n\n",
+            annotatedAsStyle ErrorSite src f,
+            "\n\nis being applied to ",
+            Pr.blue $ Pr.shown (length args),
+            " arguments, but it has the type\n\n",
+            Pr.indentN 2 $ style Type2 (renderType' env ft),
+            "\n\nwhich only accepts ",
+            Pr.blue $ Pr.shown arity,
+            maybePlural " argument" arity <> ".\n\n",
+            "Maybe you applied the function to too many arguments?\n\n",
+            debugSummary note
+          ]
+    where
+      maybePlural word n
+        | n == 1 = word
+        | otherwise = word <> "s"
   FunctionApplication {..} ->
     let fte = Type.removePureEffects False ft
         fteFreeVars = Set.map TypeVar.underlying $ ABT.freeVars fte
@@ -454,12 +528,7 @@ renderTypeError e env src = case e of
         "\n\n",
         showSourceMaybes
           src
-          [ -- these are overwriting the colored ranges for some reason?
-            --   (,Color.ForceShow) <$> rangeForAnnotated mismatchSite
-            -- , (,Color.ForceShow) <$> rangeForType foundType
-            -- , (,Color.ForceShow) <$> rangeForType expectedType
-            -- ,
-            (,Type1) . startingLine <$> (rangeForAnnotated mismatchSite),
+          [ (,Type1) . startingLine <$> (rangeForAnnotated mismatchSite),
             (,Type2) <$> rangeForAnnotated expectedLeaf
           ],
         fromOverHere'

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

@@ -11,6 +11,7 @@ import Unison.Type (Type)
 import Unison.Type qualified as Type
 import Unison.Typechecker.Context qualified as C
 import Unison.Typechecker.Extractor qualified as Ex
+import Unison.Typechecker.TypeVar (lowerType)
 import Unison.Util.Monoid (whenM)
 import Unison.Var (Var)
 import Prelude hiding (all, and, or)
@@ -63,7 +64,17 @@ data TypeError v loc
   | NotFunctionApplication
       { f :: C.Term v loc,
         ft :: C.Type v loc,
-        note :: C.ErrorNote v loc
+        note :: C.ErrorNote v loc,
+        args :: [C.Term v loc]
+      }
+  | FunctionUnderApplied
+      { 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,
+        needArgs :: [Type v loc]
       }
   | AbilityCheckFailure
       { ambient :: [C.Type v loc],
@@ -306,9 +317,27 @@ generalMismatch = do
   n <- Ex.errorNote
   mismatchSite <- Ex.innermostTerm
   ((foundLeaf, expectedLeaf), (foundType, expectedType)) <- firstLastSubtype
+  let mayNeedArgs = findUnderApplication foundLeaf expectedLeaf
+  -- If the found type is a function, and the result of that function matches the expected type,
+  -- 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] -> pure $ Mismatch ft et fl el mismatchSite n
+    [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
     _ -> error "generalMismatch: Mismatched type binding"
+  where
+    findUnderApplication found expected
+      | Right True <- C.isSubtype found expected = pure []
+      | otherwise =
+          case found of
+            Type.Arrow' i o -> (i :) <$> findUnderApplication o expected
+            Type.ForallNamed' _ body -> findUnderApplication body expected
+            Type.Effect' _ inner -> findUnderApplication inner expected
+            _ -> Nothing
 
 and,
   or,
@@ -399,15 +428,15 @@ applyingNonFunction :: (Var v) => Ex.ErrorExtractor v loc (TypeError v loc)
 applyingNonFunction = do
   _ <- Ex.typeMismatch
   n <- Ex.errorNote
-  (f, ft) <- Ex.unique $ do
+  (f, ft, args) <- Ex.unique $ do
     Ex.pathStart
-    (arity0Type, _arg, _argNum) <- Ex.inSynthesizeApp
+    _synthApp <- Ex.inSynthesizeApp
     (_, f, ft, args) <- Ex.inFunctionCall
-    let expectedArgCount = Type.arity ft
+    let expectedArgCount = Type.arityIgnoringEffects ft
         foundArgCount = length args
     -- unexpectedArgLoc = ABT.annotation arg
-    whenM (expectedArgCount < foundArgCount) $ pure (f, arity0Type)
-  pure $ NotFunctionApplication f (Type.cleanup ft) n
+    whenM (expectedArgCount < foundArgCount) $ pure (f, ft, args)
+  pure $ NotFunctionApplication f (Type.cleanup ft) n args
 
 -- | Want to collect this info:
 -- The `n`th argument to `f` is `foundType`, but I was expecting `expectedType`.

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

@@ -284,6 +284,7 @@ analyseNotes fileUri ppe src notes = do
               TypeError.Mismatch {mismatchSite} -> singleRange $ ABT.annotation mismatchSite
               TypeError.BooleanMismatch {mismatchSite} -> singleRange $ ABT.annotation mismatchSite
               TypeError.ExistentialMismatch {mismatchSite} -> singleRange $ ABT.annotation mismatchSite
+              TypeError.FunctionUnderApplied {mismatchSite} -> singleRange $ ABT.annotation mismatchSite
               TypeError.FunctionApplication {f} -> singleRange $ ABT.annotation f
               TypeError.NotFunctionApplication {f} -> singleRange $ ABT.annotation f
               TypeError.AbilityCheckFailure {abilityCheckFailureSite} -> singleRange abilityCheckFailureSite

unison-core/src/Unison/Type.hs

@@ -104,6 +104,17 @@ arity (Arrow' _ o) = 1 + arity o
 arity (Ann' a _) = arity a
 arity _ = 0
 
+-- | Like 'arity', but counts arguments past effect boundaries.
+-- E.g. for this type: `a ->{e} b -> c`,
+--   'arity' returns 1.
+--   'arityIgnoringEffects' returns 2.
+arityIgnoringEffects :: Type v a -> Int
+arityIgnoringEffects (ForallNamed' _ body) = arityIgnoringEffects body
+arityIgnoringEffects (Arrow' _ o) = 1 + arityIgnoringEffects o
+arityIgnoringEffects (Ann' a _) = arityIgnoringEffects a
+arityIgnoringEffects (Effect' _ o) = arityIgnoringEffects o
+arityIgnoringEffects _ = 0
+
 -- some smart patterns
 pattern Ref' :: TypeReference -> ABT.Term F v a
 pattern Ref' r <- ABT.Tm' (Ref r)
@@ -142,7 +153,7 @@ pattern Effects' es <- ABT.Tm' (Effects es)
 pattern Effect1' :: ABT.Term F v a -> ABT.Term F v a -> ABT.Term F v a
 pattern Effect1' e t <- ABT.Tm' (Effect e t)
 
-pattern Effect' :: (Ord v) => [Type v a] -> Type v a -> Type v a
+pattern Effect' :: [Type v a] -> Type v a -> Type v a
 pattern Effect' es t <- (unEffects1 -> Just (es, t))
 
 pattern Effect'' :: (Ord v) => [Type v a] -> Type v a -> Type v a
@@ -242,7 +253,7 @@ unEffect0 :: (Ord v) => Type v a -> ([Type v a], Type v a)
 unEffect0 (Effect1' e a) = (flattenEffects e, a)
 unEffect0 t = ([], t)
 
-unEffects1 :: (Ord v) => Type v a -> Maybe ([Type v a], Type v a)
+unEffects1 :: Type v a -> Maybe ([Type v a], Type v a)
 unEffects1 (Effect1' (Effects' es) a) = Just (es, a)
 unEffects1 _ = Nothing
 
@@ -768,6 +779,7 @@ functionResult = go False
   where
     go inArr (ForallNamed' _ body) = go inArr body
     go _inArr (Arrow' _i o) = go True o
+    go _inArr (Effect1' _e body) = go True body
     go inArr t = if inArr then Just t else Nothing
 
 -- | Bind all free variables (not in `except`) that start with a lowercase

unison-src/transcripts/idempotent/error-messages.md

@@ -368,3 +368,62 @@ a ! b = 1
     - An `ability` declaration, like unique ability Foo where ...
     - A `type` declaration, like structural type Optional a = None | Some a
 ```
+
+### Function under-application
+
+``` unison :error
+main : 'Nat
+main = do
+  multiply x y = x Nat.* y
+  add x y = x Nat.+ y
+  doMath x y = add (multiply x y)
+  doMath 1 2
+```
+
+``` ucm :added-by-ucm
+  Loading changes detected in scratch.u.
+
+  This call-site has type Nat -> Nat:
+      5 |   doMath x y = add (multiply x y)
+
+
+  But I expected the type Nat because of:
+      1 | main : 'Nat
+      2 | main = do
+      3 |   multiply x y = x Nat.* y
+      4 |   add x y = x Nat.+ y
+
+
+  It looks like the function application is missing these arguments:
+
+    Nat
+```
+
+### Function over-application
+
+``` unison :error
+main2 : 'Nat
+main2 = do
+  multiply x y = x Nat.* y
+  add x y = x Nat.+ y
+  doMath x y = add (multiply x y) 2 3
+  doMath 3 4
+```
+
+``` ucm :added-by-ucm
+  Loading changes detected in scratch.u.
+
+  It looks like this function call:
+
+      5 |   doMath x y = add (multiply x y) 2 3
+
+
+  is being applied to 3 arguments, but it has the type
+
+    Nat -> Nat -> Nat
+
+  which only accepts 2 arguments.
+
+  Maybe you applied the function to too many arguments?
+
+```

unison-src/transcripts/idempotent/fix2354.md

@@ -15,15 +15,18 @@ x = 'f
 ``` ucm :added-by-ucm
   Loading changes detected in scratch.u.
 
-  I found a value  of type:  (a1 ->{𝕖} a1) ->{𝕖} Nat
-  where I expected to find:  (a -> 𝕣1) -> 𝕣
+  This call-site has type (a1 ->{𝕖} a1) ->{𝕖} Nat:
+      1 | f : (forall a . a -> a) -> Nat
+
 
+  But I expected the type (a -> 𝕣1) -> 𝕣 because of:
       1 | f : (forall a . a -> a) -> Nat
       2 | f id = id 0
       3 | 
       4 | x = 'f
 
-    from right here:
 
-      1 | f : (forall a . a -> a) -> Nat
+  It looks like the function application is missing these arguments:
+
+    a ->{𝕖16} a
 ```