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