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.

2 files changed, 32 insertions, 12 deletions

diff --git a/compiler/GHC/HsToCore/Match/Constructor.hs b/compiler/GHC/HsToCore/Match/Constructor.hs
index 9c7ad46c22..96ab10fa4c 100644
--- a/compiler/GHC/HsToCore/Match/Constructor.hs
+++ b/compiler/GHC/HsToCore/Match/Constructor.hs
@@ -25,6 +25,7 @@ import GHC.HsToCore.Binds
 import GHC.Core.ConLike
 import GHC.Types.Basic ( Origin(..) )
 import GHC.Tc.Utils.TcType
+import GHC.Core.Multiplicity
 import GHC.HsToCore.Monad
 import GHC.HsToCore.Utils
 import GHC.Core ( CoreExpr )
@@ -98,7 +99,13 @@ matchConFamily :: NonEmpty Id
                -> DsM (MatchResult CoreExpr)
 -- Each group of eqns is for a single constructor
 matchConFamily (var :| vars) ty groups
-  = do alts <- mapM (fmap toRealAlt . matchOneConLike vars ty) groups
+  = do let mult = idMult var
+           -- Each variable in the argument list correspond to one column in the
+           -- pattern matching equations. Its multiplicity is the context
+           -- multiplicity of the pattern. We extract that multiplicity, so that
+           -- 'matchOneconLike' knows the context multiplicity, in case it needs
+           -- to come up with new variables.
+       alts <- mapM (fmap toRealAlt . matchOneConLike vars ty mult) groups
        return (mkCoAlgCaseMatchResult var ty alts)
   where
     toRealAlt alt = case alt_pat alt of
@@ -110,7 +117,8 @@ matchPatSyn :: NonEmpty Id
             -> NonEmpty EquationInfo
             -> DsM (MatchResult CoreExpr)
 matchPatSyn (var :| vars) ty eqns
-  = do alt <- fmap toSynAlt $ matchOneConLike vars ty eqns
+  = do let mult = idMult var
+       alt <- fmap toSynAlt $ matchOneConLike vars ty mult eqns
        return (mkCoSynCaseMatchResult var ty alt)
   where
     toSynAlt alt = case alt_pat alt of
@@ -121,9 +129,10 @@ type ConArgPats = HsConDetails (LPat GhcTc) (HsRecFields GhcTc (LPat GhcTc))
 
 matchOneConLike :: [Id]
                 -> Type
+                -> Mult
                 -> NonEmpty EquationInfo
                 -> DsM (CaseAlt ConLike)
-matchOneConLike vars ty (eqn1 :| eqns)   -- All eqns for a single constructor
+matchOneConLike vars ty mult (eqn1 :| eqns)   -- All eqns for a single constructor
   = do  { let inst_tys = ASSERT( all tcIsTcTyVar ex_tvs )
                            -- ex_tvs can only be tyvars as data types in source
                            -- Haskell cannot mention covar yet (Aug 2018).
@@ -163,8 +172,15 @@ matchOneConLike vars ty (eqn1 :| eqns)   -- All eqns for a single constructor
                                   , eqn_pats = conArgPats val_arg_tys args ++ pats }
                             )
               shift (_, (EqnInfo { eqn_pats = ps })) = pprPanic "matchOneCon/shift" (ppr ps)
-
-        ; arg_vars <- selectConMatchVars val_arg_tys args1
+        ; let scaled_arg_tys = map (scaleScaled mult) val_arg_tys
+            -- The 'val_arg_tys' are taken from the data type definition, they
+            -- do not take into account the context multiplicity, therefore we
+            -- need to scale them back to get the correct context multiplicity
+            -- to desugar the sub-pattern in each field. We need to know these
+            -- multiplicity because of the invariant that, in Core, binders in a
+            -- constructor pattern must be scaled by the multiplicity of the
+            -- case. See Note [Case expression invariants].
+        ; arg_vars <- selectConMatchVars scaled_arg_tys args1
                 -- Use the first equation as a source of
                 -- suggestions for the new variables
 
@@ -229,12 +245,15 @@ same_fields flds1 flds2
 
 
 -----------------
-selectConMatchVars :: [Type] -> ConArgPats -> DsM [Id]
-selectConMatchVars arg_tys (RecCon {})      = newSysLocalsDsNoLP arg_tys
-selectConMatchVars _       (PrefixCon ps)   = selectMatchVars (map unLoc ps)
-selectConMatchVars _       (InfixCon p1 p2) = selectMatchVars [unLoc p1, unLoc p2]
+selectConMatchVars :: [Scaled Type] -> ConArgPats -> DsM [Id]
+selectConMatchVars arg_tys con = case con of
+                                   (RecCon {}) -> newSysLocalsDsNoLP arg_tys
+                                   (PrefixCon ps) -> selectMatchVars (zipMults arg_tys ps)
+                                   (InfixCon p1 p2) -> selectMatchVars (zipMults arg_tys [p1, p2])
+  where
+    zipMults = zipWithEqual "selectConMatchVar" (\a b -> (scaledMult a, unLoc b))
 
-conArgPats :: [Type]      -- Instantiated argument types
+conArgPats :: [Scaled Type]-- Instantiated argument types
                           -- Used only to fill in the types of WildPats, which
                           -- are probably never looked at anyway
            -> ConArgPats
@@ -242,7 +261,7 @@ conArgPats :: [Type]      -- Instantiated argument types
 conArgPats _arg_tys (PrefixCon ps)   = map unLoc ps
 conArgPats _arg_tys (InfixCon p1 p2) = [unLoc p1, unLoc p2]
 conArgPats  arg_tys (RecCon (HsRecFields { rec_flds = rpats }))
-  | null rpats = map WildPat arg_tys
+  | null rpats = map WildPat (map scaledThing arg_tys)
         -- Important special case for C {}, which can be used for a
         -- datacon that isn't declared to have fields at all
   | otherwise  = map (unLoc . hsRecFieldArg . unLoc) rpats
diff --git a/compiler/GHC/HsToCore/Match/Literal.hs b/compiler/GHC/HsToCore/Match/Literal.hs
index 600af91468..eb8f865aa1 100644
--- a/compiler/GHC/HsToCore/Match/Literal.hs
+++ b/compiler/GHC/HsToCore/Match/Literal.hs
@@ -39,6 +39,7 @@ import GHC.Core
 import GHC.Core.Make
 import GHC.Core.TyCon
 import GHC.Core.DataCon
+import GHC.Core.Multiplicity
 import GHC.Tc.Utils.Zonk ( shortCutLit )
 import GHC.Tc.Utils.TcType
 import GHC.Types.Name
@@ -148,7 +149,7 @@ warnAboutIdentities :: DynFlags -> CoreExpr -> Type -> DsM ()
 warnAboutIdentities dflags (Var conv_fn) type_of_conv
   | wopt Opt_WarnIdentities dflags
   , idName conv_fn `elem` conversionNames
-  , Just (arg_ty, res_ty) <- splitFunTy_maybe type_of_conv
+  , Just (Scaled _ arg_ty, res_ty) <- splitFunTy_maybe type_of_conv
   , arg_ty `eqType` res_ty  -- So we are converting  ty -> ty
   = warnDs (Reason Opt_WarnIdentities)
            (vcat [ text "Call of" <+> ppr conv_fn <+> dcolon <+> ppr type_of_conv