Note [Linting linearity]
Lint ignores linearity unless `-dlinear-core-lint` is set. For why, see below.
* When do we /check linearity/ in Lint? That is, when is `-dlinear-core-lint`
lint set? Answer: we check linearity in the output of the desugarer, shortly
after type checking.
* When so we /not/ check linearity in Lint? On all passes after desugaring. Why?
Because optimisation passes are not (yet) guaranteed to maintain linearity.
They should do so semantically (GHC is careful not to duplicate computation)
but it is much harder to ensure that the statically-checkable constraints of
Linear Core are maintained. See examples below.
The current Linear Core is described in the wiki at:
https://gitlab.haskell.org/ghc/ghc/-/wikis/linear-types/implementation.
Concretely, "ignore linearity in Lint" specifically means two things:
* In `ensureEqTypes`, use `eqTypeIgnoringMultiplicity`
* In `ensureSubMult`, do nothing
Here are some examples of how the optimiser can break linearity checking. Other
examples are documented in the linear-type implementation wiki page
[https://gitlab.haskell.org/ghc/ghc/-/wikis/linear-types/implementation#core-to-core-passes]
* EXAMPLE 1: the binder swap transformation
Consider
data T = MkT {-# UNPACK # References 0
This Note does not link to any other.
Referenced by 11
- GHC.Core.Lint call site ×3
- Respecting multiplicity when comparing types GHC.Core.TyCo.Compare ×2
- Linear types GHC.Core.Multiplicity
- GHC.Core.Multiplicity call site
- GHC.Core.Unify call site
- GHC.Driver.Config.Core.Lint call site
- Return non-recursive bindings in dependency order GHC.HsToCore.Binds
- Desugar Strict binds GHC.HsToCore.Binds