Add positivity check for inductive types (#1393)

* w.i.p

* Added strict positivity condition for datatypes w.i.p

* Add negative test for str.postivity check

* Add some revisions

* the branch is back to feet

* w.i.p add lots of traces to check alg.

* Add more test and revisions

* Add negative and positive test to the new flag and the keyword

* Fix shell tests.

* Make pre-commit happy

* Fix rebase conflicts

* Make pre-commit happy

* Add shell test, rename keyword, fix error msg

* Revert change

* Necessary changes

* Remove wrong unless

* Move the positivity checker to its own folder

* Add missing juvix.yaml

* Add a negative test thanks to jan

* make some style changes

* Make ormolu happy

* Remove unnecessary instance of Show

Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>

app/GlobalOptions.hs

@@ -12,6 +12,7 @@ data GlobalOptions = GlobalOptions
     _globalShowNameIds :: Bool,
     _globalOnlyErrors :: Bool,
     _globalNoTermination :: Bool,
+    _globalNoPositivity :: Bool,
     _globalNoStdlib :: Bool,
     _globalInputFiles :: [FilePath]
   }
@@ -26,6 +27,7 @@ defaultGlobalOptions =
       _globalShowNameIds = False,
       _globalOnlyErrors = False,
       _globalNoTermination = False,
+      _globalNoPositivity = False,
       _globalNoStdlib = False,
       _globalInputFiles = []
     }
@@ -37,6 +39,7 @@ instance Semigroup GlobalOptions where
         _globalShowNameIds = o1 ^. globalShowNameIds || o2 ^. globalShowNameIds,
         _globalOnlyErrors = o1 ^. globalOnlyErrors || o2 ^. globalOnlyErrors,
         _globalNoTermination = o1 ^. globalNoTermination || o2 ^. globalNoTermination,
+        _globalNoPositivity = o1 ^. globalNoPositivity || o2 ^. globalNoPositivity,
         _globalNoStdlib = o1 ^. globalNoStdlib || o2 ^. globalNoStdlib,
         _globalInputFiles = o1 ^. globalInputFiles ++ o2 ^. globalInputFiles
       }
@@ -73,6 +76,12 @@ parseGlobalFlags b = do
           <> help "Disable termination checking"
           <> hidden b
       )
