From 137b6d83ebb9e8454b93b8d0db7021cc219dd3d1 Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Wed, 2 Oct 2024 18:59:30 +0200
Subject: [PATCH 1/2] Fix termination crash due to empty permutation (#3081)

- Fixes #3064
---
 .../Analysis/Termination/LexOrder.hs          | 33 +++++++++++------
 test/Typecheck/Positive.hs                    |  6 +++-
 tests/positive/issue3064.juvix                | 35 +++++++++++++++++++
 3 files changed, 62 insertions(+), 12 deletions(-)
 create mode 100644 tests/positive/issue3064.juvix

diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Termination/LexOrder.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Termination/LexOrder.hs
index c25f70d8ff..0e3322a565 100644
--- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Termination/LexOrder.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Termination/LexOrder.hs
@@ -131,37 +131,48 @@ recursiveBehaviour re =
     (re ^. reflexiveEdgeFun)
     (map callMatrixDiag (toList $ re ^. reflexiveEdgeMatrices))
 
+type SparseMatrix = [[Indexed SizeRel]]
+
 findOrder :: RecursiveBehaviour -> Maybe LexOrder
 findOrder rb = LexOrder <$> listToMaybe (mapMaybe (isLexOrder >=> nonEmpty) allPerms)
   where
     b0 :: [[SizeRel]]
     b0 = rb ^. recursiveBehaviourMatrix
 
-    indexed = map (zip [0 :: Int ..] . take minLength) b0
+    indexed = map (indexFrom 0 . take minLength) b0
       where
         minLength = minimum (map length b0)
 
+    startB :: SparseMatrix
     startB = removeUselessColumns indexed
 
-    -- removes columns that don't have at least one ≺ in them
-    removeUselessColumns :: [[(Int, SizeRel)]] -> [[(Int, SizeRel)]]
-    removeUselessColumns = transpose . filter (any (isLess . snd)) . transpose
+    -- removes columns that don't have at least one ≺ in them because we know
+    -- they'll never contribute to finding a decreasing lex order
+    removeUselessColumns :: SparseMatrix -> SparseMatrix
+    removeUselessColumns = transpose . filter (any (isLess . getRel)) . transpose
+
+    getIx :: Indexed SizeRel -> Int
+    getIx = (^. indexedIx)
+
+    getRel :: Indexed SizeRel -> SizeRel
+    getRel = (^. indexedThing)
 
     isLexOrder :: [Int] -> Maybe [Int]
     isLexOrder = go startB
       where
-        go :: [[(Int, SizeRel)]] -> [Int] -> Maybe [Int]
+        go :: SparseMatrix -> [Int] -> Maybe [Int]
         go [] _ = Just []
         go b perm = case perm of
-          [] -> error "The permutation should have one element at least!"
-          (p0 : ptail)
-            | Just r <- find (isLess . snd . (!! p0)) b,
-              all (notNothing . snd . (!! p0)) b,
+          [] -> Nothing
+          p0 : ptail
+            | Just r <- find (isLess . getRel . (!! p0)) b,
+              all (notNothing . getRel . (!! p0)) b,
               Just perm' <- go (b' p0) (map pred ptail) ->
