Merge pull request #22 from heliaxdev/typecheck-errors

Improve typechecker error messages

app/Commands/MicroJuvix.hs

@@ -6,10 +6,40 @@ import Commands.Extra
 import MiniJuvix.Prelude hiding (Doc)
 import Options.Applicative
 
+data MicroJuvixCommand
+  = Pretty MicroJuvixOptions
+  | TypeCheck MicroJuvixOptions
+
 newtype MicroJuvixOptions = MicroJuvixOptions
   { _mjuvixInputFile :: FilePath
   }
 
+parseMicroJuvixCommand :: Parser MicroJuvixCommand
+parseMicroJuvixCommand =
+  hsubparser $
+    mconcat
+      [ commandPretty
+      , commandTypeCheck
+      ]
+  where
+    commandPretty :: Mod CommandFields MicroJuvixCommand
+    commandPretty = command "pretty" prettyInfo
+
+    commandTypeCheck :: Mod CommandFields MicroJuvixCommand
+    commandTypeCheck = command "typecheck" typeCheckInfo
+
+    prettyInfo :: ParserInfo MicroJuvixCommand
+    prettyInfo =
+      info
+        (Pretty <$> parseMicroJuvix)
+        (progDesc "Translate a MiniJuvix file to MicroJuvix and pretty print the result")
+
+    typeCheckInfo :: ParserInfo MicroJuvixCommand
+    typeCheckInfo =
+      info
+        (TypeCheck <$> parseMicroJuvix)
+        (progDesc "Translate a MiniJuvix file to MicroJuvix and typecheck the result")
+
 parseMicroJuvix :: Parser MicroJuvixOptions
 parseMicroJuvix = do
   _mjuvixInputFile <- parseInputFile

app/Main.hs

@@ -21,6 +21,7 @@ import qualified MiniJuvix.Syntax.Concrete.Scoped.Pretty.Text as T
 import qualified MiniJuvix.Syntax.Concrete.Scoped.Scoper as M
 import qualified MiniJuvix.Syntax.MicroJuvix.Pretty.Ansi as Micro
 import qualified MiniJuvix.Syntax.MicroJuvix.TypeChecker as Micro
+import qualified MiniJuvix.Syntax.MicroJuvix.Language as Micro
 import qualified MiniJuvix.Termination as T
 import qualified MiniJuvix.Termination.CallGraph as A
 import qualified MiniJuvix.Translation.AbstractToMicroJuvix as Micro
@@ -40,7 +41,7 @@ data Command
   | Html HtmlOptions
   | Termination TerminationCommand
   | MiniHaskell MiniHaskellOptions
-  | MicroJuvix MicroJuvixOptions
+  | MicroJuvix MicroJuvixCommand
   | DisplayVersion
 
 data ScopeOptions = ScopeOptions
@@ -174,8 +175,8 @@ parseCommand =
         minfo :: ParserInfo Command
         minfo =
           info
-            (MicroJuvix <$> parseMicroJuvix)
-            (progDesc "Translate a MiniJuvix file to MicroJuvix")
+            (MicroJuvix <$> parseMicroJuvixCommand)
+            (progDesc "Subcommands related to MicroJuvix")
 
     commandMiniHaskell :: Mod CommandFields Command
     commandMiniHaskell = command "minihaskell" minfo
@@ -254,22 +255,20 @@ go c = do
       m <- parseModuleIO _htmlInputFile
       (_ , s) <- fromRightIO' printErrorAnsi $ M.scopeCheck1IO root m
       genHtml defaultOptions _htmlRecursive _htmlTheme s
-    MicroJuvix MicroJuvixOptions {..} -> do
-      m <- parseModuleIO _mjuvixInputFile
-      (_, s) <- fromRightIO' printErrorAnsi $ M.scopeCheck1IO root m
-      (_, a) <- fromRightIO' putStrLn (return $ A.translateModule s)
-      let micro = Micro.translateModule a
+    MicroJuvix (Pretty MicroJuvixOptions {..}) -> do
+      micro <- miniToMicro root _mjuvixInputFile
       Micro.printPrettyCodeDefault micro
-      putStrLn ""
+    MicroJuvix (TypeCheck MicroJuvixOptions {..}) -> do
+      micro <- miniToMicro root _mjuvixInputFile
       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
       (_, s) <- fromRightIO' printErrorAnsi $ M.scopeCheck1IO root m
       (_, a) <- fromRightIO' putStrLn (return $ A.translateModule s)
       let micro = Micro.translateModule a
