At the moment leanchecker will just say something like
uncaught exception: (kernel) type checker does not support loose bound variables, replace them with free variables before invoking it\n
It would be nice if replayConstant would include the declaration name in the error message, maybe using preprendError.