Linear types: use a predicate to check submultiplicity

Linear types currently do not support multiplicity coercions (test LinearPolyType). This restriction is enforced with a special wrapper called WpMultCoercion and by checking for reflexivity in the desugarer.

This is rather ugly. A more principled solution, once we have the predicate refactor !2857, is to use a special predicate. Then, the error can be raised during typechecking.

As a result of this ticket, the error message in LinearPolyType should be improved by pointing at the source. The error message should be shown just once (currently it is duplicated). A testcase f :: a %1 -> (); f x = () with -fdefer-type-errors is worth adding (currently it shows "Multiplicity coercions are not supported"). This ticket has no other user-visible effects. We should be able to revert the hack added in !4593 (closed).

This is blocked on the predicate refactor.

Later, we could add support for multiplicity coercions; then, this predicate would become a normal constraint. This requires changing Core and is much harder, though. I created #19517 to cover this.