diff --git a/src/Juvix/Compiler/Internal/Data/Name.hs b/src/Juvix/Compiler/Internal/Data/Name.hs
index 1d2596358c..5060a270ab 100644
--- a/src/Juvix/Compiler/Internal/Data/Name.hs
+++ b/src/Juvix/Compiler/Internal/Data/Name.hs
@@ -103,6 +103,10 @@ type ConstrName = Name
 
 type InductiveName = Name
 
+type InductiveId = NameId
+
+type InductiveParam = Name
+
 fromConcreteSymbol :: Interval -> S.Symbol -> Name
 fromConcreteSymbol loc s = fromConcreteSymbolPretty loc (S.symbolText s) s
 
diff --git a/src/Juvix/Compiler/Internal/Language.hs b/src/Juvix/Compiler/Internal/Language.hs
index 662c691513..4f080319b8 100644
--- a/src/Juvix/Compiler/Internal/Language.hs
+++ b/src/Juvix/Compiler/Internal/Language.hs
@@ -484,6 +484,8 @@ data NormalizedExpression = NormalizedExpression
   }
 
 makePrisms ''Expression
+makePrisms ''MutualStatement
+
 makeLenses ''SideIfBranch
 makeLenses ''SideIfs
 makeLenses ''CaseBranchRhs
diff --git a/src/Juvix/Compiler/Internal/Pretty/Base.hs b/src/Juvix/Compiler/Internal/Pretty/Base.hs
index 40b10142eb..490ae9305b 100644
--- a/src/Juvix/Compiler/Internal/Pretty/Base.hs
+++ b/src/Juvix/Compiler/Internal/Pretty/Base.hs
@@ -11,11 +11,13 @@ import Juvix.Compiler.Internal.Data.NameDependencyInfo
 import Juvix.Compiler.Internal.Data.TypedHole
 import Juvix.Compiler.Internal.Language
 import Juvix.Compiler.Internal.Pretty.Options
+import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.Occurrences
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.CheckerNew.Arity qualified as New
 import Juvix.Compiler.Store.Internal.Data.InfoTable
 import Juvix.Data.CodeAnn
 import Juvix.Data.Keyword.All qualified as Kw
 import Juvix.Prelude
+import Prettyprinter qualified as PP
 
 doc :: (PrettyCode c) => Options -> c -> Doc Ann
 doc opts =
@@ -407,6 +409,35 @@ instance PrettyCode TypedHole where
     vars <- ppCode _typedHoleLocalVars
     return (h <+> kwColon <+> ty <> kwAt <> vars)
 
+instance PrettyCode Polarity where
+  ppCode = return . annotate AnnKeyword . pretty
+
+instance (PrettyCode k, PrettyCode v) => PrettyCode (HashMap k v) where
+  ppCode m = do
+    res <- forM (HashMap.toList m) $ \(k, v) -> do
+      k' <- ppCode k
+      v' <- ppCode v
+      return (k' <+> "↦" <+> v')
+    return (bracesEncloseIndent res)
+
+instance PrettyCode AppLhs where
+  ppCode = \case
+    AppVar v -> ppCode v
+    AppAxiom v -> ppCode v
+    AppInductive v -> ppCode v
+
+instance PrettyCode FunctionSide where
+  ppCode = return . annotate AnnKeyword . pretty
+
+instance PrettyCode Occurrences where
+  ppCode Occurrences {..} = do
+    ps <- ppCode _occurrences
+    return
+      ( bracesEncloseIndent
+          [ header "occurrences" <+> kwAssign <+> ps
+          ]
+      )
+
 instance PrettyCode InfoTable where
   ppCode tbl = do
     inds <- ppCode (HashMap.keys (tbl ^. infoInductives))
@@ -463,6 +494,15 @@ instance (PrettyCode a) => PrettyCode (Maybe a) where
     Nothing -> return "Nothing"
     Just p -> ("Just" <+>) <$> ppCode p
 
+bracesEncloseIndent :: forall l ann. (Foldable l) => l (Doc ann) -> Doc ann
+bracesEncloseIndent ls =
+  PP.group $
+    "{"
+      <> line'
+      <> indent' (concatWith (\x y -> x <> ";" <> line <> y) ls)
+      <> line'
+      <> "}"
+
 tuple :: [Doc ann] -> Doc ann
 tuple = encloseSep "(" ")" ", "
 
diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity.hs
index 98c2a83dc7..d7b22f9cf7 100644
--- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity.hs
@@ -1,8 +1,6 @@
 module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity
   ( module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.Checker,
-    module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.Error,
   )
 where
 
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.Checker
-import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.Error
diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Checker.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Checker.hs
index c319a4fb11..34ff4ea98b 100644
--- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Checker.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Checker.hs
@@ -1,251 +1,283 @@
-module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.Checker where
+module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.Checker
+  ( checkPositivity,
+  )
+where
 
 import Data.HashMap.Strict qualified as HashMap
 import Data.HashSet qualified as HashSet
 import Juvix.Compiler.Internal.Data.InfoTable
 import Juvix.Compiler.Internal.Extra
-import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.Error
+import Juvix.Compiler.Internal.Pretty
+import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.ConstructorArg
+import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.Occurrences
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Inference
+import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.ResultBuilder
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Error
-import Juvix.Compiler.Pipeline.EntryPoint qualified as E
 import Juvix.Prelude hiding (fromEither)
 
-type NegativeTypeParameters = HashSet VarName
-
-type CheckPositivityEffects r =
-  Members
-    '[ Reader E.EntryPoint,
-       Reader InfoTable,
-       Error TypeCheckerError,
-       Inference,
-       State NegativeTypeParameters
-     ]
-    r
-
-data CheckPositivityArgs = CheckPositivityArgs
-  { _checkPositivityArgsInductive :: InductiveInfo,
-    _checkPositivityArgsConstructorName :: Name,
-    _checkPositivityArgsInductiveName :: Name,
-    _checkPositivityArgsRecursionLimit :: Int,
-    _checkPositivityArgsErrorReference :: Maybe Expression,
-    _checkPositivityArgsTypeOfConstructorArg :: Expression
+data Builder = Builder
+  { _builderPolarities :: HashMap InductiveParam Polarity,
+    _builderBlocking :: [Blocking]
   }
 
-makeLenses ''CheckPositivityArgs
+data Blocking = Blocking
+  { _blockingContext :: Polarity,
+    _blockingUnblocker :: InductiveParam,
+    -- | The unblocker has to have at least this polarity to unblock
+    _blockingUnblockerMinimum :: Polarity,
+    _blockingOccurrences :: Occurrences
+  }
+
+makeLenses ''Blocking
+makeLenses ''Builder
+
+emptyBuilder :: Builder
+emptyBuilder =
+  Builder
+    { _builderPolarities = mempty,
+      _builderBlocking = mempty
+    }
+
+functionSidePolarity :: FunctionSide -> Polarity
+functionSidePolarity = \case
+  FunctionLeft -> PolarityNonStrictlyPositive
+  FunctionRight -> PolarityStrictlyPositive
 
 checkPositivity ::
   forall r.
-  (CheckPositivityEffects r) =>
-  InductiveInfo ->
+  ( Members
+      '[ Reader InfoTable,
+         Error TypeCheckerError,
+         ResultBuilder,
+         Inference
+       ]
+      r
+  ) =>
+  Bool ->
+  MutualBlock ->
   Sem r ()
-checkPositivity indInfo = do
-  unlessM (asks (^. E.entryPointNoPositivity)) $
-    forM_ (indInfo ^. inductiveInfoConstructors) $ \ctorName -> do
-      ctor <- asks (fromJust . HashMap.lookup ctorName . (^. infoConstructors))
-      unless (indInfo ^. inductiveInfoPositive) $ do
-        numInductives <- HashMap.size <$> asks (^. infoInductives)
-        forM_
-          (constructorArgs (ctor ^. constructorInfoType))
-          $ \typeOfConstr ->
-            checkStrictlyPositiveOccurrences
-              ( CheckPositivityArgs
-                  { _checkPositivityArgsInductive = indInfo,
-                    _checkPositivityArgsConstructorName = ctorName,
-                    _checkPositivityArgsInductiveName = indInfo ^. inductiveInfoName,
-                    _checkPositivityArgsRecursionLimit = numInductives,
-                    _checkPositivityArgsErrorReference = Nothing,
-                    _checkPositivityArgsTypeOfConstructorArg = typeOfConstr ^. paramType
-                  }
-              )
-
-checkStrictlyPositiveOccurrences ::
-  forall r.
-  (CheckPositivityEffects r) =>
-  CheckPositivityArgs ->
-  Sem r ()
-checkStrictlyPositiveOccurrences p = do
-  typeOfConstrArg <- strongNormalize_ (p ^. checkPositivityArgsTypeOfConstructorArg)
-  goExpression False typeOfConstrArg
+checkPositivity noPositivityFlag mut = do
+  let ldefs :: [InductiveDef] =
+        mut
+          ^.. mutualStatements
+            . each
+            . _StatementInductive
+
+  whenJust (nonEmpty ldefs) $ \defs -> do
+    args :: [ConstructorArg] <-
+      concatMapM
+        (strongNormalize >=> mkConstructorArg)
+        ( defs
+            ^.. each
+              . inductiveConstructors
+              . each
+              . inductiveConstructorType
+        )
+    poltab <- (^. typeCheckingTablesPolarityTable) <$> getCombinedTables
+    let occ :: Occurrences = mkOccurrences args
+        inferredPolarities = computePolarities poltab defs occ
+    forM_ defs $ \def -> do
+      let params :: [InductiveParam] = def ^.. inductiveParameters . each . inductiveParamName
+          getPol p = fromMaybe PolarityUnused (inferredPolarities ^. at p)
+          polarities :: [Polarity] = map getPol params
+          defName = def ^. inductiveName
+      addPolarities (defName ^. nameId) polarities
+    poltab' <- (^. typeCheckingTablesPolarityTable) <$> getCombinedTables
+    let names :: NonEmpty InductiveName = (^. inductiveName) <$> defs
+    unless noPositivityFlag $ do
+      let neg = checkStrictlyPositive poltab' names occ
+          markedPositive d = fromJust (find ((== d) . (^. inductiveName)) defs) ^. inductivePositive
+      whenJust (nonEmpty (filter (not . markedPositive) neg)) $ \negTys ->
+        throw $
+          ErrNonStrictlyPositive
+            NonStrictlyPositive
+              { _nonStrictlyPositiveOccurrences = negTys
+              }
+
+-- NOTE we conservatively assume that axioms have all variables in negative positions
+axiomPolarity :: Polarity
+axiomPolarity = PolarityNonStrictlyPositive
+
+-- | Returns the list of non-strictly positive types
+checkStrictlyPositive ::
+  PolarityTable ->
+  NonEmpty InductiveName ->
+  Occurrences ->
+  [InductiveName]
+checkStrictlyPositive tbl mutual =
+  run
+    . execOutputList
+    . runReader PolarityStrictlyPositive
+    . go
   where
