Better error message for impossible lambdas that don't pattern-match
commita2f90a526246eed1e414d79cf55615b53e4142df
authorDavid Raymond Christiansen <david@davidchristiansen.dk>
dateTue 31 Mar 2015, 12:14 (12 years ago)
parentc2e5668
src/Idris/ElabTerm.hs+1
@@ -501,6 +501,7 @@ elab ist info emode opts fn tm
501501 if null a'
502502 then erun fc $ do apply (Var n) []; solve
503503 else elab' ina fc' (PApp fc tm [])
504+ elab' ina _ (PLam _ _ _ PImpossible) = lift . tfail . Msg $ "Only pattern-matching lambdas can be impossible"
504505 elab' ina _ (PLam fc n Placeholder sc)
505506 = do -- if n is a type constructor name, this makes no sense...
506507 ctxt <- get_context