Negative tests for --new-typechecker (#2532)

Adds all existing negative tests for the new typechecker.
- Depends on #2524

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

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

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"

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 =

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

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]

test/Typecheck/Negative.hs

@@ -8,15 +8,17 @@ type FailMsg = String
 
 data NegTest = NegTest
   { _name :: String,
-    _relDir :: Path Rel Dir,
+    _dir :: Path Abs Dir,
-    _file :: Path Rel File,
+    _file :: Path Abs File,
     _checkErr :: TypeCheckerError -> Maybe FailMsg
   }
 
+makeLenses ''NegTest
+
 testDescr :: NegTest -> TestDescr
 testDescr NegTest {..} =
-  let tRoot = root <//> _relDir
+  let tRoot = _dir
-      file' = tRoot <//> _file
+      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

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
+  ]

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
+  let tRoot = _dir
-      file' = tRoot <//> _file
+      file' = _file
    in TestDescr
         { _testName = _name,
           _testRoot = tRoot,