[typecheck] Add error infrastructure for type errors

Add a pretty error for mismatched constructor type in a pattern match

app/Main.hs

@@ -262,7 +262,7 @@ go c = do
       Micro.printPrettyCodeDefault micro
       putStrLn ""
       case Micro.checkModule micro of
-        Left er -> putStrLn er
+        Left er -> printErrorAnsi er
         Right {} -> putStrLn "Well done! It type checks"
     MiniHaskell MiniHaskellOptions {..} -> do
       m <- parseModuleIO _mhaskellInputFile

src/MiniJuvix/Syntax/MicroJuvix/Error.hs

@@ -0,0 +1,40 @@
+module MiniJuvix.Syntax.MicroJuvix.Error
+  ( module MiniJuvix.Syntax.MicroJuvix.Error,
+    module MiniJuvix.Syntax.MicroJuvix.Error.Pretty,
+    module MiniJuvix.Syntax.MicroJuvix.Error.Types,
+  )
+where
+
+import MiniJuvix.Prelude
+import MiniJuvix.Syntax.MicroJuvix.Error.Pretty
+import qualified MiniJuvix.Syntax.MicroJuvix.Error.Pretty as P
+import MiniJuvix.Syntax.MicroJuvix.Error.Types
+import Prettyprinter
+
+data TypeCheckerError
+ = ErrTooManyPatterns
+ | ErrWrongConstructorType WrongConstructorType
+ | ErrConstructorAppArgs
+ | ErrWrongType
+ | ErrExpectedFunctionType
+
+prettyT :: Text -> Doc Eann
+prettyT = pretty
+
+ppTypeCheckerError :: TypeCheckerError -> Doc Eann
+ppTypeCheckerError = \case
+  ErrWrongConstructorType e -> ppError e
+  ErrTooManyPatterns -> prettyT "too many patterns"
+  ErrConstructorAppArgs -> prettyT "constructor has wrong args"
+  ErrWrongType -> prettyT "wrong type"
+  ErrExpectedFunctionType -> prettyT "expected function type"
+
+docStream :: TypeCheckerError -> SimpleDocStream Eann
+docStream = layoutPretty defaultLayoutOptions . ppTypeCheckerError
+
+instance JuvixError TypeCheckerError where
+  renderAnsiText :: TypeCheckerError -> Text
+  renderAnsiText = renderAnsi . docStream
+
+  renderText :: TypeCheckerError -> Text
+  renderText = P.renderText . docStream

src/MiniJuvix/Syntax/MicroJuvix/Error/Pretty.hs

@@ -0,0 +1,9 @@
+module MiniJuvix.Syntax.MicroJuvix.Error.Pretty
+  ( module MiniJuvix.Syntax.MicroJuvix.Error.Pretty.Base,
+    module MiniJuvix.Syntax.MicroJuvix.Error.Pretty.Ansi,
+    module MiniJuvix.Syntax.MicroJuvix.Error.Pretty.Text)
+where
+
+import MiniJuvix.Syntax.MicroJuvix.Error.Pretty.Base
+import MiniJuvix.Syntax.MicroJuvix.Error.Pretty.Ansi
+import MiniJuvix.Syntax.MicroJuvix.Error.Pretty.Text

src/MiniJuvix/Syntax/MicroJuvix/Error/Pretty/Ansi.hs

@@ -0,0 +1,16 @@
+module MiniJuvix.Syntax.MicroJuvix.Error.Pretty.Ansi where
+
+import qualified MiniJuvix.Syntax.MicroJuvix.Pretty.Ansi as M
+
+import MiniJuvix.Prelude
+import MiniJuvix.Syntax.MicroJuvix.Error.Pretty.Base
+import Prettyprinter
+import Prettyprinter.Render.Terminal
+
+renderAnsi :: SimpleDocStream Eann -> Text
+renderAnsi = renderStrict . reAnnotateS stylize
+
+stylize :: Eann -> AnsiStyle
+stylize a = case a of
+  Highlight -> colorDull Red
+  MicroAnn m -> M.stylize m

