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.