+  _globalNoPositivity <-
+    switch
+      ( long "no-positivity"
+          <> help "Disable positivity checking for inductive types"
+          <> hidden b
+      )
   _globalNoStdlib <-
     switch
       ( long "no-stdlib"

app/Main.hs

@@ -73,6 +73,7 @@ getEntryPoint r opts = nonEmpty (opts ^. globalInputFiles) >>= Just <$> entryPoi
       EntryPoint
         { _entryPointRoot = r,
           _entryPointNoTermination = opts ^. globalNoTermination,
+          _entryPointNoPositivity = opts ^. globalNoPositivity,
           _entryPointNoStdlib = opts ^. globalNoStdlib,
           _entryPointModulePaths = l
         }

docs/org/SUMMARY.org

@@ -34,6 +34,7 @@
 - [[./notes/README.md][Notes]]
   - [[./examples/validity-predicates/README.md][Validity predicates]]
   - [[./notes/monomorphization.md][Monomorphization]]
+  - [[./notes/strictly-positive-data-types.md][Strictly positive data types]]
 
 - [[./introduction/about/what-is.md][About]]
   # - [[./introduction/about/team.md][The dev team]]

docs/org/notes/strictly-positive-data-types.org

@@ -0,0 +1,86 @@
+* Strictly positive data types
+
+We follow a syntactic description of strictly positive inductive data types.
+
+An inductive type is said to be _strictly positive_ if it does not occur or occurs
+strictly positively in the types of the arguments of its constructors. A name
+qualified as strictly positive for an inductive type if it never occurs at a negative
+position in the types of the arguments of its constructors. We refer to a negative
+position as those occurrences on the left of an arrow in a type constructor argument.
+
+In the example below, the type =X= occurs strictly positive in =c0= and negatively at
+the constructor =c1=. Therefore, =X= is not strictly positive.
+
+#+begin_src minijuvix
+axiom B : Type;
+inductive X {
+  c0 : (B -> X) -> X;
+  c1 : (X -> X) -> X;
+};
+#+end_src
+
+We could also refer to positive parameters as such parameters occurring in no negative positions.
+For example, the type =B= in the =c0= constructor above is on the left of the arrow =B->X=.
+Then, =B= is at a negative position. Negative parameters need to be considered when checking strictly
+positive data types as they may allow to define non-strictly positive data types.
+
+In the example below, the type =T0= is strictly positive. However, the type =T1= is not.
+Only after unfolding the type application =T0 (T1 A)= in the data constructor =c1=, we can
+find out that =T1= occurs at a negative position because of =T0=. More precisely,
+the type parameter =A= of =T0= is negative.
+
+#+begin_src minijuvix
+inductive T0 (A : Type) {
+  c0 : (A -> T0 A) -> T0 A;
+};
+
+inductive T1 {
+  c1 : T0 T1 -> T1;
+};
+#+end_src
+
+
+** Bypass the strict positivity condition
+
+To bypass the positivity check, a data type declaration can be annotated
+with the keyword =positive=. Another way is to use the CLI global flag =--no-positivity=
+when typechecking a =Juvix= File.
+
+#+begin_example
+$ cat tests/negative/MicroJuvix/NoStrictlyPositiveDataTypes/E5.mjuvix
+module E5;
+  positive
+  inductive T0 (A : Type){
+    c0 : (T0 A -> A) -> T0 A;
+  };
+end;
+#+end_example
+
+** Examples of non-strictly data types
+
+- =NSPos= is at a negative position in =c=.
+  #+begin_src minijuvix
+  inductive Empty {};
+  inductive NSPos {
+    c : ((NSPos -> Empty) -> NSPos) -> NSPos;
+  };
+  #+end_src
+
+- =Bad= is not strictly positive beceause of the negative parameter =A= of =Tree=.
+  #+begin_src minijuvix
+  inductive Tree (A : Type) {
+    leaf : Tree A;
+    node : (A -> Tree A) -> Tree A;
+  };
+
+  inductive Bad {
+    bad : Tree Bad -> Bad;
+  };
+  #+end_src
+
+- =A= is a negative parameter.
+  #+begin_src minijuvix
+  inductive B (A : Type) {
+    b : (A -> B (B A -> A)) -> B A;
+  };
+  #+end_src

src/Juvix/Analysis/Positivity/Checker.hs

@@ -0,0 +1,140 @@
+module Juvix.Analysis.Positivity.Checker where
+
+import Data.HashMap.Strict qualified as HashMap
+import Data.HashSet qualified as HashSet
+import Juvix.Pipeline.EntryPoint qualified as E
+import Juvix.Prelude hiding (fromEither)
+import Juvix.Syntax.MicroJuvix.Error
+import Juvix.Syntax.MicroJuvix.InfoTable
+import Juvix.Syntax.MicroJuvix.Language.Extra
+
+-------------------------------------------------------------------------------
+-- Checker for strictly positive inductive data types
+-------------------------------------------------------------------------------
+
+type NegativeTypeParameters = HashSet VarName
+
+type ErrorReference = Maybe Expression
+
+type RecursionLimit = Int
+
+checkPositivity ::
+  Members
+    '[ Reader E.EntryPoint,
+       Reader InfoTable,
+       Error TypeCheckerError,
+       State NegativeTypeParameters
+     ]
+    r =>
+  InductiveDef ->
+  Sem r ()
+checkPositivity ty = do
+  let indName = ty ^. inductiveName
+  numInductives <- HashMap.size <$> asks (^. infoInductives)
+  noCheckPositivity <- asks (^. E.entryPointNoPositivity)
+  forM_ (ty ^. inductiveConstructors) $ \ctor -> do
+    let ctorName = ctor ^. inductiveConstructorName
+    unless (noCheckPositivity || ty ^. inductivePositive) $
+      mapM_
+        (checkStrictlyPositiveOccurrences ty ctorName indName numInductives Nothing)
+        (ctor ^. inductiveConstructorParameters)
+
+checkStrictlyPositiveOccurrences ::
+  forall r.
+  Members '[Reader InfoTable, Error TypeCheckerError, State NegativeTypeParameters] r =>
+  InductiveDef ->
+  ConstrName ->
+  Name ->
+  RecursionLimit ->
+  ErrorReference ->
+  Expression ->
+  Sem r ()
+checkStrictlyPositiveOccurrences ty ctorName name recLimit ref = helper False
+  where
+    indName :: Name
+    indName = ty ^. inductiveName
+
+    -- The following `helper` function determines if there is any negative
+    -- occurence of the symbol `name` in the given expression. The `inside` flag
+    -- used below indicates whether the current search is performed on the left
+    -- of an inner arrow or not.
+
+    helper :: Bool -> Expression -> Sem r ()
+    helper inside expr = case expr of
+      ExpressionIden i -> helperIden i
+      ExpressionFunction (Function l r) -> helper True (l ^. paramType) >> helper inside r
+      ExpressionApplication tyApp -> helperApp tyApp
+      ExpressionLiteral {} -> return ()
+      ExpressionHole {} -> return ()
+      ExpressionUniverse {} -> return ()
+      where
+        helperIden :: Iden -> Sem r ()
+        helperIden = \case
+          IdenInductive ty' -> when (inside && name == ty') (strictlyPositivityError expr)
+          IdenVar name'
+            | not inside -> return ()
+            | name == name' -> strictlyPositivityError expr
+            | InductiveParameter name' `elem` ty ^. inductiveParameters -> modify (HashSet.insert name')
+            | otherwise -> return ()
+          _ -> return ()
+
+        helperApp :: Application -> Sem r ()
+        helperApp tyApp = do
+          let (hdExpr, args) = unfoldApplication tyApp
+          case hdExpr of
+            ExpressionIden (IdenInductive ty') -> do
+              when (inside && name == ty') (strictlyPositivityError expr)
+              InductiveInfo indTy' <- lookupInductive ty'
+
+              -- We now need to know whether `name` negatively occurs at `indTy'`
+              -- or not. The way to know is by checking that the type ty'
+              -- preserves the positivity condition, i.e., its type parameters
+              -- are no negative.
+
+              let paramsTy' = indTy' ^. inductiveParameters
+              helperInductiveApp indTy' (zip paramsTy' (toList args))
+            _ -> return ()
+
+        helperInductiveApp :: InductiveDef -> [(InductiveParameter, Expression)] -> Sem r ()
+        helperInductiveApp typ = \case
+          ((InductiveParameter pName, arg) : ps) -> do
+            negParms :: NegativeTypeParameters <- get
+            when (varOrInductiveInExpression name arg) $ do
+              when (HashSet.member pName negParms) (strictlyPositivityError arg)
+              when (recLimit > 0) $
+                forM_ (typ ^. inductiveConstructors) $ \ctor' ->
+                  mapM_
+                    ( checkStrictlyPositiveOccurrences
+                        ty
+                        ctorName
+                        pName
+                        (recLimit - 1)
+                        (Just (fromMaybe arg ref))
+                    )
+                    (ctor' ^. inductiveConstructorParameters)
+                    >> modify (HashSet.insert pName)
+            helperInductiveApp ty ps
+          [] -> return ()
+
+    strictlyPositivityError :: Expression -> Sem r ()
+    strictlyPositivityError expr = do
+      let errLoc = fromMaybe expr ref
+      throw
+        ( ErrNoPositivity $
+            NoPositivity
+              { _noStrictPositivityType = indName,
+                _noStrictPositivityConstructor = ctorName,
+                _noStrictPositivityArgument = errLoc
+              }
+        )
+
+varOrInductiveInExpression :: Name -> Expression -> Bool
+varOrInductiveInExpression n = \case
+  ExpressionIden (IdenVar var) -> n == var
+  ExpressionIden (IdenInductive ty) -> n == ty
+  ExpressionApplication (Application l r _) ->
+    varOrInductiveInExpression n l || varOrInductiveInExpression n r
+  ExpressionFunction (Function l r) ->
+    varOrInductiveInExpression n (l ^. paramType)
+      || varOrInductiveInExpression n r
+  _ -> False

src/Juvix/Internal/Strings.hs

@@ -182,6 +182,9 @@ cBackend = "c"
 terminating :: IsString s => s
 terminating = "terminating"
 
+positive :: IsString s => s
+positive = "positive"
+
 waveArrow :: IsString s => s
 waveArrow = "↝"
 

src/Juvix/Pipeline/EntryPoint.hs

@@ -9,6 +9,7 @@ import Juvix.Prelude
 data EntryPoint = EntryPoint
   { _entryPointRoot :: FilePath,
     _entryPointNoTermination :: Bool,
+    _entryPointNoPositivity :: Bool,
     _entryPointNoStdlib :: Bool,
     _entryPointModulePaths :: NonEmpty FilePath
   }
@@ -19,6 +20,7 @@ defaultEntryPoint mainFile =
   EntryPoint
     { _entryPointRoot = ".",
       _entryPointNoTermination = False,
+      _entryPointNoPositivity = False,
       _entryPointNoStdlib = False,
       _entryPointModulePaths = pure mainFile
     }

src/Juvix/Syntax/Abstract/Language.hs

@@ -174,7 +174,8 @@ data InductiveDef = InductiveDef
     _inductiveBuiltin :: Maybe BuiltinInductive,
     _inductiveParameters :: [FunctionParameter],
     _inductiveType :: Expression,
-    _inductiveConstructors :: [InductiveConstructorDef]
+    _inductiveConstructors :: [InductiveConstructorDef],
+    _inductivePositive :: Bool
   }
   deriving stock (Eq, Show)
 

src/Juvix/Syntax/Concrete/Language.hs

@@ -248,7 +248,8 @@ data InductiveDef (s :: Stage) = InductiveDef
     _inductiveName :: InductiveName s,
     _inductiveParameters :: [InductiveParameter s],
     _inductiveType :: Maybe (ExpressionType s),
-    _inductiveConstructors :: [InductiveConstructorDef s]
+    _inductiveConstructors :: [InductiveConstructorDef s],
+    _inductivePositive :: Bool
   }
 
 deriving stock instance (Show (ExpressionType s), Show (SymbolType s)) => Show (InductiveDef s)

