More typechecking error message improvements (#1308)

Towards #1297 .  In this PR:

- Moves some functions out of `Pipeline` and into more appropriate modules
- Adds a new type `Join` to represent two types or other things, one "expected" and one "actual", at the point where they join + we check whether they are equal; a bunch of refactoring to use this new type.  This way we don't have to remember which argument is which when calling a function that takes one "expected" thing and one "actual" thing.
- Refactors all the `decomposeXXX` functions to take a `Syntax` node to use in error messages, and to take a `Sourced UType` (*i.e.* a `UType` along with whether it is "expected" or "actual") instead of just a `UType` so we can generate accurate error messages
- Introduce a basic typechecking stack that keeps track of "what we are currently in the middle of checking", so that when we encounter an error we can say things like "while checking the definition of `foo`".  Currently this is just a basic proof of concept.
- A few other miscellaneous error message improvements.

src/Swarm/Language/LSP.hs

@@ -18,11 +18,14 @@ import Language.LSP.Server
 import Language.LSP.Types (Hover (Hover))
 import Language.LSP.Types qualified as J
 import Language.LSP.Types.Lens qualified as J
-import Language.LSP.VFS
+import Language.LSP.VFS (VirtualFile (..), virtualFileText)
 import Swarm.Language.LSP.Hover qualified as H
 import Swarm.Language.LSP.VarUsage qualified as VU
 import Swarm.Language.Parse
 import Swarm.Language.Pipeline
+import Swarm.Language.Pretty (prettyText)
+import Swarm.Language.Syntax (SrcLoc (..))
+import Swarm.Language.Typecheck (ContextualTypeErr (..))
 import System.IO (stderr)
 import Witch
 
@@ -59,7 +62,7 @@ lspMain =
 diagnosticSourcePrefix :: Text
 diagnosticSourcePrefix = "swarm-lsp"
 
-debug :: MonadIO m => Text -> m ()
+debug :: (MonadIO m) => Text -> m ()
 debug msg = liftIO $ Text.hPutStrLn stderr $ "[swarm-lsp] " <> msg
 
 validateSwarmCode :: J.NormalizedUri -> J.TextDocumentVersion -> Text -> LspM () ()
@@ -125,6 +128,16 @@ validateSwarmCode doc version content = do
       Nothing -- tags
       (Just (J.List []))
 
+showTypeErrorPos :: Text -> ContextualTypeErr -> ((Int, Int), (Int, Int), Text)
+showTypeErrorPos code (CTE l _ te) = (minusOne start, minusOne end, msg)
+ where
+  minusOne (x, y) = (x - 1, y - 1)
+
+  (start, end) = case l of
+    SrcLoc s e -> getLocRange code (s, e)
+    NoLoc -> ((1, 1), (65535, 65535)) -- unknown loc spans the whole document
+  msg = prettyText te
+
 handlers :: Handlers (LspM ())
 handlers =
   mconcat

src/Swarm/Language/Pipeline.hs

@@ -14,8 +14,6 @@ module Swarm.Language.Pipeline (
   processParsedTerm,
   processTerm',
   processParsedTerm',
-  prettyTypeErr,
-  showTypeErrorPos,
   processTermEither,
 ) where
 
@@ -37,15 +35,17 @@ import Swarm.Language.Types
 import Witch
 
 -- | A record containing the results of the language processing
---   pipeline.  Put a 'Term' in, and get one of these out.
-data ProcessedTerm
-  = ProcessedTerm
-      TModule
-      -- ^ The elaborated + type-annotated term, plus types of any embedded definitions
-      Requirements
-      -- ^ Requirements of the term
-      ReqCtx
-      -- ^ Capability context for any definitions embedded in the term
+--   pipeline.  Put a 'Term' in, and get one of these out.  A
+--   'ProcessedTerm' contains:
+--
+--   * The elaborated + type-annotated term, plus the types of any
+--     embedded definitions ('TModule')
+--
+--   * The 'Requirements' of the term
+--
+--   * The requirements context for any definitions embedded in the
+--     term ('ReqCtx')
+data ProcessedTerm = ProcessedTerm TModule Requirements ReqCtx
   deriving (Data, Show, Eq, Generic)
 
 processTermEither :: Text -> Either String ProcessedTerm
@@ -80,25 +80,7 @@ processParsedTerm = processParsedTerm' empty empty
 processTerm' :: TCtx -> ReqCtx -> Text -> Either Text (Maybe ProcessedTerm)
 processTerm' ctx capCtx txt = do
   mt <- readTerm txt
-  first (prettyTypeErr txt) $ traverse (processParsedTerm' ctx capCtx) mt
-
-prettyTypeErr :: Text -> ContextualTypeErr -> Text
-prettyTypeErr code (CTE l te) = teLoc <> prettyText te
- where
-  teLoc = case l of
-    SrcLoc s e -> (into @Text . showLoc . fst $ getLocRange code (s, e)) <> ": "
-    NoLoc -> ""
-  showLoc (r, c) = show r ++ ":" ++ show c
-
-showTypeErrorPos :: Text -> ContextualTypeErr -> ((Int, Int), (Int, Int), Text)
-showTypeErrorPos code (CTE l te) = (minusOne start, minusOne end, msg)
- where
-  minusOne (x, y) = (x - 1, y - 1)
-
-  (start, end) = case l of
-    SrcLoc s e -> getLocRange code (s, e)
-    NoLoc -> ((1, 1), (65535, 65535)) -- unknown loc spans the whole document
-  msg = prettyText te
+  first (prettyTypeErrText txt) $ traverse (processParsedTerm' ctx capCtx) mt
 
 -- | Like 'processTerm'', but use a term that has already been parsed.
 processParsedTerm' :: TCtx -> ReqCtx -> Syntax -> Either ContextualTypeErr ProcessedTerm

src/Swarm/Language/Pipeline/QQ.hs

@@ -9,6 +9,7 @@ import Language.Haskell.TH qualified as TH
 import Language.Haskell.TH.Quote
 import Swarm.Language.Parse
 import Swarm.Language.Pipeline
+import Swarm.Language.Pretty
 import Swarm.Language.Syntax
 import Swarm.Language.Types (Polytype)
 import Swarm.Util (failT, liftText)
@@ -41,7 +42,7 @@ quoteTermExp s = do
         )
   parsed <- runParserTH pos parseTerm s
   case processParsedTerm parsed of
-    Left err -> failT [prettyTypeErr (from s) err]
+    Left err -> failT [prettyTypeErrText (from s) err]
     Right ptm -> dataToExpQ ((fmap liftText . cast) `extQ` antiTermExp) ptm
 
 antiTermExp :: Term' Polytype -> Maybe TH.ExpQ

src/Swarm/Language/Pretty.hs

@@ -25,37 +25,65 @@ import Prettyprinter.Render.String qualified as RS
 import Prettyprinter.Render.Text qualified as RT
 import Swarm.Language.Capability
 import Swarm.Language.Context
+import Swarm.Language.Parse (getLocRange)
 import Swarm.Language.Syntax
 import Swarm.Language.Typecheck
 import Swarm.Language.Types
 import Witch
 
+------------------------------------------------------------
+-- PrettyPrec class + utilities
+
 -- | Type class for things that can be pretty-printed, given a
 --   precedence level of their context.
 class PrettyPrec a where
   prettyPrec :: Int -> a -> Doc ann -- can replace with custom ann type later if desired
 
 -- | Pretty-print a thing, with a context precedence level of zero.
-ppr :: PrettyPrec a => a -> Doc ann
+ppr :: (PrettyPrec a) => a -> Doc ann
 ppr = prettyPrec 0
 
+-- | Render a pretty-printed document as @Text@.
+docToText :: Doc a -> Text
+docToText = RT.renderStrict . layoutPretty defaultLayoutOptions
+
 -- | Pretty-print something and render it as @Text@.
-prettyText :: PrettyPrec a => a -> Text
-prettyText = RT.renderStrict . layoutPretty defaultLayoutOptions . ppr
+prettyText :: (PrettyPrec a) => a -> Text
+prettyText = docToText . ppr
+
+-- | Render a pretty-printed document as a @String@.
+docToString :: Doc a -> String
+docToString = RS.renderString . layoutPretty defaultLayoutOptions
 
 -- | Pretty-print something and render it as a @String@.
-prettyString :: PrettyPrec a => a -> String
-prettyString = RS.renderString . layoutPretty defaultLayoutOptions . ppr
+prettyString :: (PrettyPrec a) => a -> String
+prettyString = docToString . ppr
 
 -- | Optionally surround a document with parentheses depending on the
 --   @Bool@ argument.
 pparens :: Bool -> Doc ann -> Doc ann
 pparens True = parens
 pparens False = id
 
+-- | Surround a document with backticks.
 bquote :: Doc ann -> Doc ann
 bquote d = "`" <> d <> "`"
 
+--------------------------------------------------
+-- Bullet lists
+
+data BulletList i = BulletList
+  { bulletListHeader :: forall a. Doc a
+  , bulletListItems :: [i]
+  }
+
+instance (PrettyPrec i) => PrettyPrec (BulletList i) where
+  prettyPrec _ (BulletList hdr items) =
+    nest 2 . vcat $ hdr : map (("-" <+>) . ppr) items
+
+------------------------------------------------------------
+-- PrettyPrec instances for terms, types, etc.
+
 instance PrettyPrec Text where
   prettyPrec _ = pretty
 
@@ -72,14 +100,14 @@ instance PrettyPrec BaseTy where
 instance PrettyPrec IntVar where
   prettyPrec _ = pretty . mkVarName "u"
 
-instance PrettyPrec (t (Fix t)) => PrettyPrec (Fix t) where
+instance (PrettyPrec (t (Fix t))) => PrettyPrec (Fix t) where
   prettyPrec p = prettyPrec p . unFix
 
 instance (PrettyPrec (t (UTerm t v)), PrettyPrec v) => PrettyPrec (UTerm t v) where
   prettyPrec p (UTerm t) = prettyPrec p t
   prettyPrec p (UVar v) = prettyPrec p v
 
-instance PrettyPrec t => PrettyPrec (TypeF t) where
+instance (PrettyPrec t) => PrettyPrec (TypeF t) where
   prettyPrec _ (TyBaseF b) = ppr b
   prettyPrec _ (TyVarF v) = pretty v
   prettyPrec p (TySumF ty1 ty2) =
@@ -103,7 +131,7 @@ instance PrettyPrec UPolytype where
   prettyPrec _ (Forall [] t) = ppr t
   prettyPrec _ (Forall xs t) = hsep ("∀" : map pretty xs) <> "." <+> ppr t
 
-instance PrettyPrec t => PrettyPrec (Ctx t) where
+instance (PrettyPrec t) => PrettyPrec (Ctx t) where
   prettyPrec _ Empty = emptyDoc
   prettyPrec _ (assocs -> bs) = brackets (hsep (punctuate "," (map prettyBinding bs)))
 
@@ -206,20 +234,41 @@ appliedTermPrec (TApp f _) = case f of
   _ -> appliedTermPrec f
 appliedTermPrec _ = 10
 
+------------------------------------------------------------
+-- Error messages
+
+-- | Format a 'ContextualTypeError' for the user and render it as
+--   @Text@.
+prettyTypeErrText :: Text -> ContextualTypeErr -> Text
+prettyTypeErrText code = docToText . prettyTypeErr code
+
+-- | Format a 'ContextualTypeError' for the user.
+prettyTypeErr :: Text -> ContextualTypeErr -> Doc ann
+prettyTypeErr code (CTE l tcStack te) =
+  vcat
+    [ teLoc <> ppr te
+    , ppr (BulletList "" tcStack)
+    ]
+ where
+  teLoc = case l of
+    SrcLoc s e -> (showLoc . fst $ getLocRange code (s, e)) <> ": "
+    NoLoc -> emptyDoc
+  showLoc (r, c) = pretty r <> ":" <> pretty c
+
 instance PrettyPrec TypeErr where
   prettyPrec _ (UnifyErr ty1 ty2) =
     "Can't unify" <+> ppr ty1 <+> "and" <+> ppr ty2
-  prettyPrec _ (Mismatch Nothing ty1 ty2) =
+  prettyPrec _ (Mismatch Nothing (getJoin -> (ty1, ty2))) =
     "Type mismatch: expected" <+> ppr ty1 <> ", but got" <+> ppr ty2
-  prettyPrec _ (Mismatch (Just t) ty1 ty2) =
+  prettyPrec _ (Mismatch (Just t) (getJoin -> (ty1, ty2))) =
     nest 2 . vcat $
       [ "Type mismatch:"
       , "From context, expected" <+> bquote (ppr t) <+> "to have type" <+> bquote (ppr ty1) <> ","
       , "but it actually has type" <+> bquote (ppr ty2)
       ]
-  prettyPrec _ (LambdaArgMismatch ty1 ty2) =
+  prettyPrec _ (LambdaArgMismatch (getJoin -> (ty1, ty2))) =
     "Lambda argument has type annotation" <+> ppr ty2 <> ", but expected argument type" <+> ppr ty1
-  prettyPrec _ (FieldsMismatch expFs actFs) = fieldMismatchMsg expFs actFs
+  prettyPrec _ (FieldsMismatch (getJoin -> (expFs, actFs))) = fieldMismatchMsg expFs actFs
   prettyPrec _ (EscapedSkolem x) =
     "Skolem variable" <+> pretty x <+> "would escape its scope"
   prettyPrec _ (UnboundVar x) =
@@ -255,11 +304,10 @@ instance PrettyPrec InvalidAtomicReason where
   prettyPrec _ NestedAtomic = "nested atomic block"
   prettyPrec _ LongConst = "commands that can take multiple ticks to execute are not allowed"
 
-data BulletList i = BulletList
-  { bulletListHeader :: forall a. Doc a
-  , bulletListItems :: [i]
-  }
+instance PrettyPrec LocatedTCFrame where
+  prettyPrec p (LocatedTCFrame _ f) = prettyPrec p f
 
-instance PrettyPrec i => PrettyPrec (BulletList i) where
-  prettyPrec _ (BulletList hdr items) =
-    nest 2 . vcat $ hdr : map (("-" <+>) . ppr) items
+instance PrettyPrec TCFrame where
+  prettyPrec _ (TCDef x) = "While checking the definition of" <+> pretty x
+  prettyPrec _ TCBindL = "While checking the left-hand side of a semicolon"
+  prettyPrec _ TCBindR = "While checking the right-hand side of a semicolon"