Fix: proper error handling for typechecker errors (#189)

* Fix: proper error handling for typechecker errors

* Improve error messages

src/MiniJuvix/Syntax/MicroJuvix/Error.hs

@@ -18,6 +18,9 @@ data TypeCheckerError
   | ErrWrongType WrongType
   | ErrUnsolvedMeta UnsolvedMeta
   | ErrExpectedFunctionType ExpectedFunctionType
+  | ErrTooManyArgumentsIndType WrongNumberArgumentsIndType
+  | ErrTooFewArgumentsIndType WrongNumberArgumentsIndType
+  | ErrImpracticalPatternMatching ImpracticalPatternMatching
 
 instance ToGenericError TypeCheckerError where
   genericError :: TypeCheckerError -> GenericError
@@ -28,3 +31,6 @@ instance ToGenericError TypeCheckerError where
     ErrWrongType e -> genericError e
     ErrUnsolvedMeta e -> genericError e
     ErrExpectedFunctionType e -> genericError e
+    ErrTooManyArgumentsIndType e -> genericError e
+    ErrTooFewArgumentsIndType e -> genericError e
+    ErrImpracticalPatternMatching e -> genericError e

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

@@ -25,15 +25,18 @@ instance ToGenericError WrongConstructorType where
         _genericErrorIntervals = [i]
       }
     where
-      i = getLoc (e ^. wrongCtorTypeName)
+      ctorName = e ^. wrongCtorTypeName
+      i = getLoc ctorName
       msg =
