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 ]