Add TCAppL and TCAppR typechecking stack frames, and remove TCBind{L,R}

src/swarm-lang/Swarm/Language/Typecheck.hs

@@ -93,17 +93,19 @@ import Prelude hiding (lookup)
 data TCFrame where
   -- | Checking a definition.
   TCLet :: Var -> TCFrame
-  -- | Inferring the LHS of a bind.
-  TCBindL :: TCFrame
-  -- | Inferring the RHS of a bind.
-  TCBindR :: TCFrame
+  -- | Inferring the LHS of an application.  Stored Syntax is the term
+  --   on the RHS.
+  TCAppL :: Syntax -> TCFrame
+  -- | Checking the RHS of an application.  Stored Syntax is the term
+  -- on the LHS.
+  TCAppR :: Syntax -> TCFrame
   deriving (Show)
 
 instance PrettyPrec TCFrame where
   prettyPrec _ = \case
     TCLet x -> "While checking the definition of" <+> pretty x
-    TCBindL -> "While checking the left-hand side of a semicolon"
-    TCBindR -> "While checking the right-hand side of a semicolon"
+    TCAppL s -> "While checking a function applied to an argument: _" <+> prettyPrec 11 s
+    TCAppR s -> "While checking the argument to a function:" <+> prettyPrec 10 s <+> "_"
 
 -- | A typechecking stack frame together with the relevant @SrcLoc@.
 data LocatedTCFrame = LocatedTCFrame SrcLoc TCFrame
@@ -255,15 +257,14 @@ lookup loc x = do
 addLocToTypeErr ::
   ( Has (Throw ContextualTypeErr) sig m
   , Has (Catch ContextualTypeErr) sig m
-  , Has (Reader TCStack) sig m
   ) =>
   SrcLoc ->
   m a ->
   m a
 addLocToTypeErr l m =
   m `catchError` \case
-    CTE NoLoc _ te -> throwTypeErr l te
-    te -> throwError te
+    CTE NoLoc stk te -> throwError $ CTE l stk te
+    cte -> throwError cte
 
 ------------------------------------------------------------
 -- Dealing with variables: free variables, fresh variables,
@@ -679,13 +680,14 @@ prettyTypeErr code (CTE l tcStack te) =
     NoLoc -> emptyDoc
   showLoc (r, c) = pretty r <> ":" <> pretty c
 
--- | Filter the TCStack of extravagant Binds.
+-- | Filter the TCStack so we stop printing context outside of a def/let
 filterTCStack :: TCStack -> TCStack
 filterTCStack tcStack = case tcStack of
   [] -> []
+  -- A def/let is enough context to locate something; don't keep
+  -- printing wider context after that
   t@(LocatedTCFrame _ (TCLet _)) : _ -> [t]
-  t@(LocatedTCFrame _ TCBindR) : xs -> t : filterTCStack xs
-  t@(LocatedTCFrame _ TCBindL) : xs -> t : filterTCStack xs
+  t : xs -> t : filterTCStack xs
 
 ------------------------------------------------------------
 -- Type decomposition
@@ -892,11 +894,13 @@ infer s@(CSyntax l t cs) = addLocToTypeErr l $ case t of
   -- each time.
   SApp f x -> do
     -- Infer the type of the left-hand side and make sure it has a function type.
-    f' <- infer f
-    (argTy, resTy) <- decomposeFunTy f (Actual, f' ^. sType)
+    (f', argTy, resTy) <- withFrame l (TCAppL x) $ do
+      f' <- infer f
+      (argTy, resTy) <- decomposeFunTy f (Actual, f' ^. sType)
+      pure (f', argTy, resTy)
 
     -- Then check that the argument has the right type.
-    x' <- check x argTy
+    x' <- withFrame l (TCAppR f) $ check x argTy
 
     -- Call applyBindings explicitly, so that anything we learned
     -- about unification variables while checking the type of the
@@ -922,13 +926,12 @@ infer s@(CSyntax l t cs) = addLocToTypeErr l $ case t of
   -- the surface syntax, so the second through fourth fields are
   -- necessarily Nothing.
   SBind mx _ _ _ c1 c2 -> do
-    c1' <- withFrame l TCBindL $ infer c1
+    c1' <- infer c1
     a <- decomposeCmdTy c1 (Actual, c1' ^. sType)
     genA <- generalize a
     c2' <-
-      maybe id ((`withBinding` genA) . lvVar) mx
-        . withFrame l TCBindR
-        $ infer c2
+      maybe id ((`withBinding` genA) . lvVar) mx $
+        infer c2
 
     -- We don't actually need the result type since we're just
     -- going to return the entire type, but it's important to

test/unit/TestLanguagePipeline.hs

@@ -668,13 +668,34 @@ testLanguagePipeline =
                 "1:1: Undefined type U"
             )
         ]
-    , testCase
-        "Stop printing context after a definition. - #1336"
-        ( processCompare
-            (==)
-            "move; def x = move; say 3 end; move;"
-            "1:25: Type mismatch:\n  From context, expected `3` to have type `Text`,\n  but it actually has type `Int`\n\n  - While checking the right-hand side of a semicolon\n  - While checking the definition of x"
-        )
+    , testGroup
+        "typechecking context stack"
+        [ testCase
+            "Stop printing context after a definition. - #1336"
+            ( processCompare
+                (==)
+                "move; def x = move; say 3 end; move;"
+                "1:25: Type mismatch:\n  From context, expected `3` to have type `Text`,\n  but it actually has type `Int`\n\n  - While checking the argument to a function: say _\n  - While checking the definition of x"
+            )
+        , testCase
+            "Error inside function application + argument #2220"
+            ( process
+                "id 3 3"
+                "1:1: Unbound variable id\n\n  - While checking a function applied to an argument: _ 3\n  - While checking a function applied to an argument: _ 3"
+            )
+        , testCase
+            "Error inside function application + argument #2220"
+            ( process
+                "(\\x. x) 7 8"
+                "1:1: Type mismatch:\n  From context, expected `(\\x. x) 7` to be a function,\n  but it actually has type `Int`\n\n  - While checking a function applied to an argument: _ 8"
+            )
+        , testCase
+            "Nested error #2220"
+            ( process
+                "\"hi\" + 2"
+                "1:1: Type mismatch:\n  From context, expected `\"hi\"` to have type `Int`,\n  but it actually has type `Text`\n\n  - While checking the argument to a function: (+) _\n  - While checking a function applied to an argument: _ 2"
+            )
+        ]
     , testGroup
         "let and def types"
         [ testCase