Fix: Add check for constructor return types (#182)

* Checking indtype declar (return type)

* Add missing semicolon

* Fix typo

src/MiniJuvix/Pipeline.hs

@@ -113,7 +113,7 @@ pipelineMicroJuvix ::
   Members '[Error MiniJuvixError] r =>
   Abstract.AbstractResult ->
   Sem r MicroJuvix.MicroJuvixResult
-pipelineMicroJuvix = mapError (MiniJuvixError @MicroJuvix.TerminationError) . MicroJuvix.entryMicroJuvix
+pipelineMicroJuvix = MicroJuvix.entryMicroJuvix
 
 pipelineMicroJuvixArity ::
   Members '[Error MiniJuvixError, NameIdGen] r =>

src/MiniJuvix/Syntax/MicroJuvix/Error.hs

@@ -13,6 +13,7 @@ import MiniJuvix.Syntax.MicroJuvix.Error.Types
 
 data TypeCheckerError
   = ErrWrongConstructorType WrongConstructorType
+  | ErrWrongReturnType WrongReturnType
   | ErrArity ArityCheckerError
   | ErrWrongType WrongType
   | ErrUnsolvedMeta UnsolvedMeta
@@ -22,6 +23,7 @@ instance ToGenericError TypeCheckerError where
   genericError :: TypeCheckerError -> GenericError
   genericError = \case
     ErrWrongConstructorType e -> genericError e
+    ErrWrongReturnType e -> genericError e
     ErrArity e -> genericError e
     ErrWrongType e -> genericError e
     ErrUnsolvedMeta e -> genericError e

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

@@ -4,6 +4,7 @@ import MiniJuvix.Prelude
 import MiniJuvix.Prelude.Pretty
 import MiniJuvix.Syntax.MicroJuvix.Error.Pretty
 import MiniJuvix.Syntax.MicroJuvix.Language
+import MiniJuvix.Syntax.MicroJuvix.Language.Extra
 
 -- | the type of the constructor used in a pattern does
 -- not match the type of the inductive being matched
@@ -34,6 +35,34 @@ instance ToGenericError WrongConstructorType where
           <> line
           <> indent' (ppCode (e ^. wrongCtorTypeExpected))
 
+data WrongReturnType = WrongReturnType
+  { _wrongReturnTypeConstructorName :: Name,
+    _wrongReturnTypeExpected :: Type,
+    _wrongReturnTypeActual :: Type
+  }
+
+makeLenses ''WrongReturnType
+
+instance ToGenericError WrongReturnType where
+  genericError e =
+    GenericError
+      { _genericErrorLoc = j,
+        _genericErrorMessage = prettyError msg,
+        _genericErrorIntervals = [i, j]
+      }
+    where
+      ctorName = e ^. wrongReturnTypeConstructorName
+      i = getLoc ctorName
+      j = getLoc (typeAsExpression (e ^. wrongReturnTypeActual))
+      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))
+
 newtype UnsolvedMeta = UnsolvedMeta
   { _unsolvedMeta :: Hole
   }

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

@@ -411,7 +411,7 @@ foldExplicitApplication :: Expression -> [Expression] -> Expression
 foldExplicitApplication f = foldApplication f . zip (repeat Explicit)
 
 foldApplication :: Expression -> [(IsImplicit, Expression)] -> Expression
-foldApplication f args = case args of
+foldApplication f = \case
   [] -> f
   ((i, a) : as) -> foldApplication (ExpressionApplication (Application f a i)) as
 
@@ -434,3 +434,14 @@ unfoldTypeApplication (TypeApplication l' r' _) = second (|: r') (unfoldType l')
     unfoldType t = case t of
       TypeApp (TypeApplication l r _) -> second (`snoc` r) (unfoldType l)
       _ -> (t, [])
+
+foldTypeApp :: Type -> [Type] -> Type
+foldTypeApp ty = \case
+  [] -> ty
+  (p : ps) -> foldTypeApp (TypeApp (TypeApplication ty p Explicit)) ps
+
+foldTypeAppName :: Name -> [Name] -> Type
+foldTypeAppName tyName indParams =
+  foldTypeApp
+    (TypeIden (TypeIdenInductive tyName))
+    (map (TypeIden . TypeIdenVariable) indParams)

src/MiniJuvix/Translation/AbstractToMicroJuvix.hs

@@ -10,7 +10,9 @@ import MiniJuvix.Pipeline.EntryPoint qualified as E
 import MiniJuvix.Prelude
 import MiniJuvix.Syntax.Abstract.AbstractResult qualified as Abstract
 import MiniJuvix.Syntax.Abstract.Language qualified as Abstract
