BadDef.idr:12:1-9:
While running an elaboration script, the following error occurred:
Type mismatch between
        ()
and
        String