-        "The constructor" <+> ppCode (e ^. wrongCtorTypeName) <+> "has type:"
-          <> line
-          <> indent' (ppCode (e ^. wrongCtorTypeActual))
-          <> line
-          <> "but is expected to have type:"
-          <> line
-          <> indent' (ppCode (e ^. wrongCtorTypeExpected))
+        "The constructor"
+          <+> ppCode ctorName
+          <+> "has type:"
+            <> line
+            <> indent' (ppCode (e ^. wrongCtorTypeActual))
+            <> line
+            <> "but is expected to have type:"
+            <> line
+            <> indent' (ppCode (e ^. wrongCtorTypeExpected))
 
 data WrongReturnType = WrongReturnType
   { _wrongReturnTypeConstructorName :: Name,
@@ -53,15 +56,18 @@ instance ToGenericError WrongReturnType where
     where
       ctorName = e ^. wrongReturnTypeConstructorName
       i = getLoc ctorName
-      j = getLoc (typeAsExpression (e ^. wrongReturnTypeActual))
+      ty = e ^. wrongReturnTypeActual
+      j = getLoc (typeAsExpression ty)
       msg =
-        "The constructor" <+> ppCode ctorName <+> "has the wrong return type:"
-          <> line
-          <> indent' (ppCode (e ^. wrongReturnTypeActual))
-          <> line
-          <> "but is expected to have type:"
-          <> line
-          <> indent' (ppCode (e ^. wrongReturnTypeExpected))
+        "The constructor"
+          <+> ppCode ctorName
+          <+> "has the wrong return type:"
+            <> line
+            <> indent' (ppCode ty)
+            <> line
+            <> "but is expected to have type:"
+            <> line
+            <> indent' (ppCode (e ^. wrongReturnTypeExpected))
 
 newtype UnsolvedMeta = UnsolvedMeta
   { _unsolvedMeta :: Hole
@@ -101,14 +107,19 @@ instance ToGenericError WrongConstructorAppArgs where
     where
       i = getLoc (e ^. wrongCtorAppApp . constrAppConstructor)
       msg =
-        "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))))
+        "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))))
       numPats :: Doc ann
       numPats = pat (length (e ^. wrongCtorAppApp . constrAppParameters))
       numTypes :: Doc ann
@@ -116,6 +127,7 @@ instance ToGenericError WrongConstructorAppArgs where
 
       ctorName :: Doc Eann
       ctorName = ppCode (e ^. wrongCtorAppApp . constrAppConstructor)
+
       pat :: Int -> Doc ann
       pat n = pretty n <+> plural "pattern" "patterns" n
 
@@ -138,15 +150,19 @@ instance ToGenericError WrongType where
     where
       i = getLoc (e ^. wrongTypeExpression)
       msg =
-        "Type error near" <+> pretty (getLoc subjectExpr) <> "."
-          <> line
-          <> "The expression" <+> ppCode subjectExpr <+> "has type:"
-          <> line
-          <> indent' (ppCode (e ^. wrongTypeInferredType))
-          <> line
-          <> "but is expected to have type:"
-          <> line
-          <> indent' (ppCode (e ^. wrongTypeExpectedType))
+        "Type error near"
+          <+> pretty (getLoc subjectExpr)
+            <> "."
+            <> line
+            <> "The expression"
+          <+> ppCode subjectExpr
+          <+> "has type:"
+            <> line
+            <> indent' (ppCode (e ^. wrongTypeInferredType))
+            <> line
+            <> "but is expected to have type:"
+            <> line
+            <> indent' (ppCode (e ^. wrongTypeExpectedType))
 
       subjectExpr :: Expression
       subjectExpr = e ^. wrongTypeExpression
@@ -171,14 +187,77 @@ instance ToGenericError ExpectedFunctionType where
     where
       i = getLoc (e ^. expectedFunctionTypeExpression)
       msg =
-        "Type error near" <+> pretty (getLoc subjectExpr) <> "."
-          <> line
-          <> "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))
+        "Type error near"
+          <+> pretty (getLoc subjectExpr)
+            <> "."
+            <> line
+            <> "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))
       subjectExpr :: Expression
       subjectExpr = e ^. expectedFunctionTypeExpression
+
+data WrongNumberArgumentsIndType = WrongNumberArgumentsIndType
+  { _wrongNumberArgumentsIndTypeActualType :: Type,
+    _wrongNumberArgumentsIndTypeExpectedNumArgs :: Int,
+    _wrongNumberArgumentsIndTypeActualNumArgs :: Int
+  }
+
+makeLenses ''WrongNumberArgumentsIndType
+
+instance ToGenericError WrongNumberArgumentsIndType where
+  genericError e =
+    GenericError
+      { _genericErrorLoc = i,
+        _genericErrorMessage = prettyError msg,
+        _genericErrorIntervals = [i]
+      }
+    where
+      ty = e ^. wrongNumberArgumentsIndTypeActualType
+      i = getLoc (typeAsExpression ty)
+      expectedNumArgs = e ^. wrongNumberArgumentsIndTypeExpectedNumArgs
+      actualNumArgs = e ^. wrongNumberArgumentsIndTypeActualNumArgs
+      msg =
+        "The type"
+          <+> pretty (getTypeName ty)
+          <+> "expects"
+          <+> ( if
+                    | expectedNumArgs == 0 -> "no arguments"
+                    | expectedNumArgs == 1 -> "one argument"
+                    | otherwise -> pretty expectedNumArgs <+> "arguments"
+              )
+          <> ", but"
+          <+> ( if
+                    | actualNumArgs == 0 -> "no argument is"
+                    | actualNumArgs == 1 -> "only one argument is"
+                    | otherwise -> pretty actualNumArgs <+> "arguments are"
+              )
+          <+> "given"
+
+newtype ImpracticalPatternMatching = ImpracticalPatternMatching
+  { _impracticalPatternMatchingType :: Type
+  }
+
+makeLenses ''ImpracticalPatternMatching
+
+instance ToGenericError ImpracticalPatternMatching where
+  genericError e =
+    GenericError
+      { _genericErrorLoc = i,
+        _genericErrorMessage = prettyError msg,
+        _genericErrorIntervals = [i]
+      }
+    where
+      ty = e ^. impracticalPatternMatchingType
+      i = getLoc (typeAsExpression ty)
+      msg =
+        "The type"
+          <+> ppCode ty
+          <+> "is not an inductive data type."
+          <+> "Therefore, pattern-matching is not available here"

src/MiniJuvix/Syntax/MicroJuvix/Language/Extra.hs

@@ -429,11 +429,11 @@ unfoldApplication = fmap (fmap snd) . unfoldApplication'
 
 unfoldTypeApplication :: TypeApplication -> (Type, NonEmpty Type)
 unfoldTypeApplication (TypeApplication l' r' _) = second (|: r') (unfoldType l')
-  where
-    unfoldType :: Type -> (Type, [Type])
-    unfoldType t = case t of
-      TypeApp (TypeApplication l r _) -> second (`snoc` r) (unfoldType l)
-      _ -> (t, [])
+
+unfoldType :: Type -> (Type, [Type])
+unfoldType = \case
+  TypeApp (TypeApplication l r _) -> second (`snoc` r) (unfoldType l)
+  t -> (t, [])
 
 foldTypeApp :: Type -> [Type] -> Type
 foldTypeApp ty = \case
@@ -445,3 +445,9 @@ foldTypeAppName tyName indParams =
   foldTypeApp
     (TypeIden (TypeIdenInductive tyName))
     (map (TypeIden . TypeIdenVariable) indParams)
+
+getTypeName :: Type -> Maybe Name
+getTypeName = \case
+  (TypeIden (TypeIdenInductive tyName)) -> Just tyName
+  (TypeApp (TypeApplication l _ _)) -> getTypeName l
+  _ -> Nothing

src/MiniJuvix/Syntax/MicroJuvix/TypeChecker.hs

@@ -237,15 +237,37 @@ checkPattern funName = go
                 )
             )
     checkSaturatedInductive :: Type -> Sem r (InductiveName, [(InductiveParameter, Type)])