-      checkedMicro <- fromRightIO' putStrLn (return $ Micro.checkModule micro)
+      checkedMicro <- fromRightIO' printErrorAnsi (return $ Micro.checkModule micro)
       minihaskell <- fromRightIO' putStrLn (return $ Hask.translateModule checkedMicro)
       Hask.printPrettyCodeDefault minihaskell
     Termination (Calls opts@CallsOptions {..}) -> do
@@ -302,6 +301,13 @@ go c = do
           Nothing -> putStrLn (n <> " Fails the termination checking")
           Just (T.LexOrder k) -> putStrLn (n <> " Terminates with order " <> show (toList k))
         putStrLn ""
+    where
+      miniToMicro :: FilePath -> FilePath -> IO Micro.Module
+      miniToMicro root p = do
+        m <- parseModuleIO p
+        (_, s) <- fromRightIO' printErrorAnsi $ M.scopeCheck1IO root m
+        (_, a) <- fromRightIO' putStrLn (return $ A.translateModule s)
+        return (Micro.translateModule a)
 
 main :: IO ()
 main = execParser descr >>= go

src/MiniJuvix/Syntax/MicroJuvix/Error.hs

@@ -0,0 +1,37 @@
+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 TooManyPatterns
+ | ErrWrongConstructorType WrongConstructorType
+ | ErrWrongConstructorAppArgs WrongConstructorAppArgs
+ | ErrWrongType WrongType
+ | ErrExpectedFunctionType ExpectedFunctionType
+
+ppTypeCheckerError :: TypeCheckerError -> Doc Eann
+ppTypeCheckerError = \case
+  ErrWrongConstructorType e -> ppError e
+  ErrTooManyPatterns e -> ppError e
+  ErrWrongConstructorAppArgs e -> ppError e
+  ErrWrongType e -> ppError e
+  ErrExpectedFunctionType e -> ppError e
+
+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,65 @@
+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
+import MiniJuvix.Syntax.MicroJuvix.Language
+
+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
+
+prettyT :: Text -> Doc Eann
+prettyT = pretty
+
+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))
+
+instance PrettyError WrongConstructorAppArgs where
+  ppError e = "Type error during pattern matching."
+    <> line <> "The constructor:" <+> ctorName <+> "is being matched against" <+> numPats <> ":"
+    <> line <> indent' (ppCode (e ^. wrongCtorAppApp))
+    <> line <> "but is expected to be matched against" <+> numTypes <+> "with the following types:"
+    <> line <> indent' (hsep (ctorName : (ppCode <$> (e ^. wrongCtorAppTypes))))
+    where
+      numPats :: Doc ann
+      numPats = pat (length (e ^. wrongCtorAppApp . constrAppParameters))
+      numTypes :: Doc ann
+      numTypes = pat (length (e ^. wrongCtorAppTypes))
+      ctorName :: Doc Eann
+      ctorName = ppCode (e ^. wrongCtorAppApp . constrAppConstructor)
+      pat :: Int -> Doc ann
+      pat n = pretty n <+> plural "pattern" "patterns" n
+
+instance PrettyError WrongType where
+  ppError e = "Type error."
+    <> line <> "The expression" <+> ppCode (e ^. wrongTypeExpression) <+> "has type:"
+    <> line <> indent' (ppCode (e ^. wrongTypeInferredType))
+    <> line <> "but is expected to have type:"
+    <> line <> indent' (ppCode (e ^. wrongTypeExpectedType))
+
+instance PrettyError ExpectedFunctionType where
+  ppError e = "Type error in the expression:"
+    <> line <> indent' (ppCode (e ^. expectedFunctionTypeExpression))
+    <> line <> "the expression" <+> ppCode (e ^. expectedFunctionTypeApp) <+> "is expected to have a function type but has type:"
+    <> line <> indent' (ppCode (e ^. expectedFunctionTypeType))
+
+instance PrettyError TooManyPatterns where
+  ppError e = "Type error in the definition of" <+> ppCode (e ^. tooManyPatternsClause . clauseName) <> "."
+    <> line <> "The function clause:"
+    <> line <> indent' (ppCode (e ^. tooManyPatternsClause))
+    <> line <> "matches too many patterns. It should match the following types:"
+    <> line <> indent' (hsep (ppCode <$> (e ^. tooManyPatternsTypes)))

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,46 @@
+module MiniJuvix.Syntax.MicroJuvix.Error.Types where
+
+import MiniJuvix.Prelude
+import MiniJuvix.Syntax.MicroJuvix.Language
+
+-- | 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
+  }
+
+-- | the arguments of a constructor pattern do not match
+-- the expected arguments of the constructor
+data WrongConstructorAppArgs = WrongConstructorAppArgs
+  { _wrongCtorAppApp :: ConstructorApp,
+    _wrongCtorAppTypes :: [Type]
+  }
+
+-- | the type of an expression does not match the inferred type
+data WrongType = WrongType
+  { _wrongTypeExpression :: Expression,
+    _wrongTypeExpectedType :: Type,
+    _wrongTypeInferredType :: Type
+  }
+
+-- | The left hand expression of a function application is not
+-- a function type.
+data ExpectedFunctionType = ExpectedFunctionType
+  { _expectedFunctionTypeExpression :: Expression,
+    _expectedFunctionTypeApp :: Expression,
+    _expectedFunctionTypeType :: Type
+  }
+
+-- | A function definition clause matches too many arguments
+data TooManyPatterns = TooManyPatterns
+  { _tooManyPatternsClause :: FunctionClause,
+    _tooManyPatternsTypes :: [Type]
+  }
+
+makeLenses ''WrongConstructorType
+makeLenses ''WrongConstructorAppArgs
+makeLenses ''WrongType
+makeLenses ''ExpectedFunctionType
+makeLenses ''TooManyPatterns

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)
 
