@@ -501,6 +501,7 @@ elab ist info emode opts fn tm
501 if null a'
501 if null a'
502 then erun fc $ do apply (Var n) []; solve
502 then erun fc $ do apply (Var n) []; solve
503 else elab' ina fc' (PApp fc tm [])
503 else elab' ina fc' (PApp fc tm [])
504+ elab' ina _ (PLam _ _ _ PImpossible) = lift . tfail . Msg $ "Only pattern-matching lambdas can be impossible"
504 elab' ina _ (PLam fc n Placeholder sc)
505 elab' ina _ (PLam fc n Placeholder sc)
505 = do -- if n is a type constructor name, this makes no sense...
506 = do -- if n is a type constructor name, this makes no sense...
506 ctxt <- get_context
507 ctxt <- get_context