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.

1 files changed, 28 insertions, 4 deletions

diff --git a/compiler/GHC/ThToHs.hs b/compiler/GHC/ThToHs.hs
index 1a74f417d8..75bd004dc1 100644
--- a/compiler/GHC/ThToHs.hs
+++ b/compiler/GHC/ThToHs.hs
@@ -570,7 +570,7 @@ cvtConstr :: TH.Con -> CvtM (LConDecl GhcPs)
 cvtConstr (NormalC c strtys)
   = do  { c'   <- cNameL c
         ; tys' <- mapM cvt_arg strtys
-        ; returnL $ mkConDeclH98 c' Nothing Nothing (PrefixCon tys') }
+        ; returnL $ mkConDeclH98 c' Nothing Nothing (PrefixCon (map hsLinear tys')) }
 
 cvtConstr (RecC c varstrtys)
   = do  { c'    <- cNameL c
@@ -582,7 +582,8 @@ cvtConstr (InfixC st1 c st2)
   = do  { c'   <- cNameL c
         ; st1' <- cvt_arg st1
         ; st2' <- cvt_arg st2
-        ; returnL $ mkConDeclH98 c' Nothing Nothing (InfixCon st1' st2') }
+        ; returnL $ mkConDeclH98 c' Nothing Nothing (InfixCon (hsLinear st1')
+                                                              (hsLinear st2')) }
 
 cvtConstr (ForallC tvs ctxt con)
   = do  { tvs'      <- cvtTvs tvs
@@ -625,7 +626,7 @@ cvtConstr (GadtC c strtys ty)
   = do  { c'      <- mapM cNameL c
         ; args    <- mapM cvt_arg strtys
         ; ty'     <- cvtType ty
-        ; returnL $ mk_gadt_decl c' (PrefixCon args) ty'}
+        ; returnL $ mk_gadt_decl c' (PrefixCon $ map hsLinear args) ty'}
 
 cvtConstr (RecGadtC [] _varstrtys _ty)
   = failWith (text "RecGadtC must have at least one constructor name")
@@ -1464,7 +1465,23 @@ cvtTypeKind ty_str ty
                           _            -> return $
                                           parenthesizeHsType sigPrec x'
                  let y'' = parenthesizeHsType sigPrec y'
-                 returnL (HsFunTy noExtField x'' y'')
+                 returnL (HsFunTy noExtField HsUnrestrictedArrow x'' y'')
+             | otherwise
+             -> mk_apps
+                (HsTyVar noExtField NotPromoted (noLoc (getRdrName unrestrictedFunTyCon)))
+                tys'
+           MulArrowT
+             | Just normals <- m_normals
+             , [w',x',y'] <- normals -> do
+                 x'' <- case unLoc x' of
+                          HsFunTy{}    -> returnL (HsParTy noExtField x')
+                          HsForAllTy{} -> returnL (HsParTy noExtField x') -- #14646
+                          HsQualTy{}   -> returnL (HsParTy noExtField x') -- #15324
+                          _            -> return $
+                                          parenthesizeHsType sigPrec x'
+                 let y'' = parenthesizeHsType sigPrec y'
+                     w'' = hsTypeToArrow w'
+                 returnL (HsFunTy noExtField w'' x'' y'')
              | otherwise
              -> mk_apps
                 (HsTyVar noExtField NotPromoted (noLoc (getRdrName funTyCon)))
@@ -1597,6 +1614,13 @@ cvtTypeKind ty_str ty
            _ -> failWith (ptext (sLit ("Malformed " ++ ty_str)) <+> text (show ty))
     }
 
+hsTypeToArrow :: LHsType GhcPs -> HsArrow GhcPs
+hsTypeToArrow w = case unLoc w of
+                     HsTyVar _ _ (L _ (isExact_maybe -> Just n))
+                        | n == oneDataConName -> HsLinearArrow
+                        | n == manyDataConName -> HsUnrestrictedArrow
+                     _ -> HsExplicitMult w
+
 -- ConT/InfixT can contain both data constructor (i.e., promoted) names and
 -- other (i.e, unpromoted) names, as opposed to PromotedT, which can only
 -- contain data constructor names. See #15572/#17394. We use this function to