@@ -77,7 +78,8 @@ data FunctionDef = FunctionDef
   }
 
 data FunctionClause = FunctionClause
-  { _clausePatterns :: [Pattern],
+  { _clauseName :: FunctionName,
+    _clausePatterns :: [Pattern],
     _clauseBody :: Expression
   }
 

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 $
@@ -169,15 +172,17 @@ instance PrettyCode FunctionDef where
   ppCode f = do
     funDefName' <- ppCode (f ^. funDefName)
     funDefType' <- ppCode (f ^. funDefType)
-    clauses' <- mapM (ppClause funDefName') (f ^. funDefClauses)
+    clauses' <- mapM ppCode (f ^. funDefClauses)
     return $
       funDefName' <+> kwColonColon <+> funDefType' <> line
         <> vsep (toList clauses')
-    where
-      ppClause fun c = do
-        clausePatterns' <- mapM ppCodeAtom (c ^. clausePatterns)
-        clauseBody' <- ppCode (c ^. clauseBody)
-        return $ fun <+> hsep clausePatterns' <+> kwEquals <+> clauseBody'
+
+instance PrettyCode FunctionClause where
+  ppCode c = do
+    funName <- ppCode (c ^. clauseName)
+    clausePatterns' <- mapM ppCodeAtom (c ^. clausePatterns)
+    clauseBody' <- ppCode (c ^. clauseBody)
+    return $ funName <+> hsep clausePatterns' <+> kwEquals <+> clauseBody'
 
 instance PrettyCode Backend where
   ppCode = \case

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,17 @@ 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
-      ))
+  let inferredType = t' ^. typedType
+  when (t /= inferredType) (throw (ErrWrongType (WrongType { _wrongTypeExpression = e,
+                                                             _wrongTypeInferredType = inferredType,
+                                                             _wrongTypeExpectedType = t})))
   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 +95,15 @@ 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
