Tentatively more informative report of failure when inferring
pattern-matching predicate.
Fine-tuning unification error (using OccurCheck in evarconv).
Added a CannotSolveConstraint unification error and made experiments
in reporting the chain of causes when unification fails.