Cut off fruitless proof search earlier

In particular, trying to unify a function type with a constructor is
never going to work, so abandon as an unrecoverable error. This means
arity-based unification errors no longer make the elaborator search for
ages.