au-ts
take/put unsoundness
Can take a linear field multiple times. Can put a linear field multiple times.
same for variant types -- can take an alternative more than once. (i.e. overlapping constructor incorrectly allowed)
In the solver, when we whnf a type, we never check if this put/take operation is allowed or not. See here and here.
I think to fix this, we can either emit some constraints, saying a field/tag is taken from a type. For instance, in the solver, if we see multiple occurrences of the same field being taken, we turn that into a Shareable constraint. This requires changes to the constraint solver, and new types of constraints. Alternatively we could check them in Post, which requires us to infer kinds of types in order to determine if the type of a field is linear or not.
There are some similar validity checks, which are performed in the Post stage, e.g. taking a non-existing field, taking from a non-record type, etc. It's questionable that we check for errors in Post -- although this seems easier engineering-wise, it looks ad hoc and doesn't fit so well with the overall constraint-based approach. @liamoc What do you reckon? Can you justify it, say, in your thesis if we do it the current way?