src/Juvix/Syntax/Concrete/Lexer.hs

@@ -266,6 +266,9 @@ kwType = keyword Str.type_
 kwTerminating :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r ()
 kwTerminating = keyword Str.terminating
 
+kwPositive :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r ()
+kwPositive = keyword Str.positive
+
 kwUsing :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r ()
 kwUsing = keyword Str.using
 

src/Juvix/Syntax/Concrete/Parser.hs

@@ -428,6 +428,7 @@ lambda = do
 
 inductiveDef :: Members '[Reader ParserParams, InfoTableBuilder] r => Maybe BuiltinInductive -> ParsecS r (InductiveDef 'Parsed)
 inductiveDef _inductiveBuiltin = do
+  _inductivePositive <- isJust <$> optional kwPositive
   kwInductive
   _inductiveName <- symbol
   _inductiveParameters <- P.many inductiveParam

src/Juvix/Syntax/Concrete/Scoped/Scoper.hs

@@ -460,7 +460,7 @@ checkInductiveDef ::
   Members '[Error ScoperError, State Scope, State ScoperState, Reader LocalVars, InfoTableBuilder, NameIdGen] r =>
   InductiveDef 'Parsed ->
   Sem r (InductiveDef 'Scoped)
-checkInductiveDef InductiveDef {..} = do
+checkInductiveDef ty@InductiveDef {..} = do
   withParams _inductiveParameters $ \inductiveParameters' -> do
     inductiveType' <- mapM checkParseExpressionAtoms _inductiveType
     inductiveName' <- bindInductiveSymbol _inductiveName
@@ -471,7 +471,8 @@ checkInductiveDef InductiveDef {..} = do
           _inductiveBuiltin = _inductiveBuiltin,
           _inductiveParameters = inductiveParameters',
           _inductiveType = inductiveType',
-          _inductiveConstructors = inductiveConstructors'
+          _inductiveConstructors = inductiveConstructors',
+          _inductivePositive = ty ^. inductivePositive
         }
 
 checkTopModule_ ::

src/Juvix/Syntax/MicroJuvix/Error.hs

@@ -21,6 +21,7 @@ data TypeCheckerError
   | ErrTooManyArgumentsIndType WrongNumberArgumentsIndType
   | ErrTooFewArgumentsIndType WrongNumberArgumentsIndType
   | ErrImpracticalPatternMatching ImpracticalPatternMatching
+  | ErrNoPositivity NoPositivity
 
 instance ToGenericError TypeCheckerError where
   genericError :: TypeCheckerError -> GenericError
@@ -34,3 +35,4 @@ instance ToGenericError TypeCheckerError where
     ErrTooManyArgumentsIndType e -> genericError e
     ErrTooFewArgumentsIndType e -> genericError e
     ErrImpracticalPatternMatching e -> genericError e
+    ErrNoPositivity e -> genericError e

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

@@ -260,3 +260,32 @@ instance ToGenericError ImpracticalPatternMatching where
           <+> ppCode ty
           <+> "is not an inductive data type."
           <+> "Therefore, pattern-matching is not available here"
+
+data NoPositivity = NoPositivity
+  { _noStrictPositivityType :: Name,
+    _noStrictPositivityConstructor :: Name,
+    _noStrictPositivityArgument :: Expression
+  }
+
+makeLenses ''NoPositivity
+
+instance ToGenericError NoPositivity where
+  genericError e =
+    GenericError
+      { _genericErrorLoc = j,
+        _genericErrorMessage = prettyError msg,
+        _genericErrorIntervals = [i, j]
+      }
+    where
+      ty = e ^. noStrictPositivityType
+      ctor = e ^. noStrictPositivityConstructor
+      arg = e ^. noStrictPositivityArgument
+      i = getLoc ty
+      j = getLoc arg
+      msg =
+        "The type"
+          <+> ppCode ty
+          <+> "is not strictly positive."
+            <> line
+            <> "It appears at a negative position in one of the arguments of the constructor"
+          <+> ppCode ctor <> "."

src/Juvix/Syntax/MicroJuvix/InfoTable.hs

@@ -73,14 +73,14 @@ buildTable1 m = InfoTable {..} <> buildTable (map (^. includeModule) includes)
     _infoConstructors :: HashMap Name ConstructorInfo
     _infoConstructors =
       HashMap.fromList
-        [ (c ^. constructorName, ConstructorInfo params args ind builtin)
+        [ (c ^. inductiveConstructorName, ConstructorInfo params args ind builtin)
           | StatementInductive d <- ss,
             let ind = d ^. inductiveName,
             let n = length (d ^. inductiveConstructors),
             let params = d ^. inductiveParameters,
             let builtins = maybe (replicate n Nothing) (map Just . builtinConstructors) (d ^. inductiveBuiltin),
             (builtin, c) <- zipExact builtins (d ^. inductiveConstructors),
-            let args = c ^. constructorParameters
+            let args = c ^. inductiveConstructorParameters
         ]
     _infoFunctions :: HashMap Name FunctionInfo
     _infoFunctions =
@@ -126,7 +126,7 @@ constructorArgTypes i =
     i ^. constructorInfoArgs
   )
 
