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.

5 files changed, 31 insertions, 17 deletions

diff --git a/compiler/GHC/Tc/Deriv/Functor.hs b/compiler/GHC/Tc/Deriv/Functor.hs
index 6a13cfaccd..a1af9166fe 100644
--- a/compiler/GHC/Tc/Deriv/Functor.hs
+++ b/compiler/GHC/Tc/Deriv/Functor.hs
@@ -40,6 +40,7 @@ import GHC.Tc.Utils.TcType
 import GHC.Core.TyCon
 import GHC.Core.TyCo.Rep
 import GHC.Core.Type
+import GHC.Core.Multiplicity
 import GHC.Utils.Misc
 import GHC.Types.Var
 import GHC.Types.Var.Set
@@ -557,7 +558,7 @@ deepSubtypesContaining tv
 foldDataConArgs :: FFoldType a -> DataCon -> [a]
 -- Fold over the arguments of the datacon
 foldDataConArgs ft con
-  = map foldArg (dataConOrigArgTys con)
+  = map foldArg (map scaledThing $ dataConOrigArgTys con)
   where
     foldArg
       = case getTyVar_maybe (last (tyConAppArgs (dataConOrigResTy con))) of
diff --git a/compiler/GHC/Tc/Deriv/Generate.hs b/compiler/GHC/Tc/Deriv/Generate.hs
index a9791043a2..7fa9975790 100644
--- a/compiler/GHC/Tc/Deriv/Generate.hs
+++ b/compiler/GHC/Tc/Deriv/Generate.hs
@@ -66,6 +66,7 @@ import GHC.Core.Coercion.Axiom ( coAxiomSingleBranch )
 import GHC.Builtin.Types.Prim
 import GHC.Builtin.Types
 import GHC.Core.Type
+import GHC.Core.Multiplicity
 import GHC.Core.Class
 import GHC.Types.Var.Set
 import GHC.Types.Var.Env
@@ -210,7 +211,7 @@ gen_Eq_binds loc tycon = do
             bs_needed   = take con_arity bs_RDRs
             tys_needed  = dataConOrigArgTys data_con
         in
-        ([con1_pat, con2_pat], nested_eq_expr tys_needed as_needed bs_needed)
+        ([con1_pat, con2_pat], nested_eq_expr (map scaledThing tys_needed) as_needed bs_needed)
       where
         nested_eq_expr []  [] [] = true_Expr
         nested_eq_expr tys as bs
@@ -456,7 +457,7 @@ gen_Ord_binds loc tycon = do
     -- Returns a case alternative  Ki b1 b2 ... bv -> compare (a1,a2,...) with (b1,b2,...)
     mkInnerEqAlt op data_con
       = mkHsCaseAlt (nlConVarPat data_con_RDR bs_needed) $
-        mkCompareFields op (dataConOrigArgTys data_con)
+        mkCompareFields op (map scaledThing $ dataConOrigArgTys data_con)
       where
         data_con_RDR = getRdrName data_con
         bs_needed    = take (dataConSourceArity data_con) bs_RDRs
@@ -1044,7 +1045,7 @@ gen_Read_binds get_fixity loc tycon
         is_infix     = dataConIsInfix data_con
         is_record    = labels `lengthExceeds` 0
         as_needed    = take con_arity as_RDRs
-        read_args    = zipWithEqual "gen_Read_binds" read_arg as_needed (dataConOrigArgTys data_con)
+        read_args    = zipWithEqual "gen_Read_binds" read_arg as_needed (map scaledThing $ dataConOrigArgTys data_con)
         (read_a1:read_a2:_) = read_args
 
         prefix_prec = appPrecedence
@@ -1187,7 +1188,7 @@ gen_Show_binds get_fixity loc tycon
                  where
                    nm       = wrapOpParens (unpackFS l)
 
-             show_args               = zipWithEqual "gen_Show_binds" show_arg bs_needed arg_tys
+             show_args               = zipWithEqual "gen_Show_binds" show_arg bs_needed (map scaledThing arg_tys)
              (show_arg1:show_arg2:_) = show_args
              show_prefix_args        = intersperse (nlHsVar showSpace_RDR) show_args
 