src/MiniJuvix/Syntax/MicroJuvix/Error/Pretty/Base.hs

@@ -0,0 +1,25 @@
+module MiniJuvix.Syntax.MicroJuvix.Error.Pretty.Base where
+
+import qualified MiniJuvix.Syntax.MicroJuvix.Pretty as M
+import Prettyprinter
+import MiniJuvix.Prelude
+import MiniJuvix.Syntax.MicroJuvix.Error.Types
+
+data Eann = Highlight
+  | MicroAnn M.Ann
+
+ppCode :: M.PrettyCode c => c -> Doc Eann
+ppCode = reAnnotate MicroAnn . M.runPrettyCode M.defaultOptions
+
+indent' :: Doc ann -> Doc ann
+indent' = indent 2
+
+class PrettyError e where
+  ppError :: e -> Doc Eann
+
+instance PrettyError WrongConstructorType where
+  ppError e = "Type error during pattern matching."
+    <> line <> "The constructor" <+> (ppCode (e ^. wrongCtorTypeName)) <+> "has type:"
+    <> line <> indent' (ppCode (e ^. wrongCtorTypeActual))
+    <> line <> "but is expected to have type:"
+    <> line <> indent' (ppCode (e ^. wrongCtorTypeExpected))

src/MiniJuvix/Syntax/MicroJuvix/Error/Pretty/Text.hs

@@ -0,0 +1,9 @@
+module MiniJuvix.Syntax.MicroJuvix.Error.Pretty.Text where
+
+import MiniJuvix.Prelude
+import MiniJuvix.Syntax.MicroJuvix.Error.Pretty.Base
+import Prettyprinter
+import Prettyprinter.Render.Text
+
+renderText :: SimpleDocStream Eann -> Text
+renderText = renderStrict

src/MiniJuvix/Syntax/MicroJuvix/Error/Types.hs

@@ -0,0 +1,13 @@
+module MiniJuvix.Syntax.MicroJuvix.Error.Types where
+import MiniJuvix.Syntax.MicroJuvix.Language
+import Lens.Micro.Platform (makeLenses)
+
+-- | the type of the constructor used in a pattern does
+-- not match the type of the inductive being matched
+data WrongConstructorType = WrongConstructorType
+  { _wrongCtorTypeName :: Name,
+    _wrongCtorTypeExpected :: Type,
+    _wrongCtorTypeActual :: Type
+  }
+
+makeLenses ''WrongConstructorType

src/MiniJuvix/Syntax/MicroJuvix/Language.hs

@@ -29,6 +29,7 @@ data Name = Name
   { _nameText :: Text,
     _nameId :: NameId,
     _nameKind :: NameKind
+    -- TODO: Add Location here so we can print out line numbers
   }
   deriving stock (Show)
 

src/MiniJuvix/Syntax/MicroJuvix/Pretty.hs

@@ -0,0 +1,9 @@
+module MiniJuvix.Syntax.MicroJuvix.Pretty
+  ( module MiniJuvix.Syntax.MicroJuvix.Pretty.Base,
+    module MiniJuvix.Syntax.MicroJuvix.Pretty.Ansi,
+    module MiniJuvix.Syntax.MicroJuvix.Pretty.Ann,
+  ) where
+
+import MiniJuvix.Syntax.MicroJuvix.Pretty.Base
+import MiniJuvix.Syntax.MicroJuvix.Pretty.Ansi
+import MiniJuvix.Syntax.MicroJuvix.Pretty.Ann

src/MiniJuvix/Syntax/MicroJuvix/Pretty/Base.hs

@@ -22,6 +22,9 @@ defaultOptions =
 class PrettyCode c where
   ppCode :: Member (Reader Options) r => c -> Sem r (Doc Ann)
 
