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;