-constructorType :: Member (Reader InfoTable) r => Name -> Sem r Expression
+constructorType :: Member (Reader InfoTable) r => ConstrName -> Sem r Expression
 constructorType c = do
   info <- lookupConstructor c
   let (inductiveParams, constrArgs) = constructorArgTypes info

src/Juvix/Syntax/MicroJuvix/Language.hs

@@ -135,12 +135,14 @@ data InductiveDef = InductiveDef
   { _inductiveName :: InductiveName,
     _inductiveBuiltin :: Maybe BuiltinInductive,
     _inductiveParameters :: [InductiveParameter],
-    _inductiveConstructors :: [InductiveConstructorDef]
+    _inductiveConstructors :: [InductiveConstructorDef],
+    _inductivePositive :: Bool
   }
 
 data InductiveConstructorDef = InductiveConstructorDef
-  { _constructorName :: ConstrName,
+  { _inductiveConstructorName :: ConstrName,
-    _constructorParameters :: [Expression]
+    _inductiveConstructorParameters :: [Expression],
+    _inductiveConstructorReturnType :: Expression
   }
 
 data FunctionParameter = FunctionParameter

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

@@ -381,10 +381,10 @@ unfoldApplication' :: Application -> (Expression, NonEmpty (IsImplicit, Expressi
 unfoldApplication' (Application l' r' i') = second (|: (i', r')) (unfoldExpressionApp l')
 
 unfoldExpressionApp :: Expression -> (Expression, [(IsImplicit, Expression)])
-unfoldExpressionApp e = case e of
+unfoldExpressionApp = \case
   ExpressionApplication (Application l r i) ->
     second (`snoc` (i, r)) (unfoldExpressionApp l)
-  _ -> (e, [])
+  e -> (e, [])
 
 unfoldApplication :: Application -> (Expression, NonEmpty Expression)
 unfoldApplication = fmap (fmap snd) . unfoldApplication'

src/Juvix/Syntax/MicroJuvix/MicroJuvixArityResult.hs

@@ -3,12 +3,13 @@ module Juvix.Syntax.MicroJuvix.MicroJuvixArityResult
   )
 where
 
+import Juvix.Pipeline.EntryPoint qualified as E
 import Juvix.Prelude
 import Juvix.Syntax.MicroJuvix.Language
-import Juvix.Syntax.MicroJuvix.MicroJuvixResult (MicroJuvixResult)
+import Juvix.Syntax.MicroJuvix.MicroJuvixResult qualified as M
 
 data MicroJuvixArityResult = MicroJuvixArityResult
-  { _resultMicroJuvixResult :: MicroJuvixResult,
+  { _resultMicroJuvixResult :: M.MicroJuvixResult,
     _resultModules :: NonEmpty Module
   }
 
@@ -16,3 +17,6 @@ makeLenses ''MicroJuvixArityResult
 
 mainModule :: Lens' MicroJuvixArityResult Module
 mainModule = resultModules . _head
+
+microJuvixArityResultEntryPoint :: Lens' MicroJuvixArityResult E.EntryPoint
+microJuvixArityResultEntryPoint = resultMicroJuvixResult . M.microJuvixResultEntryPoint

src/Juvix/Syntax/MicroJuvix/MicroJuvixResult.hs

@@ -4,6 +4,7 @@ module Juvix.Syntax.MicroJuvix.MicroJuvixResult
   )
 where
 
+import Juvix.Pipeline.EntryPoint qualified as E
 import Juvix.Prelude
 import Juvix.Syntax.Abstract.AbstractResult qualified as Abstract
 import Juvix.Syntax.MicroJuvix.InfoTable
@@ -16,3 +17,6 @@ data MicroJuvixResult = MicroJuvixResult
   }
 
 makeLenses ''MicroJuvixResult
+
+microJuvixResultEntryPoint :: Lens' MicroJuvixResult E.EntryPoint
+microJuvixResultEntryPoint = resultAbstract . Abstract.abstractResultEntryPoint

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

@@ -154,8 +154,8 @@ instance PrettyCode Hole where
 
 instance PrettyCode InductiveConstructorDef where
   ppCode c = do
-    constructorName' <- ppCode (c ^. constructorName)
+    constructorName' <- ppCode (c ^. inductiveConstructorName)
-    constructorParameters' <- mapM ppCodeAtom (c ^. constructorParameters)
+    constructorParameters' <- mapM ppCodeAtom (c ^. inductiveConstructorParameters)
     return (hsep $ constructorName' : constructorParameters')
 
 indent' :: Member (Reader Options) r => Doc a -> Sem r (Doc a)

src/Juvix/Syntax/MicroJuvix/TypeChecker.hs

@@ -6,7 +6,9 @@ module Juvix.Syntax.MicroJuvix.TypeChecker
 where
 
 import Data.HashMap.Strict qualified as HashMap
+import Juvix.Analysis.Positivity.Checker
 import Juvix.Internal.NameIdGen
+import Juvix.Pipeline.EntryPoint qualified as E
 import Juvix.Prelude hiding (fromEither)
 import Juvix.Syntax.MicroJuvix.Error
 import Juvix.Syntax.MicroJuvix.InfoTable
@@ -21,15 +23,19 @@ addIdens idens = modify (HashMap.union idens)
 
 registerConstructor :: Members '[State TypesTable, Reader InfoTable] r => InductiveConstructorDef -> Sem r ()
 registerConstructor ctr = do
-  ty <- constructorType (ctr ^. constructorName)
+  ty <- constructorType (ctr ^. inductiveConstructorName)
-  modify (HashMap.insert (ctr ^. constructorName) ty)
+  modify (HashMap.insert (ctr ^. inductiveConstructorName) ty)
 
 entryMicroJuvixTyped ::
   Members '[Error TypeCheckerError, NameIdGen] r =>
   MicroJuvixArityResult ->
   Sem r MicroJuvixTypedResult
 entryMicroJuvixTyped res@MicroJuvixArityResult {..} = do