+runPrettyCode :: PrettyCode c => Options -> c -> Doc Ann
+runPrettyCode opts = run . runReader opts . ppCode
+
 instance PrettyCode Name where
   ppCode n =
     return $

src/MiniJuvix/Syntax/MicroJuvix/TypeChecker.hs

@@ -3,7 +3,7 @@ import MiniJuvix.Prelude
 import MiniJuvix.Syntax.MicroJuvix.Language
 import MiniJuvix.Syntax.MicroJuvix.InfoTable
 import qualified Data.HashMap.Strict as HashMap
-import MiniJuvix.Syntax.MicroJuvix.Pretty.Text
+import MiniJuvix.Syntax.MicroJuvix.Error
 
 type Err = Text
 
@@ -13,10 +13,10 @@ newtype LocalVars = LocalVars {
   deriving newtype (Semigroup, Monoid)
 makeLenses ''LocalVars
 
-checkModule :: Module -> Either Err Module
+checkModule :: Module -> Either TypeCheckerError Module
 checkModule m = run $ runError $ runReader (buildTable m) (checkModule' m)
 
-checkModule' :: Members '[Reader InfoTable, Error Err] r =>
+checkModule' :: Members '[Reader InfoTable, Error TypeCheckerError] r =>
   Module -> Sem r Module
 checkModule' Module {..} = do
   _moduleBody' <- checkModuleBody _moduleBody
@@ -25,7 +25,7 @@ checkModule' Module {..} = do
     ..
     }
 
-checkModuleBody :: Members '[Reader InfoTable, Error Err] r =>
+checkModuleBody :: Members '[Reader InfoTable, Error TypeCheckerError] r =>
   ModuleBody -> Sem r ModuleBody
 checkModuleBody ModuleBody {..} = do
   _moduleStatements' <- mapM checkStatement _moduleStatements
@@ -33,7 +33,7 @@ checkModuleBody ModuleBody {..} = do
     _moduleStatements = _moduleStatements'
     }
 
-checkStatement :: Members '[Reader InfoTable, Error Err] r =>
+checkStatement :: Members '[Reader InfoTable, Error TypeCheckerError] r =>
   Statement -> Sem r Statement
 checkStatement s = case s of
   StatementFunction fun -> StatementFunction <$> checkFunctionDef fun
@@ -41,7 +41,7 @@ checkStatement s = case s of
   StatementInductive {} -> return s
   StatementAxiom {} -> return s
 
-checkFunctionDef :: Members '[Reader InfoTable, Error Err] r =>
+checkFunctionDef :: Members '[Reader InfoTable, Error TypeCheckerError] r =>
   FunctionDef -> Sem r FunctionDef
 checkFunctionDef FunctionDef {..} = do
   info <- lookupFunction _funDefName
@@ -51,26 +51,14 @@ checkFunctionDef FunctionDef {..} = do
     ..
     }
 
-checkExpression :: Members '[Reader InfoTable, Error Err, Reader LocalVars] r =>
+checkExpression :: Members '[Reader InfoTable, Error TypeCheckerError, Reader LocalVars] r =>
   Type -> Expression -> Sem r Expression
 checkExpression t e = do
   t' <- inferExpression' e
