Note [Linting linearity]

GHC/Core/Lint.hs:3124 compiler

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