Linear types (#15981)

This is the first step towards implementation of the linear types proposal
(https://github.com/ghc-proposals/ghc-proposals/pull/111).

It features

* A language extension -XLinearTypes
* Syntax for linear functions in the surface language
* Linearity checking in Core Lint, enabled with -dlinear-core-lint
* Core-to-core passes are mostly compatible with linearity
* Fields in a data type can be linear or unrestricted; linear fields
  have multiplicity-polymorphic constructors.
  If -XLinearTypes is disabled, the GADT syntax defaults to linear fields

The following items are not yet supported:

* a # m -> b syntax (only prefix FUN is supported for now)
* Full multiplicity inference (multiplicities are really only checked)
* Decent linearity error messages
* Linear let, where, and case expressions in the surface language
  (each of these currently introduce the unrestricted variant)
* Multiplicity-parametric fields
* Syntax for annotating lambda-bound or let-bound with a multiplicity
* Syntax for non-linear/multiple-field-multiplicity records
* Linear projections for records with a single linear field
* Linear pattern synonyms
* Multiplicity coercions (test LinearPolyType)

A high-level description can be found at
https://ghc.haskell.org/trac/ghc/wiki/LinearTypes/Implementation
Following the link above you will find a description of the changes made to Core.
This commit has been authored by

* Richard Eisenberg
* Krzysztof Gogolewski
* Matthew Pickering
* Arnaud Spiwack

With contributions from:

* Mark Barbone
* Alexander Vershilov

Updates haddock submodule.

3 files changed, 199 insertions, 0 deletions

diff --git a/docs/users_guide/exts/levity_polymorphism.rst b/docs/users_guide/exts/levity_polymorphism.rst
index d7954915a0..a65f878b41 100644
--- a/docs/users_guide/exts/levity_polymorphism.rst
+++ b/docs/users_guide/exts/levity_polymorphism.rst
@@ -89,6 +89,8 @@ These functions do not bind a levity-polymorphic variable, and
 so are accepted. Their polymorphism allows users to use these to conveniently
 stub out functions that return unboxed types.
 
+.. _printing-levity-polymorphic-types:
+
 Printing levity-polymorphic types
 ---------------------------------
 
diff --git a/docs/users_guide/exts/linear_types.rst b/docs/users_guide/exts/linear_types.rst
new file mode 100644
index 0000000000..1b725f36cc
--- /dev/null
+++ b/docs/users_guide/exts/linear_types.rst
@@ -0,0 +1,196 @@
+Linear types
+============
+
+.. extension:: LinearTypes
+    :shortdesc: Enable linear types.
+
+    :since: 8.12.1
+
+    Enable the linear arrow ``a #-> b`` and the multiplicity-polymorphic arrow
+    ``a # m -> b``.
+
+**This extension is currently considered experimental, expect bugs,
+warts, and bad error messages; everything down to the syntax is
+subject to change**.  See, in particular,
+:ref:`linear-types-limitations` below. We encourage you to experiment
+with this extension and report issues in the GHC bug tracker `the GHC
+bug tracker <https://gitlab.haskell.org/ghc/ghc/issues>`__, adding the
+tag ``LinearTypes``.
+
+A function ``f`` is linear if: when its result is consumed *exactly
+once*, then its argument is consumed *exactly once*. Intuitively, it
+means that in every branch of the definition of ``f``, its argument
+``x`` must be used exactly once. Which can be done by
+
+* Returning ``x`` unmodified
+* Passing ``x`` to a *linear* function
+* Pattern-matching on ``x`` and using each argument exactly once in the
+  same fashion.
+* Calling it as a function and using the result exactly once in the same
+  fashion.
+
+With ``-XLinearTypes``, you can write ``f :: a #-> b`` to mean that
+``f`` is a linear function from ``a`` to ``b``.  If
+:extension:`UnicodeSyntax` is enabled, the ``#->`` arrow can be
+written as ``⊸``.
+
+To allow uniform handling of linear ``a #-> b`` and unrestricted ``a
+-> b`` functions, there is a new function type ``a # m -> b``. This
+syntax is, however, not implemented yet, see
+:ref:`linear-types-limitations`. Here, ``m`` is a type of new kind
+``Multiplicity``. We have:
+
+::
+
+    data Multiplicity = One | Many  -- Defined in GHC.Types
+
+    type a #-> b = a # 'One  -> b
+    type a  -> b = a # 'Many -> b
+
+(See :ref:`promotion`).
+
+We say that a variable whose multiplicity constraint is ``Many`` is
+*unrestricted*.
+
+The multiplicity-polymorphic arrow ``a # m -> b`` is available in a prefix
+version as ``GHC.Exts.FUN m a b``, which can be applied
+partially. See, however :ref:`linear-types-limitations`.
+
+Linear and multiplicity-polymorphic arrows are *always declared*,
+never inferred. That is, if you don't give an appropriate type
+signature to a function, it will be inferred as being a regular
+function of type ``a -> b``.
+
+Data types
+----------
+By default, all fields in algebraic data types are linear (even if
+``-XLinearTypes`` is not turned on). Given
+
+::
+
+    data T1 a = MkT1 a
+
+the value ``MkT1 x`` can be constructed and deconstructed in a linear context:
+
+::
+
+    construct :: a #-> MkT1 a
+    construct x = MkT1 x
+
+    deconstruct :: MkT1 a #-> a
+    deconstruct (MkT1 x) = x  -- must consume `x` exactly once
+
+When used as a value, ``MkT1`` is given a multiplicity-polymorphic
+type: ``MkT1 :: forall {m} a. a # m -> T1 a``. This makes it possible
+to use ``MkT1`` in higher order functions. The additional multiplicity
+argument ``m`` is marked as inferred (see
+:ref:`inferred-vs-specified`), so that there is no conflict with
+visible type application. When displaying types, unless
+``-XLinearTypes`` is enabled, multiplicity polymorphic functions are
+printed as regular functions (see :ref:`printing-linear-types`);
+therefore constructors appear to have regular function types.
+
+::
+
+    mkList :: [a] -> [MkT1 a]
+    mkList xs = map MkT1 xs
+
+Hence the linearity of type constructors is invisible when
+``-XLinearTypes`` is off.
+
+Whether a data constructor field is linear or not can be customized using the GADT syntax. Given
+
+::
+
+    data T2 a b c where
+        MkT2 :: a -> b #-> c #-> T2 a b  -- Note unrestricted arrow in the first argument
+
+the value ``MkT2 x y z`` can be constructed only if ``x`` is
+unrestricted. On the other hand, a linear function which is matching
+on ``MkT2 x y z`` must consume ``y`` and ``z`` exactly once, but there
+is no restriction on ``x``.
+
+If :extension:`LinearTypes` is disabled, all fields are considered to be linear
+fields, including GADT fields defined with the ``->`` arrow.
+
+In a ``newtype`` declaration, the field must be linear. Attempting to
+write an unrestricted newtype constructor with GADT syntax results in
+an error.
+
+.. _printing-linear-types:
+
+Printing multiplicity-polymorphic types
+---------------------------------------
+If :extension:`LinearTypes` is disabled, multiplicity variables in types are defaulted
+to ``Many`` when printing, in the same manner as described in :ref:`printing-levity-polymorphic-types`.
+In other words, without :extension:`LinearTypes`, multiplicity-polymorphic functions
+``a # m -> b`` are printed as normal Haskell2010 functions ``a -> b``. This allows
+existing libraries to be generalized to linear types in a backwards-compatible
+manner; the general types are visible only if the user has enabled
+:extension:`LinearTypes`.
+(Note that a library can declare a linear function in the contravariant position,
+i.e. take a linear function as an argument. In this case, linearity cannot be
+hidden; it is an essential part of the exposed interface.)
+
+.. _linear-types-limitations:
+
+Limitations
+-----------
+Linear types are still considered experimental and come with several
+limitations. If you have read the full design in the proposal (see
+:ref:`linear-types-references` below), here is a run down of the
+missing pieces.
+
+- The syntax ``a # p -> b`` is not yet implemented. You can use ``GHC.Exts.FUN
+  p a b`` instead. However, be aware of the next point.
+- Multiplicity polymorphism is incomplete and experimental. You may
+  have success using it, or you may not. Expect it to be really unreliable.
+- There is currently no support for multiplicity annotations such as
+  ``x :: a # p``, ``\(x :: a # p) -> ...``.
+- All ``case``, ``let`` and ``where`` statements consume their
+  right-hand side, or scrutiny, ``Many`` times. That is, the following
+  will not type check:
+
+  ::
+
+      g :: A #-> (A, B)
+      h :: A #-> B #-> C
+
+      f :: A #-> C
+      f x =
+        case g x of
+          (y, z) -> h y z
+
+  This can be worked around by defining extra functions which are
+  specified to be linear, such as:
+
+  ::
+
+      g :: A #-> (A, B)
+      h :: A #-> B #-> C
+
+      f :: A #-> C
+      f x = f' (g x)
+        where
+          f' :: (A, B) #-> C
+          f' (y, z) = h y z
+- There is no support for linear pattern synonyms.
+- ``@``-patterns and view patterns are not linear.
+- The projection function for a record with a single linear field should be
+  multiplicity-polymorphic; currently it's unrestricted.
+- Attempting to use of linear types in Template Haskell will probably
+  not work.
+
+.. _linear-types-references:
+
+Design and further reading
+--------------------------
+
+* The design for this extension is described in details in the `Linear
+  types proposal
+  <https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0111-linear-types.rst>`__
+* This extension has been originally conceived of in the paper `Linear
+  Haskell: practical linearity in a higher-order polymorphic language
+  <https://www.microsoft.com/en-us/research/publication/linear-haskell-practical-linearity-higher-order-polymorphic-language/>`__
+  (POPL 2018)
+* There is a `wiki page dedicated to the linear types extension <https://gitlab.haskell.org/ghc/ghc/-/wikis/linear-types>`__
diff --git a/docs/users_guide/exts/types.rst b/docs/users_guide/exts/types.rst
index f5fd5d130e..2cd9d059f5 100644
--- a/docs/users_guide/exts/types.rst
+++ b/docs/users_guide/exts/types.rst
@@ -22,6 +22,7 @@ Types
     type_applications
     rank_polymorphism
     impredicative_types
+    linear_types
     type_errors
     defer_type_errors
     roles