DataDef.idr:74:1-9:
While running an elaboration script, the following error occurred:
Prelude.Either.Either is already defined as a datatype.
Tacs.idr:299:15:
When checking right hand side of testElab3 with expected type
        DPair Ty (Tm [])

Unifying ty and ARR ty t would lead to infinite value
AgdaStyleReflection.idr:315:5:
When checking right hand side of baz with expected type
        (Nat, Void)

PROOF SEARCH FAILURE is not defined.