Merge pull request #3270 from dunhamsteve/impossible-lam

[ parser ] Add support for impossible lambdas

CHANGELOG_NEXT.md

@@ -46,6 +46,9 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO
   environment variable adds to the "Package Search Paths." Functionally this is
   not a breaking change.
 
+* The compiler now supports `impossible` in a non-case lambda. You can now
+  write `\ Refl impossible`.
+
 * The compiler now parses `~x.fun` as unquoting `x` rather than `x.fun`
   and `~(f 5).fun` as unquoting `(f 5)` rather than `(f 5).fun`.
 

libs/test/Test/Golden.idr

@@ -427,7 +427,7 @@ testsInDir :
   (poolName : String) ->
   {default [] requirements : List Requirement} ->
   {default Nothing codegen : Codegen} ->
-  IO TestPool
+  Lazy (IO TestPool)
 testsInDir dirName poolName = do
   Right names <- listDir dirName
     | Left e => die $ "failed to list " ++ dirName ++ ": " ++ show e

src/Idris/Parser.idr

@@ -782,10 +782,21 @@ mutual
            commit
            switch <- optional (bounds $ decoratedKeyword fname "case")
            case switch of
-             Nothing => continueLam
+             Nothing => continueLamImpossible <|> continueLam
              Just r  => continueLamCase r
 
      where
+       continueLamImpossible : Rule PTerm
+       continueLamImpossible = do
+           lhs <- bounds (opExpr plhs fname indents)
+           end <- bounds (decoratedKeyword fname "impossible")
+           pure (
+             let fc = boundToFC fname (mergeBounds lhs end)
+                 alt = (MkImpossible fc lhs.val)
+                 fcCase = boundToFC fname lhs
+                 n = MN "lcase" 0 in
+             (PLam fcCase top Explicit (PRef fcCase n) (PInfer fcCase) $
+                 PCase (virtualiseFC fc) [] (PRef fcCase n) [alt]))
 
        bindAll : List (RigCount, WithBounds PTerm, PTerm) -> PTerm -> PTerm
        bindAll [] scope = scope

tests/idris2/error/perror032/LambdaImpossible.idr

@@ -0,0 +1,2 @@
+foo : 2 = 3 -> Void
+foo = (\Refl impossible)

tests/idris2/error/perror032/expected

@@ -0,0 +1 @@
+1/1: Building LambdaImpossible (LambdaImpossible.idr)

tests/idris2/error/perror032/run

@@ -0,0 +1,3 @@
+. ../../../testutils.sh
+
+check LambdaImpossible.idr