-                Just (fst (r !! p0) : perm')
+                Just (getIx (r !! p0) : perm')
             | otherwise -> Nothing
           where
-            b' i = map r' (filter (not . isLess . snd . (!! i)) b)
+            b' :: Int -> SparseMatrix
+            b' i = map r' (filter (not . isLess . getRel . (!! i)) b)
               where
                 r' r = case splitAt i r of
                   (x, y) -> x ++ drop 1 y
diff --git a/test/Typecheck/Positive.hs b/test/Typecheck/Positive.hs
index 459f51f881..2c0b20e088 100644
--- a/test/Typecheck/Positive.hs
+++ b/test/Typecheck/Positive.hs
@@ -339,7 +339,11 @@ tests =
     posTest
       "Default argument with trait in signature"
       $(mkRelDir ".")
-      $(mkRelFile "issue2994.juvix")
+      $(mkRelFile "issue2994.juvix"),
+    posTest
+      "Termination crash because of empty permutation"
+      $(mkRelDir ".")
+      $(mkRelFile "issue3064.juvix")
   ]
     <> [ compilationTest t | t <- Compilation.tests
        ]
diff --git a/tests/positive/issue3064.juvix b/tests/positive/issue3064.juvix
new file mode 100644
index 0000000000..0156b65af2
--- /dev/null
+++ b/tests/positive/issue3064.juvix
@@ -0,0 +1,35 @@
+module issue3064;
+
+import Stdlib.Prelude open;
+
+type Expression :=
+  -- Put both of these into a Const type
+  | Const Nat
+  | Str String
+  | Var String
+  | Lam String Expression
+  | App Expression Expression;
+
+axiom undefined : {A : Type} -> A;
+
+Environment : Type := List (Pair String Expression) ;
+
+type Return :=
+  | RNatural Nat
+  | RString String;
+
+terminating eval (env : Environment) : Expression -> Maybe Return
+  | (Const x) := RNatural x          |> just
+  | (Str str) := RString str         |> just
+  | (App f x) := eval-lookup env f x
+  | (Var var) := lookup-var env var >>= eval env
+  | _ := undefined;
+
+eval-lookup (env : Environment) (f : Expression) (x : Expression) : Maybe Return :=
+  let recursive : _ -- Expression -> Return
+      | (Lam variable body) := eval ((variable , x) :: env) body
+      | _ := undefined;
+  in recursive f;
+
+lookup-var (env : Environment) (to-lookup : String) : Maybe Expression
+  := (snd <$> find \{ x := fst x == to-lookup } env);

From 8c37d9b439acc66455cff963a11821bbd0ac15b4 Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Thu, 3 Oct 2024 10:02:45 +0200
Subject: [PATCH 2/2] Merge typechecker negative tests (#3076)

---
 test/Typecheck/Negative.hs    | 103 +++++++++++++++++++++-
 test/Typecheck/NegativeNew.hs | 161 ----------------------------------
 2 files changed, 102 insertions(+), 162 deletions(-)
 delete mode 100644 test/Typecheck/NegativeNew.hs

diff --git a/test/Typecheck/Negative.hs b/test/Typecheck/Negative.hs
index b4557189d0..3ea6ac2d34 100644
--- a/test/Typecheck/Negative.hs
+++ b/test/Typecheck/Negative.hs
@@ -39,7 +39,10 @@ allTests =
         (map (mkTest . testDescr) tests),
       testGroup
         "Non-strictly positive data types"
-        (map (mkTest . testDescr) negPositivityTests)
+        (map (mkTest . testDescr) negPositivityTests),
+      testGroup
+        "Arity tests"
+        (map (mkTest . testDescr) arityTests)
     ]
 
 root :: Path Abs Dir
@@ -286,3 +289,101 @@ negPositivityTests =
       \case
         ErrNonStrictlyPositive NonStrictlyPositive {} -> Nothing
         _ -> wrongError
+
+arityTests :: [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,
+    negTest "Evil: issue 2540" $(mkRelDir "Internal/Positivity") $(mkRelFile "Evil.juvix") $
+      \case
+        ErrNonStrictlyPositive {} -> Nothing
+        _ -> wrongError,
+    negTest "Evil: issue 2540 using Axiom" $(mkRelDir "Internal/Positivity") $(mkRelFile "EvilWithAxiom.juvix") $
+      \case
+        ErrNonStrictlyPositive {} -> Nothing
+        _ -> wrongError,
+    negTest "FreeT: issue 2540" $(mkRelDir "Internal/Positivity") $(mkRelFile "FreeT.juvix") $
+      \case
+        ErrNonStrictlyPositive {} -> Nothing
+        _ -> wrongError
+  ]
+
+negArityTest :: String -> Path Rel Dir -> Path Rel File -> (ArityCheckerError -> Maybe FailMsg) -> NegTest
+negArityTest _name rdir rfile ariErr =
+  let _dir = root <//> rdir
+   in NegTest
+        { _file = _dir <//> rfile,
+          _checkErr = \case
+            ErrArityCheckerError e -> ariErr e
+            e -> error (show e),
+          _name,
+          _dir
+        }
diff --git a/test/Typecheck/NegativeNew.hs b/test/Typecheck/NegativeNew.hs
deleted file mode 100644
index c705bd5ab9..0000000000
--- a/test/Typecheck/NegativeNew.hs
+++ /dev/null
@@ -1,161 +0,0 @@
-module Typecheck.NegativeNew where
-
-import Base
-import Data.HashSet qualified as HashSet
-import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Error
-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 <- testDefaultEntryPointIO tRoot file'
-            result <- testRunIOEither entryPoint upToCore
-            case mapLeft fromJuvixError result of
-              Left (Just tyError) -> whenJust (_checkErr tyError) assertFailure
-              Left Nothing -> assertFailure "An error occurred 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,
-    negTest "Evil: issue 2540" $(mkRelDir "Internal/Positivity") $(mkRelFile "Evil.juvix") $
-      \case
-        ErrNonStrictlyPositive {} -> Nothing
-        _ -> wrongError,
-    negTest "Evil: issue 2540 using Axiom" $(mkRelDir "Internal/Positivity") $(mkRelFile "EvilWithAxiom.juvix") $
-      \case
-        ErrNonStrictlyPositive {} -> Nothing
-        _ -> wrongError,
-    negTest "FreeT: issue 2540" $(mkRelDir "Internal/Positivity") $(mkRelFile "FreeT.juvix") $
-      \case
-        ErrNonStrictlyPositive {} -> Nothing
-        _ -> wrongError
-  ]