-  (idens, r) <- runState (mempty :: TypesTable) (runReader table (mapM checkModule _resultModules))
+  (idens, r) <-
+    runState (mempty :: TypesTable)
+      . runReader entryPoint
+      . runReader table
+      $ mapM checkModule _resultModules
   return
     MicroJuvixTypedResult
       { _resultMicroJuvixArityResult = res,
@@ -40,12 +46,16 @@ entryMicroJuvixTyped res@MicroJuvixArityResult {..} = do
     table :: InfoTable
     table = buildTable _resultModules
 
+    entryPoint :: E.EntryPoint
+    entryPoint = res ^. microJuvixArityResultEntryPoint
+
 checkModule ::
-  Members '[Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable] r =>
+  Members '[Reader E.EntryPoint, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable] r =>
   Module ->
   Sem r Module
 checkModule Module {..} = do
-  _moduleBody' <- checkModuleBody _moduleBody
+  _moduleBody' <-
+    (evalState (mempty :: NegativeTypeParameters) . checkModuleBody) _moduleBody
   return
     Module
       { _moduleBody = _moduleBody',
@@ -53,7 +63,8 @@ checkModule Module {..} = do
       }
 
 checkModuleBody ::
-  Members '[Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable] r =>
+  forall r.
+  Members '[Reader E.EntryPoint, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State NegativeTypeParameters] r =>
   ModuleBody ->
   Sem r ModuleBody
 checkModuleBody ModuleBody {..} = do
@@ -64,19 +75,20 @@ checkModuleBody ModuleBody {..} = do
       }
 
 checkInclude ::
-  Members '[Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable] r =>
+  Members '[Reader E.EntryPoint, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable] r =>
   Include ->
   Sem r Include
 checkInclude = traverseOf includeModule checkModule
 
 checkStatement ::
-  Members '[Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable] r =>
+  Members '[Reader E.EntryPoint, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State NegativeTypeParameters] r =>
   Statement ->
   Sem r Statement
 checkStatement s = case s of
   StatementFunction fun -> StatementFunction <$> checkFunctionDef fun
   StatementForeign {} -> return s
   StatementInductive ind -> do
+    checkInductiveDef ind
     mapM_ registerConstructor (ind ^. inductiveConstructors)
     ty <- inductiveType (ind ^. inductiveName)
     modify (HashMap.insert (ind ^. inductiveName) ty)
@@ -138,6 +150,55 @@ checkFunctionParameter (FunctionParameter mv i e) = do
   e' <- checkExpression (smallUniverse (getLoc e)) e
   return (FunctionParameter mv i e')
 
+checkInductiveDef ::
+  Members '[Reader InfoTable, Error TypeCheckerError, State NegativeTypeParameters, Reader E.EntryPoint] r =>
+  InductiveDef ->
+  Sem r ()
+checkInductiveDef ty@InductiveDef {..} = do
+  checkPositivity ty
+  mapM_ (checkConstructorDef ty) _inductiveConstructors
+
+checkConstructorDef ::
+  Members
+    '[ Reader E.EntryPoint,
+       Reader InfoTable,
+       Error TypeCheckerError,
+       State NegativeTypeParameters
+     ]
+    r =>
+  InductiveDef ->
+  InductiveConstructorDef ->
+  Sem r ()
+checkConstructorDef ty ctor = do
+  checkConstructorReturnType ty ctor
+
+checkConstructorReturnType ::
+  Members '[Reader InfoTable, Error TypeCheckerError] r =>
+  InductiveDef ->
+  InductiveConstructorDef ->
+  Sem r ()
+checkConstructorReturnType indType ctor = do
+  let ctorName = ctor ^. inductiveConstructorName
+      ctorReturnType = ctor ^. inductiveConstructorReturnType
+      tyName = indType ^. inductiveName
+      indParams = map (^. inductiveParamName) (indType ^. inductiveParameters)
+      expectedReturnType =
+        foldExplicitApplication
+          (ExpressionIden (IdenInductive tyName))
+          (map (ExpressionIden . IdenVar) indParams)
+  when
+    (ctorReturnType /= expectedReturnType)
+    ( throw
+        ( ErrWrongReturnType
+            ( WrongReturnType
+                { _wrongReturnTypeConstructorName = ctorName,
+                  _wrongReturnTypeExpected = expectedReturnType,
+                  _wrongReturnTypeActual = ctorReturnType
+                }
+            )
+        )
+    )
+
 inferExpression ::
   Members '[Reader InfoTable, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference] r =>
   Expression ->

src/Juvix/Syntax/Universe.hs

@@ -12,7 +12,7 @@ data Universe = Universe
 newtype SmallUniverse = SmallUniverse
   { _smallUniverseLoc :: Interval
   }
-  deriving stock (Generic)
+  deriving stock (Generic, Show)
 
 instance Eq SmallUniverse where
   _ == _ = True

src/Juvix/Translation/AbstractToMicroJuvix.hs

@@ -267,8 +267,6 @@ goInductiveParameter f =
     (Nothing, _, _) -> unsupported "unnamed inductive parameters"
 
 goInductiveDef ::
-  forall r.
-  Member (Error TypeCheckerError) r =>
   Abstract.InductiveDef ->
   Sem r InductiveDef
 goInductiveDef i =
@@ -277,44 +275,28 @@ goInductiveDef i =
       | otherwise -> do
           inductiveParameters' <- mapM goInductiveParameter (i ^. Abstract.inductiveParameters)
           let indTypeName = i ^. Abstract.inductiveName
-              indParamNames = map (^. inductiveParamName) inductiveParameters'
+          inductiveConstructors' <-
-          inductiveConstructors' <- mapM (goConstructorDef indTypeName indParamNames) (i ^. Abstract.inductiveConstructors)
+            mapM
+              goConstructorDef
+              (i ^. Abstract.inductiveConstructors)
           return
             InductiveDef
               { _inductiveName = indTypeName,
                 _inductiveParameters = inductiveParameters',
                 _inductiveBuiltin = i ^. Abstract.inductiveBuiltin,
-                _inductiveConstructors = inductiveConstructors'
+                _inductiveConstructors = inductiveConstructors',
+                _inductivePositive = i ^. Abstract.inductivePositive
               }
   where
