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, 8 insertions, 7 deletions

diff --git a/compiler/GHC/Tc/TyCl/Build.hs b/compiler/GHC/Tc/TyCl/Build.hs
index af49e9e28c..5361ff0160 100644
--- a/compiler/GHC/Tc/TyCl/Build.hs
+++ b/compiler/GHC/Tc/TyCl/Build.hs
@@ -36,6 +36,7 @@ import GHC.Core.TyCon
 import GHC.Core.Type
 import GHC.Types.Id
 import GHC.Tc.Utils.TcType
+import GHC.Core.Multiplicity
 
 import GHC.Types.SrcLoc( SrcSpan, noSrcSpan )
 import GHC.Driver.Session
@@ -65,7 +66,7 @@ mkNewTyConRhs tycon_name tycon con
     roles    = tyConRoles tycon
     res_kind = tyConResKind tycon
     con_arg_ty = case dataConRepArgTys con of
-                   [arg_ty] -> arg_ty
+                   [arg_ty] -> scaledThing arg_ty
                    tys -> pprPanic "mkNewTyConRhs" (ppr con <+> ppr tys)
     rhs_ty = substTyWith (dataConUnivTyVars con)
                          (mkTyVarTys tvs) con_arg_ty
@@ -110,7 +111,7 @@ buildDataCon :: FamInstEnvs
            -> [EqSpec]                 -- Equality spec
            -> KnotTied ThetaType       -- Does not include the "stupid theta"
                                        -- or the GADT equalities
-           -> [KnotTied Type]          -- Arguments
+           -> [KnotTied (Scaled Type)] -- Arguments
            -> KnotTied Type            -- Result types
            -> KnotTied TyCon           -- Rep tycon
            -> NameEnv ConTag           -- Maps the Name of each DataCon to its
@@ -132,7 +133,7 @@ buildDataCon fam_envs src_name declared_infix prom_info src_bangs impl_bangs
         ; traceIf (text "buildDataCon 1" <+> ppr src_name)
         ; us <- newUniqueSupply
         ; dflags <- getDynFlags
-        ; let stupid_ctxt = mkDataConStupidTheta rep_tycon arg_tys univ_tvs
+        ; let stupid_ctxt = mkDataConStupidTheta rep_tycon (map scaledThing arg_tys) univ_tvs
               tag = lookupNameEnv_NF tag_map src_name
               -- See Note [Constructor tag allocation], fixes #14657
               data_con = mkDataCon src_name declared_infix prom_info
@@ -184,10 +185,10 @@ buildPatSyn src_name declared_infix matcher@(matcher_id,_) builder
     -- compatible with the pattern synonym
     ASSERT2((and [ univ_tvs `equalLength` univ_tvs1
                  , ex_tvs `equalLength` ex_tvs1
-                 , pat_ty `eqType` substTy subst pat_ty1
+                 , pat_ty `eqType` substTy subst (scaledThing pat_ty1)
                  , prov_theta `eqTypes` substTys subst prov_theta1
                  , req_theta `eqTypes` substTys subst req_theta1
-                 , compareArgTys arg_tys (substTys subst arg_tys1)
+                 , compareArgTys arg_tys (substTys subst (map scaledThing arg_tys1))
                  ])
             , (vcat [ ppr univ_tvs <+> twiddle <+> ppr univ_tvs1
                     , ppr ex_tvs <+> twiddle <+> ppr ex_tvs1
@@ -202,7 +203,7 @@ buildPatSyn src_name declared_infix matcher@(matcher_id,_) builder
   where
     ((_:_:univ_tvs1), req_theta1, tau) = tcSplitSigmaTy $ idType matcher_id
     ([pat_ty1, cont_sigma, _], _)      = tcSplitFunTys tau
-    (ex_tvs1, prov_theta1, cont_tau)   = tcSplitSigmaTy cont_sigma
+    (ex_tvs1, prov_theta1, cont_tau)   = tcSplitSigmaTy (scaledThing cont_sigma)
     (arg_tys1, _) = (tcSplitFunTys cont_tau)
     twiddle = char '~'
     subst = zipTvSubst (univ_tvs1 ++ ex_tvs1)
@@ -314,7 +315,7 @@ buildClass tycon_name binders roles fds
                                    univ_bndrs
                                    [{- No GADT equalities -}]
                                    [{- No theta -}]
-                                   arg_tys
+                                   (map unrestricted arg_tys) -- type classes are unrestricted
                                    (mkTyConApp rec_tycon (mkTyVarTys univ_tvs))
                                    rec_tycon
                                    (mkTyConTagMap rec_tycon)