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.