Add new case for positivity checker: type cannot occur as arg of bound var (#2542)

This PR fixes our positivity checker to support inductive definitions with type families as type parameters. This kind of ind. type is type-checked using the global flag `--new-type checker.` For example, the following definition is not allowed: ``` module Evil; type Evil (f : Type -> Type) := magic : f (Evil f) -> Evil f; ``` - Closes #2540
2025-01-05 22:46:08 +03:00 · 2023-11-30 15:03:54 +01:00 · 2023-11-30 15:03:54 +01:00 · 7de9f2f0f3
commit 7de9f2f0f3
parent ca7d0fa06d
13 changed files with 287 additions and 149 deletions
--- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity.hs
@ -1,6 +1,8 @@
 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
--- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Checker.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Checker.hs
@ -1,10 +1,10 @@
-- | Checker for strictly positive inductive data types
 module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.Checker 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.Translation.FromInternal.Analysis.TypeChecking.Data.Inference
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Error
 import Juvix.Compiler.Pipeline.EntryPoint qualified as E
@ -12,12 +12,6 @@ import Juvix.Prelude hiding (fromEither)

 type NegativeTypeParameters = HashSet VarName

-type ErrorReference = Maybe Expression
-
-type TypeOfConstructor = Expression
-
-type RecursionLimit = Int
-
 type CheckPositivityEffects r =
  Members
    '[ Reader E.EntryPoint,
@ -28,157 +22,201 @@ type CheckPositivityEffects r =
     ]
    r