@@ -1378,7 +1379,7 @@ gen_data dflags data_type_name constr_names loc rep_tc
 
     gfoldl_eqn con
       = ([nlVarPat k_RDR, z_Pat, nlConVarPat con_name as_needed],
-                   foldl' mk_k_app (z_Expr `nlHsApp` nlHsVar con_name) as_needed)
+                   foldl' mk_k_app (z_Expr `nlHsApp` (eta_expand_data_con con)) as_needed)
                    where
                      con_name ::  RdrName
                      con_name = getRdrName con
@@ -1398,9 +1399,18 @@ gen_data dflags data_type_name constr_names loc rep_tc
 
     gunfold_alt dc = mkHsCaseAlt (mk_unfold_pat dc) (mk_unfold_rhs dc)
     mk_unfold_rhs dc = foldr nlHsApp
-                           (z_Expr `nlHsApp` nlHsVar (getRdrName dc))
+                           (z_Expr `nlHsApp` (eta_expand_data_con dc))
                            (replicate (dataConSourceArity dc) (nlHsVar k_RDR))
 
+    eta_expand_data_con dc =
+        mkHsLam eta_expand_pats
+          (foldl nlHsApp (nlHsVar (getRdrName dc)) eta_expand_hsvars)
+      where
+        eta_expand_pats = map nlVarPat eta_expand_vars
+        eta_expand_hsvars = map nlHsVar eta_expand_vars
+        eta_expand_vars = take (dataConSourceArity dc) as_RDRs
+
+
     mk_unfold_pat dc    -- Last one is a wild-pat, to avoid
                         -- redundant test, and annoying warning
       | tag-fIRST_TAG == n_cons-1 = nlWildPat   -- Last constructor
@@ -1448,7 +1458,7 @@ gen_data dflags data_type_name constr_names loc rep_tc
 
 kind1, kind2 :: Kind
 kind1 = typeToTypeKind
-kind2 = liftedTypeKind `mkVisFunTy` kind1
+kind2 = liftedTypeKind `mkVisFunTyMany` kind1
 
 gfoldl_RDR, gunfold_RDR, toConstr_RDR, dataTypeOf_RDR, mkConstr_RDR,
     mkDataType_RDR, conIndex_RDR, prefix_RDR, infix_RDR,
@@ -1960,7 +1970,7 @@ genAuxBindSpec dflags loc (DerivCon2Tag tycon)
 
     sig_ty = mkLHsSigWcType $ L loc $ XHsType $ NHsCoreTy $
              mkSpecSigmaTy (tyConTyVars tycon) (tyConStupidTheta tycon) $
-             mkParentType tycon `mkVisFunTy` intPrimTy
+             mkParentType tycon `mkVisFunTyMany` intPrimTy
 
     lots_of_constructors = tyConFamilySize tycon > 8
                         -- was: mAX_FAMILY_SIZE_FOR_VEC_RETURNS
@@ -1984,7 +1994,7 @@ genAuxBindSpec dflags loc (DerivTag2Con tycon)
   where
     sig_ty = mkLHsSigWcType $ L loc $
              XHsType $ NHsCoreTy $ mkSpecForAllTys (tyConTyVars tycon) $
-             intTy `mkVisFunTy` mkParentType tycon
+             intTy `mkVisFunTyMany` mkParentType tycon
 
     rdr_name = tag2con_RDR dflags tycon
 
diff --git a/compiler/GHC/Tc/Deriv/Generics.hs b/compiler/GHC/Tc/Deriv/Generics.hs
index ced6f4b690..ea9862d305 100644
--- a/compiler/GHC/Tc/Deriv/Generics.hs
+++ b/compiler/GHC/Tc/Deriv/Generics.hs
@@ -29,6 +29,7 @@ import GHC.Tc.Deriv.Functor
 import GHC.Core.DataCon
 import GHC.Core.TyCon
 import GHC.Core.FamInstEnv ( FamInst, FamFlavor(..), mkSingleCoAxiom )
+import GHC.Core.Multiplicity
 import GHC.Tc.Instance.Family
 import GHC.Unit.Module ( moduleName, moduleNameFS
                         , moduleUnit, unitFS, getModule )
@@ -168,7 +169,7 @@ canDoGenerics tc
         -- then we can't build the embedding-projection pair, because
         -- it relies on instantiating *polymorphic* sum and product types
         -- at the argument types of the constructors
-    bad_con dc = if (any bad_arg_type (dataConOrigArgTys dc))
+    bad_con dc = if (any bad_arg_type (map scaledThing $ dataConOrigArgTys dc))
                   then (NotValid (ppr dc <+> text
                     "must not have exotic unlifted or polymorphic arguments"))
                   else (if (not (isVanillaDataCon dc))
@@ -575,7 +576,7 @@ tc_mkRepTy gk_ tycon k =
         mkD    a   = mkTyConApp d1 [ k, metaDataTy, sumP (tyConDataCons a) ]
         mkC      a = mkTyConApp c1 [ k
                                    , metaConsTy a
-                                   , prod (dataConInstOrigArgTys a
+                                   , prod (map scaledThing . dataConInstOrigArgTys a
                                             . mkTyVarTys . tyConTyVars $ tycon)
                                           (dataConSrcBangs    a)
                                           (dataConImplBangs   a)
@@ -741,7 +742,7 @@ mk1Sum gk_ us i n datacon = (from_alt, to_alt)
     argTys = dataConOrigArgTys datacon
     n_args = dataConSourceArity datacon
 
-    datacon_varTys = zip (map mkGenericLocal [us .. us+n_args-1]) argTys
+    datacon_varTys = zip (map mkGenericLocal [us .. us+n_args-1]) (map scaledThing argTys)
     datacon_vars = map fst datacon_varTys
 
     datacon_rdr  = getRdrName datacon
diff --git a/compiler/GHC/Tc/Deriv/Infer.hs b/compiler/GHC/Tc/Deriv/Infer.hs
index 56dafd2097..17eff9a74b 100644
--- a/compiler/GHC/Tc/Deriv/Infer.hs
+++ b/compiler/GHC/Tc/Deriv/Infer.hs
@@ -41,6 +41,7 @@ import GHC.Tc.Utils.TcType
 import GHC.Core.TyCon
 import GHC.Core.TyCo.Ppr (pprTyVars)
 import GHC.Core.Type
+import GHC.Core.Multiplicity
 import GHC.Tc.Solver
 import GHC.Tc.Validity (validDerivPred)
 import GHC.Tc.Utils.Unify (buildImplicationFor, checkConstraints)
@@ -186,10 +187,10 @@ inferConstraintsStock (DerivInstTys { dit_cls_tys     = cls_tys
                             dataConInstOrigArgTys data_con all_rep_tc_args
                        -- No constraints for unlifted types
                        -- See Note [Deriving and unboxed types]
-                     , not (isUnliftedType arg_ty)
+                     , not (isUnliftedType (irrelevantMult arg_ty))
                      , let orig = DerivOriginDC data_con arg_n wildcard
                      , preds_and_mbSubst
-                         <- get_arg_constraints orig arg_t_or_k arg_ty
+                         <- get_arg_constraints orig arg_t_or_k (irrelevantMult arg_ty)
                      ]
                    preds = concat predss
                    -- If the constraints require a subtype to be of kind
diff --git a/compiler/GHC/Tc/Deriv/Utils.hs b/compiler/GHC/Tc/Deriv/Utils.hs
index 66adb4e554..e118c69830 100644
--- a/compiler/GHC/Tc/Deriv/Utils.hs
+++ b/compiler/GHC/Tc/Deriv/Utils.hs
@@ -48,6 +48,7 @@ import GHC.Tc.Utils.Monad
 import GHC.Tc.Utils.TcType
 import GHC.Builtin.Names.TH (liftClassKey)
 import GHC.Core.TyCon
+import GHC.Core.Multiplicity
 import GHC.Core.TyCo.Ppr (pprSourceTyCon)
 import GHC.Core.Type
 import GHC.Utils.Misc
@@ -853,7 +854,7 @@ cond_stdOK deriv_ctxt permissive dflags tc rep_tc
       = bad "has existential type variables in its type"
       | not (null theta) -- 4.
       = bad "has constraints in its type"
-      | not (permissive || all isTauTy (dataConOrigArgTys con)) -- 5.
+      | not (permissive || all isTauTy (map scaledThing $ dataConOrigArgTys con)) -- 5.
       = bad "has a higher-rank type"
       | otherwise
       = IsValid
@@ -887,7 +888,7 @@ cond_args cls _ _ rep_tc
                              2 (text "for type" <+> quotes (ppr ty)))
   where
     bad_args = [ arg_ty | con <- tyConDataCons rep_tc
-                        , arg_ty <- dataConOrigArgTys con
+                        , Scaled _ arg_ty <- dataConOrigArgTys con
                         , isLiftedType_maybe arg_ty /= Just True
                         , not (ok_ty arg_ty) ]