From dc7900e8cf83dc898112c0da45d0f12bdf70a96b Mon Sep 17 00:00:00 2001 From: Jonathan Cubides Date: Tue, 28 Nov 2023 14:03:45 +0100 Subject: [PATCH 1/7] W.i.p --- .../FromInternal/Analysis/Positivity.hs | 2 + .../Analysis/Positivity/Checker.hs | 220 ++++++++++-------- .../FromInternal/Analysis/Positivity/Error.hs | 20 ++ .../Analysis/Positivity/Error/Types.hs | 75 ++++++ .../Analysis/TypeChecking/Error.hs | 8 +- .../Analysis/TypeChecking/Error/Types.hs | 33 --- test/Typecheck/Negative.hs | 38 ++- tests/negative/Internal/Positivity/E10.juvix | 4 +- tests/negative/Internal/Positivity/E11.juvix | 4 +- tests/negative/Internal/Positivity/Evil.juvix | 4 + .../Internal/Positivity/EvilWithAxiom.juvix | 6 + .../negative/Internal/Positivity/FreeT.juvix | 5 + 12 files changed, 272 insertions(+), 147 deletions(-) create mode 100644 src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Error.hs create mode 100644 src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Error/Types.hs create mode 100644 tests/negative/Internal/Positivity/Evil.juvix create mode 100644 tests/negative/Internal/Positivity/EvilWithAxiom.juvix create mode 100644 tests/negative/Internal/Positivity/FreeT.juvix 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..311d5f2c6b 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,97 +22,119 @@ 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) + mapM_ + ( \typeOfConstr -> + checkStrictlyPositiveOccurrences + ( CheckPositivityArgs + { _checkPositivityArgsInductive = ty, + _checkPositivityArgsConstructorName = + ctor ^. inductiveConstructorName, + _checkPositivityArgsInductiveName = ty ^. inductiveName, + _checkPositivityArgsRecursionLimit = numInductives, + _checkPositivityArgsErrorReference = Nothing, + _checkPositivityArgsTypeOfConstructor = typeOfConstr + } + ) + ) + (constructorArgs (ctor ^. inductiveConstructorType)) 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) IdenVar name' @@ -127,25 +143,26 @@ checkStrictlyPositiveOccurrences ty ctorName name recLimit ref = | 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 ExpressionIden (IdenInductive ty') -> do when (inside && name == ty') (strictlyPositivityError 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 @@ -157,28 +174,31 @@ checkStrictlyPositiveOccurrences ty ctorName name recLimit ref = 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 let errLoc = fromMaybe expr ref throw - ( ErrNoPositivity $ - NoPositivity - { _noStrictPositivityType = indName, - _noStrictPositivityConstructor = ctorName, - _noStrictPositivityArgument = errLoc - } - ) + . ErrNonStrictlyPositive + . ErrTypeInNegativePosition + $ TypeInNegativePosition + { _typeInNegativePositionType = indName, + _typeInNegativePositionConstructor = ctorName, + _typeInNegativePositionArgument = 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..245bd97dee --- /dev/null +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Error.hs @@ -0,0 +1,20 @@ +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..52e75bc209 --- /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..9883fbd623 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 @@ -47,8 +48,13 @@ instance ToGenericError TypeCheckerError where ErrExpectedFunctionType e -> genericError e ErrTooManyArgumentsIndType e -> genericError e ErrTooFewArgumentsIndType e -> genericError e +<<<<<<< HEAD ErrInvalidPatternMatching e -> genericError e ErrNoPositivity e -> genericError e +======= + ErrImpracticalPatternMatching e -> genericError e + ErrNonStrictlyPositive e -> genericError e +>>>>>>> 781ad323 (W.i.p) ErrUnsupportedTypeFunction e -> genericError e ErrInvalidInstanceType e -> genericError e ErrInvalidCoercionType e -> genericError e 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..d39052f10e 100644 --- a/test/Typecheck/Negative.hs +++ b/test/Typecheck/Negative.hs @@ -263,38 +263,58 @@ 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, + 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; From ef242281a4c23077798b843f71d7d9da40fe3bec Mon Sep 17 00:00:00 2001 From: Jonathan Cubides Date: Wed, 29 Nov 2023 14:16:07 +0100 Subject: [PATCH 2/7] w.i.p --- .../FromInternal/Analysis/Positivity/Checker.hs | 1 - tests/negative/Internal/Positivity/Test.agda | 7 +++++++ 2 files changed, 7 insertions(+), 1 deletion(-) create mode 100644 tests/negative/Internal/Positivity/Test.agda 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 311d5f2c6b..c390deec7a 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Checker.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Checker.hs @@ -164,7 +164,6 @@ checkStrictlyPositiveOccurrences p = do 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) diff --git a/tests/negative/Internal/Positivity/Test.agda b/tests/negative/Internal/Positivity/Test.agda new file mode 100644 index 0000000000..1d18905381 --- /dev/null +++ b/tests/negative/Internal/Positivity/Test.agda @@ -0,0 +1,7 @@ +module Test where + open import Agda.Primitive + postulate B : Set lzero + postulate b : B + + data A ( f : Set lzero -> Set lzero -> Set lzero) : Set lzero where + magic : A f -> f B (A f) -> A f \ No newline at end of file From d5a4f9286d8d6991770a0431b3be31e335827873 Mon Sep 17 00:00:00 2001 From: Jonathan Cubides Date: Wed, 29 Nov 2023 18:52:18 +0100 Subject: [PATCH 3/7] w.i.p --- .../Analysis/Positivity/Checker.hs | 32 +++++++++++--- .../FromInternal/Analysis/Positivity/Error.hs | 8 ++-- .../Analysis/Positivity/Error/Types.hs | 42 +++++++++---------- test/Typecheck/Negative.hs | 1 + 4 files changed, 51 insertions(+), 32 deletions(-) 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 c390deec7a..6fff70d224 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Checker.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Checker.hs @@ -136,10 +136,10 @@ checkStrictlyPositiveOccurrences p = do 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 () @@ -147,8 +147,14 @@ checkStrictlyPositiveOccurrences p = do 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 @@ -166,7 +172,9 @@ checkStrictlyPositiveOccurrences p = do (InductiveParameter pName' _ty', tyArg) : ps -> do 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 @@ -187,8 +195,8 @@ checkStrictlyPositiveOccurrences p = do args goInductiveApp indType' ps - strictlyPositivityError :: Expression -> Sem r () - strictlyPositivityError expr = do + throwNegativePositonError :: Expression -> Sem r () + throwNegativePositonError expr = do let errLoc = fromMaybe expr ref throw . ErrNonStrictlyPositive @@ -199,6 +207,18 @@ checkStrictlyPositiveOccurrences p = do _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 diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Error.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Error.hs index 245bd97dee..64d00e1f16 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Error.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Error.hs @@ -1,8 +1,7 @@ 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, - ) - + ( 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 @@ -17,4 +16,3 @@ instance ToGenericError NonStrictlyPositiveError where 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 index 52e75bc209..f67ee243e0 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Error/Types.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Error/Types.hs @@ -1,5 +1,4 @@ -module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.Error.Types -where +module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.Error.Types where import Juvix.Compiler.Internal.Extra import Juvix.Compiler.Internal.Pretty (fromGenericOptions) @@ -7,8 +6,7 @@ import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Er import Juvix.Data.PPOutput import Juvix.Prelude - -data TypeInNegativePosition = TypeInNegativePosition +data TypeInNegativePosition = TypeInNegativePosition { _typeInNegativePositionType :: Name, _typeInNegativePositionConstructor :: Name, _typeInNegativePositionArgument :: Expression @@ -33,14 +31,15 @@ instance ToGenericError TypeInNegativePosition where 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 + 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 @@ -48,7 +47,6 @@ data TypeAsArgumentOfBoundVar = TypeAsArgumentOfBoundVar makeLenses ''TypeAsArgumentOfBoundVar - instance ToGenericError TypeAsArgumentOfBoundVar where genericError e = ask >>= generr where @@ -61,15 +59,17 @@ instance ToGenericError TypeAsArgumentOfBoundVar where } where opts' = fromGenericOptions opts - ty = e ^. typeAsArgumentOfBoundVarType + 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 <> "." + 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/test/Typecheck/Negative.hs b/test/Typecheck/Negative.hs index d39052f10e..dc7d92c91a 100644 --- a/test/Typecheck/Negative.hs +++ b/test/Typecheck/Negative.hs @@ -2,6 +2,7 @@ module Typecheck.Negative where import Base import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Error +import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.Error import Juvix.Data.Effect.TaggedLock type FailMsg = String From f86cd86ae44fdfaeeca289b0e31c61c7ef2db331 Mon Sep 17 00:00:00 2001 From: Jonathan Cubides Date: Wed, 29 Nov 2023 18:57:50 +0100 Subject: [PATCH 4/7] w.i.p --- .../Translation/FromInternal/Analysis/TypeChecking/Error.hs | 5 ----- test/Typecheck/Negative.hs | 2 +- 2 files changed, 1 insertion(+), 6 deletions(-) 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 9883fbd623..e478205e9d 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error.hs @@ -48,13 +48,8 @@ instance ToGenericError TypeCheckerError where ErrExpectedFunctionType e -> genericError e ErrTooManyArgumentsIndType e -> genericError e ErrTooFewArgumentsIndType e -> genericError e -<<<<<<< HEAD ErrInvalidPatternMatching e -> genericError e - ErrNoPositivity e -> genericError e -======= - ErrImpracticalPatternMatching e -> genericError e ErrNonStrictlyPositive e -> genericError e ->>>>>>> 781ad323 (W.i.p) ErrUnsupportedTypeFunction e -> genericError e ErrInvalidInstanceType e -> genericError e ErrInvalidCoercionType e -> genericError e diff --git a/test/Typecheck/Negative.hs b/test/Typecheck/Negative.hs index dc7d92c91a..a13ab499eb 100644 --- a/test/Typecheck/Negative.hs +++ b/test/Typecheck/Negative.hs @@ -1,8 +1,8 @@ module Typecheck.Negative where import Base -import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Error import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.Error +import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Error import Juvix.Data.Effect.TaggedLock type FailMsg = String From fbcdfd4fe45006f5ff146a665116f2ec7695c37e Mon Sep 17 00:00:00 2001 From: Jonathan Cubides Date: Wed, 29 Nov 2023 19:00:29 +0100 Subject: [PATCH 5/7] Remove test file --- tests/negative/Internal/Positivity/Test.agda | 7 ------- 1 file changed, 7 deletions(-) delete mode 100644 tests/negative/Internal/Positivity/Test.agda diff --git a/tests/negative/Internal/Positivity/Test.agda b/tests/negative/Internal/Positivity/Test.agda deleted file mode 100644 index 1d18905381..0000000000 --- a/tests/negative/Internal/Positivity/Test.agda +++ /dev/null @@ -1,7 +0,0 @@ -module Test where - open import Agda.Primitive - postulate B : Set lzero - postulate b : B - - data A ( f : Set lzero -> Set lzero -> Set lzero) : Set lzero where - magic : A f -> f B (A f) -> A f \ No newline at end of file From 373b350932fb40e1b3454e4ccb00345ba5ff39e4 Mon Sep 17 00:00:00 2001 From: Jonathan Cubides Date: Wed, 29 Nov 2023 20:18:29 +0100 Subject: [PATCH 6/7] Fix test suite. Overlooked NegativeNew!! --- .../FromInternal/Analysis/TypeChecking/Error.hs | 2 +- test/Typecheck/Negative.hs | 16 ++-------------- test/Typecheck/NegativeNew.hs | 13 +++++++++++++ 3 files changed, 16 insertions(+), 15 deletions(-) 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 e478205e9d..c81801c871 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error.hs @@ -75,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/test/Typecheck/Negative.hs b/test/Typecheck/Negative.hs index a13ab499eb..6bfe0b0122 100644 --- a/test/Typecheck/Negative.hs +++ b/test/Typecheck/Negative.hs @@ -298,24 +298,12 @@ negPositivityTests = \case ErrNonStrictlyPositive (ErrTypeInNegativePosition {}) -> Nothing _ -> wrongError, - NegTest "E10 uses type synonym" $(mkRelDir "Internal/Positivity") $(mkRelFile "E10.juvix") $ + 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") $ + negTest "E11 uses type synonym" $(mkRelDir "Internal/Positivity") $(mkRelFile "E11.juvix") $ \case ErrNonStrictlyPositive (ErrTypeInNegativePosition {}) -> 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/test/Typecheck/NegativeNew.hs b/test/Typecheck/NegativeNew.hs index 3b4fb9bca5..a6a5891c07 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 ] From 46f1f913301b0b772f85e46fc03d49a9b9b5d28a Mon Sep 17 00:00:00 2001 From: Jonathan Cubides Date: Thu, 30 Nov 2023 13:41:49 +0100 Subject: [PATCH 7/7] Fix style issues --- .../Analysis/Positivity/Checker.hs | 31 +++++++++---------- test/Typecheck/Negative.hs | 2 +- test/Typecheck/NegativeNew.hs | 2 +- 3 files changed, 17 insertions(+), 18 deletions(-) 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 6fff70d224..a7a9171deb 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Checker.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Checker.hs @@ -43,21 +43,20 @@ checkPositivity ty = do forM_ (ty ^. inductiveConstructors) $ \ctor -> do unless (ty ^. inductivePositive) $ do numInductives <- HashMap.size <$> asks (^. infoInductives) - mapM_ - ( \typeOfConstr -> - checkStrictlyPositiveOccurrences - ( CheckPositivityArgs - { _checkPositivityArgsInductive = ty, - _checkPositivityArgsConstructorName = - ctor ^. inductiveConstructorName, - _checkPositivityArgsInductiveName = ty ^. inductiveName, - _checkPositivityArgsRecursionLimit = numInductives, - _checkPositivityArgsErrorReference = Nothing, - _checkPositivityArgsTypeOfConstructor = typeOfConstr - } - ) - ) + forM_ (constructorArgs (ctor ^. inductiveConstructorType)) + $ \typeOfConstr -> + checkStrictlyPositiveOccurrences + ( CheckPositivityArgs + { _checkPositivityArgsInductive = ty, + _checkPositivityArgsConstructorName = + ctor ^. inductiveConstructorName, + _checkPositivityArgsInductiveName = ty ^. inductiveName, + _checkPositivityArgsRecursionLimit = numInductives, + _checkPositivityArgsErrorReference = Nothing, + _checkPositivityArgsTypeOfConstructor = typeOfConstr + } + ) checkStrictlyPositiveOccurrences :: forall r. @@ -147,10 +146,10 @@ checkStrictlyPositiveOccurrences p = do goApp tyApp = do let (hdExpr, args) = unfoldApplication tyApp case hdExpr of - ax@(ExpressionIden (IdenAxiom _)) -> do + ax@(ExpressionIden IdenAxiom {}) -> do when (isJust $ find (varOrInductiveInExpression name) args) $ throwTypeAsArgumentOfBoundVarError ax - var@(ExpressionIden (IdenVar _)) -> do + var@(ExpressionIden IdenVar {}) -> do when (isJust $ find (varOrInductiveInExpression name) args) $ throwTypeAsArgumentOfBoundVarError var ExpressionIden (IdenInductive ty') -> do diff --git a/test/Typecheck/Negative.hs b/test/Typecheck/Negative.hs index 6bfe0b0122..d8758b2aa9 100644 --- a/test/Typecheck/Negative.hs +++ b/test/Typecheck/Negative.hs @@ -264,7 +264,7 @@ negPositivityTests :: [NegTest] negPositivityTests = [ negTest "E1" $(mkRelDir "Internal/Positivity") $(mkRelFile "E1.juvix") $ \case - ErrNonStrictlyPositive (ErrTypeInNegativePosition {}) -> Nothing + ErrNonStrictlyPositive ErrTypeInNegativePosition {} -> Nothing _ -> wrongError, negTest "E2" $(mkRelDir "Internal/Positivity") $(mkRelFile "E2.juvix") $ \case diff --git a/test/Typecheck/NegativeNew.hs b/test/Typecheck/NegativeNew.hs index a6a5891c07..5cc4e3945b 100644 --- a/test/Typecheck/NegativeNew.hs +++ b/test/Typecheck/NegativeNew.hs @@ -150,7 +150,7 @@ arityTests = _ -> wrongError, negTest "Evil: issue 2540" $(mkRelDir "Internal/Positivity") $(mkRelFile "Evil.juvix") $ \case - ErrNonStrictlyPositive (ErrTypeAsArgumentOfBoundVar {}) -> Nothing + ErrNonStrictlyPositive ErrTypeAsArgumentOfBoundVar {} -> Nothing _ -> wrongError, negTest "Evil: issue 2540 using Axiom" $(mkRelDir "Internal/Positivity") $(mkRelFile "EvilWithAxiom.juvix") $ \case