Note [Linear types]

This module is the entry point for linear types.

The detailed design is in the _Linear Haskell_ article
[https://arxiv.org/abs/1710.09756]. Other important resources in the linear
types implementation wiki page
[https://gitlab.haskell.org/ghc/ghc/wikis/linear-types/implementation], and the
proposal [https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0111-linear-types.rst] which
describes the concrete design at length.

For the busy developer, though, here is a high-level view of linear types is the following:

- Function arrows are annotated with a multiplicity (as defined by type `Mult`
  and its smart constructors in this module)
    - Multiplicities, in Haskell, are types of kind `GHC.Types.Multiplicity`.
      as in

        map :: forall (p :: Multiplicity). (a %p -> b) -> [a] %p -> [b]

    - The type constructor for function types (FUN) has type

        FUN :: forall (m :: Multiplicity) -> forall {r1) {r2}. TYPE r1 -> TYPE r2 -> Type

      The argument order is explained in https://gitlab.haskell.org/ghc/ghc/-/issues/20164
    - (->) retains its backward compatible meaning:

        (->) a b = a -> b = a %'Many -> b

      To achieve this, `(->)` is defined as a type synonym to `FUN Many` (see
      below).
- A ground multiplicity (that is, without a variable) can be `One` or `Many`
  (`Many` is generally rendered as ω in the scientific literature).
  Functions whose type is annotated with `One` are linear functions, functions whose
  type is annotated with `Many` are regular functions, often called “unrestricted”
  to contrast them with linear functions.
- A linear function is defined as a function such that *if* its result is
  consumed exactly once, *then* its argument is consumed exactly once. You can
  think of “consuming exactly once” as evaluating a value in normal form exactly
  once (though not necessarily in one go). The _Linear Haskell_ article (see
  supra) has a more precise definition of “consuming exactly once”.
- Data constructors are linear by default.
  See Note [Data constructors are linear by default].
- Multiplicities form a semiring.
- Multiplicities can also be variables and we can universally quantify over
  these variables. This is referred to as “multiplicity
  polymorphism”. Furthermore, multiplicity can be formal semiring expressions
  combining variables.
- Contrary to the paper, the sum of two multiplicities is always `Many`. This
  will have to change, however, if we want to add a multiplicity for 0. Whether
  we want to is still debated.
- Case expressions have a multiplicity annotation too. A case expression with
  multiplicity `One`, consumes its scrutinee exactly once (provided the entire
  case expression is consumed exactly once); whereas a case expression with
  multiplicity `Many` can consume its scrutinee as many time as it wishes (no
  matter how much the case expression is consumed).

For linear types in the linter see Note [Linting linearity] in GHC.Core.Lint.