[ parser ] Add support for impossible lambdas

[dunhamsteve]

Description

A user on the Discord was having trouble figuring out the syntax for creating a lambda whose cases are impossible. It is currently supported via a case lambda: \case Refl impossible, but not with a bare lambda. The error message is unclear on what to do.

With this change we can now write expressions like \Refl impossible for impossible lambdas.

Should this change go in the CHANGELOG?

• [x] If this is a fix, user-facing change, a compiler change, or a new paper implementation, I have updated CHANGELOG_NEXT.md (and potentially also CONTRIBUTORS.md).

[dunhamsteve]

The build failure is weird. An ENOMEM starting runtests. I’m going to force CI to run again.

[dunhamsteve]

I haven't sorted this out yet, but I think it's going to happen to any other PR that adds a test.

The test runner fails to load after this PR adds a test. It did not fail prior to merging, when there was one less test. The issue does not reproduce locally. I am also on aarch64, also using homebrew chez, and using the same version of macos as the build VM. The error message looks like it's running out of some resource when scanning a small directory during the runtests initialization. (possibly a file handle? - it's ENOMEM, which is used for other resources too). Removing another test (perror001) resolves the issue.

The error message is:

./build/exec/runtests /Users/runner/work/Idris2/Idris2/build/exec/idris2  --timing --failure-file failures --threads 3 --only  --except 
failed to list allschemes: Cannot allocate memory
make[1]: *** [test] Error 1
make: *** [test] Error 2

[dunhamsteve]

So the test runner assigns a lot of IO TestPool to global variables, like so:

ttimpTests : IO TestPool
ttimpTests = testsInDir "ttimp" "TTImp"

where testsInDir starts ike:

testsInDir dirName poolName = do
  Right names <- listDir dirName
    | Left e => die $ "failed to list " ++ dirName ++ ": " ++ show e
   ...

and listDir begins:

listDir name = do Right d <- openDir name
                    | Left e => pure $ Left e
    ...

I believe the openDir name gets run eagerly, and we have a bunch of filehandles or some other resource held open. If I block it like so:

 testsInDir dirName poolName = do
+  _ <- pure ()
   Right names <- listDir dirName
     | Left e => die $ "failed to list " ++ dirName ++ ": " ++ show e
   ...

the problem goes away. For a big more clarity, I just do declare testsInDir lazy instead.

I can also PR this change separately if desired.

[andrevidela]

amazing detective work on the CI. The diff looks good to me, in it goes