@@ -454,6 +454,10 @@ unify ctxt env topx topy inj holes usersupp from =
454454 return [] -- lift $ tfail err
455455
456456 unApp fn bnames appx@(App fx ax) appy@(App fy ay)
457+ -- shortcut for the common case where we just want to check the
458+ -- arguments are correct
459+ | (injectiveApp fx && fx == fy)
460+ = un' False bnames ax ay
457461 | (injectiveApp fx && injectiveApp fy)
458462 || (injectiveApp fx && metavarApp fy && ax == ay)
459463 || (injectiveApp fy && metavarApp fx && ax == ay)