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.