@@ -18,6 +18,7 @@ import Idris.AbsSyntaxTree
1818import Idris.ASTUtils
1919import Idris.Erasure
2020import Idris.Error
21+import Idris.Output
2122
2223import Debug.Trace
2324
@@ -112,7 +113,9 @@ compile codegen f mtm
112113 where checkMVs = do i <- getIState
113114 case map fst (idris_metavars i) \\ primDefs of
114115 [] -> return ()
115− ms -> ifail $ "There are undefined holes: " ++ show ms
116+ ms -> do iputStrLn $ "WARNING: There are incomplete holes:\n " ++ show ms
117+ iputStrLn "\nEvaluation of any of these will crash at run time."
118+ return ()
116119 checkTotality = do i <- getIState
117120 case idris_totcheckfail i of
118121 [] -> return ()
@@ -227,6 +230,9 @@ irTerm :: Vars -> [Name] -> Term -> Idris LExp
227230irTerm vs env tm@(App _ f a) = do
228231 ist <- getIState
229232 case unApply tm of
233+ (P _ n _, args)
234+ | n `elem` map fst (idris_metavars ist) \\ primDefs
235+ -> return $ LError $ "ABORT: Attempt to evaluate hole " ++ show n
230236 (P _ (UN m) _, args)
231237 | m == txt "mkForeignPrim"
232238 -> doForeign vs env (reverse (drop 4 args)) -- drop implicits