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