diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity.hs index d7b22f9cf7..98c2a83dc7 100644 --- 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 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 6a3a51f6ed..a7a9171deb 100644 --- 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) - - helperCaseBranch :: CaseBranch -> Sem r () - helperCaseBranch b = helper inside (b ^. caseBranchExpression) - - helperLet :: Let -> Sem r () - helperLet l = do - helper inside (l ^. letExpression) - mapM_ helperLetClause (l ^. letClauses) - - helperLetClause :: LetClause -> Sem r () - helperLetClause = \case - LetFunDef f -> helperFunctionDef f - LetMutualBlock b -> helperMutualBlockLet b - - helperMutualBlockLet :: MutualBlockLet -> Sem r () - helperMutualBlockLet b = mapM_ helperFunctionDef (b ^. mutualLet) - - helperFunctionDef :: FunctionDef -> Sem r () - helperFunctionDef d = do - helper inside (d ^. funDefType) - helper inside (d ^. funDefBody) - - helperSimpleLambda :: SimpleLambda -> Sem r () - helperSimpleLambda (SimpleLambda (SimpleBinder _ lamVarTy) lamBody) = do - helper inside lamVarTy - helper inside lamBody - - helperLambda :: Lambda -> Sem r () - helperLambda l = mapM_ goClause (l ^. lambdaClauses) + goCase :: Case -> Sem r () + goCase l = do + go inside (l ^. caseExpression) + mapM_ goCaseBranch (l ^. caseBranches) + + goCaseBranch :: CaseBranch -> Sem r () + goCaseBranch b = go inside (b ^. caseBranchExpression) + + goLet :: Let -> Sem r () + goLet l = do + go inside (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 inside (d ^. funDefType) + go inside (d ^. funDefBody) + + goSimpleLambda :: SimpleLambda -> Sem r () + goSimpleLambda (SimpleLambda (SimpleBinder _ lamVarTy) lamBody) = do + go inside lamVarTy + go inside lamBody + + 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 + . ErrNonStrictlyPositive + . ErrTypeInNegativePosition + $ TypeInNegativePosition + { _typeInNegativePositionType = indName, + _typeInNegativePositionConstructor = ctorName, + _typeInNegativePositionArgument = errLoc + } + + throwTypeAsArgumentOfBoundVarError :: Expression -> Sem r () + throwTypeAsArgumentOfBoundVarError expr = do let errLoc = fromMaybe expr ref throw - ( ErrNoPositivity $ - NoPositivity - { _noStrictPositivityType = indName, - _noStrictPositivityConstructor = ctorName, - _noStrictPositivityArgument = errLoc - } - ) + . ErrNonStrictlyPositive + . ErrTypeAsArgumentOfBoundVar + $ TypeAsArgumentOfBoundVar + { _typeAsArgumentOfBoundVarType = indName, + _typeAsArgumentOfBoundVarConstructor = ctorName, + _typeAsArgumentOfBoundVarReference = errLoc + } varOrInductiveInExpression :: Name -> Expression -> Bool varOrInductiveInExpression n = \case diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Error.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Error.hs new file mode 100644 index 0000000000..64d00e1f16 --- /dev/null +++ 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 diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Error/Types.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Error/Types.hs new file mode 100644 index 0000000000..f67ee243e0 --- /dev/null +++ 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 <> "." 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 f68300f853..c81801c871 100644 --- 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" 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 e00c93706a..254f04f728 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 @@ -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 } diff --git a/test/Typecheck/Negative.hs b/test/Typecheck/Negative.hs index 7c608c4b4f..d8758b2aa9 100644 --- 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 ] diff --git a/test/Typecheck/NegativeNew.hs b/test/Typecheck/NegativeNew.hs index 3b4fb9bca5..5cc4e3945b 100644 --- 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 ] diff --git a/tests/negative/Internal/Positivity/E10.juvix b/tests/negative/Internal/Positivity/E10.juvix index aa23323ebd..c7eab9353f 100644 --- 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; diff --git a/tests/negative/Internal/Positivity/E11.juvix b/tests/negative/Internal/Positivity/E11.juvix index 30782bd10c..f5a66e87d6 100644 --- 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; diff --git a/tests/negative/Internal/Positivity/Evil.juvix b/tests/negative/Internal/Positivity/Evil.juvix new file mode 100644 index 0000000000..bece368363 --- /dev/null +++ b/tests/negative/Internal/Positivity/Evil.juvix @@ -0,0 +1,4 @@ +module Evil; + +type Evil (f : Type -> Type) := + magic : f (Evil f) -> Evil f; diff --git a/tests/negative/Internal/Positivity/EvilWithAxiom.juvix b/tests/negative/Internal/Positivity/EvilWithAxiom.juvix new file mode 100644 index 0000000000..8f2bfbffac --- /dev/null +++ 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; diff --git a/tests/negative/Internal/Positivity/FreeT.juvix b/tests/negative/Internal/Positivity/FreeT.juvix new file mode 100644 index 0000000000..239458c5bf --- /dev/null +++ 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;