@@ -454,6 +454,10 @@ unify ctxt env topx topy inj holes usersupp from =
454 return [] -- lift $ tfail err
454 return [] -- lift $ tfail err
456 unApp fn bnames appx@(App fx ax) appy@(App fy ay)
456 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
457 | (injectiveApp fx && injectiveApp fy)
461 | (injectiveApp fx && injectiveApp fy)
458 || (injectiveApp fx && metavarApp fy && ax == ay)
462 || (injectiveApp fx && metavarApp fy && ax == ay)
459 || (injectiveApp fy && metavarApp fx && ax == ay)
463 || (injectiveApp fy && metavarApp fx && ax == ay)