When I try to typecheck some of my code in batch mode, Agda reports about unsolved metas and terminates. What does it (unsolved metas) mean and is there any reason to not supress this with --allow-unsolved-metas option ?