Tacs.idr:298: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:328:5:
When checking right hand side of baz with expected type
        (Nat, Void)

PROOF SEARCH FAILURE is not defined.