-    goConstructorDef :: Name -> [Name] -> Abstract.InductiveConstructorDef -> Sem r InductiveConstructorDef
+    goConstructorDef :: Abstract.InductiveConstructorDef -> Sem r InductiveConstructorDef
-    goConstructorDef indName paramNames c = do
+    goConstructorDef c = do
-      (_constructorParameters', actualReturnType) <- viewConstructorType (c ^. Abstract.constructorType)
+      (cParams, cReturnType) <- viewConstructorType (c ^. Abstract.constructorType)
-      let ctorName = c ^. Abstract.constructorName
+      return
-          foldTypeAppName :: Name -> [Name] -> Expression
+        InductiveConstructorDef
-          foldTypeAppName tyName indParams =
+          { _inductiveConstructorName = c ^. Abstract.constructorName,
-            foldExplicitApplication
+            _inductiveConstructorParameters = cParams,
-              (ExpressionIden (IdenInductive tyName))
+            _inductiveConstructorReturnType = cReturnType
-              (map (ExpressionIden . IdenVar) indParams)
+          }
-          expectedReturnType :: Expression
-          expectedReturnType = foldTypeAppName indName paramNames
-      if
-          | actualReturnType == expectedReturnType ->
-              return
-                InductiveConstructorDef
-                  { _constructorName = ctorName,
-                    _constructorParameters = _constructorParameters'
-                  }
-          | otherwise ->
-              throw
-                ( ErrWrongReturnType
-                    ( WrongReturnType
-                        { _wrongReturnTypeConstructorName = ctorName,
-                          _wrongReturnTypeExpected = expectedReturnType,
-                          _wrongReturnTypeActual = actualReturnType
-                        }
-                    )
-                )
 
 goTypeApplication :: Abstract.Application -> Sem r Application
 goTypeApplication (Abstract.Application l r i) = do

src/Juvix/Translation/MicroJuvixToMiniC.hs

@@ -485,7 +485,7 @@ mkInductiveName :: Micro.InductiveDef -> Text
 mkInductiveName i = mkName (i ^. Micro.inductiveName)
 
 mkInductiveConstructorNames :: Micro.InductiveDef -> [Text]
-mkInductiveConstructorNames i = mkName . view Micro.constructorName <$> i ^. Micro.inductiveConstructors
+mkInductiveConstructorNames i = mkName . view Micro.inductiveConstructorName <$> i ^. Micro.inductiveConstructors
 
 mkInductiveTypeDef :: Micro.InductiveDef -> [CCode]
 mkInductiveTypeDef i =
@@ -638,13 +638,13 @@ goInductiveConstructorNew i ctor = ctorNewFun
     ctorNewFun = if null ctorParams then return ctorNewNullary else ctorNewNary
 
     baseName :: Text
-    baseName = mkName (ctor ^. Micro.constructorName)
+    baseName = mkName (ctor ^. Micro.inductiveConstructorName)
 
     inductiveName :: Text
     inductiveName = mkInductiveName i
 
     ctorParams :: [Micro.PolyType]
-    ctorParams = map mkPolyType' (ctor ^. Micro.constructorParameters)
+    ctorParams = map mkPolyType' (ctor ^. Micro.inductiveConstructorParameters)
 
     ctorNewNullary :: [CCode]
     ctorNewNullary =
@@ -791,7 +791,7 @@ goInductiveConstructorNew i ctor = ctorNewFun
         )
 
 inductiveCtorParams :: Members '[Reader Micro.InfoTable] r => Micro.InductiveConstructorDef -> Sem r [CDeclType]
-inductiveCtorParams ctor = mapM (goType . mkPolyType') (ctor ^. Micro.constructorParameters)
+inductiveCtorParams ctor = mapM (goType . mkPolyType') (ctor ^. Micro.inductiveConstructorParameters)
 
 inductiveCtorArgs :: Members '[Reader Micro.InfoTable] r => Micro.InductiveConstructorDef -> Sem r [Declaration]
 inductiveCtorArgs ctor = namedArgs asCtorArg <$> inductiveCtorParams ctor
@@ -814,10 +814,10 @@ goInductiveConstructorDef ctor = do
     ctorDecl = if null ctorParams then return ctorBool else ctorStruct
 
     baseName :: Text
-    baseName = mkName (ctor ^. Micro.constructorName)
+    baseName = mkName (ctor ^. Micro.inductiveConstructorName)
 
     ctorParams :: [Micro.PolyType]
-    ctorParams = map mkPolyType' (ctor ^. Micro.constructorParameters)
+    ctorParams = map mkPolyType' (ctor ^. Micro.inductiveConstructorParameters)
 
     ctorBool :: Declaration
     ctorBool = typeDefWrap (asTypeDef baseName) BoolType
@@ -848,7 +848,7 @@ goProjections inductiveTypeDef ctor = do
   return (ExternalFunc <$> zipWith projFunction [0 ..] params)
   where
     baseName :: Text
-    baseName = mkName (ctor ^. Micro.constructorName)
+    baseName = mkName (ctor ^. Micro.inductiveConstructorName)
 
     localName :: Text
     localName = "a"

src/Juvix/Translation/MicroJuvixToMonoJuvix.hs

@@ -125,7 +125,7 @@ buildConcreteTable info =
       let def :: Micro.InductiveDef
           def = info ^?! Micro.infoInductives . at ind . _Just . Micro.inductiveInfoDef
           constructorNames :: [Micro.Name]
-          constructorNames = def ^.. Micro.inductiveConstructors . each . Micro.constructorName
+          constructorNames = def ^.. Micro.inductiveConstructors . each . Micro.inductiveConstructorName
           k :: NonEmpty Micro.ConcreteType
           k = tc ^. Micro.typeCallArguments
           iden :: PolyIden
@@ -265,10 +265,10 @@ goInductiveDefConcrete def = do
   where
     goConstructor :: Micro.InductiveConstructorDef -> Sem r InductiveConstructorDef
     goConstructor c = do
-      params' <- mapM (goType . Micro.mkConcreteType') (c ^. Micro.constructorParameters)
+      params' <- mapM (goType . Micro.mkConcreteType') (c ^. Micro.inductiveConstructorParameters)
       return
         InductiveConstructorDef
