Better type error messages when there are unification variables involved

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,23 @@ instance PrettyPrec BaseTy where
 instance PrettyPrec IntVar where
   prettyPrec _ = pretty . mkVarName "u"
 
-instance PrettyPrec (t (Fix t)) => PrettyPrec (Fix t) where
+data Wildcard = Wildcard
+  deriving (Eq, Ord, Show)
+
+-- | We can use the 'Wildcard' value to replace unification variables
+--   when we don't care about them, e.g. to print out the shape of a
+--   type like @(_ -> _) * _@
+instance PrettyPrec Wildcard where
+  prettyPrec _ _ = "_"
+
+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 +140,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 +243,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)
+      , "From context, expected" <+> bquote (ppr t) <+> "to" <+> typeDescription Expected ty1 <> ","
+      , "but it" <+> typeDescription Actual ty2
       ]
-  prettyPrec _ (LambdaArgMismatch ty1 ty2) =
-    "Lambda argument has type annotation" <+> ppr ty2 <> ", but expected argument type" <+> ppr ty1
-  prettyPrec _ (FieldsMismatch expFs actFs) = fieldMismatchMsg expFs actFs
+  prettyPrec _ (LambdaArgMismatch (getJoin -> (ty1, ty2))) =
+    "Lambda argument has type annotation" <+> bquote (ppr ty2) <> ", but expected argument type" <+> bquote (ppr ty1)
+  prettyPrec _ (FieldsMismatch (getJoin -> (expFs, actFs))) = fieldMismatchMsg expFs actFs
   prettyPrec _ (EscapedSkolem x) =
     "Skolem variable" <+> pretty x <+> "would escape its scope"
   prettyPrec _ (UnboundVar x) =
@@ -237,6 +295,60 @@ instance PrettyPrec TypeErr where
   prettyPrec _ (InvalidAtomic reason t) =
     "Invalid atomic block:" <+> ppr reason <> ":" <+> ppr t
 
+-- | Given a type and its source, construct an appropriate description
+--   of it to go in a type mismatch error message.
+typeDescription :: Source -> UType -> Doc a
+typeDescription src ty
+  | not (hasAnyUVars ty) =
+      withSource src "have" "actually has" <+> "type" <+> bquote (ppr ty)
+  | Just f <- isTopLevelConstructor ty =
+      withSource src "be" "is actually" <+> tyNounPhrase f
+  | otherwise =
+      withSource src "have" "actually has" <+> "a type like" <+> bquote (ppr (fmap (const Wildcard) ty))
+
+-- | Check whether a type contains any unification variables at all.
+hasAnyUVars :: UType -> Bool
+hasAnyUVars = ucata (const True) or
+
+-- | Check whether a type consists of a top-level type constructor
+--   immediately applied to unification variables.
+isTopLevelConstructor :: UType -> Maybe (TypeF ())
+isTopLevelConstructor (UTyCmd (UVar {})) = Just $ TyCmdF ()
+isTopLevelConstructor (UTyDelay (UVar {})) = Just $ TyDelayF ()
+isTopLevelConstructor (UTySum (UVar {}) (UVar {})) = Just $ TySumF () ()
+isTopLevelConstructor (UTyProd (UVar {}) (UVar {})) = Just $ TyProdF () ()
+isTopLevelConstructor (UTyFun (UVar {}) (UVar {})) = Just $ TyFunF () ()
+isTopLevelConstructor _ = Nothing
+
+-- | Return an English noun phrase describing things with the given
+--   top-level type constructor.
+tyNounPhrase :: TypeF () -> Doc a
+tyNounPhrase = \case
+  TyBaseF b -> baseTyNounPhrase b
+  TyVarF {} -> "a type variable"
+  TyCmdF {} -> "a command"
+  TyDelayF {} -> "a delayed expression"
+  TySumF {} -> "a sum"
+  TyProdF {} -> "a pair"
+  TyFunF {} -> "a function"
+  TyRcdF {} -> "a record"
+
+-- | Return an English noun phrase describing things with the given
+--   base type.
+baseTyNounPhrase :: BaseTy -> Doc a
+baseTyNounPhrase = \case
+  BVoid -> "void"
+  BUnit -> "the unit value"
+  BInt -> "an integer"
+  BText -> "text"
+  BDir -> "a direction"
+  BBool -> "a boolean"
+  BActor -> "an actor"
+  BKey -> "a key"
+
+-- | Generate an appropriate message when the sets of fields in two
+--   record types do not match, explaining which fields are extra and
+--   which are missing.
 fieldMismatchMsg :: Set Var -> Set Var -> Doc a
 fieldMismatchMsg expFs actFs =
   nest 2 . vcat $
@@ -255,11 +367,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"