From ca7d0fa06d7fca30c8d9abe87dfb2afc1b9bd8c9 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Tue, 28 Nov 2023 18:24:03 +0100 Subject: [PATCH] Negative tests for `--new-typechecker` (#2532) Adds all existing negative tests for the new typechecker. - Depends on #2524 --- .../Analysis/TypeChecking/Checker.hs | 6 +- .../Analysis/TypeChecking/CheckerNew.hs | 6 +- .../Analysis/TypeChecking/Error.hs | 33 +++- .../Analysis/TypeChecking/Error/Types.hs | 6 +- test/Arity/Negative.hs | 2 +- test/Typecheck.hs | 3 +- test/Typecheck/Negative.hs | 98 +++++++----- test/Typecheck/NegativeNew.hs | 150 ++++++++++++++++++ test/Typecheck/Positive.hs | 4 +- 9 files changed, 248 insertions(+), 60 deletions(-) create mode 100644 test/Typecheck/NegativeNew.hs diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs index 45f866271a..97291b056e 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs @@ -538,7 +538,7 @@ matchIsImplicit expected actual = unless (expected == actual ^. patternArgIsImplicit) ( throw - ( ErrArity + ( ErrArityCheckerError ( ErrWrongPatternIsImplicit WrongPatternIsImplicit { _wrongPatternIsImplicitExpected = expected, @@ -629,7 +629,7 @@ checkPattern = go return app {_constrAppType = Just appTy, _constrAppParameters = pis} appErr :: ConstructorApp -> Int -> TypeCheckerError appErr app expected = - ErrArity + ErrArityCheckerError ( ErrWrongConstructorAppLength ( WrongConstructorAppLength { _wrongConstructorAppLength = app, @@ -955,7 +955,7 @@ viewInductiveApp ty = do case r of Just h' -> viewInductiveApp h' Nothing -> return (Left h) - _ -> throw (ErrImpracticalPatternMatching (ImpracticalPatternMatching ty)) + _ -> throw (ErrInvalidPatternMatching (InvalidPatternMatching ty)) where viewTypeApp :: Expression -> (Expression, [Expression]) viewTypeApp tyapp = case tyapp of diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs index 355994a8e8..f97e142a48 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs @@ -652,7 +652,7 @@ matchIsImplicit expected actual = unless (expected == actual ^. patternArgIsImplicit) . throw - . ErrArity + . ErrArityCheckerError $ ErrWrongPatternIsImplicit WrongPatternIsImplicit { _wrongPatternIsImplicitExpected = expected, @@ -745,7 +745,7 @@ checkPattern = go appErr :: ConstructorApp -> Int -> TypeCheckerError appErr app expected = - ErrArity + ErrArityCheckerError ( ErrWrongConstructorAppLength ( WrongConstructorAppLength { _wrongConstructorAppLength = app, @@ -1369,7 +1369,7 @@ viewInductiveApp ty = do case r of Just h' -> viewInductiveApp h' Nothing -> return (Left h) - _ -> throw (ErrImpracticalPatternMatching (ImpracticalPatternMatching ty)) + _ -> throw (ErrInvalidPatternMatching (InvalidPatternMatching ty)) where viewTypeApp :: Expression -> (Expression, [Expression]) viewTypeApp tyapp = case tyapp of 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 894d228318..f68300f853 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error.hs @@ -10,17 +10,17 @@ import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.E import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Error.Pretty import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Error.Types import Juvix.Prelude +import Prelude (show) data TypeCheckerError = ErrWrongConstructorType WrongConstructorType | ErrWrongReturnType WrongReturnType - | ErrArity ArityCheckerError | ErrWrongType WrongType | ErrUnsolvedMeta UnsolvedMeta | ErrExpectedFunctionType ExpectedFunctionType | ErrTooManyArgumentsIndType WrongNumberArgumentsIndType | ErrTooFewArgumentsIndType WrongNumberArgumentsIndType - | ErrImpracticalPatternMatching ImpracticalPatternMatching + | ErrInvalidPatternMatching InvalidPatternMatching | ErrNoPositivity NoPositivity | ErrUnsupportedTypeFunction UnsupportedTypeFunction | ErrInvalidInstanceType InvalidInstanceType @@ -42,13 +42,12 @@ instance ToGenericError TypeCheckerError where genericError = \case ErrWrongConstructorType e -> genericError e ErrWrongReturnType e -> genericError e - ErrArity e -> genericError e ErrWrongType e -> genericError e ErrUnsolvedMeta e -> genericError e ErrExpectedFunctionType e -> genericError e ErrTooManyArgumentsIndType e -> genericError e ErrTooFewArgumentsIndType e -> genericError e - ErrImpracticalPatternMatching e -> genericError e + ErrInvalidPatternMatching e -> genericError e ErrNoPositivity e -> genericError e ErrUnsupportedTypeFunction e -> genericError e ErrInvalidInstanceType e -> genericError e @@ -64,3 +63,29 @@ instance ToGenericError TypeCheckerError where ErrTraitNotTerminating e -> genericError e ErrArityCheckerError e -> genericError e ErrDefaultArgLoop e -> genericError e + +instance Show TypeCheckerError where + show = \case + ErrWrongConstructorType {} -> "ErrWrongConstructorType" + ErrWrongReturnType {} -> "ErrWrongReturnType" + ErrWrongType {} -> "ErrWrongType" + ErrUnsolvedMeta {} -> "ErrUnsolvedMeta" + ErrExpectedFunctionType {} -> "ErrExpectedFunctionType" + ErrTooManyArgumentsIndType {} -> "ErrTooManyArgumentsIndType" + ErrTooFewArgumentsIndType {} -> "ErrTooFewArgumentsIndType" + ErrInvalidPatternMatching {} -> "ErrInvalidPatternMatching" + ErrNoPositivity {} -> "ErrNoPositivity" + ErrUnsupportedTypeFunction {} -> "ErrUnsupportedTypeFunction" + ErrInvalidInstanceType {} -> "ErrInvalidInstanceType" + ErrInvalidCoercionType {} -> "ErrInvalidCoercionType" + ErrWrongCoercionArgument {} -> "ErrWrongCoercionArgument" + ErrCoercionCycles {} -> "ErrCoercionCycles" + ErrTargetNotATrait {} -> "ErrTargetNotATrait" + ErrNotATrait {} -> "ErrNotATrait" + ErrNoInstance {} -> "ErrNoInstance" + ErrAmbiguousInstances {} -> "ErrAmbiguousInstances" + ErrSubsumedInstance {} -> "ErrSubsumedInstance" + ErrExplicitInstanceArgument {} -> "ErrExplicitInstanceArgument" + ErrTraitNotTerminating {} -> "ErrTraitNotTerminating" + ErrArityCheckerError {} -> "ErrArityCheckerError" + ErrDefaultArgLoop {} -> "ErrDefaultArgLoop" 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 0fdb482269..e00c93706a 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 @@ -281,13 +281,13 @@ instance ToGenericError WrongNumberArgumentsIndType where ) <+> "given" -newtype ImpracticalPatternMatching = ImpracticalPatternMatching +newtype InvalidPatternMatching = InvalidPatternMatching { _impracticalPatternMatchingType :: Expression } -makeLenses ''ImpracticalPatternMatching +makeLenses ''InvalidPatternMatching -instance ToGenericError ImpracticalPatternMatching where +instance ToGenericError InvalidPatternMatching where genericError e = ask >>= generr where generr opts = diff --git a/test/Arity/Negative.hs b/test/Arity/Negative.hs index 775d69a6ef..ef27f1b7de 100644 --- a/test/Arity/Negative.hs +++ b/test/Arity/Negative.hs @@ -1,4 +1,4 @@ -module Arity.Negative (allTests) where +module Arity.Negative where import Base import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Error diff --git a/test/Typecheck.hs b/test/Typecheck.hs index d23bdb8330..d4def3866b 100644 --- a/test/Typecheck.hs +++ b/test/Typecheck.hs @@ -2,8 +2,9 @@ module Typecheck (allTests) where import Base import Typecheck.Negative qualified as N +import Typecheck.NegativeNew qualified as NewNeg import Typecheck.Positive qualified as P import Typecheck.PositiveNew qualified as New allTests :: TestTree -allTests = testGroup "Type checker tests" [New.allTests, P.allTests, N.allTests] +allTests = testGroup "Type checker tests" [New.allTests, P.allTests, N.allTests, NewNeg.allTests] diff --git a/test/Typecheck/Negative.hs b/test/Typecheck/Negative.hs index 45f3c56809..7c608c4b4f 100644 --- a/test/Typecheck/Negative.hs +++ b/test/Typecheck/Negative.hs @@ -8,15 +8,17 @@ type FailMsg = String data NegTest = NegTest { _name :: String, - _relDir :: Path Rel Dir, - _file :: Path Rel File, + _dir :: Path Abs Dir, + _file :: Path Abs File, _checkErr :: TypeCheckerError -> Maybe FailMsg } +makeLenses ''NegTest + testDescr :: NegTest -> TestDescr testDescr NegTest {..} = - let tRoot = root _relDir - file' = tRoot _file + let tRoot = _dir + file' = _file in TestDescr { _testName = _name, _testRoot = tRoot, @@ -44,201 +46,211 @@ allTests = root :: Path Abs Dir root = relToProject $(mkRelDir "tests/negative") +negTest :: String -> Path Rel Dir -> Path Rel File -> (TypeCheckerError -> Maybe FailMsg) -> NegTest +negTest _name rdir rfile _checkErr = + let _dir = root rdir + in NegTest + { _file = _dir rfile, + _name, + _dir, + _checkErr + } + wrongError :: Maybe FailMsg wrongError = Just "Incorrect error" tests :: [NegTest] tests = - [ NegTest + [ negTest "Constructor in pattern type error" $(mkRelDir "Internal") $(mkRelFile "PatternConstructor.juvix") $ \case ErrWrongConstructorType {} -> Nothing _ -> wrongError, - NegTest + negTest "Check pattern with hole type" $(mkRelDir "265") $(mkRelFile "M.juvix") $ \case ErrWrongConstructorType {} -> Nothing _ -> wrongError, - NegTest + negTest "Type vs inferred type mismatch" $(mkRelDir "Internal") $(mkRelFile "WrongType.juvix") $ \case ErrWrongType {} -> Nothing _ -> wrongError, - NegTest + negTest "Function application with non-function type" $(mkRelDir "Internal") $(mkRelFile "ExpectedFunctionType.juvix") $ \case ErrExpectedFunctionType {} -> Nothing _ -> wrongError, - NegTest + negTest "Unsolved hole" $(mkRelDir "Internal") $(mkRelFile "UnsolvedMeta.juvix") $ \case ErrUnsolvedMeta {} -> Nothing _ -> wrongError, - NegTest + negTest "Multiple type errors are captured" $(mkRelDir "Internal") $(mkRelFile "MultiWrongType.juvix") $ \case ErrWrongType {} -> Nothing _ -> wrongError, - NegTest + negTest "Unexpected braces in pattern" $(mkRelDir "issue1337") $(mkRelFile "Braces.juvix") $ \case - ErrArity (ErrWrongPatternIsImplicit {}) -> Nothing + ErrArityCheckerError (ErrWrongPatternIsImplicit {}) -> Nothing _ -> wrongError, - NegTest + negTest "Unexpected double braces in pattern" $(mkRelDir "issue1337") $(mkRelFile "DoubleBraces.juvix") $ \case - ErrArity (ErrWrongPatternIsImplicit {}) -> Nothing + ErrArityCheckerError (ErrWrongPatternIsImplicit {}) -> Nothing _ -> wrongError, - NegTest + negTest "Wrong return type name for a constructor of a simple data type" $(mkRelDir "Internal") $(mkRelFile "WrongReturnType.juvix") $ \case ErrWrongReturnType {} -> Nothing _ -> wrongError, - NegTest + negTest "Too few arguments for the return type of a constructor" $(mkRelDir "Internal") $(mkRelFile "WrongReturnTypeTooFewArguments.juvix") $ \case ErrWrongType {} -> Nothing _ -> wrongError, - NegTest + negTest "Ambiguous hole" $(mkRelDir "Internal") $(mkRelFile "IdenFunctionArgsNoExplicit.juvix") $ \case ErrUnsolvedMeta {} -> Nothing _ -> wrongError, - NegTest + negTest "Cycle in hole" $(mkRelDir "issue1700") $(mkRelFile "SelfApplication.juvix") $ \case ErrUnsolvedMeta {} -> Nothing _ -> wrongError, - NegTest + negTest "Negative integer literal cannot be used as a Nat" $(mkRelDir "Internal") $(mkRelFile "LiteralInteger.juvix") $ \case ErrNoInstance {} -> Nothing _ -> wrongError, - NegTest + negTest "Integer literal cannot be used as a String" $(mkRelDir "Internal") $(mkRelFile "LiteralIntegerString.juvix") $ \case ErrNoInstance {} -> Nothing _ -> wrongError, - NegTest + negTest "Unsupported type function" $(mkRelDir "Internal") $(mkRelFile "UnsupportedTypeFunction.juvix") $ \case ErrUnsupportedTypeFunction {} -> Nothing _ -> wrongError, - NegTest + negTest "Instance target not a trait" $(mkRelDir "Internal") $(mkRelFile "TargetNotATrait.juvix") $ \case ErrTargetNotATrait {} -> Nothing _ -> wrongError, - NegTest + negTest "Not a trait" $(mkRelDir "Internal") $(mkRelFile "NotATrait.juvix") $ \case ErrNotATrait {} -> Nothing _ -> wrongError, - NegTest + negTest "No instance" $(mkRelDir "Internal") $(mkRelFile "NoInstance.juvix") $ \case ErrNoInstance {} -> Nothing _ -> wrongError, - NegTest + negTest "Ambiguous instances" $(mkRelDir "Internal") $(mkRelFile "AmbiguousInstances.juvix") $ \case ErrAmbiguousInstances {} -> Nothing _ -> wrongError, - NegTest + negTest "Subsumed instance" $(mkRelDir "Internal") $(mkRelFile "SubsumedInstance.juvix") $ \case ErrSubsumedInstance {} -> Nothing _ -> wrongError, - NegTest + negTest "Explicit instance argument" $(mkRelDir "Internal") $(mkRelFile "ExplicitInstanceArgument.juvix") $ \case ErrExplicitInstanceArgument {} -> Nothing _ -> wrongError, - NegTest + negTest "Instance termination" $(mkRelDir "Internal") $(mkRelFile "InstanceTermination.juvix") $ \case ErrTraitNotTerminating {} -> Nothing _ -> wrongError, - NegTest + negTest "Default value wrong type" $(mkRelDir "Internal") $(mkRelFile "DefaultTypeError.juvix") $ \case ErrWrongType {} -> Nothing _ -> wrongError, - NegTest + negTest "Coercion target not a trait" $(mkRelDir "Internal") $(mkRelFile "CoercionTargetNotATrait.juvix") $ \case ErrTargetNotATrait {} -> Nothing _ -> wrongError, - NegTest + negTest "Invalid coercion type" $(mkRelDir "Internal") $(mkRelFile "InvalidCoercionType.juvix") $ \case ErrInvalidCoercionType {} -> Nothing _ -> wrongError, - NegTest + negTest "Wrong coercion argument" $(mkRelDir "Internal") $(mkRelFile "WrongCoercionArgument.juvix") $ \case ErrWrongCoercionArgument {} -> Nothing _ -> wrongError, - NegTest + negTest "Ambiguous coercions" $(mkRelDir "Internal") $(mkRelFile "AmbiguousCoercions.juvix") $ \case ErrAmbiguousInstances {} -> Nothing _ -> wrongError, - NegTest + negTest "Coercion cycles" $(mkRelDir "Internal") $(mkRelFile "LoopingCoercion.juvix") @@ -249,39 +261,39 @@ tests = negPositivityTests :: [NegTest] negPositivityTests = - [ NegTest "E1" $(mkRelDir "Internal/Positivity") $(mkRelFile "E1.juvix") $ + [ negTest "E1" $(mkRelDir "Internal/Positivity") $(mkRelFile "E1.juvix") $ \case ErrNoPositivity {} -> Nothing _ -> wrongError, - NegTest "E2" $(mkRelDir "Internal/Positivity") $(mkRelFile "E2.juvix") $ + negTest "E2" $(mkRelDir "Internal/Positivity") $(mkRelFile "E2.juvix") $ \case ErrNoPositivity {} -> Nothing _ -> wrongError, - NegTest "E3" $(mkRelDir "Internal/Positivity") $(mkRelFile "E3.juvix") $ + negTest "E3" $(mkRelDir "Internal/Positivity") $(mkRelFile "E3.juvix") $ \case ErrNoPositivity {} -> Nothing _ -> wrongError, - NegTest "E4" $(mkRelDir "Internal/Positivity") $(mkRelFile "E4.juvix") $ + negTest "E4" $(mkRelDir "Internal/Positivity") $(mkRelFile "E4.juvix") $ \case ErrNoPositivity {} -> Nothing _ -> wrongError, - NegTest "E5" $(mkRelDir "Internal/Positivity") $(mkRelFile "E5.juvix") $ + negTest "E5" $(mkRelDir "Internal/Positivity") $(mkRelFile "E5.juvix") $ \case ErrNoPositivity {} -> Nothing _ -> wrongError, - NegTest "E6" $(mkRelDir "Internal/Positivity") $(mkRelFile "E6.juvix") $ + negTest "E6" $(mkRelDir "Internal/Positivity") $(mkRelFile "E6.juvix") $ \case ErrNoPositivity {} -> Nothing _ -> wrongError, - NegTest "E7" $(mkRelDir "Internal/Positivity") $(mkRelFile "E7.juvix") $ + negTest "E7" $(mkRelDir "Internal/Positivity") $(mkRelFile "E7.juvix") $ \case ErrNoPositivity {} -> Nothing _ -> wrongError, - NegTest "E8" $(mkRelDir "Internal/Positivity") $(mkRelFile "E8.juvix") $ + negTest "E8" $(mkRelDir "Internal/Positivity") $(mkRelFile "E8.juvix") $ \case ErrNoPositivity {} -> Nothing _ -> wrongError, - NegTest "E9" $(mkRelDir "Internal/Positivity") $(mkRelFile "E9.juvix") $ + negTest "E9" $(mkRelDir "Internal/Positivity") $(mkRelFile "E9.juvix") $ \case ErrNoPositivity {} -> Nothing _ -> wrongError diff --git a/test/Typecheck/NegativeNew.hs b/test/Typecheck/NegativeNew.hs new file mode 100644 index 0000000000..3b4fb9bca5 --- /dev/null +++ b/test/Typecheck/NegativeNew.hs @@ -0,0 +1,150 @@ +module Typecheck.NegativeNew where + +import Base +import Data.HashSet qualified as HashSet +import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Error +import Juvix.Data.Effect.TaggedLock +import Typecheck.Negative qualified as Old + +type FailMsg = String + +root :: Path Abs Dir +root = relToProject $(mkRelDir "tests/negative") + +negTest :: String -> Path Rel Dir -> Path Rel File -> (TypeCheckerError -> Maybe FailMsg) -> Old.NegTest +negTest _name rdir rfile _checkErr = + let _dir = root rdir + in Old.NegTest + { _file = _dir rfile, + _name, + _dir, + _checkErr + } + +testDescr :: Old.NegTest -> TestDescr +testDescr Old.NegTest {..} = + let tRoot = _dir + file' = _file + in TestDescr + { _testName = _name, + _testRoot = tRoot, + _testAssertion = Single $ do + entryPoint <- set entryPointNewTypeCheckingAlgorithm True <$> defaultEntryPointIO' LockModeExclusive tRoot file' + result <- runIOEither' LockModeExclusive entryPoint upToCore + case mapLeft fromJuvixError result of + Left (Just tyError) -> whenJust (_checkErr tyError) assertFailure + Left Nothing -> assertFailure "An error ocurred but it was not in the type checker." + Right _ -> assertFailure "The type checker did not find an error." + } + +allTests :: TestTree +allTests = + testGroup + "New typechecker negative tests" + [ testGroup + "New typechecker General negative typechecking tests" + (map (mkTest . testDescr) (filter (not . isIgnored) Old.tests)), + testGroup + "Non-strictly positive data types" + (map (mkTest . testDescr) Old.negPositivityTests), + testGroup + "Arity tests" + (map (mkTest . testDescr) arityTests) + ] + +isIgnored :: Old.NegTest -> Bool +isIgnored t = HashSet.member (t ^. Old.name) ignored + +ignored :: HashSet String +ignored = + HashSet.fromList + [] + +wrongError :: Maybe FailMsg +wrongError = Just "Incorrect error" + +negArityTest :: String -> Path Rel Dir -> Path Rel File -> (ArityCheckerError -> Maybe FailMsg) -> Old.NegTest +negArityTest _name rdir rfile ariErr = + let _dir = root rdir + in Old.NegTest + { _file = _dir rfile, + _checkErr = \case + ErrArityCheckerError e -> ariErr e + e -> error (show e), + _name, + _dir + } + +arityTests :: [Old.NegTest] +arityTests = + [ negTest + "Too many arguments in expression" + $(mkRelDir "Internal") + $(mkRelFile "TooManyArguments.juvix") + $ \case + ErrExpectedFunctionType {} -> Nothing + _ -> wrongError, + negTest + "Pattern match a function type" + $(mkRelDir "Internal") + $(mkRelFile "FunctionPattern.juvix") + $ \case + ErrInvalidPatternMatching {} -> Nothing + _ -> wrongError, + negTest + "Function type (* → *) application" + $(mkRelDir "Internal") + $(mkRelFile "FunctionApplied.juvix") + $ \case + ErrExpectedFunctionType {} -> Nothing + _ -> wrongError, + negArityTest + "Expected explicit pattern" + $(mkRelDir "Internal") + $(mkRelFile "ExpectedExplicitPattern.juvix") + $ \case + ErrWrongPatternIsImplicit {} -> Nothing + _ -> wrongError, + negArityTest + "Expected explicit argument" + $(mkRelDir "Internal") + $(mkRelFile "ExpectedExplicitArgument.juvix") + $ \case + ErrExpectedExplicitArgument {} -> Nothing + _ -> wrongError, + negArityTest + "Function clause with two many patterns in the lhs" + $(mkRelDir "Internal") + $(mkRelFile "LhsTooManyPatterns.juvix") + $ \case + ErrLhsTooManyPatterns {} -> Nothing + _ -> wrongError, + negTest + "Too many arguments for the return type of a constructor" + $(mkRelDir "Internal") + $(mkRelFile "WrongReturnTypeTooManyArguments.juvix") + $ \case + ErrExpectedFunctionType {} -> Nothing + _ -> wrongError, + negArityTest + "Lazy builtin not fully applied" + $(mkRelDir "Internal") + $(mkRelFile "LazyBuiltin.juvix") + $ \case + ErrBuiltinNotFullyApplied {} -> Nothing + _ -> wrongError, + negArityTest + "issue 2293: Non-terminating function with arity error" + $(mkRelDir "Internal") + $(mkRelFile "issue2293.juvix") + $ \case + ErrWrongConstructorAppLength {} -> Nothing + _ -> wrongError, + negTest + "Detect default argument cycle in the arity checker" + $(mkRelDir "Internal") + $(mkRelFile "DefaultArgCycleArity.juvix") + $ \case + ErrDefaultArgLoop {} -> Nothing + _ -> wrongError + ] diff --git a/test/Typecheck/Positive.hs b/test/Typecheck/Positive.hs index 8aacaea7ee..ad1879b39a 100644 --- a/test/Typecheck/Positive.hs +++ b/test/Typecheck/Positive.hs @@ -43,8 +43,8 @@ rootNegTests = relToProject $(mkRelDir "tests/negative/") -- Testing --no-positivity flag with all related negative tests testNoPositivityFlag :: N.NegTest -> TestDescr testNoPositivityFlag N.NegTest {..} = - let tRoot = rootNegTests _relDir - file' = tRoot _file + let tRoot = _dir + file' = _file in TestDescr { _testName = _name, _testRoot = tRoot,