-    checkSaturatedInductive t = do
-      (ind, args) <- viewInductiveApp t
+    checkSaturatedInductive ty = do
+      (ind, args) <- viewInductiveApp ty
       params <-
         (^. inductiveInfoDef . inductiveParameters)
           <$> lookupInductive ind
       let numArgs = length args
           numParams = length params
-      when (numArgs < numParams) (error "unsaturated inductive type")
-      when (numArgs > numParams) (error "too many arguments to inductive type")
+      when
+        (numArgs < numParams)
+        ( throw
+            ( ErrTooFewArgumentsIndType
+                ( WrongNumberArgumentsIndType
+                    { _wrongNumberArgumentsIndTypeActualType = ty,
+                      _wrongNumberArgumentsIndTypeActualNumArgs = numArgs,
+                      _wrongNumberArgumentsIndTypeExpectedNumArgs = numParams
+                    }
+                )
+            )
+        )
+      when
+        (numArgs > numParams)
+        ( throw
+            ( ErrTooManyArgumentsIndType
+                ( WrongNumberArgumentsIndType
+                    { _wrongNumberArgumentsIndTypeActualType = ty,
+                      _wrongNumberArgumentsIndTypeActualNumArgs = numArgs,
+                      _wrongNumberArgumentsIndTypeExpectedNumArgs = numParams
+                    }
+                )
+            )
+        )
       return (ind, zip params args)
 
 freshHole :: Members '[Inference, NameIdGen] r => Interval -> Sem r Hole
@@ -393,7 +415,7 @@ viewInductiveApp ::
   Sem r (InductiveName, [Type])
 viewInductiveApp ty = case t of
   TypeIden (TypeIdenInductive n) -> return (n, as)
-  _ -> throw @TypeCheckerError (error "only inductive types can be pattern matched")
+  _ -> throw (ErrImpracticalPatternMatching (ImpracticalPatternMatching ty))
   where
     (t, as) = viewTypeApp ty
 

src/MiniJuvix/Translation/AbstractToMicroJuvix.hs

@@ -278,11 +278,11 @@ goInductiveDef i = case i ^. Abstract.inductiveType of
   Just {} -> unsupported "inductive indices"
   _ -> helper
   where
-    indTypeName = i ^. Abstract.inductiveName
     helper = do
       inductiveParameters' <- mapM goInductiveParameter (i ^. Abstract.inductiveParameters)
