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, 24 insertions, 19 deletions

diff --git a/compiler/GHC/Core/Make.hs b/compiler/GHC/Core/Make.hs
index 2156ce70ce..9ea1ed85e0 100644
--- a/compiler/GHC/Core/Make.hs
+++ b/compiler/GHC/Core/Make.hs
@@ -72,6 +72,7 @@ import GHC.Hs.Utils      ( mkChunkified, chunkify )
 import GHC.Core.Type
 import GHC.Core.Coercion ( isCoVar )
 import GHC.Core.DataCon  ( DataCon, dataConWorkId )
+import GHC.Core.Multiplicity
 import GHC.Builtin.Types.Prim
 import GHC.Types.Id.Info
 import GHC.Types.Demand
@@ -168,16 +169,16 @@ mkCoreAppTyped d (fun, fun_ty) arg
   where
     (arg_ty, res_ty) = splitFunTy fun_ty
 
-mkValApp :: CoreExpr -> CoreExpr -> Type -> Type -> CoreExpr
+mkValApp :: CoreExpr -> CoreExpr -> Scaled Type -> Type -> CoreExpr
 -- Build an application (e1 e2),
 -- or a strict binding  (case e2 of x -> e1 x)
 -- using the latter when necessary to respect the let/app invariant
 --   See Note [Core let/app invariant] in GHC.Core
-mkValApp fun arg arg_ty res_ty
+mkValApp fun arg (Scaled w arg_ty) res_ty
   | not (needsCaseBinding arg_ty arg)
   = App fun arg                -- The vastly common case
   | otherwise
-  = mkStrictApp fun arg arg_ty res_ty
+  = mkStrictApp fun arg (Scaled w arg_ty) res_ty
 
 {- *********************************************************************
 *                                                                      *
@@ -186,33 +187,33 @@ mkValApp fun arg arg_ty res_ty
 ********************************************************************* -}
 
 mkWildEvBinder :: PredType -> EvVar
-mkWildEvBinder pred = mkWildValBinder pred
+mkWildEvBinder pred = mkWildValBinder Many pred
 
 -- | Make a /wildcard binder/. This is typically used when you need a binder
 -- that you expect to use only at a *binding* site.  Do not use it at
 -- occurrence sites because it has a single, fixed unique, and it's very
 -- easy to get into difficulties with shadowing.  That's why it is used so little.
 -- See Note [WildCard binders] in GHC.Core.Opt.Simplify.Env
-mkWildValBinder :: Type -> Id
-mkWildValBinder ty = mkLocalIdOrCoVar wildCardName ty
+mkWildValBinder :: Mult -> Type -> Id
+mkWildValBinder w ty = mkLocalIdOrCoVar wildCardName w ty
   -- "OrCoVar" since a coercion can be a scrutinee with -fdefer-type-errors
   -- (e.g. see test T15695). Ticket #17291 covers fixing this problem.
 
-mkWildCase :: CoreExpr -> Type -> Type -> [CoreAlt] -> CoreExpr
+mkWildCase :: CoreExpr -> Scaled Type -> Type -> [CoreAlt] -> CoreExpr
 -- Make a case expression whose case binder is unused
 -- The alts and res_ty should not have any occurrences of WildId
-mkWildCase scrut scrut_ty res_ty alts
-  = Case scrut (mkWildValBinder scrut_ty) res_ty alts
+mkWildCase scrut (Scaled w scrut_ty) res_ty alts
+  = Case scrut (mkWildValBinder w scrut_ty) res_ty alts
 
-mkStrictApp :: CoreExpr -> CoreExpr -> Type -> Type -> CoreExpr
+mkStrictApp :: CoreExpr -> CoreExpr -> Scaled Type -> Type -> CoreExpr
 -- Build a strict application (case e2 of x -> e1 x)
-mkStrictApp fun arg arg_ty res_ty
+mkStrictApp fun arg (Scaled w arg_ty) res_ty
   = Case arg arg_id res_ty [(DEFAULT,[],App fun (Var arg_id))]
        -- mkDefaultCase looks attractive here, and would be sound.
        -- But it uses (exprType alt_rhs) to compute the result type,
        -- whereas here we already know that the result type is res_ty
   where
-    arg_id = mkWildValBinder arg_ty
+    arg_id = mkWildValBinder w arg_ty
         -- Lots of shadowing, but it doesn't matter,
         -- because 'fun' and 'res_ty' should not have a free wild-id
         --