-    indInfo = p ^. checkPositivityArgsInductive
-    ctorName = p ^. checkPositivityArgsConstructorName
-    name = p ^. checkPositivityArgsInductiveName
-    recLimit = p ^. checkPositivityArgsRecursionLimit
-    ref = p ^. checkPositivityArgsErrorReference
-
-    indName :: Name
-    indName = indInfo ^. inductiveInfoName
-
-    {- The following `go` function determines if there is any negative
-     occurrence 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.
-    -}
-    goExpression :: Bool -> Expression -> Sem r ()
-    goExpression inside expr = case expr of
-      ExpressionApplication tyApp -> goApp tyApp
-      ExpressionCase l -> goCase l
-      ExpressionFunction (Function l r) -> goLeft (l ^. paramType) >> go r
-      ExpressionHole {} -> return ()
-      ExpressionInstanceHole {} -> return ()
-      ExpressionIden i -> goIden i
-      ExpressionLambda l -> goLambda l
-      ExpressionLet l -> goLet l
-      ExpressionLiteral {} -> return ()
-      ExpressionSimpleLambda l -> goSimpleLambda l
-      ExpressionUniverse {} -> return ()
+    go :: forall r'. (Members '[Output InductiveName, Reader Polarity] r') => Occurrences -> Sem r' ()
+    go occ = forM_ (HashMap.toList (occ ^. occurrences)) (uncurry goApp)
+
+    mutualSet :: HashSet InductiveName
+    mutualSet = hashSet mutual
+
+    isMutual :: InductiveName -> Bool
+    isMutual d = HashSet.member d mutualSet
+
+    goArg ::
+      forall r'.
+      (Members '[Output InductiveName, Reader Polarity] r') =>
+      Polarity ->
+      Occurrences ->
+      Sem r' ()
+    goArg p occ = localPolarity p (go occ)
+
+    goApp ::
+      forall r'.
+      (Members '[Output InductiveName, Reader Polarity] r') =>
+      (FunctionSide, AppLhs) ->
+      [Occurrences] ->
+      Sem r' ()
+    goApp (side, lhs) occ = local (functionSidePolarity side <>) $ case lhs of
+      AppVar {} -> local (const PolarityNonStrictlyPositive) (mapM_ go occ)
+      AppAxiom {} -> local (<> axiomPolarity) (mapM_ go occ)
+      AppInductive d -> do
+        ctx <- ask
+        let pols = getPolarities d
+        case ctx of
+          PolarityUnused -> impossible
+          PolarityStrictlyPositive -> return ()
+          PolarityNonStrictlyPositive -> when (isMutual d) (output d)
+        mapM_ (uncurry goArg) (zip pols occ)
       where
-        go :: Expression -> Sem r ()
-        go = goExpression inside
-
-        goLeft :: Expression -> Sem r ()
-        goLeft = goExpression True
-
-        goCase :: Case -> Sem r ()
-        goCase l = do
-          go (l ^. caseExpression)
-          mapM_ goCaseBranch (l ^. caseBranches)
-
-        goSideIfBranch :: SideIfBranch -> Sem r ()
-        goSideIfBranch b = do
-          go (b ^. sideIfBranchCondition)
-          go (b ^. sideIfBranchBody)
-
-        goSideIfs :: SideIfs -> Sem r ()
-        goSideIfs s = do
-          mapM_ goSideIfBranch (s ^. sideIfBranches)
-          mapM_ go (s ^. sideIfElse)
-
-        goCaseBranchRhs :: CaseBranchRhs -> Sem r ()
-        goCaseBranchRhs = \case
-          CaseBranchRhsExpression e -> go e
-          CaseBranchRhsIf s -> goSideIfs s
-
-        goCaseBranch :: CaseBranch -> Sem r ()
-        goCaseBranch b = goCaseBranchRhs (b ^. caseBranchRhs)
-
-        goLet :: Let -> Sem r ()
-        goLet l = do
-          go (l ^. letExpression)
-          mapM_ goLetClause (l ^. letClauses)
-
-        goLetClause :: LetClause -> Sem r ()
-        goLetClause = \case
-          LetFunDef f -> goFunctionDef f
-          LetMutualBlock b -> goMutualBlockLet b
-
-        goMutualBlockLet :: MutualBlockLet -> Sem r ()
-        goMutualBlockLet b = mapM_ goFunctionDef (b ^. mutualLet)
-
-        goFunctionDef :: FunctionDef -> Sem r ()
-        goFunctionDef d = do
-          go (d ^. funDefType)
-          go (d ^. funDefBody)
-
-        goSimpleLambda :: SimpleLambda -> Sem r ()
-        goSimpleLambda (SimpleLambda (SimpleBinder _ lamVarTy) lamBody) = do
-          go lamVarTy
-          go lamBody
-
-        goLambda :: Lambda -> Sem r ()
-        goLambda l = mapM_ goClause (l ^. lambdaClauses)
+        getPolarities :: InductiveName -> [Polarity]
+        getPolarities n = fromMaybe err (tbl ^. polarityTable . at (n ^. nameId))
           where
