ErrorReflection.idr:68:7-20:
   |
68 | bad = Lam (Var Here)
   |       ~~~~~~~~~~~~~~
When checking right hand side of bad with expected type
        Tm [] TUnit

DSL type error: (t(504) => t'(503)) doesn't match ()