-      let indTy :: Type = foldTypeAppName indTypeName (map (^. inductiveParamName) inductiveParameters')
-      inductiveConstructors' <- mapM (goConstructorDef indTy) (i ^. Abstract.inductiveConstructors)
+      let indTypeName = i ^. Abstract.inductiveName
+          indParamNames = map (^. inductiveParamName) inductiveParameters'
+      inductiveConstructors' <- mapM (goConstructorDef indTypeName indParamNames) (i ^. Abstract.inductiveConstructors)
       return
         InductiveDef
           { _inductiveName = indTypeName,
@@ -290,10 +290,16 @@ goInductiveDef i = case i ^. Abstract.inductiveType of
             _inductiveConstructors = inductiveConstructors'
           }
       where
-        goConstructorDef :: Type -> Abstract.InductiveConstructorDef -> Sem r InductiveConstructorDef
-        goConstructorDef expectedReturnType c = do
+        goConstructorDef :: Name -> [Name] -> Abstract.InductiveConstructorDef -> Sem r InductiveConstructorDef
+        goConstructorDef expectedTypeName expectedNameParms c = do
           (_constructorParameters', actualReturnType) <- viewConstructorType (c ^. Abstract.constructorType)
           let ctorName = c ^. Abstract.constructorName
+              expectedReturnType :: Type
+              expectedReturnType = foldTypeAppName expectedTypeName expectedNameParms
+              expectedNumArgs = length expectedNameParms
+              (_, actualReturnTypeParams) = unfoldType actualReturnType
+              actualNumArgs = length actualReturnTypeParams
+              sameTypeName = Just expectedTypeName == getTypeName actualReturnType
           if
               | actualReturnType == expectedReturnType ->
                   return
@@ -301,10 +307,37 @@ goInductiveDef i = case i ^. Abstract.inductiveType of
                       { _constructorName = ctorName,
                         _constructorParameters = _constructorParameters'
                       }
+              | sameTypeName,
+                actualNumArgs < expectedNumArgs ->
+                  throw
+                    ( ErrTooFewArgumentsIndType
+                        ( WrongNumberArgumentsIndType
+                            { _wrongNumberArgumentsIndTypeActualType = actualReturnType,
+                              _wrongNumberArgumentsIndTypeActualNumArgs = actualNumArgs,
+                              _wrongNumberArgumentsIndTypeExpectedNumArgs = expectedNumArgs
+                            }
+                        )
+                    )
+              | sameTypeName,
+                actualNumArgs > expectedNumArgs ->
+                  throw
+                    ( ErrTooManyArgumentsIndType
+                        ( WrongNumberArgumentsIndType
+                            { _wrongNumberArgumentsIndTypeActualType = actualReturnType,
+                              _wrongNumberArgumentsIndTypeActualNumArgs = actualNumArgs,
+                              _wrongNumberArgumentsIndTypeExpectedNumArgs = expectedNumArgs
+                            }
+                        )
+                    )
               | otherwise ->
                   throw
                     ( ErrWrongReturnType
-                        (WrongReturnType ctorName expectedReturnType actualReturnType)
+                        ( WrongReturnType
+                            { _wrongReturnTypeConstructorName = ctorName,
+                              _wrongReturnTypeExpected = expectedReturnType,
+                              _wrongReturnTypeActual = actualReturnType
+                            }
+                        )
                     )
 
 goTypeApplication :: Abstract.Application -> Sem r TypeApplication

test/TypeCheck/Negative.hs

@@ -85,10 +85,17 @@ tests =
         ErrWrongReturnType {} -> Nothing
         _ -> wrongError,
     NegTest
-      "Wrong return type for a constructor of a data type with parameters "
+      "Too few arguments for the return type of a constructor"
       "MicroJuvix"
-      "WrongReturnTypeParameters.mjuvix"
+      "WrongReturnTypeTooFewArguments.mjuvix"
       $ \case
-        ErrWrongReturnType {} -> Nothing
+        ErrTooFewArgumentsIndType {} -> Nothing
+        _ -> wrongError,
+    NegTest
+      "Too many arguments for the return type of a constructor"
+      "MicroJuvix"
+      "WrongReturnTypeTooManyArguments.mjuvix"
+      $ \case
+        ErrTooManyArgumentsIndType {} -> Nothing
         _ -> wrongError
   ]

tests/negative/MicroJuvix/WrongReturnTypeParameters.mjuvix

@@ -1,7 +1,7 @@
 module WrongReturnTypeParameters;
 
 inductive A (B : Type) {
-c : A;
+c : A B B;
 };
 
 end;

tests/negative/MicroJuvix/WrongReturnTypeTooFewArguments.mjuvix

@@ -0,0 +1,7 @@
+module WrongReturnTypeTooFewArguments;
+
+inductive A (B : Type) {
+c : A;
+};
+
+end;

tests/negative/MicroJuvix/WrongReturnTypeTooManyArguments.mjuvix

@@ -0,0 +1,7 @@
+module WrongReturnTypeTooManyArguments;
+
+inductive A (B : Type) {
+c : A B B;
+};
+
+end;