@@ -226,7 +227,7 @@ mkStrictApp fun arg arg_ty res_ty
 mkIfThenElse :: CoreExpr -> CoreExpr -> CoreExpr -> CoreExpr
 mkIfThenElse guard then_expr else_expr
 -- Not going to be refining, so okay to take the type of the "then" clause
-  = mkWildCase guard boolTy (exprType then_expr)
+  = mkWildCase guard (linear boolTy) (exprType then_expr)
          [ (DataAlt falseDataCon, [], else_expr),       -- Increasing order of tag!
            (DataAlt trueDataCon,  [], then_expr) ]
 
@@ -236,7 +237,7 @@ castBottomExpr :: CoreExpr -> Type -> CoreExpr
 -- See Note [Empty case alternatives] in GHC.Core
 castBottomExpr e res_ty
   | e_ty `eqType` res_ty = e
-  | otherwise            = Case e (mkWildValBinder e_ty) res_ty []
+  | otherwise            = Case e (mkWildValBinder One e_ty) res_ty []
   where
     e_ty = exprType e
 
@@ -448,6 +449,10 @@ unitExpr = Var unitDataConId
 -- just the identity.
 --
 -- If necessary, we pattern match on a \"big\" tuple.
+--
+-- A tuple selector is not linear in its argument. Consequently, the case
+-- expression built by `mkTupleSelector` must consume its scrutinee 'Many'
+-- times. And all the argument variables must have multiplicity 'Many'.
 mkTupleSelector, mkTupleSelector1
     :: [Id]         -- ^ The 'Id's to pattern match the tuple against
     -> Id           -- ^ The 'Id' to select
@@ -542,7 +547,7 @@ mkTupleCase uniqs vars body scrut_var scrut
 
     one_tuple_case chunk_vars (us, vs, body)
       = let (uniq, us') = takeUniqFromSupply us
-            scrut_var = mkSysLocal (fsLit "ds") uniq
+            scrut_var = mkSysLocal (fsLit "ds") uniq Many
               (mkBoxedTupleTy (map idType chunk_vars))
             body' = mkSmallTupleCase chunk_vars body scrut_var (Var scrut_var)
         in (us', scrut_var:vs, body')
@@ -648,8 +653,8 @@ mkBuildExpr :: (MonadFail m, MonadThings m, MonadUnique m)
 mkBuildExpr elt_ty mk_build_inside = do
     n_tyvar <- newTyVar alphaTyVar
     let n_ty = mkTyVarTy n_tyvar
-        c_ty = mkVisFunTys [elt_ty, n_ty] n_ty
-    [c, n] <- sequence [mkSysLocalM (fsLit "c") c_ty, mkSysLocalM (fsLit "n") n_ty]
+        c_ty = mkVisFunTysMany [elt_ty, n_ty] n_ty
+    [c, n] <- sequence [mkSysLocalM (fsLit "c") Many c_ty, mkSysLocalM (fsLit "n") Many n_ty]
 
     build_inside <- mk_build_inside (c, c_ty) (n, n_ty)
 
@@ -874,7 +879,7 @@ runtimeErrorTy :: Type
 -- forall (rr :: RuntimeRep) (a :: rr). Addr# -> a
 --   See Note [Error and friends have an "open-tyvar" forall]
 runtimeErrorTy = mkSpecForAllTys [runtimeRep1TyVar, openAlphaTyVar]
-                                 (mkVisFunTy addrPrimTy openAlphaTy)
+                                 (mkVisFunTyMany addrPrimTy openAlphaTy)
 
 {- Note [Error and friends have an "open-tyvar" forall]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -964,7 +969,7 @@ be relying on anything from it.
 aBSENT_ERROR_ID
  = mkVanillaGlobalWithInfo absentErrorName absent_ty arity_info
  where
-   absent_ty = mkSpecForAllTys [alphaTyVar] (mkVisFunTy addrPrimTy alphaTy)
+   absent_ty = mkSpecForAllTys [alphaTyVar] (mkVisFunTyMany addrPrimTy alphaTy)
    -- Not runtime-rep polymorphic. aBSENT_ERROR_ID is only used for
    -- lifted-type things; see Note [Absent errors] in GHC.Core.Opt.WorkWrap.Utils
    arity_info = vanillaIdInfo `setArityInfo` 1