-  unlessM (matchTypes t (t' ^. typedType)) (throwErr
-      ("wrong type" <> "\nExpression:" <> renderPrettyCodeDefault e
-      <> "\nInferred type: " <> renderPrettyCodeDefault (t' ^. typedType)
-      <> "\nExpected type: " <> renderPrettyCodeDefault t
-      ))
+  when (t /= t' ^. typedType) (throw ErrWrongType)
   return (ExpressionTyped t')
 
-matchTypes :: Members '[Reader InfoTable] r =>
-  Type -> Type -> Sem r Bool
-matchTypes a b = do
-  a' <- normalizeType a
-  b' <- normalizeType b
-  return $
-    a' == TypeAny || b' == TypeAny || a' == b'
-
-inferExpression :: Members '[Reader InfoTable, Error Err, Reader LocalVars] r =>
+inferExpression :: Members '[Reader InfoTable, Error TypeCheckerError, Reader LocalVars] r =>
    Expression -> Sem r Expression
 inferExpression = fmap ExpressionTyped . inferExpression'
 
@@ -104,13 +92,13 @@ unfoldFunType t = case t of
   TypeFunction (Function l r) -> first (l:) (unfoldFunType r)
   _ -> ([], t)
 
-checkFunctionClause :: forall r. Members '[Reader InfoTable, Error Err] r =>
+checkFunctionClause :: forall r. Members '[Reader InfoTable, Error TypeCheckerError] r =>
   FunctionInfo -> FunctionClause -> Sem r FunctionClause
 checkFunctionClause info FunctionClause{..} = do
   let (argTys, rty) = unfoldFunType (info ^. functionInfoType)
       (patTys, restTys) = splitAt (length _clausePatterns) argTys
       bodyTy = foldFunType restTys rty
-  when (length patTys /= length _clausePatterns) (throwErr "too many patterns")
+  when (length patTys /= length _clausePatterns) (throw ErrTooManyPatterns)
   locals <- mconcat <$> zipWithM checkPattern patTys _clausePatterns
   clauseBody' <- runReader locals (checkExpression bodyTy _clauseBody)
   return FunctionClause {
@@ -118,7 +106,7 @@ checkFunctionClause info FunctionClause{..} = do
     ..
     }
 
-checkPattern :: forall r. Members '[Reader InfoTable, Error Err] r =>
+checkPattern :: forall r. Members '[Reader InfoTable, Error TypeCheckerError] r =>
   Type -> Pattern -> Sem r LocalVars
 checkPattern type_ pat = LocalVars . HashMap.fromList <$> go type_ pat
   where
@@ -128,18 +116,16 @@ checkPattern type_ pat = LocalVars . HashMap.fromList <$> go type_ pat
     PatternVariable v -> return [(v, ty)]
     PatternConstructorApp a -> do
       info <- lookupConstructor (a ^. constrAppConstructor)
-      when (TypeIden (TypeIdenInductive (info ^. constructorInfoInductive)) /= ty) (throwErr "wrong type for constructor")
+      let inductiveTy = TypeIden (TypeIdenInductive (info ^. constructorInfoInductive))
+      when (inductiveTy /= ty) (throw (ErrWrongConstructorType (WrongConstructorType (a ^. constrAppConstructor) ty inductiveTy)))
       goConstr a
     where
     goConstr :: ConstructorApp -> Sem r [(VarName, Type)]
     goConstr (ConstructorApp c ps) = do
       tys <- (^. constructorInfoArgs) <$> lookupConstructor c
-      when (length tys /= length ps) (throwErr "wrong number of arguments in constructor app")
+      when (length tys /= length ps) (throw ErrConstructorAppArgs)
       concat <$> zipWithM go tys ps
 
-throwErr :: Members '[Error Err] r => Err -> Sem r a
-throwErr = throw
-
 -- TODO currently equivalent to id
 normalizeType :: forall r. Members '[Reader InfoTable] r => Type -> Sem r Type
 normalizeType t = case t of
@@ -158,7 +144,7 @@ normalizeType t = case t of
     r' <- normalizeType r
     return (Function l' r')
 
-inferExpression' :: forall r. Members '[Reader InfoTable, Error Err, Reader LocalVars] r =>
+inferExpression' :: forall r. Members '[Reader InfoTable, Error TypeCheckerError, Reader LocalVars] r =>
    Expression -> Sem r TypedExpression
 inferExpression' e = case e of
   ExpressionIden i -> inferIden i
@@ -197,4 +183,4 @@ inferExpression' e = case e of
   getFunctionType :: Type -> Sem r Function
   getFunctionType t = case t of
     TypeFunction f -> return f
-    _ -> throwErr ("expected function type " <> show t)
+    _ -> throw ErrExpectedFunctionType