Tacs.idr:251:15:
When checking right hand side of testElab3:
Unifying ty and ARR ty t would lead to infinite value