+import MiniJuvix.Syntax.MicroJuvix.Error
 import MiniJuvix.Syntax.MicroJuvix.Language
+import MiniJuvix.Syntax.MicroJuvix.Language.Extra
 import MiniJuvix.Syntax.MicroJuvix.MicroJuvixResult
 import MiniJuvix.Syntax.Universe
 import MiniJuvix.Syntax.Usage
@@ -30,15 +32,23 @@ iniState =
 makeLenses ''TranslationState
 
 entryMicroJuvix ::
-  Members '[Error TerminationError] r =>
+  Members '[Error MiniJuvixError] r =>
   Abstract.AbstractResult ->
   Sem r MicroJuvixResult
 entryMicroJuvix abstractResults = do
-  unless noTerminationOption (checkTermination topModule infoTable)
+  unless
+    noTerminationOption
+    ( mapError
+        (MiniJuvixError @TerminationError)
+        (checkTermination topModule infoTable)
+    )
   _resultModules' <-
     evalState
       iniState
-      (mapM goModule (abstractResults ^. Abstract.resultModules))
+      ( mapM
+          (mapError (MiniJuvixError @TypeCheckerError) . goModule)
+          (abstractResults ^. Abstract.resultModules)
+      )
   return
     MicroJuvixResult
       { _resultAbstract = abstractResults,
@@ -49,10 +59,11 @@ entryMicroJuvix abstractResults = do
     infoTable = abstractResults ^. Abstract.resultTable
     noTerminationOption =
       abstractResults
-        ^. Abstract.abstractResultEntryPoint . E.entryPointNoTermination
+        ^. Abstract.abstractResultEntryPoint
+          . E.entryPointNoTermination
 
 goModule ::
-  Member (State TranslationState) r =>
+  Members '[State TranslationState, Error TypeCheckerError] r =>
   Abstract.TopModule ->
   Sem r Module
 goModule m = do
@@ -66,10 +77,10 @@ goModule m = do
 unsupported :: Text -> a
 unsupported thing = error ("Abstract to MicroJuvix: Not yet supported: " <> thing)
 
-goModuleBody :: Member (State TranslationState) r => Abstract.ModuleBody -> Sem r ModuleBody
+goModuleBody :: Members '[State TranslationState, Error TypeCheckerError] r => Abstract.ModuleBody -> Sem r ModuleBody
 goModuleBody b = ModuleBody <$> mapMaybeM goStatement (b ^. Abstract.moduleStatements)
 
-goImport :: Member (State TranslationState) r => Abstract.TopModule -> Sem r (Maybe Include)
+goImport :: Members '[State TranslationState, Error TypeCheckerError] r => Abstract.TopModule -> Sem r (Maybe Include)
 goImport m = do
   inc <- gets (HashSet.member (m ^. Abstract.moduleName) . (^. translationStateIncluded))
   if
@@ -85,7 +96,7 @@ goImport m = do
             )
 
 goStatement ::
-  Member (State TranslationState) r =>
+  Members [State TranslationState, Error TypeCheckerError] r =>
   Abstract.Statement ->
   Sem r (Maybe Statement)
 goStatement = \case
@@ -97,7 +108,7 @@ goStatement = \case
   Abstract.StatementInductive i -> Just . StatementInductive <$> goInductiveDef i
 
 goTypeIden :: Abstract.Iden -> TypeIden
-goTypeIden i = case i of
+goTypeIden = \case
   Abstract.IdenFunction {} -> unsupported "functions in types"
   Abstract.IdenConstructor {} -> unsupported "constructors in types"
   Abstract.IdenVar v -> TypeIdenVariable v
@@ -254,31 +265,47 @@ goInductiveParameter f =
     (Just {}, _, _) -> unsupported "only type variables of small types are allowed"
     (Nothing, _, _) -> unsupported "unnamed inductive parameters"
 
-goInductiveDef :: forall r. Abstract.InductiveDef -> Sem r InductiveDef
+goConstructorType :: Abstract.Expression -> Sem r [Type]
+goConstructorType = fmap fst . viewConstructorType
+
+goInductiveDef ::
+  forall r.
+  Members '[Error TypeCheckerError] r =>
+  Abstract.InductiveDef ->
+  Sem r InductiveDef
 goInductiveDef i = case i ^. Abstract.inductiveType of
+  Just Abstract.ExpressionUniverse {} -> helper
   Just {} -> unsupported "inductive indices"
-  _ -> do
+  _ -> helper
-    _inductiveParameters' <- mapM goInductiveParameter (i ^. Abstract.inductiveParameters)
-    _inductiveConstructors' <- mapM goConstructorDef (i ^. Abstract.inductiveConstructors)
-    return
-      InductiveDef
-        { _inductiveName = indName,
-          _inductiveParameters = _inductiveParameters',
-          _inductiveConstructors = _inductiveConstructors'
-        }
   where
