Linear types: submultiplicity evidence

This ticket concerns interaction between linear types and GADTs. It requires significant design work and is not intended for near future.

If a function a %q -> b uses its argument p times in its body, we have to check that p <= q. This is done in tcSubMult.

However, this check currently supports only manifest inequalities 1 <= p, p <= Many and p <= p. If we have an equality p ~ q obtained from a GADT, we cannot use it to get p <= q. This is the failing test LinearPolyType.

To solve this ticket, we likely need some form of multiplicity casts/submultiplicity evidence in Core, and theory behind them.

Ticket #18756 is related. Once we have predicates, submultiplicity can become one. This ticket is the next stage: having nontrivial evidence for submultiplicity. Perhaps, as a first step, we could support equalities only.

We could later expose (<=) :: Multiplicity -> Multiplicity -> Constraint to users, but this is going very far. In theory, with this type, we could generalize the type of fields (Note [Linear fields generalization]) even if they are not linear - though I'm not sure if this is a good idea.

Once implemented, it's worth checking if the testcase from #21278 (closed) is affected, see my comment in that ticket.