Linear types: remember usage environment of a case
Every Core expression has a well-defined type (exprType
). With linear types, it should likewise have a well-defined usage environment.
For case expressions, the usage environment is computed by checking all branches and taking sup. However, this trick doesn't work when there are no branches.
Current workaround: empty case has a special Bottom
usage, which denotes an arbitrary usage (0, 1, Many).
Wart: this means that we have to overapproximate, e.g. in scaleUsage x Bottom
we have to guess whether to return x
or Zero
and we cannot take infimum.
Desired solution:
(1) Just like a case expression remembers its type (Note [Why does Case have a 'Type' field?]
in Core.hs
), it should remember its usage environment. This data should be verified by Lint.
(2) Once this is done, we can remove the Bottom
usage and the second field of UsageEnv
. In this step, we have to infer the correct usage environment for empty case in the typechecker.