-    indName = i ^. Abstract.inductiveName
+    indTypeName = i ^. Abstract.inductiveName
-    goConstructorDef :: Abstract.InductiveConstructorDef -> Sem r InductiveConstructorDef
+    helper = do
-    goConstructorDef c = do
+      inductiveParameters' <- mapM goInductiveParameter (i ^. Abstract.inductiveParameters)
-      _constructorParameters' <- goConstructorType (c ^. Abstract.constructorType)
+      let indTy :: Type = foldTypeAppName indTypeName (map (^. inductiveParamName) inductiveParameters')
+      inductiveConstructors' <- mapM (goConstructorDef indTy) (i ^. Abstract.inductiveConstructors)
       return
-        InductiveConstructorDef
+        InductiveDef
-          { _constructorName = c ^. Abstract.constructorName,
+          { _inductiveName = indTypeName,
-            _constructorParameters = _constructorParameters'
+            _inductiveParameters = inductiveParameters',
+            _inductiveConstructors = inductiveConstructors'
           }
-    -- TODO check that the return type corresponds with the inductive type
+      where
-    goConstructorType :: Abstract.Expression -> Sem r [Type]
+        goConstructorDef :: Type -> Abstract.InductiveConstructorDef -> Sem r InductiveConstructorDef
-    goConstructorType = fmap fst . viewConstructorType
+        goConstructorDef expectedReturnType c = do
+          (_constructorParameters', actualReturnType) <- viewConstructorType (c ^. Abstract.constructorType)
+          let ctorName = c ^. Abstract.constructorName
+          if
+              | actualReturnType == expectedReturnType ->
+                  return
+                    InductiveConstructorDef
+                      { _constructorName = ctorName,
+                        _constructorParameters = _constructorParameters'
+                      }
+              | otherwise ->
+                  throw
+                    ( ErrWrongReturnType
+                        (WrongReturnType ctorName expectedReturnType actualReturnType)
+                    )
 
 goTypeApplication :: Abstract.Application -> Sem r TypeApplication
 goTypeApplication (Abstract.Application l r i) = do
@@ -292,7 +319,7 @@ goTypeApplication (Abstract.Application l r i) = do
       }
 
 viewConstructorType :: Abstract.Expression -> Sem r ([Type], Type)
-viewConstructorType e = case e of
+viewConstructorType = \case
   Abstract.ExpressionFunction f -> first toList <$> viewFunctionType f
   Abstract.ExpressionIden i -> return ([], TypeIden (goTypeIden i))
   Abstract.ExpressionHole {} -> unsupported "holes in constructor type"

test/TypeCheck/Negative.hs

@@ -76,5 +76,19 @@ tests =
       "MultiWrongType.mjuvix"
       $ \case
         ErrWrongType {} -> Nothing
+        _ -> wrongError,
+    NegTest
+      "Wrong return type name for a constructor of a simple data type"
+      "MicroJuvix"
+      "WrongReturnType.mjuvix"
+      $ \case
+        ErrWrongReturnType {} -> Nothing
+        _ -> wrongError,
+    NegTest
+      "Wrong return type for a constructor of a data type with parameters "
+      "MicroJuvix"
+      "WrongReturnTypeParameters.mjuvix"
+      $ \case
+        ErrWrongReturnType {} -> Nothing
         _ -> wrongError
   ]

tests/negative/MicroJuvix/FunctionApplied.mjuvix

@@ -1,6 +1,6 @@
 module FunctionApplied;
   inductive T (A : Type) {
-    c : A → T;
+    c : A → T A;
   };
 
   f : {A : Type} → A → T A;

tests/negative/MicroJuvix/WrongReturnType.mjuvix

@@ -0,0 +1,8 @@
+module WrongReturnType;
+
+axiom B : Type;
+inductive A {
+c : B;
+};
+
+end;

tests/negative/MicroJuvix/WrongReturnTypeParameters.mjuvix

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

tests/positive/Polymorphism.mjuvix

@@ -11,8 +11,7 @@ inductive Nat {
 
 inductive List (A : Type) {
  nil : List A;
- -- TODO check that the return type is saturated with the proper variable
+ cons : A → List A → List A;
- cons : A → List A → Nat;
 };
 
 inductive Bool {

tests/positive/PolymorphismHoles.mjuvix

@@ -11,8 +11,7 @@ inductive Nat {
 
 inductive List (A : Type) {
  nil : List A;
- -- TODO check that the return type is saturated with the proper variable
+ cons : A → List A → List A;
- cons : A → List A → Nat;
 };
 
 inductive Bool {