+data CheckPositivityArgs = CheckPositivityArgs
+  { _checkPositivityArgsInductive :: InductiveDef,
+    _checkPositivityArgsConstructorName :: Name,
+    _checkPositivityArgsInductiveName :: Name,
+    _checkPositivityArgsRecursionLimit :: Int,
+    _checkPositivityArgsErrorReference :: Maybe Expression,
+    _checkPositivityArgsTypeOfConstructor :: Expression
+  }
+
+makeLenses ''CheckPositivityArgs
+
 checkPositivity ::
  forall r.
  (CheckPositivityEffects 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
-        args = constructorArgs (ctor ^. inductiveConstructorType)
-    unless (noCheckPositivity || ty ^. inductivePositive) $
-      forM_
-        args
-        (checkStrictlyPositiveOccurrences ty ctorName indName numInductives Nothing)
+  unlessM (asks (^. E.entryPointNoPositivity)) $
+    forM_ (ty ^. inductiveConstructors) $ \ctor -> do
+      unless (ty ^. inductivePositive) $ do
+        numInductives <- HashMap.size <$> asks (^. infoInductives)
+        forM_
+          (constructorArgs (ctor ^. inductiveConstructorType))
+          $ \typeOfConstr ->
+            checkStrictlyPositiveOccurrences
+              ( CheckPositivityArgs
+                  { _checkPositivityArgsInductive = ty,
+                    _checkPositivityArgsConstructorName =
+                      ctor ^. inductiveConstructorName,
+                    _checkPositivityArgsInductiveName = ty ^. inductiveName,
+                    _checkPositivityArgsRecursionLimit = numInductives,
+                    _checkPositivityArgsErrorReference = Nothing,
+                    _checkPositivityArgsTypeOfConstructor = typeOfConstr
+                  }
+              )

 checkStrictlyPositiveOccurrences ::
  forall r.
  (CheckPositivityEffects r) =>
-  InductiveDef ->
-  ConstrName ->
-  Name ->
-  RecursionLimit ->
-  ErrorReference ->
-  TypeOfConstructor ->
+  CheckPositivityArgs ->
  Sem r ()
-checkStrictlyPositiveOccurrences ty ctorName name recLimit ref =
-  strongNormalize >=> helper False
+checkStrictlyPositiveOccurrences p = do
+  typeOfConstr <- strongNormalize (p ^. checkPositivityArgsTypeOfConstructor)
+  go False typeOfConstr
  where
+    ty = p ^. checkPositivityArgsInductive
+    ctorName = p ^. checkPositivityArgsConstructorName
+    name = p ^. checkPositivityArgsInductiveName
+    recLimit = p ^. checkPositivityArgsRecursionLimit
+    ref = p ^. checkPositivityArgsErrorReference
+
    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
-      ExpressionApplication tyApp -> helperApp tyApp
-      ExpressionCase l -> helperCase l
-      ExpressionFunction (Function l r) -> helper True (l ^. paramType) >> helper inside r
+    {- The following `go` 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.
+    -}
+    go :: Bool -> Expression -> Sem r ()
+    go inside expr = case expr of
+      ExpressionApplication tyApp -> goApp tyApp
+      ExpressionCase l -> goCase l
+      ExpressionFunction (Function l r) -> go True (l ^. paramType) >> go inside r
      ExpressionHole {} -> return ()
      ExpressionInstanceHole {} -> return ()
-      ExpressionIden i -> helperIden i
-      ExpressionLambda l -> helperLambda l
-      ExpressionLet l -> helperLet l
+      ExpressionIden i -> goIden i
+      ExpressionLambda l -> goLambda l
+      ExpressionLet l -> goLet l
      ExpressionLiteral {} -> return ()
-      ExpressionSimpleLambda l -> helperSimpleLambda l
+      ExpressionSimpleLambda l -> goSimpleLambda l
      ExpressionUniverse {} -> return ()
      where
-        helperCase :: Case -> Sem r ()
-        helperCase l = do
-          helper inside (l ^. caseExpression)
-          mapM_ helperCaseBranch (l ^. caseBranches)
+        goCase :: Case -> Sem r ()
+        goCase l = do
+          go inside (l ^. caseExpression)
+          mapM_ goCaseBranch (l ^. caseBranches)

-        helperCaseBranch :: CaseBranch -> Sem r ()
-        helperCaseBranch b = helper inside (b ^. caseBranchExpression)
+        goCaseBranch :: CaseBranch -> Sem r ()
+        goCaseBranch b = go inside (b ^. caseBranchExpression)

-        helperLet :: Let -> Sem r ()
-        helperLet l = do
-          helper inside (l ^. letExpression)
-          mapM_ helperLetClause (l ^. letClauses)
+        goLet :: Let -> Sem r ()
+        goLet l = do
+          go inside (l ^. letExpression)
+          mapM_ goLetClause (l ^. letClauses)

-        helperLetClause :: LetClause -> Sem r ()
-        helperLetClause = \case
-          LetFunDef f -> helperFunctionDef f
-          LetMutualBlock b -> helperMutualBlockLet b
+        goLetClause :: LetClause -> Sem r ()
+        goLetClause = \case
+          LetFunDef f -> goFunctionDef f
+          LetMutualBlock b -> goMutualBlockLet b

-        helperMutualBlockLet :: MutualBlockLet -> Sem r ()
-        helperMutualBlockLet b = mapM_ helperFunctionDef (b ^. mutualLet)
+        goMutualBlockLet :: MutualBlockLet -> Sem r ()
+        goMutualBlockLet b = mapM_ goFunctionDef (b ^. mutualLet)

-        helperFunctionDef :: FunctionDef -> Sem r ()
-        helperFunctionDef d = do
-          helper inside (d ^. funDefType)
-          helper inside (d ^. funDefBody)
+        goFunctionDef :: FunctionDef -> Sem r ()
+        goFunctionDef d = do
+          go inside (d ^. funDefType)
+          go inside (d ^. funDefBody)

-        helperSimpleLambda :: SimpleLambda -> Sem r ()
-        helperSimpleLambda (SimpleLambda (SimpleBinder _ lamVarTy) lamBody) = do
-          helper inside lamVarTy
-          helper inside lamBody
+        goSimpleLambda :: SimpleLambda -> Sem r ()
+        goSimpleLambda (SimpleLambda (SimpleBinder _ lamVarTy) lamBody) = do
+          go inside lamVarTy
+          go inside lamBody

-        helperLambda :: Lambda -> Sem r ()
-        helperLambda l = mapM_ goClause (l ^. lambdaClauses)
+        goLambda :: Lambda -> Sem r ()
+        goLambda l = mapM_ goClause (l ^. lambdaClauses)
          where
            goClause :: LambdaClause -> Sem r ()
-            goClause (LambdaClause _ b) = helper inside b
+            goClause (LambdaClause _ b) = go inside b

-        helperIden :: Iden -> Sem r ()
-        helperIden = \case
+        goIden :: Iden -> Sem r ()
+        goIden = \case
          IdenInductive ty' ->
-            when (inside && name == ty') (strictlyPositivityError expr)
+            when (inside && name == ty') (throwNegativePositonError expr)
          IdenVar name'
            | not inside -> return ()
-            | name == name' -> strictlyPositivityError expr
+            | name == name' -> throwNegativePositonError expr
            | name' `elem` ty ^.. inductiveParameters . each . inductiveParamName -> modify (HashSet.insert name')
          _ -> return ()

-        helperApp :: Application -> Sem r ()
-        helperApp tyApp = do
+        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') (strictlyPositivityError expr)
+              when (inside && name == ty') (throwNegativePositonError expr)
              InductiveInfo indType' <- 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.
-
+              {- 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' = indType' ^. inductiveParameters
-              helperInductiveApp indType' (zip paramsTy' (toList args))
+              goInductiveApp indType' (zip paramsTy' (toList args))
            _ -> return ()

-        helperInductiveApp :: InductiveDef -> [(InductiveParameter, Expression)] -> Sem r ()
-        helperInductiveApp indType' = \case
+        goInductiveApp :: InductiveDef -> [(InductiveParameter, Expression)] -> Sem r ()
+        goInductiveApp indType' = \case
+          [] -> return ()
          (InductiveParameter pName' _ty', tyArg) : ps -> do
-            -- TODO handle _ty'
            negParms :: NegativeTypeParameters <- get
            when (varOrInductiveInExpression name tyArg) $ do
-              when (HashSet.member pName' negParms) (strictlyPositivityError tyArg)
+              when
+                (HashSet.member pName' negParms)
+                (throwNegativePositonError tyArg)
              when (recLimit > 0) $
                forM_ (indType' ^. inductiveConstructors) $ \ctor' -> do
                  let ctorName' = ctor' ^. inductiveConstructorName
                      errorRef = fromMaybe tyArg ref
                      args = constructorArgs (ctor' ^. inductiveConstructorType)
                  mapM_
-                    ( checkStrictlyPositiveOccurrences
-                        indType'
-                        ctorName'
-                        pName'
-                        (recLimit - 1)
-                        (Just errorRef)
+                    ( \tyConstr' ->
+                        checkStrictlyPositiveOccurrences
+                          CheckPositivityArgs
+                            { _checkPositivityArgsInductive = indType',
+                              _checkPositivityArgsConstructorName = ctorName',
+                              _checkPositivityArgsInductiveName = pName',
+                              _checkPositivityArgsRecursionLimit = recLimit - 1,
+                              _checkPositivityArgsErrorReference = Just errorRef,
+                              _checkPositivityArgsTypeOfConstructor = tyConstr'
+                            }
                    )
                    args
-            helperInductiveApp indType' ps
-          [] -> return ()
+            goInductiveApp indType' ps

-    strictlyPositivityError :: Expression -> Sem r ()
-    strictlyPositivityError expr = do
+    throwNegativePositonError :: Expression -> Sem r ()
+    throwNegativePositonError expr = do
      let errLoc = fromMaybe expr ref
      throw
-        ( ErrNoPositivity $
-            NoPositivity
-              { _noStrictPositivityType = indName,
-                _noStrictPositivityConstructor = ctorName,
-                _noStrictPositivityArgument = errLoc
-              }
-        )
+        . 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
--- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Error.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Error.hs
@ -0,0 +1,18 @@
+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
--- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Error/Types.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Error/Types.hs
@ -0,0 +1,75 @@
+module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.Error.Types where
+
+import Juvix.Compiler.Internal.Extra
+import Juvix.Compiler.Internal.Pretty (fromGenericOptions)
+import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Error.Pretty
+import Juvix.Data.PPOutput
+import Juvix.Prelude
+
+data TypeInNegativePosition = TypeInNegativePosition
+  { _typeInNegativePositionType :: Name,
+    _typeInNegativePositionConstructor :: Name,
+    _typeInNegativePositionArgument :: Expression
+  }
+
+makeLenses ''TypeInNegativePosition
+
+instance ToGenericError TypeInNegativePosition where
+  genericError e = ask >>= generr
+    where
+      generr opts =
+        return
+          GenericError
+            { _genericErrorLoc = j,
+              _genericErrorMessage = ppOutput msg,
+              _genericErrorIntervals = [i, j]
+            }
+        where
+          opts' = fromGenericOptions opts
+          ty = e ^. typeInNegativePositionType
+          ctor = e ^. typeInNegativePositionConstructor
+          arg = e ^. typeInNegativePositionArgument
+          i = getLoc ty
+          j = getLoc arg
+          msg =
+            "The type"
+              <+> ppCode opts' ty
+              <+> "is not strictly positive."
+                <> line
+                <> "It appears at a negative position in one of the type arguments of the constructor"
+              <+> ppCode opts' ctor <> "."
+
+data TypeAsArgumentOfBoundVar = TypeAsArgumentOfBoundVar
+  { _typeAsArgumentOfBoundVarType :: Name,
+    _typeAsArgumentOfBoundVarConstructor :: Name,
+    _typeAsArgumentOfBoundVarReference :: Expression
+  }
+
+makeLenses ''TypeAsArgumentOfBoundVar
+
+instance ToGenericError TypeAsArgumentOfBoundVar where
+  genericError e = ask >>= generr
+    where
+      generr opts =
+        return
+          GenericError
+            { _genericErrorLoc = j,
+              _genericErrorMessage = ppOutput msg,
+              _genericErrorIntervals = [i, j]
+            }
+        where
+          opts' = fromGenericOptions opts
+          ty = e ^. typeAsArgumentOfBoundVarType
+          ctor = e ^. typeAsArgumentOfBoundVarConstructor
+          var = e ^. typeAsArgumentOfBoundVarReference
+          i = getLoc ty
+          j = getLoc var
+          msg =
+            "The type"
+              <+> ppCode opts' ty
+              <+> "is not strictly positive."
+                <> line
+                <> "It appears as an argument of the bound variable"
+              <+> ppCode opts' var
+              <+> "in one of the type arguments of the constructor"
+              <+> ppCode opts' ctor <> "."
--- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error.hs
@ -7,6 +7,7 @@ module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Er
 where

 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
@ -21,7 +22,7 @@ data TypeCheckerError
  | ErrTooManyArgumentsIndType WrongNumberArgumentsIndType
  | ErrTooFewArgumentsIndType WrongNumberArgumentsIndType
  | ErrInvalidPatternMatching InvalidPatternMatching
-  | ErrNoPositivity NoPositivity
+  | ErrNonStrictlyPositive NonStrictlyPositiveError
  | ErrUnsupportedTypeFunction UnsupportedTypeFunction
  | ErrInvalidInstanceType InvalidInstanceType
  | ErrInvalidCoercionType InvalidCoercionType
@ -48,7 +49,7 @@ instance ToGenericError TypeCheckerError where
    ErrTooManyArgumentsIndType e -> genericError e
    ErrTooFewArgumentsIndType e -> genericError e
    ErrInvalidPatternMatching e -> genericError e
-    ErrNoPositivity e -> genericError e
+    ErrNonStrictlyPositive e -> genericError e
    ErrUnsupportedTypeFunction e -> genericError e
    ErrInvalidInstanceType e -> genericError e
    ErrInvalidCoercionType e -> genericError e
@ -74,8 +75,8 @@ instance Show TypeCheckerError where
    ErrTooManyArgumentsIndType {} -> "ErrTooManyArgumentsIndType"
    ErrTooFewArgumentsIndType {} -> "ErrTooFewArgumentsIndType"
    ErrInvalidPatternMatching {} -> "ErrInvalidPatternMatching"
-    ErrNoPositivity {} -> "ErrNoPositivity"
    ErrUnsupportedTypeFunction {} -> "ErrUnsupportedTypeFunction"
+    ErrNonStrictlyPositive {} -> "ErrNonStrictlyPositive"
    ErrInvalidInstanceType {} -> "ErrInvalidInstanceType"
    ErrInvalidCoercionType {} -> "ErrInvalidCoercionType"
    ErrWrongCoercionArgument {} -> "ErrWrongCoercionArgument"
--- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error/Types.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error/Types.hs
@ -307,39 +307,6 @@ instance ToGenericError InvalidPatternMatching where
              <+> "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 = ask >>= generr
-    where
-      generr opts =
-        return
-          GenericError
-            { _genericErrorLoc = j,
-              _genericErrorMessage = ppOutput msg,
-              _genericErrorIntervals = [i, j]
-            }
-        where
-          opts' = fromGenericOptions opts
-          ty = e ^. noStrictPositivityType
-          ctor = e ^. noStrictPositivityConstructor
-          arg = e ^. noStrictPositivityArgument
-          i = getLoc ty
-          j = getLoc arg
-          msg =
-            "The type"
-              <+> ppCode opts' ty
-              <+> "is not strictly positive."
-                <> line
-                <> "It appears at a negative position in one of the arguments of the constructor"
-              <+> ppCode opts' ctor <> "."
-
 newtype UnsupportedTypeFunction = UnsupportedTypeFunction
  { _unsupportedTypeFunction :: FunctionDef
  }
--- a/test/Typecheck/Negative.hs
+++ b/test/Typecheck/Negative.hs
@ -1,6 +1,7 @@
 module Typecheck.Negative where

 import Base
+import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.Error
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Error
 import Juvix.Data.Effect.TaggedLock

@ -263,38 +264,46 @@ negPositivityTests :: [NegTest]
 negPositivityTests =
  [ negTest "E1" $(mkRelDir "Internal/Positivity") $(mkRelFile "E1.juvix") $
      \case
-        ErrNoPositivity {} -> Nothing
+        ErrNonStrictlyPositive ErrTypeInNegativePosition {} -> Nothing
        _ -> wrongError,
    negTest "E2" $(mkRelDir "Internal/Positivity") $(mkRelFile "E2.juvix") $
      \case
-        ErrNoPositivity {} -> Nothing
+        ErrNonStrictlyPositive (ErrTypeInNegativePosition {}) -> Nothing
        _ -> wrongError,
    negTest "E3" $(mkRelDir "Internal/Positivity") $(mkRelFile "E3.juvix") $
      \case
-        ErrNoPositivity {} -> Nothing
+        ErrNonStrictlyPositive (ErrTypeInNegativePosition {}) -> Nothing
        _ -> wrongError,
    negTest "E4" $(mkRelDir "Internal/Positivity") $(mkRelFile "E4.juvix") $
      \case
-        ErrNoPositivity {} -> Nothing
+        ErrNonStrictlyPositive (ErrTypeInNegativePosition {}) -> Nothing
        _ -> wrongError,
    negTest "E5" $(mkRelDir "Internal/Positivity") $(mkRelFile "E5.juvix") $
      \case
-        ErrNoPositivity {} -> Nothing
+        ErrNonStrictlyPositive (ErrTypeInNegativePosition {}) -> Nothing
        _ -> wrongError,
    negTest "E6" $(mkRelDir "Internal/Positivity") $(mkRelFile "E6.juvix") $
      \case
-        ErrNoPositivity {} -> Nothing
+        ErrNonStrictlyPositive (ErrTypeInNegativePosition {}) -> Nothing
        _ -> wrongError,
    negTest "E7" $(mkRelDir "Internal/Positivity") $(mkRelFile "E7.juvix") $
      \case
-        ErrNoPositivity {} -> Nothing
+        ErrNonStrictlyPositive (ErrTypeInNegativePosition {}) -> Nothing
        _ -> wrongError,
    negTest "E8" $(mkRelDir "Internal/Positivity") $(mkRelFile "E8.juvix") $
      \case
-        ErrNoPositivity {} -> Nothing
+        ErrNonStrictlyPositive (ErrTypeInNegativePosition {}) -> Nothing
        _ -> wrongError,
    negTest "E9" $(mkRelDir "Internal/Positivity") $(mkRelFile "E9.juvix") $
      \case
-        ErrNoPositivity {} -> Nothing
+        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") $
+      \case
+        ErrNonStrictlyPositive (ErrTypeInNegativePosition {}) -> Nothing
        _ -> wrongError
  ]
--- a/test/Typecheck/NegativeNew.hs
+++ b/test/Typecheck/NegativeNew.hs
@ -2,6 +2,7 @@ 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 Juvix.Data.Effect.TaggedLock
 import Typecheck.Negative qualified as Old
@ -146,5 +147,17 @@ arityTests =
      $(mkRelFile "DefaultArgCycleArity.juvix")
      $ \case
        ErrDefaultArgLoop {} -> Nothing
+        _ -> wrongError,
+    negTest "Evil: issue 2540" $(mkRelDir "Internal/Positivity") $(mkRelFile "Evil.juvix") $
+      \case
+        ErrNonStrictlyPositive ErrTypeAsArgumentOfBoundVar {} -> Nothing
+        _ -> wrongError,
+    negTest "Evil: issue 2540 using Axiom" $(mkRelDir "Internal/Positivity") $(mkRelFile "EvilWithAxiom.juvix") $
+      \case
+        ErrNonStrictlyPositive (ErrTypeAsArgumentOfBoundVar {}) -> Nothing
+        _ -> wrongError,
+    negTest "FreeT: issue 2540" $(mkRelDir "Internal/Positivity") $(mkRelFile "FreeT.juvix") $
+      \case
+        ErrNonStrictlyPositive (ErrTypeAsArgumentOfBoundVar {}) -> Nothing
        _ -> wrongError
  ]
--- a/tests/negative/Internal/Positivity/E10.juvix
+++ b/tests/negative/Internal/Positivity/E10.juvix
@ -2,6 +2,6 @@ module E10;

 type T0 (A : Type) := t : (A -> T0 A) -> T0 A;

-alias : Type -> Type := T0;
+T0alias : Type -> Type := T0;

-type T1 := c : alias T1 -> T1;
+type T1 := c : T0alias T1 -> T1;
--- a/tests/negative/Internal/Positivity/E11.juvix
+++ b/tests/negative/Internal/Positivity/E11.juvix
@ -2,7 +2,7 @@ module E11;

 type T0 (A : Type) := t : (A -> T0 A) -> T0 _;

-alias : Type -> Type -> Type
+aliasFun : Type -> Type -> Type
  | A B := A -> B;

-type T1 := c : alias T1 T1 -> _;
+type T1 := c : aliasFun T1 T1 -> T1;
--- a/tests/negative/Internal/Positivity/Evil.juvix
+++ b/tests/negative/Internal/Positivity/Evil.juvix
@ -0,0 +1,4 @@
+module Evil;
+
+type Evil (f : Type -> Type) :=
+  magic : f (Evil f) -> Evil f;
--- a/tests/negative/Internal/Positivity/EvilWithAxiom.juvix
+++ b/tests/negative/Internal/Positivity/EvilWithAxiom.juvix
@ -0,0 +1,6 @@
+module EvilWithAxiom;
+
+axiom g : Type -> Type;
+
+type Evil (f : Type -> Type) :=
+  magic : g (Evil f) -> Evil f;
--- a/tests/negative/Internal/Positivity/FreeT.juvix
+++ b/tests/negative/Internal/Positivity/FreeT.juvix
@ -0,0 +1,5 @@
+module FreeT;
+
+type Free (f : Type -> Type) (A : Type) : Type :=
+  | Leaf : A -> Free f A
+  | Branch : f (Free f A) -> Free f A;