-          { _constructorName = c ^. Micro.constructorName,
+          { _constructorName = c ^. Micro.inductiveConstructorName,
             _constructorParameters = params'
           }
 
@@ -380,14 +380,14 @@ goInductiveDefPoly def poly
       where
         goConstructorDef :: Micro.InductiveConstructorDef -> Sem r InductiveConstructorDef
         goConstructorDef cdef = do
-          cpolyInfo <- fromJust <$> lookupPolyConstructor (cdef ^. Micro.constructorName)
+          cpolyInfo <- fromJust <$> lookupPolyConstructor (cdef ^. Micro.inductiveConstructorName)
           let concrete :: ConcreteIdenInfo
               concrete = fromJust (cpolyInfo ^. polyConcretes . at k)
               params :: [Micro.ConcreteType]
               params =
                 map
                   (Micro.substitutionConcrete (concrete ^. concreteTypeSubs))
-                  (cdef ^. Micro.constructorParameters)
+                  (cdef ^. Micro.inductiveConstructorParameters)
           _constructorParameters <- mapM goType params
           return
             InductiveConstructorDef

src/Juvix/Translation/MicroJuvixToMonoJuvix/TypeCallsMapBuilder.hs

@@ -57,7 +57,7 @@ goInductiveParameter :: InductiveParameter -> Sem r ()
 goInductiveParameter _ = return ()
 
 goInductiveConstructorDef :: Members '[State TypeCallsMap, Reader Caller, Reader InfoTable] r => InductiveConstructorDef -> Sem r ()
-goInductiveConstructorDef c = mapM_ goExpression (c ^. constructorParameters)
+goInductiveConstructorDef c = mapM_ goExpression (c ^. inductiveConstructorParameters)
 
 goParam :: Members '[State TypeCallsMap, Reader Caller, Reader InfoTable] r => FunctionParameter -> Sem r ()
 goParam (FunctionParameter _ _ ty) = goExpression ty

src/Juvix/Translation/ScopedToAbstract.hs

@@ -241,7 +241,7 @@ goInductive ::
   Members '[InfoTableBuilder, Builtins, Error ScoperError] r =>
   InductiveDef 'Scoped ->
   Sem r Abstract.InductiveDef
-goInductive InductiveDef {..} = do
+goInductive ty@InductiveDef {..} = do
   _inductiveParameters' <- mapM goInductiveParameter _inductiveParameters
   _inductiveType' <- mapM goExpression _inductiveType
   _inductiveConstructors' <- mapM goConstructorDef _inductiveConstructors
@@ -252,7 +252,8 @@ goInductive InductiveDef {..} = do
             _inductiveBuiltin = _inductiveBuiltin,
             _inductiveName = goSymbol _inductiveName,
             _inductiveType = fromMaybe (Abstract.ExpressionUniverse (smallUniverse loc)) _inductiveType',
-            _inductiveConstructors = _inductiveConstructors'
+            _inductiveConstructors = _inductiveConstructors',
+            _inductivePositive = ty ^. inductivePositive
           }
   whenJust _inductiveBuiltin (registerBuiltinInductive indDef)
   inductiveInfo <- registerInductive indDef

test/Scope/Positive.hs

@@ -40,6 +40,7 @@ testDescr PosTest {..} =
                   EntryPoint
                     { _entryPointRoot = cwd,
                       _entryPointNoTermination = False,
+                      _entryPointNoPositivity = False,
                       _entryPointNoStdlib = noStdlib,
                       _entryPointModulePaths = pure entryFile
                     }

test/Termination/Positive.hs

@@ -38,7 +38,15 @@ testDescrFlag N.NegTest {..} =
         { _testName = _name,
           _testRoot = tRoot,
           _testAssertion = Single $ do
-            let entryPoint = EntryPoint "." True True (pure _file)
+            let entryPoint =
+                  EntryPoint
+                    { _entryPointRoot = ".",
+                      _entryPointNoTermination = True,
+                      _entryPointNoPositivity = False,
+                      _entryPointNoStdlib = True,
+                      _entryPointModulePaths = pure _file
+                    }
+
             (void . runIO) (upToMicroJuvix entryPoint)
         }
 
@@ -70,7 +78,7 @@ allTests =
         "Well-known terminating functions"
         (map (mkTest . testDescr) tests),
       testGroup
-        "Bypass checking using --non-termination flag on negative tests"
+        "Bypass termination checking using --non-termination flag on negative tests"
         (map (mkTest . testDescrFlag) negTests),
       testGroup
         "Terminating keyword"

test/TypeCheck/Negative.hs

@@ -1,4 +1,4 @@
-module TypeCheck.Negative (allTests) where
+module TypeCheck.Negative where
 
 import Base
 import Juvix.Pipeline
@@ -31,8 +31,14 @@ testDescr NegTest {..} =
 allTests :: TestTree
 allTests =
   testGroup
-    "TypeCheck negative tests"
+    "Typecheck negative tests"
-    (map (mkTest . testDescr) tests)
+    [ testGroup
+        "General typechecking errors"
+        (map (mkTest . testDescr) tests),
+      testGroup
+        "Non-strictly positive data types"
+        (map (mkTest . testDescr) negPositivityTests)
+    ]
 
 root :: FilePath
 root = "tests/negative"
@@ -113,3 +119,43 @@ tests =
         ErrWrongReturnType {} -> Nothing
         _ -> wrongError
   ]
+
+negPositivityTests :: [NegTest]
+negPositivityTests =
+  [ NegTest "E1" "MicroJuvix/Positivity" "E1.juvix" $
+      \case
+        ErrNoPositivity {} -> Nothing
+        _ -> wrongError,
+    NegTest "E2" "MicroJuvix/Positivity" "E2.juvix" $
+      \case
+        ErrNoPositivity {} -> Nothing
+        _ -> wrongError,
+    NegTest "E3" "MicroJuvix/Positivity" "E3.juvix" $
+      \case
+        ErrNoPositivity {} -> Nothing
+        _ -> wrongError,
+    NegTest "E4" "MicroJuvix/Positivity" "E4.juvix" $
+      \case
+        ErrNoPositivity {} -> Nothing
+        _ -> wrongError,
+    NegTest "E5" "MicroJuvix/Positivity" "E5.juvix" $
+      \case
+        ErrNoPositivity {} -> Nothing
+        _ -> wrongError,
+    NegTest "E6" "MicroJuvix/Positivity" "E6.juvix" $
+      \case
+        ErrNoPositivity {} -> Nothing
+        _ -> wrongError,
+    NegTest "E7" "MicroJuvix/Positivity" "E7.juvix" $
+      \case
+        ErrNoPositivity {} -> Nothing
+        _ -> wrongError,
+    NegTest "E8" "MicroJuvix/Positivity" "E8.juvix" $
+      \case
+        ErrNoPositivity {} -> Nothing
+        _ -> wrongError,
+    NegTest "E9" "MicroJuvix/Positivity" "E9.juvix" $
+      \case
+        ErrNoPositivity {} -> Nothing
+        _ -> wrongError
+  ]

test/TypeCheck/Positive.hs

@@ -2,6 +2,7 @@ module TypeCheck.Positive where
 
 import Base
 import Juvix.Pipeline
+import TypeCheck.Negative qualified as N
 
 data PosTest = PosTest
   { _name :: String,
@@ -23,11 +24,66 @@ testDescr PosTest {..} =
             (void . runIO) (upToMicroJuvixTyped entryPoint)
         }
 
