expected

BadDef.idr:14:1-8:
   |
14 | %runElab mkBadDef1
   | ~~~~~~~~
While running an elaboration script, the following error occurred:
Type mismatch between
        ()
and
        String