Description
This is a pretty non-specific title for a pretty non-specific issue.
Basically, static argument transform should be absolutely good a transformation now that we have a rule for recursive-let to be multiplicity aliases (which we absolutely need for recursive join points anyway).
But, the current implementation of Static Argument Transform (SAT.hs) produces (intermediate) terms which do not preserve linearity. From the file documentation:
Example: transform this
map :: forall a b. (a->b) -> [a] -> [b] map = /\ab. \(f:a->b) (as:[a]) -> body[map]to
map :: forall a b. (a->b) -> [a] -> [b] map = /\ab. \(f:a->b) (as:[a]) -> letrec map' :: [a] -> [b] -- The "worker function map' = \(as:[a]) -> let map :: forall a' b'. (a -> b) -> [a] -> [b] -- The "shadow function map = /\a'b'. \(f':(a->b) (as:[a]). map' as in body[map] in map' as
The non-recursive, inner, let map is not linear in f, even if the original map were (because f is summarily dropped).
For the moment, static argument transform must be deactivated for linear arguments. But better would be to re-engineer it a smidge, so that the we don't have to perform any inlining and beta-reduction before getting a manifestly linear term.