+--------------------------------------------------------------------------------
+-- Testing --no-positivity flag with all related negative tests
+--------------------------------------------------------------------------------
+
+rootNegTests :: FilePath
+rootNegTests = "tests/negative/"
+
+testNoPositivityFlag :: N.NegTest -> TestDescr
+testNoPositivityFlag N.NegTest {..} =
+  let tRoot = rootNegTests </> _relDir
+   in TestDescr
+        { _testName = _name,
+          _testRoot = tRoot,
+          _testAssertion = Single $ do
+            let entryPoint =
+                  EntryPoint
+                    { _entryPointRoot = ".",
+                      _entryPointNoTermination = False,
+                      _entryPointNoPositivity = True,
+                      _entryPointNoStdlib = False,
+                      _entryPointModulePaths = pure _file
+                    }
+
+            (void . runIO) (upToMicroJuvix entryPoint)
+        }
+
+negPositivityTests :: [N.NegTest]
+negPositivityTests = N.negPositivityTests
+
+testPositivityKeyword :: [PosTest]
+testPositivityKeyword =
+  [ PosTest
+      "Mark T0 data type as strictly positive"
+      "MicroJuvix/Positivity"
+      "E5.juvix"
+  ]
+
+positivityTestGroup :: TestTree
+positivityTestGroup =
+  testGroup
+    "Positive tests for the positivity condition"
+    [ testGroup
+        "Bypass positivity checking using --non-positivity flag on negative tests"
+        (map (mkTest . testNoPositivityFlag) negPositivityTests),
+      testGroup
+        "Usages of the positive keyword"
+        (map (mkTest . testDescr) testPositivityKeyword)
+    ]
+
+--------------------------------------------------------------------------------
+
 allTests :: TestTree
 allTests =
   testGroup
-    "Scope positive tests"
+    "Typecheck positive tests"
-    (map (mkTest . testDescr) tests)
+    [ testGroup
+        "General typechecking tests"
+        (map (mkTest . testDescr) tests),
+      positivityTestGroup
+    ]
 
 tests :: [PosTest]
 tests =

tests/CLI/help.test

@@ -1,6 +1,7 @@
 $ juvix --help
 > /Usage: juvix \(\(\-v\|\-\-version\) \| \(\-h\|\-\-help\) \| \[\-\-no\-colors\] \[\-\-show\-name\-ids\] 
-               \[\-\-only\-errors\] \[\-\-no\-termination\] \[\-\-no\-stdlib\] COMMAND\).*/
+               \[\-\-only\-errors\] \[\-\-no\-termination\] \[\-\-no\-positivity\] 
+               \[\-\-no\-stdlib\] COMMAND\).*/
 >= 0
 
 

tests/negative/MicroJuvix/Positivity/E1.juvix

@@ -0,0 +1,8 @@
+module E1;
+
+axiom B : Type;
+inductive X  {
+  c : (X -> B) -> X;
+};
+
+end;

tests/negative/MicroJuvix/Positivity/E2.juvix

@@ -0,0 +1,9 @@
+module E2;
+
+open import NegParam;
+
+inductive D {
+d : T D -> D;
+};
+
+end;

tests/negative/MicroJuvix/Positivity/E3.juvix

@@ -0,0 +1,8 @@
+module E3;
+
+axiom B : Type;
+inductive X  {
+  c : B -> (X -> B) -> X;
+};
+
+end;

tests/negative/MicroJuvix/Positivity/E4.juvix

@@ -0,0 +1,12 @@
+module E4;
+
+inductive Tree (A : Type) {
+  leaf : Tree A;
+  node : (A -> Tree A) -> Tree A;
+};
+
+inductive Bad {
+  bad : Tree Bad -> Bad;
+};
+
+end;

tests/negative/MicroJuvix/Positivity/E5.juvix

@@ -0,0 +1,16 @@
+module E5;
+
+inductive T0 (A : Type){
+c0 : (A -> T0 A) -> T0 A;
+};
+
+axiom B : Type;
+inductive T1 (A : Type) {
+c1 : (B -> T0 A) -> T1 A;
+};
+
+inductive T2 {
+c2 : (B -> (B -> T1 T2)) -> T2;
+};
+
+end;

tests/negative/MicroJuvix/Positivity/E6.juvix

@@ -0,0 +1,8 @@
+module E6;
+
+axiom A : Type;
+inductive T (A : Type) {
+c : (A -> (A -> (T A -> A))) -> T A;
+};
+
+end;

tests/negative/MicroJuvix/Positivity/E7.juvix

@@ -0,0 +1,11 @@
+module E7;
+
+inductive T0 (A : Type) (B : Type) {
+c0 : (B -> A) -> T0 A B;
+};
+
+inductive T1 (A : Type) {
+c1 : (A -> T0 A (T1 A)) -> T1 A;
+};
+
+end;

tests/negative/MicroJuvix/Positivity/E8.juvix

@@ -0,0 +1,5 @@
+module E8;
+inductive B (A : Type) {
+b : (A -> B (B A -> A)) -> B A;
+};
+end;

tests/negative/MicroJuvix/Positivity/E9.juvix

@@ -0,0 +1,11 @@
+module E9;
+
+inductive B {
+b : B;
+};
+
+inductive T {
+  c : ((B → T) -> T) -> T;
+};
+
+end;

tests/negative/MicroJuvix/Positivity/NegParam.juvix

@@ -0,0 +1,5 @@
+module NegParam;
+inductive T (A : Type) {
+c : (A -> T A) -> T A;
+};
+end;

tests/negative/MicroJuvix/Positivity/errorE5.test

@@ -0,0 +1,6 @@
+$ juvix typecheck tests/negative/MicroJuvix/Positivity/E5.juvix --no-colors
+>2 /.*\.juvix\:13:21\-23\: error\:
+The type T2 is not strictly positive.
+It appears at a negative position in one of the arguments of the constructor c2.
+/
+>= 1

tests/negative/MicroJuvix/Positivity/errorE9.test

@@ -0,0 +1,6 @@
+$ juvix typecheck tests/negative/MicroJuvix/Positivity/E9.juvix --no-colors
+>2 /.*\.juvix\:8:13\-14\: error\:
+The type T is not strictly positive.
+It appears at a negative position in one of the arguments of the constructor c.
+/
+>= 1

tests/positive/MicroJuvix/Positivity/E5.juvix

@@ -0,0 +1,17 @@
+module E5;
+
+inductive T0 (A : Type){
+c0 : (A -> T0 A) -> T0 A;
+};
+
+axiom B : Type;
+inductive T1 (A : Type) {
+c1 : (B -> T0 A) -> T1 A;
+};
+
+positive
+inductive T2 {
+c2 : (B -> (B -> T1 T2)) -> T2;
+};
+
+end;