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
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
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.