Expand Note [Linear types] with the stance on linting linearity

Per the discussion on #22123

2 files changed, 146 insertions, 39 deletions

diff --git a/compiler/GHC/Core/Lint.hs b/compiler/GHC/Core/Lint.hs
index ea443e3b91..bb192a3278 100644
--- a/compiler/GHC/Core/Lint.hs
+++ b/compiler/GHC/Core/Lint.hs
@@ -2863,21 +2863,86 @@ we behave as follows (#15057, #T15664):
 
 Note [Linting linearity]
 ~~~~~~~~~~~~~~~~~~~~~~~~
-There is one known optimisations that have not yet been updated
-to work with Linear Lint:
-
-* Optimisations can create a letrec which uses a variable linearly, e.g.
-    letrec f True = f False
-           f False = x
-    in f True
-  uses 'x' linearly, but this is not seen by the linter.
-  Plan: make let-bound variables remember the usage environment.
-  See ticket #18694.
-
-We plan to fix this issue in the very near future.
-For now, -dcore-lint enables only linting output of the desugarer,
-and full Linear Lint has to be enabled separately with -dlinear-core-lint.
-Ticket #19165 concerns enabling Linear Lint with -dcore-lint.
+Core understands linear types: linearity is checked with the flag
+`-dlinear-core-lint`. Why not make `-dcore-lint` check linearity?  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. The current Linear Core is described in the wiki at:
+https://gitlab.haskell.org/ghc/ghc/-/wikis/linear-types/implementation.
+
+Why don't the optimisation passes maintain the static types of Linear Core?
+Because doing so would cripple some important optimisations.  Here is an
+example:
+
+  data T = MkT {-# UNPACK #-} !Int
+
+The wrapper for MkT is
+
+  $wMkT :: Int %1 -> T
+  $wMkT n = case %1 n of
+    I# n' -> MkT n'
+
+This introduces, in particular, a `case %1` (this is not actual Haskell or Core
+syntax), where the `%1` means that the `case` expression consumes its scrutinee
+linearly.
+
+Now, `case %1` interacts with the binder swap optimisation in a non-trivial
+way. Take a slightly modified version of the code for $wMkT:
+
+  case %1 x of z {
+    I# n' -> (x, n')
+  }
+
+Binder-swap wants to change this to
+
+  case %1 x of z {
+    I# n' -> let x = z in (x, n')
+  }
+
+Now, this is not something that a linear type checker usually considers
+well-typed. It is not something that `-dlinear-core-lint` considers to be
+well-typed either. But it's only because `-dlinear-core-lint` is not good
+enough. However, making `-dlinear-core-lint` recognise this expression as valid
+is not obvious. There are many such interactions between a linear type system
+and GHC optimisations documented in the linear-type implementation wiki page
+[https://gitlab.haskell.org/ghc/ghc/-/wikis/linear-types/implementation#core-to-core-passes].
+
+PRINCIPLE: The type system bends to the optimisation, not the other way around.
+
+In the original linear-types implementation, we had tried to make every
+optimisation pass produce code that passes `-dlinear-core-lint`. It had proved
+very difficult. And we kept finding corner case after corner case.  Plus, we
+used to restrict transformations when `-dlinear-core-lint` couldn't typecheck
+the result. There are still occurrences of such restrictions in the code. But
+our current stance is that such restrictions can be removed.
+
+For instance, some optimisations can create a letrec which uses a variable
+linearly, e.g.
+
+  letrec f True = f False
+         f False = x
+  in f True
+
+uses 'x' linearly, but this is not seen by the linter. This issue is discussed
+in  ticket #18694.
+
+Plus in many cases, in order to make a transformation compatible with linear
+linting, we ended up restricting to avoid producing patterns that were not
+recognised as linear by the linter. This violates the above principle.
+
+In the future, we may be able to lint the linearity of the output of
+Core-to-Core passes (#19165). But right now, we can't. Therefore, in virtue of
+the principle above, after the desguarer, the optimiser should take no special
+pains to preserve linearity (in the type system sense).
+
+In general the optimiser tries hard not to lose sharing, so it probably doesn't
+actually make linear things non-linear. We postulate that any program
+transformation which breaks linearity would negatively impact performance, and
+therefore wouldn't be suitable for an optimiser. An alternative to linting
+linearity after each pass is to prove this statement.
+
+There is a useful discussion at https://gitlab.haskell.org/ghc/ghc/-/issues/22123
 
 Note [checkCanEtaExpand]
 ~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/compiler/GHC/Core/Multiplicity.hs b/compiler/GHC/Core/Multiplicity.hs
index 4132533b1b..89cb89936b 100644
--- a/compiler/GHC/Core/Multiplicity.hs
+++ b/compiler/GHC/Core/Multiplicity.hs
@@ -51,22 +51,30 @@ 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/pull/111] which
+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)
-    - Because, as a type constructor, the type of function now has an extra
-      argument, the notation (->) is no longer suitable. We named the function
-      type constructor `FUN`.
-    - (->) retains its backward compatible meaning: `(->) a b = a -> b`. To
-      achieve this, `(->)` is defined as a type synonym to `FUN Many` (see
+    - 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).
-- Multiplicities can be reified in Haskell as types of kind
-  `GHC.Types.Multiplicity`
-- Ground multiplicity (that is, without a variable) can be `One` or `Many`
+- 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”
@@ -75,19 +83,9 @@ For the busy developer, though, here is a high-level view of linear types is the
   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
-  infra) has a more precise definition of “consuming exactly once”.
-- Data types can have unrestricted fields (the canonical example being the
-  `Unrestricted` data type), then these don't need to be consumed for a value to
-  be consumed exactly once. So consuming a value of type `Unrestricted` exactly
-  once means forcing it at least once.
-- Why “at least once”? Because if `case u of { C x y -> f (C x y) }` is linear
-  (provided `f` is a linear function). So we might as well have done `case u of
-  { !z -> f z }`. So, we can observe constructors as many times as we want, and
-  we are actually allowed to force the same thing several times because laziness
-  means that we are really forcing a the value once, and observing its
-  constructor several times. The type checker and the linter recognise some (but
-  not all) of these multiple forces as indeed linear. Mostly just enough to
-  support variable patterns.
+  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
@@ -102,6 +100,8 @@ For the busy developer, though, here is a high-level view of linear types is the
   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.
+
 Note [Usages]
 ~~~~~~~~~~~~~
 In the _Linear Haskell_ paper, you'll find typing rules such as these:
@@ -208,8 +208,8 @@ branch.
 
 Note [Data constructors are linear by default]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Data constructors defined without -XLinearTypes (as well as data constructors
-defined with the Haskell 98 in all circumstances) have all their fields linear.
+All data constructors defined without -XLinearTypes, as well as data constructors
+defined with the Haskell 98 in all circumstances, have all their fields linear.
 
 That is, in
 
@@ -219,10 +219,52 @@ We have
 
     Just :: a %1 -> Just a
 
+Irrespective of whether -XLinearTypes is turned on or not. Furthermore, when
+-XLinearTypes is turned off, the declaration
+
+    data Endo a where { MkIntEndo :: (Int -> Int) -> T Int }
+
+gives
+
+    MkIntEndo :: (Int -> Int) %1 -> T Int
+
+With -XLinearTypes turned on, instead, this would give
+
+    data EndoU a where { MkIntEndoU :: (Int -> Int) -> T Int }
+    MkIntEndoU :: (Int -> Int) -> T Int
+
+With -XLinearTypes turned on, to get a linear field with GADT syntax we
+would need to write
+
+    data EndoL a where { MkIntEndoL :: (Int -> Int) %1 -> T Int }
+
 The goal is to maximise reuse of types between linear code and traditional
 code. This is argued at length in the proposal and the article (links in Note
 [Linear types]).
 
+Unrestricted field don't need to be consumed for a value to be consumed exactly
+once. So consuming a value of type `IntEndoU a` exactly once means forcing it at
+least once.
+
+Why “at least once”? Because if `case u of { MkIntEndoL x -> f (MkIntEndoL x) }`
+is linear (provided `f` is a linear function). But we might as well have done
+`case u of { !z -> f z }`. So, we can observe constructors as many times as we
+want, and we are actually allowed to force the same thing several times because
+laziness means that we are really forcing the value once, and observing its
+constructor several times. The type checker and the linter recognise some (but
+not all) of these multiple forces as indeed linear. Mostly just enough to
+support variable patterns.
+
+In summary:
+
+- Fields of data constructors defined with Haskell 98 syntax are always linear
+  (even if `-XLinearTypes` is off). This choice has been made to favour sharing
+  types between linearly typed Haskell and traditional Haskell. To avoid an
+  ecosystem split.
+- When `-XLinearTypes` is off, GADT-syntax declaration can only use the regular
+  arrow `(->)`. However all the fields are linear.
+
+
 Note [Polymorphisation of linear fields]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 The choice in Note [Data constructors are linear by default] has an impact on