From b09d4602e7c79bfb2e6b27b4fdb1c6a847957253 Mon Sep 17 00:00:00 2001
From: janmasrovira <janmasrovira@gmail.com>
Date: Tue, 14 Jun 2022 08:56:48 +0200
Subject: [PATCH] Add negative test for AppLeftImplicit error (#154)

---
 test/Scope/Negative.hs                | 9 ++++++++-
 tests/negative/AppLeftImplicit.mjuvix | 6 ++++++
 2 files changed, 14 insertions(+), 1 deletion(-)
 create mode 100644 tests/negative/AppLeftImplicit.mjuvix

diff --git a/test/Scope/Negative.hs b/test/Scope/Negative.hs
index c9cdcea97..2642b1abf 100644
--- a/test/Scope/Negative.hs
+++ b/test/Scope/Negative.hs
@@ -24,7 +24,7 @@ testDescr NegTest {..} =
           _testRoot = tRoot,
           _testAssertion = Single $ do
             let entryPoint = defaultEntryPoint _file
-            res <- runIOEither (upToScoping entryPoint)
+            res <- runIOEither (upToAbstract entryPoint)
             case mapLeft fromMiniJuvixError res of
               Left (Just err) -> whenJust (_checkErr err) assertFailure
               Left Nothing -> assertFailure "The scope checker did not find an error."
@@ -175,6 +175,13 @@ tests =
       $ \case
         ErrWrongLocationCompileBlock {} -> Nothing
         _ -> wrongError,
+    NegTest
+      "Implicit argument on the left of an application"
+      "."
+      "AppLeftImplicit.mjuvix"
+      $ \case
+        ErrAppLeftImplicit {} -> Nothing
+        _ -> wrongError,
     NegTest
       "Multiple compile blocks for the same name"
       "CompileBlocks"
diff --git a/tests/negative/AppLeftImplicit.mjuvix b/tests/negative/AppLeftImplicit.mjuvix
new file mode 100644
index 000000000..046ccae3d
--- /dev/null
+++ b/tests/negative/AppLeftImplicit.mjuvix
@@ -0,0 +1,6 @@
+module AppLeftImplicit;
+
+ x : Type;
+ x ≔ {x};
+
+end;