From 3f1a40c8c1a254b27bfe4ab681622f11511b3c0b Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Wed, 22 Nov 2023 11:33:57 +0100 Subject: [PATCH 1/5] add all old tests --- test/Typecheck.hs | 3 +- test/Typecheck/Negative.hs | 94 ++++++++++++++++++++--------------- test/Typecheck/NegativeNew.hs | 43 ++++++++++++++++ test/Typecheck/Positive.hs | 4 +- 4 files changed, 100 insertions(+), 44 deletions(-) create mode 100644 test/Typecheck/NegativeNew.hs 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..5b05995846 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 _ -> wrongError, - NegTest + negTest "Unexpected double braces in pattern" $(mkRelDir "issue1337") $(mkRelFile "DoubleBraces.juvix") $ \case ErrArity (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..22274fa788 --- /dev/null +++ b/test/Typecheck/NegativeNew.hs @@ -0,0 +1,43 @@ +module Typecheck.NegativeNew where + +import Base +import Data.HashSet qualified as HashSet +import Juvix.Data.Effect.TaggedLock +import Typecheck.Negative qualified as Old + +root :: Path Abs Dir +root = relToProject $(mkRelDir "tests/negative") + +negTest :: String -> Path Rel Dir -> Path Rel File -> Old.NegTest +negTest _name rdir rfile = + let _dir = root rdir + _file = _dir rfile + in Old.NegTest {..} + +testDescr :: Old.NegTest -> TestDescr +testDescr Old.NegTest {..} = + TestDescr + { _testName = _name, + _testRoot = _dir, + _testAssertion = Single $ do + entryPoint <- set entryPointNewTypeCheckingAlgorithm True <$> defaultEntryPointIO' LockModeExclusive _dir _file + (void . runIOExclusive entryPoint) upToInternalTyped + } + +allTests :: TestTree +allTests = + testGroup + "New typechecker negative tests" + [ testGroup + "New typechecker General negative typechecking tests" + (map (mkTest . testDescr) (filter (not . isIgnored) Old.tests)) + ] + +isIgnored :: Old.NegTest -> Bool +isIgnored t = HashSet.member (t ^. Old.name) ignored + +ignored :: HashSet String +ignored = + HashSet.fromList + [ + ] 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, From 9af4b6634dded40274166fdf05744823f4d3e793 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Fri, 24 Nov 2023 11:46:37 +0100 Subject: [PATCH 2/5] wip --- test/Typecheck/NegativeNew.hs | 43 +++++++++++++++++++++++------------ 1 file changed, 29 insertions(+), 14 deletions(-) diff --git a/test/Typecheck/NegativeNew.hs b/test/Typecheck/NegativeNew.hs index 22274fa788..7c7197fe0f 100644 --- a/test/Typecheck/NegativeNew.hs +++ b/test/Typecheck/NegativeNew.hs @@ -2,27 +2,40 @@ 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 -> Old.NegTest -negTest _name rdir rfile = +negTest :: String -> Path Rel Dir -> Path Rel File -> (TypeCheckerError -> Maybe FailMsg) -> Old.NegTest +negTest _name rdir rfile _checkErr = let _dir = root rdir - _file = _dir rfile - in Old.NegTest {..} + in Old.NegTest + { _file = _dir rfile, + _name, + _dir, + _checkErr + } testDescr :: Old.NegTest -> TestDescr testDescr Old.NegTest {..} = - TestDescr - { _testName = _name, - _testRoot = _dir, - _testAssertion = Single $ do - entryPoint <- set entryPointNewTypeCheckingAlgorithm True <$> defaultEntryPointIO' LockModeExclusive _dir _file - (void . runIOExclusive entryPoint) upToInternalTyped - } + 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 upToInternalTyped + 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 = @@ -30,7 +43,10 @@ allTests = "New typechecker negative tests" [ testGroup "New typechecker General negative typechecking tests" - (map (mkTest . testDescr) (filter (not . isIgnored) Old.tests)) + (map (mkTest . testDescr) (filter (not . isIgnored) Old.tests)), + testGroup + "Non-strictly positive data types" + (map (mkTest . testDescr) Old.negPositivityTests) ] isIgnored :: Old.NegTest -> Bool @@ -39,5 +55,4 @@ isIgnored t = HashSet.member (t ^. Old.name) ignored ignored :: HashSet String ignored = HashSet.fromList - [ - ] + [] From 7748e87e11f96f2a20d512c883d9ce42e734574a Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Fri, 24 Nov 2023 13:18:56 +0100 Subject: [PATCH 3/5] adapt arity tests --- .../Analysis/TypeChecking/Checker.hs | 2 +- .../Analysis/TypeChecking/CheckerNew.hs | 2 +- .../Analysis/TypeChecking/Error.hs | 4 +- .../Analysis/TypeChecking/Error/Types.hs | 6 +- test/Arity/Negative.hs | 2 +- test/Typecheck/NegativeNew.hs | 94 ++++++++++++++++++- 6 files changed, 101 insertions(+), 9 deletions(-) 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..aff2cd4cd1 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs @@ -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..cfd7b4950a 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs @@ -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..0a74acbd50 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error.hs @@ -20,7 +20,7 @@ data TypeCheckerError | ErrExpectedFunctionType ExpectedFunctionType | ErrTooManyArgumentsIndType WrongNumberArgumentsIndType | ErrTooFewArgumentsIndType WrongNumberArgumentsIndType - | ErrImpracticalPatternMatching ImpracticalPatternMatching + | ErrInvalidPatternMatching InvalidPatternMatching | ErrNoPositivity NoPositivity | ErrUnsupportedTypeFunction UnsupportedTypeFunction | ErrInvalidInstanceType InvalidInstanceType @@ -48,7 +48,7 @@ instance ToGenericError TypeCheckerError where 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 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/NegativeNew.hs b/test/Typecheck/NegativeNew.hs index 7c7197fe0f..f59272c010 100644 --- a/test/Typecheck/NegativeNew.hs +++ b/test/Typecheck/NegativeNew.hs @@ -46,7 +46,10 @@ allTests = (map (mkTest . testDescr) (filter (not . isIgnored) Old.tests)), testGroup "Non-strictly positive data types" - (map (mkTest . testDescr) Old.negPositivityTests) + (map (mkTest . testDescr) Old.negPositivityTests), + testGroup + "Arity tests" + (map (mkTest . testDescr) arityTests) ] isIgnored :: Old.NegTest -> Bool @@ -56,3 +59,92 @@ 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 + _ -> wrongError, + _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 + ] From aa05a77e8fbd31a05c89ffecf00b084845511d22 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Fri, 24 Nov 2023 15:42:46 +0100 Subject: [PATCH 4/5] fix negative tests --- .../Analysis/TypeChecking/Checker.hs | 4 +-- .../Analysis/TypeChecking/CheckerNew.hs | 4 +-- .../Analysis/TypeChecking/Error.hs | 29 +++++++++++++++++-- test/Typecheck/Negative.hs | 4 +-- test/Typecheck/NegativeNew.hs | 4 +-- 5 files changed, 35 insertions(+), 10 deletions(-) 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 aff2cd4cd1..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, 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 cfd7b4950a..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, 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 0a74acbd50..85676619b1 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error.hs @@ -6,6 +6,7 @@ module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Er ) where +import Prelude (show) import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Error import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Error.Pretty import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Error.Types @@ -14,7 +15,6 @@ import Juvix.Prelude data TypeCheckerError = ErrWrongConstructorType WrongConstructorType | ErrWrongReturnType WrongReturnType - | ErrArity ArityCheckerError | ErrWrongType WrongType | ErrUnsolvedMeta UnsolvedMeta | ErrExpectedFunctionType ExpectedFunctionType @@ -42,7 +42,6 @@ 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 @@ -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/test/Typecheck/Negative.hs b/test/Typecheck/Negative.hs index 5b05995846..7c608c4b4f 100644 --- a/test/Typecheck/Negative.hs +++ b/test/Typecheck/Negative.hs @@ -108,14 +108,14 @@ tests = $(mkRelDir "issue1337") $(mkRelFile "Braces.juvix") $ \case - ErrArity (ErrWrongPatternIsImplicit {}) -> Nothing + ErrArityCheckerError (ErrWrongPatternIsImplicit {}) -> Nothing _ -> wrongError, negTest "Unexpected double braces in pattern" $(mkRelDir "issue1337") $(mkRelFile "DoubleBraces.juvix") $ \case - ErrArity (ErrWrongPatternIsImplicit {}) -> Nothing + ErrArityCheckerError (ErrWrongPatternIsImplicit {}) -> Nothing _ -> wrongError, negTest "Wrong return type name for a constructor of a simple data type" diff --git a/test/Typecheck/NegativeNew.hs b/test/Typecheck/NegativeNew.hs index f59272c010..3b4fb9bca5 100644 --- a/test/Typecheck/NegativeNew.hs +++ b/test/Typecheck/NegativeNew.hs @@ -30,7 +30,7 @@ testDescr Old.NegTest {..} = _testRoot = tRoot, _testAssertion = Single $ do entryPoint <- set entryPointNewTypeCheckingAlgorithm True <$> defaultEntryPointIO' LockModeExclusive tRoot file' - result <- runIOEither' LockModeExclusive entryPoint upToInternalTyped + 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." @@ -70,7 +70,7 @@ negArityTest _name rdir rfile ariErr = { _file = _dir rfile, _checkErr = \case ErrArityCheckerError e -> ariErr e - _ -> wrongError, + e -> error (show e), _name, _dir } From df590547dfb7df9ac44499301699d7d810ef735a Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Fri, 24 Nov 2023 15:44:34 +0100 Subject: [PATCH 5/5] ormolu --- .../Translation/FromInternal/Analysis/TypeChecking/Error.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 85676619b1..f68300f853 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error.hs @@ -6,11 +6,11 @@ module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Er ) where -import Prelude (show) import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Error 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