-            goClause :: LambdaClause -> Sem r ()
-            goClause (LambdaClause _ b) = go b
-
-        goIden :: Iden -> Sem r ()
-        goIden = \case
-          IdenInductive ty' ->
-            when (inside && name == ty') (throwNegativePositonError expr)
-          IdenVar name'
-            | not inside -> return ()
-            | name == name' -> throwNegativePositonError expr
-            | name' `elem` indInfo ^.. inductiveInfoParameters . each . inductiveParamName -> modify (HashSet.insert name')
-            | otherwise -> return ()
-          _ -> return ()
-
-        goApp :: Application -> Sem r ()
-        goApp tyApp = do
-          let (hdExpr, args) = unfoldApplication tyApp
-          case hdExpr of
-            ax@(ExpressionIden IdenAxiom {}) -> do
-              when (isJust $ find (varOrInductiveInExpression name) args) $
-                throwTypeAsArgumentOfBoundVarError ax
-            var@(ExpressionIden IdenVar {}) -> do
-              when (isJust $ find (varOrInductiveInExpression name) args) $
-                throwTypeAsArgumentOfBoundVarError var
-            ExpressionIden (IdenInductive ty') -> do
-              when (inside && name == ty') (throwNegativePositonError expr)
-              indInfo' <- 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' = indInfo' ^. inductiveInfoParameters
-              goInductiveApp indInfo' (zip paramsTy' (toList args))
-            _ -> return ()
-
-        goInductiveApp :: InductiveInfo -> [(InductiveParameter, Expression)] -> Sem r ()
-        goInductiveApp indInfo' = \case
-          [] -> return ()
-          (InductiveParameter pName' _ty', tyArg) : ps -> do
-            negParms :: NegativeTypeParameters <- get
-            when (varOrInductiveInExpression name tyArg) $ do
-              when
-                (HashSet.member pName' negParms)
-                (throwNegativePositonError tyArg)
-              when (recLimit > 0) $
-                forM_ (indInfo' ^. inductiveInfoConstructors) $ \ctorName' -> do
-                  ctorType' <- lookupConstructorType ctorName'
-                  let errorRef = fromMaybe tyArg ref
-                      args = constructorArgs ctorType'
-                  mapM_
-                    ( \tyConstr' ->
-                        checkStrictlyPositiveOccurrences
-                          CheckPositivityArgs
-                            { _checkPositivityArgsInductive = indInfo',
-                              _checkPositivityArgsConstructorName = ctorName',
-                              _checkPositivityArgsInductiveName = pName',
-                              _checkPositivityArgsRecursionLimit = recLimit - 1,
-                              _checkPositivityArgsErrorReference = Just errorRef,
-                              _checkPositivityArgsTypeOfConstructorArg = tyConstr' ^. paramType
-                            }
-                    )
-                    args
-            goInductiveApp indInfo' ps
-
-    throwNegativePositonError :: Expression -> Sem r ()
-    throwNegativePositonError expr = do
-      let errLoc = fromMaybe expr ref
-      throw
-        . ErrNonStrictlyPositive
-        . ErrTypeInNegativePosition
-        $ TypeInNegativePosition
-          { _typeInNegativePositionType = indName,
-            _typeInNegativePositionConstructor = ctorName,
-            _typeInNegativePositionArgument = errLoc
-          }
-
-    throwTypeAsArgumentOfBoundVarError :: Expression -> Sem r ()
-    throwTypeAsArgumentOfBoundVarError expr = do
-      let errLoc = fromMaybe expr ref
-      throw
-        . ErrNonStrictlyPositive
-        . ErrTypeAsArgumentOfBoundVar
-        $ TypeAsArgumentOfBoundVar
-          { _typeAsArgumentOfBoundVarType = indName,
-            _typeAsArgumentOfBoundVarConstructor = ctorName,
-            _typeAsArgumentOfBoundVarReference = 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
+            err :: a
+            err = impossibleError ("Didn't find polarities for inductive " <> ppTrace n)
+
+localPolarity :: (Members '[Reader Polarity] r) => Polarity -> Sem r () -> Sem r ()
+localPolarity p = case p of
+  PolarityUnused -> const (return ())
+  PolarityNonStrictlyPositive -> local (p <>)
+  PolarityStrictlyPositive -> local (p <>)
+
+computePolarities ::
+  PolarityTable ->
+  NonEmpty InductiveDef ->
+  Occurrences ->
+  HashMap InductiveParam Polarity
+computePolarities tab defs topOccurrences =
+  (^. builderPolarities)
+    . run
+    . runReader PolarityStrictlyPositive
+    . execState emptyBuilder
+    $ go topOccurrences
+  where
+    defsByName :: HashMap InductiveName InductiveDef
+    defsByName = indexedByHash (^. inductiveName) defs
+
+    getDef :: InductiveName -> InductiveDef
+    getDef d = fromJust (defsByName ^. at d)
+
+    -- Gets the current polarities of an inductive definition in the current mutual block
+    getInductivePolarities ::
+      (Members '[State Builder] r) =>
+      InductiveName ->
+      Sem r [(InductiveParam, Maybe Polarity)]
+    getInductivePolarities d = do
+      b <- get
+      let params = getDef d ^. inductiveParameters
+      return
+        [ (name, b ^. builderPolarities . at name)
+          | p :: InductiveParameter <- params,
+            let name = p ^. inductiveParamName
+        ]
+
+    go :: forall r. (Members '[State Builder, Reader Polarity] r) => Occurrences -> Sem r ()
+    go o = do
+      sequence_
+        [ addPolarity param (functionSidePolarity side)
+          | ((side, AppVar param), _) <- HashMap.toList (o ^. occurrences)
+        ]
+      forM_ (HashMap.toList (o ^. occurrences)) (uncurry goApp)
+      where
+        addPolarity :: InductiveParam -> Polarity -> Sem r ()
+        addPolarity var p = do
+          newPol <- (p <>) <$> ask
+          modify (over (builderPolarities . at var) (Just . maybe newPol (newPol <>)))
+          unblock var newPol
+
+    unblock :: forall r. (Members '[State Builder] r) => InductiveParam -> Polarity -> Sem r ()
+    unblock p newPol = unblockGo
+      where
+        unblockGo :: Sem r ()
+        unblockGo = do
+          b <- gets (^. builderBlocking)
+          whenJust (findAndRemove isTriggered b) $ \(triggered, rest) -> do
+            modify (set builderBlocking (maybeToList (increaseMinimum triggered) ++ rest))
+            runBlocking triggered
+            unblockGo
+
+        increaseMinimum :: Blocking -> Maybe Blocking
+        increaseMinimum = case newPol of
+          PolarityNonStrictlyPositive -> const Nothing
+          PolarityStrictlyPositive -> Just . set blockingUnblockerMinimum PolarityNonStrictlyPositive
+          PolarityUnused -> impossible
+
+        isTriggered :: Blocking -> Bool
+        isTriggered b = (b ^. blockingUnblockerMinimum <= newPol) && (b ^. blockingUnblocker == p)
+
+        runBlocking :: Blocking -> Sem r ()
+        runBlocking b = runReader (b ^. blockingContext) (go (b ^. blockingOccurrences))
+
+    goApp ::
+      forall r.
+      (Members '[State Builder, Reader Polarity] r) =>
+      (FunctionSide, AppLhs) ->
+      [Occurrences] ->
+      Sem r ()
+    goApp (side, lhs) os = local (functionSidePolarity side <>) $ case lhs of
+      AppVar {} -> goVarArgs os
+      AppAxiom {} -> goAxiomArgs os
+      AppInductive a -> goInductive a os
+
+    goAxiomArgs :: (Members '[State Builder, Reader Polarity] r) => [Occurrences] -> Sem r ()
+    goAxiomArgs os = local (<> axiomPolarity) (mapM_ go os)
+
+    goVarArgs :: (Members '[State Builder, Reader Polarity] r) => [Occurrences] -> Sem r ()
+    goVarArgs os = local (const PolarityNonStrictlyPositive) (mapM_ go os)
+
+    block ::
+      (Members '[State Builder, Reader Polarity] r) =>
+      Polarity ->
+      InductiveParam ->
+      Occurrences ->
+      Sem r ()
+    block minPol param o = do
+      ctx <- ask
+      let b =
+            Blocking
+              { _blockingContext = ctx,
+                _blockingUnblocker = param,
+                _blockingOccurrences = o,
+                _blockingUnblockerMinimum = minPol
+              }
+      modify (over builderBlocking (b :))
+
+    goInductive ::
+      (Members '[State Builder, Reader Polarity] r) =>
+      InductiveName ->
+      [Occurrences] ->
+      Sem r ()
+    goInductive d os = do
+      case tab ^. polarityTable . at (d ^. nameId) of
+        Just (pols :: [Polarity]) ->
+          forM_ (zip pols os) $ \(pol :: Polarity, o :: Occurrences) -> do
+            localPolarity pol (go o)
+        Nothing -> do
+          pols :: [(InductiveParam, Maybe Polarity)] <- getInductivePolarities d
+          forM_ (zip pols os) $ \((p :: InductiveParam, mpol :: Maybe Polarity), o :: Occurrences) ->
+            case mpol of
+              Nothing -> block PolarityStrictlyPositive p o
+              Just pol -> case pol of
+                PolarityUnused -> impossible
+                PolarityStrictlyPositive -> do
+                  block PolarityNonStrictlyPositive p o
+                  localPolarity PolarityStrictlyPositive (go o)
+                PolarityNonStrictlyPositive -> localPolarity PolarityNonStrictlyPositive (go o)
diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/ConstructorArg.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/ConstructorArg.hs
new file mode 100644
index 0000000000..fb37227581
--- /dev/null
+++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/ConstructorArg.hs
@@ -0,0 +1,67 @@
+module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.ConstructorArg
+  ( mkConstructorArg,
+    module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.ConstructorArg.Base,
+  )
+where
+
+import Juvix.Compiler.Internal.Extra.Base
+import Juvix.Compiler.Internal.Language
+import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.ConstructorArg.Base
+import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Error
+import Juvix.Prelude
+
+mkConstructorArg :: (Members '[Error TypeCheckerError] r) => NormalizedExpression -> Sem r [ConstructorArg]
+mkConstructorArg = mapM (goArg . (^. paramType)) . fst . unfoldFunType . (^. normalizedExpression)
+
+goArg :: forall r. (Members '[Error TypeCheckerError] r) => Expression -> Sem r ConstructorArg
+goArg ty = case ty of
+  ExpressionIden i -> goApplicationHelper (ExpressionIden i, [])
+  ExpressionApplication i -> goApplication i
+  ExpressionUniverse {} -> return ConstructorArgType
+  ExpressionFunction i -> goFunction i
+  ExpressionLiteral {} -> invalid
+  ExpressionHole {} -> invalid
+  ExpressionInstanceHole {} -> invalid
+  ExpressionLet {} -> invalid
+  ExpressionSimpleLambda {} -> invalid
+  ExpressionLambda {} -> invalid
+  ExpressionCase {} -> invalid
+  where
+    invalid :: forall a. Sem r a
+    invalid =
+      throw $
+        ErrInvalidConstructorArgType
+          InvalidConstructorArgType
+            { _invalidConstructorArgType = ty
+            }
+
+    getIden :: Expression -> Sem r Iden
+    getIden = \case
+      ExpressionIden i -> return i
+      _ -> invalid
+
+    goFunction :: Function -> Sem r ConstructorArg
+    goFunction fun = do
+      l <- goArg (fun ^. functionLeft . paramType)
+      r <- goArg (fun ^. functionRight)
+      return $
+        ConstructorArgFun
+          Fun
+            { _funLeft = l,
+              _funRight = r
+            }
+
+    goApplication :: Application -> Sem r ConstructorArg
+    goApplication = goApplicationHelper . second toList . unfoldApplication
+
+    goApplicationHelper :: (Expression, [Expression]) -> Sem r ConstructorArg
+    goApplicationHelper (f, args) = do
+      i <- getIden f
+      cargs <- mapM goArg args
+      lhs :: AppLhs <- case i of
+        IdenFunction {} -> invalid
+        IdenConstructor {} -> invalid
+        IdenVar v -> return (AppVar v)
+        IdenAxiom v -> return (AppAxiom v)
+        IdenInductive v -> return (AppInductive v)
+      return (ConstructorArgApp (App lhs cargs))
diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/ConstructorArg/Base.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/ConstructorArg/Base.hs
new file mode 100644
index 0000000000..08aa4b093e
--- /dev/null
+++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/ConstructorArg/Base.hs
@@ -0,0 +1,27 @@
+module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.ConstructorArg.Base where
+
+import Juvix.Compiler.Internal.Language
+import Juvix.Prelude
+
+data ConstructorArg
+  = ConstructorArgFun Fun
+  | ConstructorArgApp App
+  | ConstructorArgType
+
+data Fun = Fun
+  { _funLeft :: ConstructorArg,
+    _funRight :: ConstructorArg
+  }
+
+data AppLhs
+  = AppVar VarName
+  | AppAxiom AxiomName
+  | AppInductive InductiveName
+  deriving stock (Eq, Show, Generic)
+
+instance Hashable AppLhs
+
+data App = App
+  { _appLhs :: AppLhs,
+    _appArgs :: [ConstructorArg]
+  }
diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Error.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Error.hs
deleted file mode 100644
index 64d00e1f16..0000000000
--- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Error.hs
+++ /dev/null
@@ -1,18 +0,0 @@
-module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.Error
-  ( module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.Error,
-    module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.Error.Types,
-  )
-where
-
-import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.Error.Types
-import Juvix.Prelude
-
-data NonStrictlyPositiveError
-  = ErrTypeInNegativePosition TypeInNegativePosition
-  | ErrTypeAsArgumentOfBoundVar TypeAsArgumentOfBoundVar
-
-instance ToGenericError NonStrictlyPositiveError where
-  genericError :: (Member (Reader GenericOptions) r) => NonStrictlyPositiveError -> Sem r GenericError
-  genericError = \case
-    ErrTypeInNegativePosition e -> genericError e
-    ErrTypeAsArgumentOfBoundVar e -> genericError e
diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Occurrences.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Occurrences.hs
new file mode 100644
index 0000000000..b8bd3d8ea8
--- /dev/null
+++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Occurrences.hs
@@ -0,0 +1,87 @@
+module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.Occurrences
+  ( module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.ConstructorArg.Base,
+    Occurrences (..),
+    FunctionSide (..),
+    mkOccurrences,
+    occurrences,
+  )
+where
+
+import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.ConstructorArg.Base
+import Juvix.Prelude
+import Juvix.Prelude.Pretty
+
+data FunctionSide
+  = FunctionLeft
+  | FunctionRight
+  deriving stock (Show, Eq, Generic)
+
+instance Pretty FunctionSide where
+  pretty = \case
+    FunctionLeft -> "left"
+    FunctionRight -> "right"
+
+instance Hashable FunctionSide
+
+instance Semigroup FunctionSide where
+  a <> b = case (a, b) of
+    (FunctionLeft, _) -> FunctionLeft
+    (_, FunctionLeft) -> FunctionLeft
+    (FunctionRight, FunctionRight) -> FunctionRight
+
+instance Monoid FunctionSide where
+  mempty = FunctionRight
+
+newtype Occurrences = Occurrences
+  { _occurrences :: HashMap (FunctionSide, AppLhs) [Occurrences]
+  }
+  deriving stock (Show)
+
+makeLenses ''Occurrences
+
+emptyOccurrences :: Occurrences
+emptyOccurrences =
+  Occurrences
+    { _occurrences = mempty
+    }
+
+mkOccurrences :: [ConstructorArg] -> Occurrences
+mkOccurrences =
+  run
+    . runReader FunctionRight
+    . execState emptyOccurrences
+    . mapM_ addArg
+  where
+    addArg :: forall r'. (Members '[Reader FunctionSide, State Occurrences] r') => ConstructorArg -> Sem r' ()
+    addArg = \case
+      ConstructorArgFun fun -> goFun fun
+      ConstructorArgApp a -> goApp a
+      ConstructorArgType -> return ()
+      where
+        goApp :: App -> Sem r' ()
+        goApp (App lhs args) = case lhs of
+          AppVar {} -> goArgs (<> FunctionLeft)
+          AppAxiom {} -> goArgs id
+          AppInductive {} -> goArgs id
+          where
+            goArgs :: (FunctionSide -> FunctionSide) -> Sem r' ()
+            goArgs recurModif = do
+              side <- ask
+              let numArgs = length args
+                  iniOccs = replicate numArgs emptyOccurrences
+                  k = (side, lhs)
+              occs :: [Occurrences] <- fromMaybe iniOccs <$> gets (^. occurrences . at k)
+              st :: Occurrences <- get
+              occs' :: [Occurrences] <- local recurModif . for (zipExact occs args) $ \(occ, arg) -> do
+                put occ
+                addArg arg
+                get
+              put (set (occurrences . at k) (Just occs') st)
+
+        goFun :: Fun -> Sem r' ()
+        goFun (Fun funl funr) = do
+          onSide FunctionLeft (addArg funl)
+          onSide FunctionRight (addArg funr)
+          where
+            onSide :: FunctionSide -> Sem r' () -> Sem r' ()
+            onSide side = local (side <>)
diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs
index 987471e72b..1989a3c98e 100644
--- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs
@@ -131,7 +131,7 @@ checkCoercionCycles ::
   (Members '[ResultBuilder, Error TypeCheckerError] r) =>
   Sem r ()
 checkCoercionCycles = do
-  ctab <- getCombinedCoercionTable
+  ctab <- (^. typeCheckingTablesCoercionTable) <$> getCombinedTables
   let s = toList $ cyclicCoercions ctab
   whenJust (nonEmpty s) $
     throw
@@ -151,10 +151,7 @@ checkModule ::
   Module ->
   Sem r Module
 checkModule Module {..} = runReader (mempty @InsertedArgsStack) $ do
-  _moduleBody' <-
-    evalState (mempty :: NegativeTypeParameters)
-      . checkModuleBody
-      $ _moduleBody
+  _moduleBody' <- checkModuleBody _moduleBody
   return
     Module
       { _moduleBody = _moduleBody',
@@ -164,7 +161,7 @@ checkModule Module {..} = runReader (mempty @InsertedArgsStack) $ do
       }
 
 checkModuleBody ::
-  (Members '[HighlightBuilder, Reader BuiltinsTable, Reader EntryPoint, State NegativeTypeParameters, Reader InfoTable, Error TypeCheckerError, NameIdGen, ResultBuilder, Termination, Reader InsertedArgsStack] r) =>
+  (Members '[HighlightBuilder, Reader BuiltinsTable, Reader EntryPoint, Reader InfoTable, Error TypeCheckerError, NameIdGen, ResultBuilder, Termination, Reader InsertedArgsStack] r) =>
   ModuleBody ->
   Sem r ModuleBody
 checkModuleBody ModuleBody {..} = do
@@ -180,14 +177,14 @@ checkImport :: Import -> Sem r Import
 checkImport = return
 
 checkMutualBlock ::
-  (Members '[HighlightBuilder, Reader BuiltinsTable, Reader EntryPoint, State NegativeTypeParameters, Reader InfoTable, Error TypeCheckerError, NameIdGen, ResultBuilder, Termination, Reader InsertedArgsStack] r) =>
+  (Members '[HighlightBuilder, Reader BuiltinsTable, Reader EntryPoint, Reader InfoTable, Error TypeCheckerError, NameIdGen, ResultBuilder, Termination, Reader InsertedArgsStack] r) =>
   MutualBlock ->
   Sem r MutualBlock
 checkMutualBlock s = runReader emptyLocalVars (checkTopMutualBlock s)
 
 checkInductiveDef ::
   forall r.
-  (Members '[HighlightBuilder, Reader BuiltinsTable, Reader EntryPoint, Reader InfoTable, ResultBuilder, Error TypeCheckerError, NameIdGen, State NegativeTypeParameters, Termination, Output TypedHole, Output CastHole, Reader InsertedArgsStack, Reader LocalVars] r) =>
+  (Members '[HighlightBuilder, Reader BuiltinsTable, Reader EntryPoint, Reader InfoTable, ResultBuilder, Error TypeCheckerError, NameIdGen, Termination, Output TypedHole, Output CastHole, Reader InsertedArgsStack, Reader LocalVars] r) =>
   InductiveDef ->
   Sem r InductiveDef
 checkInductiveDef InductiveDef {..} = runInferenceDef $ do
@@ -209,7 +206,6 @@ checkInductiveDef InductiveDef {..} = runInferenceDef $ do
               _inductivePragmas,
               _inductiveDocComment
             }
-    checkPositivity (inductiveInfoFromInductiveDef d)
     return d
   where
     checkParams :: Sem (Inference ': r) [(Name, Expression)]
@@ -249,11 +245,33 @@ checkInductiveDef InductiveDef {..} = runInferenceDef $ do
             )
 
 checkTopMutualBlock ::
-  (Members '[HighlightBuilder, Reader BuiltinsTable, State NegativeTypeParameters, Reader EntryPoint, Reader LocalVars, Reader InfoTable, Error TypeCheckerError, NameIdGen, ResultBuilder, Termination, Reader InsertedArgsStack] r) =>
+  (Members '[HighlightBuilder, Reader BuiltinsTable, Reader EntryPoint, Reader LocalVars, Reader InfoTable, Error TypeCheckerError, NameIdGen, ResultBuilder, Termination, Reader InsertedArgsStack] r) =>
   MutualBlock ->
   Sem r MutualBlock
 checkTopMutualBlock (MutualBlock ds) =
-  MutualBlock <$> runInferenceDefs (mapM checkMutualStatement ds)
+  MutualBlock
+    <$> runInferenceDefs
+      ( do
+          ls <- mapM checkMutualStatement ds
+          checkBlockPositivity (MutualBlock ls)
+          return ls
+      )
+
+checkBlockPositivity ::
+  ( Members
+      '[ Reader InfoTable,
+         Error TypeCheckerError,
+         ResultBuilder,
+         Reader EntryPoint,
+         Inference
+       ]
+      r
+  ) =>
+  MutualBlock ->
+  Sem r ()
+checkBlockPositivity m = do
+  noPos <- asks (^. entryPointNoPositivity)
+  checkPositivity noPos m
 
 resolveCastHoles ::
   forall a r.
@@ -286,7 +304,7 @@ resolveCastHoles s = do
     getNatTy = mkBuiltinInductive BuiltinNat
 
 checkMutualStatement ::
-  (Members '[HighlightBuilder, Reader BuiltinsTable, State NegativeTypeParameters, Reader EntryPoint, Inference, Reader LocalVars, Reader InfoTable, Error TypeCheckerError, NameIdGen, ResultBuilder, Termination, Reader InsertedArgsStack] r) =>
+  (Members '[HighlightBuilder, Reader BuiltinsTable, Reader EntryPoint, Inference, Reader LocalVars, Reader InfoTable, Error TypeCheckerError, NameIdGen, ResultBuilder, Termination, Reader InsertedArgsStack] r) =>
   MutualStatement ->
   Sem r MutualStatement
 checkMutualStatement = \case
@@ -395,7 +413,7 @@ checkInstanceType FunctionDef {..} = do
       tab <- ask
       unless (isTrait tab _instanceInfoInductive) $
         throw (ErrTargetNotATrait (TargetNotATrait _funDefType))
-      itab <- getCombinedInstanceTable
+      itab <- (^. typeCheckingTablesInstanceTable) <$> getCombinedTables
       is <- subsumingInstances itab ii
       unless (null is) $
         throw (ErrSubsumedInstance (SubsumedInstance ii is (getLoc _funDefName)))
diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/Inference.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/Inference.hs
index b9b61a98ed..175852f6ea 100644
--- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/Inference.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/Inference.hs
@@ -622,6 +622,7 @@ strongNormalize'' ty = do
                 { _typeCheckingTablesCoercionTable = mempty,
                   _typeCheckingTablesInstanceTable = mempty,
                   _typeCheckingTablesTypesTable = mempty,
+                  _typeCheckingTablesPolarityTable = mempty,
                   _typeCheckingTablesFunctionsTable = ftab
                 }
           }
diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/ResultBuilder.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/ResultBuilder.hs
index ea35c7a3a6..e4f5fc730e 100644
--- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/ResultBuilder.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/ResultBuilder.hs
@@ -13,10 +13,10 @@ data ResultBuilder :: Effect where
   AddIdenTypes :: TypesTable -> ResultBuilder m ()
   AddInstanceInfo :: InstanceInfo -> ResultBuilder m ()
   AddCoercionInfo :: CoercionInfo -> ResultBuilder m ()
+  AddPolarities :: InductiveId -> [Polarity] -> ResultBuilder m ()
   LookupFunctionDef :: FunctionName -> ResultBuilder m (Maybe Expression)
   LookupIdenType :: NameId -> ResultBuilder m (Maybe Expression)
-  GetCombinedInstanceTable :: ResultBuilder m InstanceTable
-  GetCombinedCoercionTable :: ResultBuilder m CoercionTable
+  GetCombinedTables :: ResultBuilder m TypeCheckingTables
 
 makeSem ''ResultBuilder
 
@@ -42,6 +42,8 @@ runResultBuilder' ::
   Sem (ResultBuilder ': r) a ->
   Sem r (ResultBuilderState, a)
 runResultBuilder' inis = reinterpret (runState inis) $ \case
+  AddPolarities name pol ->
+    overBothTables (set (typeCheckingTablesPolarityTable . polarityTable . at name) (Just pol))
   AddFunctionDef name def ->
     overBothTables (set (typeCheckingTablesFunctionsTable . functionsTable . at name) (Just def))
   AddIdenType nid ty ->
@@ -56,10 +58,8 @@ runResultBuilder' inis = reinterpret (runState inis) $ \case
     gets (^. resultBuilderStateCombinedTables . typeCheckingTablesFunctionsTable . functionsTable . at name)
   LookupIdenType nid ->
     gets (^. resultBuilderStateCombinedTables . typeCheckingTablesTypesTable . typesTable . at nid)
-  GetCombinedInstanceTable ->
-    gets (^. resultBuilderStateCombinedTables . typeCheckingTablesInstanceTable)
-  GetCombinedCoercionTable ->
-    gets (^. resultBuilderStateCombinedTables . typeCheckingTablesCoercionTable)
+  GetCombinedTables ->
+    gets (^. resultBuilderStateCombinedTables)
   where
     overBothTables :: (Members '[State ResultBuilderState] r') => (TypeCheckingTables -> TypeCheckingTables) -> Sem r' ()
     overBothTables f = modify $ \res ->
@@ -70,12 +70,12 @@ runResultBuilder' inis = reinterpret (runState inis) $ \case
 
 lookupInstanceInfo :: (Members '[ResultBuilder] r) => Name -> Sem r (Maybe [InstanceInfo])
 lookupInstanceInfo name = do
-  tab <- getCombinedInstanceTable
+  tab <- (^. typeCheckingTablesInstanceTable) <$> getCombinedTables
   return $ lookupInstanceTable tab name
 
 lookupCoercionInfo :: (Members '[ResultBuilder] r) => Name -> Sem r (Maybe [CoercionInfo])
 lookupCoercionInfo name = do
-  tab <- getCombinedCoercionTable
+  tab <- (^. typeCheckingTablesCoercionTable) <$> getCombinedTables
   return $ lookupCoercionTable tab name
 
 runResultBuilder :: ImportContext -> Sem (ResultBuilder ': r) a -> Sem r (ResultBuilderState, a)
diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error.hs
index 2f38e57bc3..8ead6846c4 100644
--- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error.hs
@@ -8,7 +8,6 @@ where
 
 import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping.Error.Types (BuiltinNotDefined)
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Error
-import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.Error
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Error.Pretty
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Error.Types
 import Juvix.Prelude
@@ -23,7 +22,7 @@ data TypeCheckerError
   | ErrTooManyArgumentsIndType WrongNumberArgumentsIndType
   | ErrTooFewArgumentsIndType WrongNumberArgumentsIndType
   | ErrInvalidPatternMatching InvalidPatternMatching
-  | ErrNonStrictlyPositive NonStrictlyPositiveError
+  | ErrNonStrictlyPositive NonStrictlyPositive
   | ErrUnsupportedTypeFunction UnsupportedTypeFunction
   | ErrInvalidInstanceType InvalidInstanceType
   | ErrInvalidCoercionType InvalidCoercionType
@@ -40,6 +39,7 @@ data TypeCheckerError
   | ErrArityCheckerError ArityCheckerError
   | ErrDefaultArgLoop DefaultArgLoop
   | ErrBadScope BadScope
+  | ErrInvalidConstructorArgType InvalidConstructorArgType
 
 instance ToGenericError TypeCheckerError where
   genericError :: (Member (Reader GenericOptions) r) => TypeCheckerError -> Sem r GenericError
@@ -52,7 +52,6 @@ instance ToGenericError TypeCheckerError where
     ErrTooManyArgumentsIndType e -> genericError e
     ErrTooFewArgumentsIndType e -> genericError e
     ErrInvalidPatternMatching e -> genericError e
-    ErrNonStrictlyPositive e -> genericError e
     ErrUnsupportedTypeFunction e -> genericError e
     ErrInvalidInstanceType e -> genericError e
     ErrInvalidCoercionType e -> genericError e
@@ -69,6 +68,8 @@ instance ToGenericError TypeCheckerError where
     ErrArityCheckerError e -> genericError e
     ErrDefaultArgLoop e -> genericError e
     ErrBadScope e -> genericError e
+    ErrInvalidConstructorArgType e -> genericError e
+    ErrNonStrictlyPositive e -> genericError e
 
 instance Show TypeCheckerError where
   show = \case
@@ -81,7 +82,6 @@ instance Show TypeCheckerError where
     ErrTooFewArgumentsIndType {} -> "ErrTooFewArgumentsIndType"
     ErrInvalidPatternMatching {} -> "ErrInvalidPatternMatching"
     ErrUnsupportedTypeFunction {} -> "ErrUnsupportedTypeFunction"
-    ErrNonStrictlyPositive {} -> "ErrNonStrictlyPositive"
     ErrInvalidInstanceType {} -> "ErrInvalidInstanceType"
     ErrInvalidCoercionType {} -> "ErrInvalidCoercionType"
     ErrWrongCoercionArgument {} -> "ErrWrongCoercionArgument"
@@ -97,3 +97,5 @@ instance Show TypeCheckerError where
     ErrDefaultArgLoop {} -> "ErrDefaultArgLoop"
     ErrBuiltinNotDefined {} -> "ErrBuiltinNotDefined"
     ErrBadScope {} -> "ErrBadScope"
+    ErrInvalidConstructorArgType {} -> "ErrInvalidConstructorArgType"
+    ErrNonStrictlyPositive {} -> "ErrNonStrictlyPositive"
diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error/Types.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error/Types.hs
index 30156e4141..e42e6835c8 100644
--- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error/Types.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error/Types.hs
@@ -665,3 +665,67 @@ instance ToGenericError BadScope where
                 <> "As a workaround, explicitly provide a type in the place where you think the variable got inserted."
                 <> line
                 <> "More information at https://github.com/anoma/juvix/issues/2247"
+
+newtype InvalidConstructorArgType = InvalidConstructorArgType
+  { _invalidConstructorArgType :: Expression
+  }
+
+makeLenses ''InvalidConstructorArgType
+
+instance ToGenericError InvalidConstructorArgType where
+  genericError e = ask >>= generr
+    where
+      generr opts =
+        return
+          GenericError
+            { _genericErrorLoc = i,
+              _genericErrorMessage = ppOutput msg,
+              _genericErrorIntervals = [i]
+            }
+        where
+          opts' = fromGenericOptions opts
+          ty = e ^. invalidConstructorArgType
+          i = getLoc ty
+          msg :: Doc Ann =
+            "The type of this constructor argument is not valid:"
+              <> line
+              <> ppCode opts' ty
+
+newtype NonStrictlyPositive = NonStrictlyPositive
+  { -- This list contains occurrences of the inductive types in non-strictly
+    -- positive positions. Thus it may contain repeated names
+    _nonStrictlyPositiveOccurrences :: NonEmpty InductiveName
+  }
+
+makeLenses ''NonStrictlyPositive
+
+instance ToGenericError NonStrictlyPositive where
+  genericError e = ask >>= generr
+    where
+      generr opts =
+        return
+          GenericError
+            { _genericErrorLoc = i,
+              _genericErrorMessage = ppOutput msg,
+              _genericErrorIntervals = map getLoc (toList occs)
+            }
+        where
+          opts' = fromGenericOptions opts
+          occs :: NonEmpty InductiveName = e ^. nonStrictlyPositiveOccurrences
+          tys = nubHashableNonEmpty occs
+          i = getLoc (tys ^. _head1)
+          msg :: Doc Ann =
+            "The positivity checker failed because the inductive"
+              <+> ( case tys of
+                      d :| [] -> "type" <+> ppCode opts' d <+> "is"
+                      _ -> "types" <> line <> itemize (ppCode opts' <$> tys) <> line <> "are"
+                  )
+              <+> "not strictly positive."
+                <> line
+                <> line
+                <> "A type D is strictly positive iff two conditions hold:"
+                <> line
+                <> itemize
+                  [ "D does not appear applied to a bound variable",
+                    "D does not appear on the left of an arrow in any argument type of its constructors"
+                  ]
diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Traits/Resolver.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Traits/Resolver.hs
index bb7c1a1517..4260821ee6 100644
--- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Traits/Resolver.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Traits/Resolver.hs
@@ -34,10 +34,11 @@ resolveTraitInstance ::
 resolveTraitInstance TypedHole {..} = do
   vars <- overM localTypes (mapM strongNormalize_) _typedHoleLocalVars
   infoTab <- ask
-  tab0 <- getCombinedInstanceTable
-  let tab = foldr (flip updateInstanceTable) tab0 (varsToInstances infoTab vars)
+  combtabs <- getCombinedTables
+  let tab0 = combtabs ^. typeCheckingTablesInstanceTable
+      tab = foldr (flip updateInstanceTable) tab0 (varsToInstances infoTab vars)
+      ctab = combtabs ^. typeCheckingTablesCoercionTable
   ty <- strongNormalize _typedHoleType
-  ctab <- getCombinedCoercionTable
   is <- lookupInstance ctab tab (ty ^. normalizedExpression)
   case is of
     [(cs, ii, subs)] ->
diff --git a/src/Juvix/Compiler/Store/Internal/Data/PolarityTable.hs b/src/Juvix/Compiler/Store/Internal/Data/PolarityTable.hs
new file mode 100644
index 0000000000..450809a4a5
--- /dev/null
+++ b/src/Juvix/Compiler/Store/Internal/Data/PolarityTable.hs
@@ -0,0 +1,18 @@
+module Juvix.Compiler.Store.Internal.Data.PolarityTable where
+
+import Juvix.Compiler.Internal.Language
+import Juvix.Extra.Serialize
+import Juvix.Prelude
+
+newtype PolarityTable = PolarityTable
+  { -- | The value should have the same length as the length of _inductiveParameters
+    _polarityTable :: HashMap InductiveId [Polarity]
+  }
+  deriving newtype (Semigroup, Monoid)
+  deriving stock (Generic)
+
+instance Serialize PolarityTable
+
+instance NFData PolarityTable
+
+makeLenses ''PolarityTable
diff --git a/src/Juvix/Compiler/Store/Internal/Data/TypeCheckingTables.hs b/src/Juvix/Compiler/Store/Internal/Data/TypeCheckingTables.hs
index 010d95ac70..d9fef9ae63 100644
--- a/src/Juvix/Compiler/Store/Internal/Data/TypeCheckingTables.hs
+++ b/src/Juvix/Compiler/Store/Internal/Data/TypeCheckingTables.hs
@@ -3,6 +3,7 @@ module Juvix.Compiler.Store.Internal.Data.TypeCheckingTables
     module Juvix.Compiler.Store.Internal.Data.CoercionInfo,
     module Juvix.Compiler.Store.Internal.Data.FunctionsTable,
     module Juvix.Compiler.Store.Internal.Data.InstanceInfo,
+    module Juvix.Compiler.Store.Internal.Data.PolarityTable,
     module Juvix.Compiler.Store.Internal.Data.TypesTable,
   )
 where
@@ -10,6 +11,7 @@ where
 import Juvix.Compiler.Store.Internal.Data.CoercionInfo
 import Juvix.Compiler.Store.Internal.Data.FunctionsTable
 import Juvix.Compiler.Store.Internal.Data.InstanceInfo
+import Juvix.Compiler.Store.Internal.Data.PolarityTable
 import Juvix.Compiler.Store.Internal.Data.TypesTable
 import Juvix.Extra.Serialize
 import Juvix.Prelude
@@ -17,6 +19,7 @@ import Juvix.Prelude
 data TypeCheckingTables = TypeCheckingTables
   { _typeCheckingTablesTypesTable :: TypesTable,
     _typeCheckingTablesFunctionsTable :: FunctionsTable,
+    _typeCheckingTablesPolarityTable :: PolarityTable,
     _typeCheckingTablesInstanceTable :: InstanceTable,
     _typeCheckingTablesCoercionTable :: CoercionTable
   }
@@ -34,6 +37,7 @@ instance Monoid TypeCheckingTables where
       { _typeCheckingTablesTypesTable = mempty,
         _typeCheckingTablesFunctionsTable = mempty,
         _typeCheckingTablesInstanceTable = mempty,
+        _typeCheckingTablesPolarityTable = mempty,
         _typeCheckingTablesCoercionTable = mempty
       }
 
@@ -42,6 +46,7 @@ instance Semigroup TypeCheckingTables where
     TypeCheckingTables
       { _typeCheckingTablesTypesTable = mappendField' typeCheckingTablesTypesTable,
         _typeCheckingTablesFunctionsTable = mappendField' typeCheckingTablesFunctionsTable,
+        _typeCheckingTablesPolarityTable = mappendField' typeCheckingTablesPolarityTable,
         _typeCheckingTablesInstanceTable = mappendField' typeCheckingTablesInstanceTable,
         _typeCheckingTablesCoercionTable = mappendField' typeCheckingTablesCoercionTable
       }
diff --git a/src/Juvix/Compiler/Store/Internal/Language.hs b/src/Juvix/Compiler/Store/Internal/Language.hs
index 1c9e5ff204..3a0b407b1b 100644
--- a/src/Juvix/Compiler/Store/Internal/Language.hs
+++ b/src/Juvix/Compiler/Store/Internal/Language.hs
@@ -53,23 +53,13 @@ computeCombinedInfoTable = mconcatMap (^. internalModuleInfoTable) . HashMap.ele
 computeTypeCheckingTables :: InternalModuleTable -> TypeCheckingTables
 computeTypeCheckingTables itab =
   TypeCheckingTables
-    { _typeCheckingTablesTypesTable = computeTypesTable,
-      _typeCheckingTablesInstanceTable = computeInstanceTable,
-      _typeCheckingTablesFunctionsTable = computeFunctionsTable,
-      _typeCheckingTablesCoercionTable = computeCoercionTable
+    { _typeCheckingTablesTypesTable = computeTable typeCheckingTablesTypesTable,
+      _typeCheckingTablesInstanceTable = computeTable typeCheckingTablesInstanceTable,
+      _typeCheckingTablesFunctionsTable = computeTable typeCheckingTablesFunctionsTable,
+      _typeCheckingTablesPolarityTable = computeTable typeCheckingTablesPolarityTable,
+      _typeCheckingTablesCoercionTable = computeTable typeCheckingTablesCoercionTable
     }
   where
-    computeTypesTable :: TypesTable
-    computeTypesTable = mconcatMap (^. internalModuleTypeCheckingTables . typeCheckingTablesTypesTable) (itab ^. internalModuleTable)
-
-    computeFunctionsTable :: FunctionsTable
-    computeFunctionsTable =
-      mconcatMap
-        (^. internalModuleTypeCheckingTables . typeCheckingTablesFunctionsTable)
-        (itab ^. internalModuleTable)
-
-    computeInstanceTable :: InstanceTable
-    computeInstanceTable = mconcatMap (^. internalModuleTypeCheckingTables . typeCheckingTablesInstanceTable) (itab ^. internalModuleTable)
-
-    computeCoercionTable :: CoercionTable
-    computeCoercionTable = mconcatMap (^. internalModuleTypeCheckingTables . typeCheckingTablesCoercionTable) (itab ^. internalModuleTable)
+    computeTable :: (Monoid tbl) => Lens' TypeCheckingTables tbl -> tbl
+    computeTable l =
+      mconcatMap (^. internalModuleTypeCheckingTables . l) (itab ^. internalModuleTable)
diff --git a/src/Juvix/Data.hs b/src/Juvix/Data.hs
index 80d71a58cc..dad143f1c7 100644
--- a/src/Juvix/Data.hs
+++ b/src/Juvix/Data.hs
@@ -23,6 +23,7 @@ module Juvix.Data
     module Juvix.Data.DependencyInfo,
     module Juvix.Data.TopModulePathKey,
     module Juvix.Data.Keyword,
+    module Juvix.Data.Polarity,
   )
 where
 
@@ -41,6 +42,7 @@ import Juvix.Data.Loc
 import Juvix.Data.Logger
 import Juvix.Data.NameId qualified
 import Juvix.Data.NumThreads
+import Juvix.Data.Polarity
 import Juvix.Data.Pragmas
 import Juvix.Data.Processed
 import Juvix.Data.ProjectionKind
diff --git a/src/Juvix/Data/Polarity.hs b/src/Juvix/Data/Polarity.hs
new file mode 100644
index 0000000000..ca68cc61e7
--- /dev/null
+++ b/src/Juvix/Data/Polarity.hs
@@ -0,0 +1,30 @@
+module Juvix.Data.Polarity where
+
+import Juvix.Extra.Serialize
+import Juvix.Prelude.Base
+import Juvix.Prelude.Pretty
+
+-- | NOTE that Order of constructors is relevant for the derived instances
+data Polarity
+  = PolarityUnused
+  | PolarityStrictlyPositive
+  | PolarityNonStrictlyPositive
+  deriving stock (Ord, Enum, Bounded, Eq, Generic, Data, Show)
+
+instance Hashable Polarity
+
+instance Serialize Polarity
+
+instance NFData Polarity
+
+instance Semigroup Polarity where
+  a <> b = max a b
+
+instance Monoid Polarity where
+  mempty = PolarityUnused
+
+instance Pretty Polarity where
+  pretty = \case
+    PolarityNonStrictlyPositive -> "non-strictly-positive"
+    PolarityStrictlyPositive -> "strictly-positive"
+    PolarityUnused -> "unused"
diff --git a/src/Juvix/Prelude/Base/Foundation.hs b/src/Juvix/Prelude/Base/Foundation.hs
index 23dc232e1e..bb84182627 100644
--- a/src/Juvix/Prelude/Base/Foundation.hs
+++ b/src/Juvix/Prelude/Base/Foundation.hs
@@ -447,6 +447,20 @@ zip4Exact [] [] [] [] = []
 zip4Exact (x1 : t1) (x2 : t2) (x3 : t3) (x4 : t4) = (x1, x2, x3, x4) : zip4Exact t1 t2 t3 t4
 zip4Exact _ _ _ _ = error "zip4Exact"
 
+-- | Returns the first element that returns Just and the list with the remaining elements
+findJustAndRemove :: forall a b. (a -> Maybe b) -> [a] -> Maybe (b, [a])
+findJustAndRemove p = go []
+  where
+    go :: [a] -> [a] -> Maybe (b, [a])
+    go acc = \case
+      [] -> Nothing
+      x : xs -> case p x of
+        Just b -> Just (b, reverse acc ++ xs)
+        Nothing -> go (x : acc) xs
+
+findAndRemove :: (a -> Bool) -> [a] -> Maybe (a, [a])
+findAndRemove p = findJustAndRemove (\a -> guard (p a) $> a)
+
 --------------------------------------------------------------------------------
 -- NonEmpty
 --------------------------------------------------------------------------------
@@ -598,6 +612,9 @@ massert b = assert b (pure ())
 iterateN :: Int -> (a -> a) -> a -> a
 iterateN n f = (!! n) . iterate f
 
+nubHashableNonEmpty :: (Hashable a) => NonEmpty a -> NonEmpty a
+nubHashableNonEmpty = nonEmpty' . HashSet.toList . HashSet.fromList . toList
+
 nubHashable :: (Hashable a) => [a] -> [a]
 nubHashable = HashSet.toList . HashSet.fromList
 
diff --git a/test/Typecheck/Negative.hs b/test/Typecheck/Negative.hs
index 9c957268ba..b4557189d0 100644
--- a/test/Typecheck/Negative.hs
+++ b/test/Typecheck/Negative.hs
@@ -1,7 +1,6 @@
 module Typecheck.Negative where
 
 import Base
-import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.Error
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Error
 
 type FailMsg = String
@@ -268,48 +267,22 @@ tests =
 
 negPositivityTests :: [NegTest]
 negPositivityTests =
-  [ negTest "E1" $(mkRelDir "Internal/Positivity") $(mkRelFile "E1.juvix") $
-      \case
-        ErrNonStrictlyPositive ErrTypeInNegativePosition {} -> Nothing
-        _ -> wrongError,
-    negTest "E2" $(mkRelDir "Internal/Positivity") $(mkRelFile "E2.juvix") $
-      \case
-        ErrNonStrictlyPositive (ErrTypeInNegativePosition {}) -> Nothing
-        _ -> wrongError,
-    negTest "E3" $(mkRelDir "Internal/Positivity") $(mkRelFile "E3.juvix") $
-      \case
-        ErrNonStrictlyPositive (ErrTypeInNegativePosition {}) -> Nothing
-        _ -> wrongError,
-    negTest "E4" $(mkRelDir "Internal/Positivity") $(mkRelFile "E4.juvix") $
-      \case
-        ErrNonStrictlyPositive (ErrTypeInNegativePosition {}) -> Nothing
-        _ -> wrongError,
-    negTest "E5" $(mkRelDir "Internal/Positivity") $(mkRelFile "E5.juvix") $
-      \case
-        ErrNonStrictlyPositive (ErrTypeInNegativePosition {}) -> Nothing
-        _ -> wrongError,
-    negTest "E6" $(mkRelDir "Internal/Positivity") $(mkRelFile "E6.juvix") $
-      \case
-        ErrNonStrictlyPositive (ErrTypeInNegativePosition {}) -> Nothing
-        _ -> wrongError,
-    negTest "E7" $(mkRelDir "Internal/Positivity") $(mkRelFile "E7.juvix") $
-      \case
-        ErrNonStrictlyPositive (ErrTypeInNegativePosition {}) -> Nothing
-        _ -> wrongError,
-    negTest "E8" $(mkRelDir "Internal/Positivity") $(mkRelFile "E8.juvix") $
-      \case
-        ErrNonStrictlyPositive (ErrTypeInNegativePosition {}) -> Nothing
-        _ -> wrongError,
-    negTest "E9" $(mkRelDir "Internal/Positivity") $(mkRelFile "E9.juvix") $
-      \case
-        ErrNonStrictlyPositive (ErrTypeInNegativePosition {}) -> Nothing
-        _ -> wrongError,
-    negTest "E10 uses type synonym" $(mkRelDir "Internal/Positivity") $(mkRelFile "E10.juvix") $
-      \case
-        ErrNonStrictlyPositive (ErrTypeInNegativePosition {}) -> Nothing
-        _ -> wrongError,
-    negTest "E11 uses type synonym" $(mkRelDir "Internal/Positivity") $(mkRelFile "E11.juvix") $
+  [ mk "E1" $(mkRelFile "E1.juvix"),
+    mk "E2" $(mkRelFile "E2.juvix"),
+    mk "E3" $(mkRelFile "E3.juvix"),
+    mk "E4" $(mkRelFile "E4.juvix"),
+    mk "E5" $(mkRelFile "E5.juvix"),
+    mk "E6" $(mkRelFile "E6.juvix"),
+    mk "E7" $(mkRelFile "E7.juvix"),
+    mk "E8" $(mkRelFile "E8.juvix"),
+    mk "E9" $(mkRelFile "E9.juvix"),
+    mk "E10 uses type synonym" $(mkRelFile "E10.juvix"),
+    mk "E11 uses type synonym" $(mkRelFile "E11.juvix"),
+    mk "Box left hand side" $(mkRelFile "box.juvix")
+  ]
+  where
+    mk :: String -> Path Rel File -> NegTest
+    mk testname testfile = negTest testname $(mkRelDir "Internal/Positivity") testfile $
       \case
-        ErrNonStrictlyPositive (ErrTypeInNegativePosition {}) -> Nothing
+        ErrNonStrictlyPositive NonStrictlyPositive {} -> Nothing
         _ -> wrongError
-  ]
diff --git a/test/Typecheck/NegativeNew.hs b/test/Typecheck/NegativeNew.hs
index 3fcfb9a8a0..c705bd5ab9 100644
--- a/test/Typecheck/NegativeNew.hs
+++ b/test/Typecheck/NegativeNew.hs
@@ -2,7 +2,6 @@ module Typecheck.NegativeNew where
 
 import Base
 import Data.HashSet qualified as HashSet
-import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.Error
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Error
 import Typecheck.Negative qualified as Old
 
@@ -149,14 +148,14 @@ arityTests =
         _ -> wrongError,
     negTest "Evil: issue 2540" $(mkRelDir "Internal/Positivity") $(mkRelFile "Evil.juvix") $
       \case
-        ErrNonStrictlyPositive ErrTypeAsArgumentOfBoundVar {} -> Nothing
+        ErrNonStrictlyPositive {} -> Nothing
         _ -> wrongError,
     negTest "Evil: issue 2540 using Axiom" $(mkRelDir "Internal/Positivity") $(mkRelFile "EvilWithAxiom.juvix") $
       \case
-        ErrNonStrictlyPositive (ErrTypeAsArgumentOfBoundVar {}) -> Nothing
+        ErrNonStrictlyPositive {} -> Nothing
         _ -> wrongError,
     negTest "FreeT: issue 2540" $(mkRelDir "Internal/Positivity") $(mkRelFile "FreeT.juvix") $
       \case
-        ErrNonStrictlyPositive (ErrTypeAsArgumentOfBoundVar {}) -> Nothing
+        ErrNonStrictlyPositive {} -> Nothing
         _ -> wrongError
   ]
diff --git a/test/Typecheck/Positive.hs b/test/Typecheck/Positive.hs
index 55928a82c8..459f51f881 100644
--- a/test/Typecheck/Positive.hs
+++ b/test/Typecheck/Positive.hs
@@ -57,12 +57,21 @@ testNoPositivityFlag N.NegTest {..} =
 negPositivityTests :: [N.NegTest]
 negPositivityTests = N.negPositivityTests
 
+-- | Positive tests for the positivity checker
 testWellDefinedInductiveDefs :: [PosTest]
 testWellDefinedInductiveDefs =
   [ posTest
       "Rose tree definition is well-defined"
       $(mkRelDir "Internal/Positivity")
-      $(mkRelFile "RoseTree.juvix")
+      $(mkRelFile "RoseTree.juvix"),
+    posTest
+      "Mutually recursive types and phantom types"
+      $(mkRelDir "Internal/Positivity2")
+      $(mkRelFile "main.juvix"),
+    posTest
+      "Issue 3048"
+      $(mkRelDir "issue3048")
+      $(mkRelFile "main.juvix")
   ]
 
 testPositivityKeyword :: [PosTest]
diff --git a/tests/Compilation/positive/test079.juvix b/tests/Compilation/positive/test079.juvix
index 0c09c285da..0520475b28 100644
--- a/tests/Compilation/positive/test079.juvix
+++ b/tests/Compilation/positive/test079.juvix
@@ -7,10 +7,10 @@ type Nat :=
   | zero
   | suc Nat;
 
-type Foldable := mkFoldable {for : {B : Type} -> (B -> Nat -> B) -> B -> Box -> B};
-
 type Box := mkBox {unbox : Nat};
 
+type Foldable := mkFoldable {for : {B : Type} -> (B -> Nat -> B) -> B -> Box -> B};
+
 one : Nat := zero;
 
 open Foldable public;
diff --git a/tests/negative/Internal/Positivity/box.juvix b/tests/negative/Internal/Positivity/box.juvix
new file mode 100644
index 0000000000..d1085aed02
--- /dev/null
+++ b/tests/negative/Internal/Positivity/box.juvix
@@ -0,0 +1,5 @@
+module box;
+
+type Box (A : Type) := mkBox A;
+
+type P (A : Type) := mkP : (Box (P A) -> P A) -> P A;
diff --git a/tests/positive/Internal/Positivity2/Package.juvix b/tests/positive/Internal/Positivity2/Package.juvix
new file mode 100644
index 0000000000..dc768cdde3
--- /dev/null
+++ b/tests/positive/Internal/Positivity2/Package.juvix
@@ -0,0 +1,9 @@
+module Package;
+
+import PackageDescription.V2 open;
+
+package : Package :=
+  defaultPackage@?{
+    name := "positivity2";
+    dependencies := []
+  };
diff --git a/tests/positive/Internal/Positivity2/main.juvix b/tests/positive/Internal/Positivity2/main.juvix
new file mode 100644
index 0000000000..d46d62baec
--- /dev/null
+++ b/tests/positive/Internal/Positivity2/main.juvix
@@ -0,0 +1,58 @@
+module main;
+
+type T := mkT;
+
+type Phantom (H : Type) := phantom;
+
+type Phantom2 (H : Type) := phantom2 (Phantom H);
+
+type Box (A : Type) := box A;
+
+module M1;
+  type T1 (x y : Type) := mkT1 y (x -> x) x;
+  type T2 (x : (Type -> Type) -> Type) := mkT2 (x (T1 T));
+end;
+
+module M2;
+  type T1 (x : Type) := mkT1 (T2 x);
+
+  type T2 (x : Type) := mkT2 (x -> T);
+
+  -- type T3 := mkT3 (T1 T3);
+end;
+
+module M3;
+  type List (x : Type) :=
+    | nil
+    | cons x (List x);
+end;
+
+module E1;
+  type Alice (A : Type) := alice (Phantom2 (Alice A) -> Alice A);
+
+  type Bob (C : Type) := bob (Carol C) (Bob C) (Phantom (Bob C) -> T);
+
+  type Carol (C : Type) := carol (Alice C);
+end;
+
+module E3;
+  type NotBad (A : Type) := notBad (A -> NotBad A);
+end;
+
+module E5;
+  type Ghost1 (A : Type) := ghost1 (Ghost2 ((Ghost1 (A -> A)) -> Ghost2 A));
+
+  type Ghost2 (B : Type) := ghost2 Ok (Ghost1 B);
+
+  type Ok  := mkOk (Ghost1 (Ok -> Ok));
+end;
+
+module E6;
+  type Nat :=
+    | zero
+    | suc Nat;
+
+  type Box := mkBox {unbox : Nat};
+
+  type Foldable := mkFoldable {for : {B : Type} -> (B -> Nat -> B) -> B -> Box -> B};
+end;
diff --git a/tests/positive/issue3048/Other.juvix b/tests/positive/issue3048/Other.juvix
new file mode 100644
index 0000000000..e947739e98
--- /dev/null
+++ b/tests/positive/issue3048/Other.juvix
@@ -0,0 +1,5 @@
+module Other;
+
+type T1 := mkT1;
+type T2 := mkT2;
+type T3 := mkT3;
diff --git a/tests/positive/issue3048/Package.juvix b/tests/positive/issue3048/Package.juvix
new file mode 100644
index 0000000000..6e4702c194
--- /dev/null
+++ b/tests/positive/issue3048/Package.juvix
@@ -0,0 +1,10 @@
+module Package;
+
+import PackageDescription.V2 open;
+
+package : Package :=
+  defaultPackage@?{
+    name := "issue3048";
+    dependencies :=
+      [github "anoma" "juvix-stdlib" "v0.7.0"; github "anoma" "juvix-containers" "v0.15.0"]
+  };
diff --git a/tests/positive/issue3048/main.juvix b/tests/positive/issue3048/main.juvix
new file mode 100644
index 0000000000..4681b7ecb9
--- /dev/null
+++ b/tests/positive/issue3048/main.juvix
@@ -0,0 +1,16 @@
+module main;
+
+import Other;
+
+type AVLTree (A : Type) :=
+  node (AVLTree A)
+       (AVLTree A)
+       (AVLTree A)
+       (AVLTree A)
+       (AVLTree A)
+       (AVLTree A)
+       (AVLTree A)
+       (AVLTree A)
+       (AVLTree A);
+
+type Foo := mkFoo (AVLTree Foo);