+checkFunctionClause info clause@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 (TooManyPatterns {
+                                                                                _tooManyPatternsClause = clause,
+                                                                                _tooManyPatternsTypes = patTys})))
   locals <- mconcat <$> zipWithM checkPattern patTys _clausePatterns
   clauseBody' <- runReader locals (checkExpression bodyTy _clauseBody)
   return FunctionClause {
@@ -118,7 +111,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,17 +121,23 @@ 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
+    goConstr app@(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 (ErrWrongConstructorAppArgs (appErr app tys)))
       concat <$> zipWithM go tys ps
-
-throwErr :: Members '[Error Err] r => Err -> Sem r a
-throwErr = throw
+    appErr :: ConstructorApp -> [Type] -> WrongConstructorAppArgs
+    appErr app tys = WrongConstructorAppArgs { _wrongCtorAppApp = app,
+                                               _wrongCtorAppTypes = tys}
 
 -- TODO currently equivalent to id
 normalizeType :: forall r. Members '[Reader InfoTable] r => Type -> Sem r Type
@@ -158,7 +157,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
@@ -184,8 +183,9 @@ inferExpression' e = case e of
       return (TypedExpression (info ^. axiomInfoType) (ExpressionIden i))
   inferApplication :: Application -> Sem r TypedExpression
   inferApplication a = do
-    l <- inferExpression' (a ^. appLeft)
-    fun <- getFunctionType (l ^. typedType)
+    let leftExp = a ^. appLeft
+    l <- inferExpression' leftExp
+    fun <- getFunctionType leftExp (l ^. typedType)
     r <- checkExpression (fun ^. funLeft) (a ^. appRight)
     return TypedExpression {
       _typedExpression = ExpressionApplication Application {
@@ -194,7 +194,10 @@ inferExpression' e = case e of
           },
       _typedType = fun ^. funRight
       }
-  getFunctionType :: Type -> Sem r Function
-  getFunctionType t = case t of
-    TypeFunction f -> return f
-    _ -> throwErr ("expected function type " <> show t)
+    where
+      getFunctionType :: Expression -> Type -> Sem r Function
+      getFunctionType appExp t = case t of
+        TypeFunction f -> return f
+        _ -> throw (ErrExpectedFunctionType (ExpectedFunctionType { _expectedFunctionTypeExpression = e,
+                                                                    _expectedFunctionTypeApp = appExp,
+                                                                    _expectedFunctionTypeType = t}))

src/MiniJuvix/Translation/AbstractToMicroJuvix.hs

@@ -73,15 +73,19 @@ goFunction (A.Function l r) = Function (goFunctionParameter l) (goType r)
 goFunctionDef :: A.FunctionDef -> FunctionDef
 goFunctionDef f =
   FunctionDef
-    { _funDefName = goSymbol (f ^. A.funDefName),
+    { _funDefName = _funDefName',
       _funDefType = goType (f ^. A.funDefTypeSig),
-      _funDefClauses = fmap goFunctionClause (f ^. A.funDefClauses)
+      _funDefClauses = fmap (goFunctionClause _funDefName') (f ^. A.funDefClauses)
     }
+  where
+    _funDefName' :: Name
+    _funDefName' = goSymbol (f ^. A.funDefName)
 
-goFunctionClause :: A.FunctionClause -> FunctionClause
-goFunctionClause c =
+goFunctionClause :: Name -> A.FunctionClause -> FunctionClause
+goFunctionClause n c =
   FunctionClause
-    { _clausePatterns = map goPattern (c ^. A.clausePatterns),
+    { _clauseName = n,
+      _clausePatterns = map goPattern (c ^. A.clausePatterns),
       _clauseBody = goExpression (c ^. A.clauseBody)
     }
 

test/Base.hs

@@ -9,8 +9,10 @@ import Test.Tasty
 import Test.Tasty.HUnit
 import MiniJuvix.Prelude
 import qualified MiniJuvix.Syntax.Concrete.Language as M
+import qualified MiniJuvix.Syntax.Abstract.Language as A
 import qualified MiniJuvix.Syntax.Concrete.Parser as M
 import qualified MiniJuvix.Syntax.Concrete.Scoped.Scoper as M
+import qualified MiniJuvix.Translation.ScopedToAbstract as A
 
 parseModuleIO :: FilePath -> IO (M.Module 'M.Parsed 'M.ModuleTop)
 parseModuleIO = fromRightIO id . M.runModuleParserIO
@@ -21,6 +23,9 @@ parseTextModuleIO = fromRightIO id . return . M.runModuleParser "literal string"
 scopeModuleIO :: M.Module 'M.Parsed 'M.ModuleTop -> IO (M.Module 'M.Scoped 'M.ModuleTop)
 scopeModuleIO = fmap snd . fromRightIO' printErrorAnsi . M.scopeCheck1IO "."
 
+translateModuleIO :: M.Module 'M.Scoped 'M.ModuleTop -> IO A.TopModule
+translateModuleIO = fmap snd . fromRightIO id . return . A.translateModule
+
 data AssertionDescr =
   Single Assertion
   | Steps ((String -> IO ()) -> Assertion)

test/Main.hs

@@ -2,12 +2,14 @@ module Main (main) where
 
 import Base
 
+import qualified TypeCheck
 import qualified Scope
 
 negatives :: TestTree
 negatives = testGroup "MiniJuvix tests" $
   [
-  Scope.allTests
+  Scope.allTests,
+  TypeCheck.allTests
   ]
 
 allTests :: TestTree

test/TypeCheck.hs

@@ -0,0 +1,7 @@
+module TypeCheck (allTests) where
+
+import Base
+import qualified TypeCheck.Negative as N
+
+allTests :: TestTree
+allTests = testGroup "TypeCheck tests" [N.allTests]

test/TypeCheck/Negative.hs

@@ -0,0 +1,64 @@
+module TypeCheck.Negative (allTests) where
+
+import Base
+import MiniJuvix.Syntax.MicroJuvix.Error
+import qualified MiniJuvix.Syntax.MicroJuvix.TypeChecker as T
+import qualified MiniJuvix.Translation.AbstractToMicroJuvix as A
+
+type FailMsg = String
+
+data NegTest = NegTest
+  { name :: String,
+    relDir :: FilePath,
+    file :: FilePath,
+    checkErr :: TypeCheckerError -> Maybe FailMsg }
+
+testDescr :: NegTest -> TestDescr
+testDescr NegTest {..} = TestDescr {
+  testName = name,
+  testRoot = root </> relDir,
+  testAssertion = Single $ do
+      p <- parseModuleIO file
+           >>= scopeModuleIO
+           >>= translateModuleIO
+           >>| A.translateModule
+           >>| T.checkModule
+
+      case p of
+        Left err -> whenJust (checkErr err) assertFailure
+        Right _ -> assertFailure "The type checker did not find an error."
+  }
+
+allTests :: TestTree
+allTests = testGroup "TypeCheck negative tests"
+  (map (mkTest . testDescr) tests)
+
+root :: FilePath
+root = "tests/negative"
+
+wrongError :: Maybe FailMsg
+wrongError = Just "Incorrect error"
+
+tests :: [NegTest]
+tests = [
+  NegTest "Constructor in pattern type error" "MicroJuvix"
+    "PatternConstructor.mjuvix" $ \case
+      ErrWrongConstructorType {} -> Nothing
+      _ -> wrongError
+  , NegTest "Constructor pattern length mismatch" "MicroJuvix"
+    "PatternConstructorApp.mjuvix" $ \case
+      ErrWrongConstructorAppArgs {} -> Nothing
+      _ -> wrongError
+  , NegTest "Type vs inferred type mismatch" "MicroJuvix"
+    "WrongType.mjuvix" $ \case
+      ErrWrongType {} -> Nothing
+      _ -> wrongError
+  , NegTest "Function application with non-function type" "MicroJuvix"
+    "ExpectedFunctionType.mjuvix" $ \case
+      ErrExpectedFunctionType {} -> Nothing
+      _ -> wrongError
+  , NegTest "Function definition clause with two many match patterns" "MicroJuvix"
+    "TooManyPatterns.mjuvix" $ \case
+      ErrTooManyPatterns {} -> Nothing
+      _ -> wrongError
+        ]

tests/negative/MicroJuvix/ExpectedFunctionType.mjuvix

@@ -0,0 +1,12 @@
+module ExpectedFunctionType;
+  inductive A {
+    a : A;
+  };
+
+  inductive B {
+    b : B;
+  };
+
+  f : A;
+  f ≔ a b;
+end;

tests/negative/MicroJuvix/PatternConstructor.mjuvix

@@ -0,0 +1,13 @@
+module PatternConstructor;
+  inductive A {
+    a : A;
+  };
+
+  inductive B {
+    b : B;
+  };
+
+  f : A → B;
+  f b ≔ b;
+
+end;

tests/negative/MicroJuvix/PatternConstructorApp.mjuvix

@@ -0,0 +1,13 @@
+module PatternConstructorApp;
+  inductive A {
+    a : A -> A;
+  };
+
+  inductive B {
+    b : B;
+  };
+
+  f : A → B;
+  f (a x _) ≔ b;
+
+end;

tests/negative/MicroJuvix/TooManyPatterns.mjuvix

@@ -0,0 +1,8 @@
+module TooManyPatterns;
+  inductive A {
+    a : A;
+  };
+
+  f : A -> A;
+  f a _ ≔ a;
+end;

tests/negative/MicroJuvix/WrongType.mjuvix

@@ -0,0 +1,12 @@
+module WrongType;
+  inductive A {
+    a : A;
+  };
+
+  inductive B {
+    b : B;
+  };
+
+  f : A;
+  f ≔ b;
+end;