Linear types (#15981)

This is the first step towards implementation of the linear types proposal (ghc-proposals/ghc-proposals#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.
tweag · Jun 8, 2020 · 9a2cb22 · 9a2cb22
1 parent 2b792fa
commit 9a2cb22
Show file tree

Hide file tree

Showing 324 changed files with 6,040 additions and 2,011 deletions.
diff --git a/.gitmodules b/.gitmodules
@@ -89,7 +89,7 @@
 	ignore = untracked
 [submodule "utils/haddock"]
 	path = utils/haddock
-	url = https://gitlab.haskell.org/ghc/haddock.git
+	url = https://github.com/tweag/haddock.git
 	ignore = untracked
 	branch = ghc-head
 [submodule "nofib"]

diff --git a/compiler/GHC.hs b/compiler/GHC.hs
@@ -197,7 +197,7 @@ module GHC (
         -- ** Data constructors
         DataCon,
         dataConType, dataConTyCon, dataConFieldLabels,
-        dataConIsInfix, isVanillaDataCon, dataConUserType,
+        dataConIsInfix, isVanillaDataCon, dataConWrapperType,
         dataConSrcBangs,
         StrictnessMark(..), isMarkedStrict,
 

diff --git a/compiler/GHC/Builtin/Names.hs b/compiler/GHC/Builtin/Names.hs
@@ -1903,6 +1903,15 @@ typeSymbolAppendFamNameKey = mkPreludeTyConUnique 190
 unsafeEqualityTyConKey :: Unique
 unsafeEqualityTyConKey = mkPreludeTyConUnique 191
 
+-- Linear types
+multiplicityTyConKey :: Unique
+multiplicityTyConKey = mkPreludeTyConUnique 192
+
+unrestrictedFunTyConKey :: Unique
+unrestrictedFunTyConKey = mkPreludeTyConUnique 193
+
+multMulTyConKey :: Unique
+multMulTyConKey = mkPreludeTyConUnique 194
 
 ---------------- Template Haskell -------------------
 --      GHC.Builtin.Names.TH: USES TyConUniques 200-299
@@ -2077,6 +2086,12 @@ typeLitNatDataConKey      = mkPreludeDataConUnique 113
 unsafeReflDataConKey :: Unique
 unsafeReflDataConKey      = mkPreludeDataConUnique 114
 
+-- Multiplicity
+
+oneDataConKey, manyDataConKey :: Unique
+oneDataConKey = mkPreludeDataConUnique 115
+manyDataConKey = mkPreludeDataConUnique 116
+
 ---------------- Template Haskell -------------------
 --      GHC.Builtin.Names.TH: USES DataUniques 200-250
 -----------------------------------------------------

diff --git a/compiler/GHC/Builtin/Names/TH.hs b/compiler/GHC/Builtin/Names/TH.hs
@@ -98,7 +98,7 @@ templateHaskellNames = [
     -- Type
     forallTName, forallVisTName, varTName, conTName, infixTName, appTName,
     appKindTName, equalityTName, tupleTName, unboxedTupleTName,
-    unboxedSumTName, arrowTName, listTName, sigTName, litTName,
+    unboxedSumTName, arrowTName, mulArrowTName, listTName, sigTName, litTName,
     promotedTName, promotedTupleTName, promotedNilTName, promotedConsTName,
     wildCardTName, implicitParamTName,
     -- TyLit
@@ -438,8 +438,8 @@ recordPatSynName = libFun (fsLit "recordPatSyn") recordPatSynIdKey
 
 -- data Type = ...
 forallTName, forallVisTName, varTName, conTName, infixTName, tupleTName,
-    unboxedTupleTName, unboxedSumTName, arrowTName, listTName, appTName,
-    appKindTName, sigTName, equalityTName, litTName, promotedTName,
+    unboxedTupleTName, unboxedSumTName, arrowTName, mulArrowTName, listTName,
+    appTName, appKindTName, sigTName, equalityTName, litTName, promotedTName,
     promotedTupleTName, promotedNilTName, promotedConsTName,
     wildCardTName, implicitParamTName :: Name
 forallTName         = libFun (fsLit "forallT")        forallTIdKey
@@ -450,6 +450,7 @@ tupleTName          = libFun (fsLit "tupleT")         tupleTIdKey
 unboxedTupleTName   = libFun (fsLit "unboxedTupleT")  unboxedTupleTIdKey
 unboxedSumTName     = libFun (fsLit "unboxedSumT")    unboxedSumTIdKey
 arrowTName          = libFun (fsLit "arrowT")         arrowTIdKey
+mulArrowTName       = libFun (fsLit "mulArrowT")      mulArrowTIdKey
 listTName           = libFun (fsLit "listT")          listTIdKey
 appTName            = libFun (fsLit "appT")           appTIdKey
 appKindTName        = libFun (fsLit "appKindT")       appKindTIdKey
@@ -1046,6 +1047,10 @@ interruptibleIdKey = mkPreludeMiscIdUnique 442
 funDepIdKey :: Unique
 funDepIdKey = mkPreludeMiscIdUnique 445
 
+-- mulArrow
+mulArrowTIdKey :: Unique
+mulArrowTIdKey = mkPreludeMiscIdUnique 446
+
 -- data TySynEqn = ...
 tySynEqnIdKey :: Unique
 tySynEqnIdKey = mkPreludeMiscIdUnique 460

diff --git a/compiler/GHC/Builtin/PrimOps.hs b/compiler/GHC/Builtin/PrimOps.hs
@@ -579,7 +579,7 @@ primOpType op
     Compare _occ ty -> compare_fun_ty ty
 
     GenPrimOp _occ tyvars arg_tys res_ty ->
-        mkSpecForAllTys tyvars (mkVisFunTys arg_tys res_ty)
+        mkSpecForAllTys tyvars (mkVisFunTysMany arg_tys res_ty)
 
 primOpOcc :: PrimOp -> OccName
 primOpOcc op = case primOpInfo op of
@@ -739,9 +739,9 @@ commutableOp :: PrimOp -> Bool
 -- Utils:
 
 dyadic_fun_ty, monadic_fun_ty, compare_fun_ty :: Type -> Type
-dyadic_fun_ty  ty = mkVisFunTys [ty, ty] ty
-monadic_fun_ty ty = mkVisFunTy  ty ty
-compare_fun_ty ty = mkVisFunTys [ty, ty] intPrimTy
+dyadic_fun_ty  ty = mkVisFunTysMany [ty, ty] ty
+monadic_fun_ty ty = mkVisFunTyMany  ty ty
+compare_fun_ty ty = mkVisFunTysMany [ty, ty] intPrimTy
 
 -- Output stuff:
 

diff --git a/compiler/GHC/Builtin/Types.hs b/compiler/GHC/Builtin/Types.hs
@@ -125,7 +125,17 @@ module GHC.Builtin.Types (
         int8ElemRepDataConTy, int16ElemRepDataConTy, int32ElemRepDataConTy,
         int64ElemRepDataConTy, word8ElemRepDataConTy, word16ElemRepDataConTy,
         word32ElemRepDataConTy, word64ElemRepDataConTy, floatElemRepDataConTy,
-        doubleElemRepDataConTy
+
+        doubleElemRepDataConTy,
+
+        -- * Multiplicity and friends
+        multiplicityTyConName, oneDataConName, manyDataConName, multiplicityTy,
+        multiplicityTyCon, oneDataCon, manyDataCon, oneDataConTy, manyDataConTy,
+        oneDataConTyCon, manyDataConTyCon,
+        multMulTyCon,
+
+        unrestrictedFunTyCon, unrestrictedFunTyConName
+
     ) where
 
 #include "HsVersions.h"
@@ -142,6 +152,7 @@ import {-# SOURCE #-} GHC.Builtin.Uniques
 -- others:
 import GHC.Core.Coercion.Axiom
 import GHC.Types.Id
+import GHC.Types.Var (VarBndr (Bndr))
 import GHC.Settings.Constants ( mAX_TUPLE_SIZE, mAX_CTUPLE_SIZE, mAX_SUM_SIZE )
 import GHC.Unit.Module        ( Module )
 import GHC.Core.Type
@@ -150,6 +161,7 @@ import GHC.Core.DataCon
 import {-# SOURCE #-} GHC.Core.ConLike
 import GHC.Core.TyCon
 import GHC.Core.Class     ( Class, mkClass )
+import GHC.Core.Multiplicity
 import GHC.Types.Name.Reader
 import GHC.Types.Name as Name
 import GHC.Types.Name.Env ( NameEnv, mkNameEnv, lookupNameEnv, lookupNameEnv_NF )
@@ -240,6 +252,7 @@ wiredInTyCons = [ -- Units are not treated like other tuples, because they
                 , vecElemTyCon
                 , constraintKindTyCon
                 , liftedTypeKindTyCon
+                , multiplicityTyCon
                 ]
 
 mkWiredInTyConName :: BuiltInSyntax -> Module -> FastString -> Unique -> TyCon -> Name
@@ -461,6 +474,20 @@ constraintKindTyConName = mkWiredInTyConName UserSyntax gHC_TYPES (fsLit "Constr
 liftedTypeKindTyConName :: Name
 liftedTypeKindTyConName = mkWiredInTyConName UserSyntax gHC_TYPES (fsLit "Type") liftedTypeKindTyConKey liftedTypeKindTyCon
 
+multiplicityTyConName :: Name
+multiplicityTyConName = mkWiredInTyConName UserSyntax gHC_TYPES (fsLit "Multiplicity")
+                          multiplicityTyConKey multiplicityTyCon
+
+oneDataConName, manyDataConName :: Name
+oneDataConName = mkWiredInDataConName BuiltInSyntax gHC_TYPES (fsLit "One") oneDataConKey oneDataCon
+manyDataConName = mkWiredInDataConName BuiltInSyntax gHC_TYPES (fsLit "Many") manyDataConKey manyDataCon
+ -- It feels wrong to have One and Many be BuiltInSyntax. But otherwise,
+ -- `Many`, in particular, is considered out of scope unless an appropriate
+ -- file is open. The problem with this is that `Many` appears implicitly in
+ -- types every time there is an `(->)`, hence out-of-scope errors get
+ -- reported. Making them built-in make it so that they are always considered in
+ -- scope.
+
 runtimeRepTyConName, vecRepDataConName, tupleRepDataConName, sumRepDataConName :: Name
 runtimeRepTyConName = mkWiredInTyConName UserSyntax gHC_TYPES (fsLit "RuntimeRep") runtimeRepTyConKey runtimeRepTyCon
 vecRepDataConName = mkWiredInDataConName UserSyntax gHC_TYPES (fsLit "VecRep") vecRepDataConKey vecRepDataCon
@@ -544,16 +571,20 @@ pcTyCon name cType tyvars cons
                 False           -- Not in GADT syntax
 
 pcDataCon :: Name -> [TyVar] -> [Type] -> TyCon -> DataCon
-pcDataCon n univs = pcDataConWithFixity False n univs
+pcDataCon n univs tys = pcDataConW n univs (map linear tys)
+
+pcDataConW :: Name -> [TyVar] -> [Scaled Type] -> TyCon -> DataCon
+pcDataConW n univs tys = pcDataConWithFixity False n univs
                       []    -- no ex_tvs
                       univs -- the univs are precisely the user-written tyvars
+                      tys
 
 pcDataConWithFixity :: Bool      -- ^ declared infix?
                     -> Name      -- ^ datacon name
                     -> [TyVar]   -- ^ univ tyvars
                     -> [TyCoVar] -- ^ ex tycovars
                     -> [TyCoVar] -- ^ user-written tycovars
-                    -> [Type]    -- ^ args
+                    -> [Scaled Type]    -- ^ args
                     -> TyCon
                     -> DataCon
 pcDataConWithFixity infx n = pcDataConWithFixity' infx n (dataConWorkerUnique (nameUnique n))
@@ -567,7 +598,7 @@ pcDataConWithFixity infx n = pcDataConWithFixity' infx n (dataConWorkerUnique (n
 
 pcDataConWithFixity' :: Bool -> Name -> Unique -> RuntimeRepInfo
                      -> [TyVar] -> [TyCoVar] -> [TyCoVar]
-                     -> [Type] -> TyCon -> DataCon
+                     -> [Scaled Type] -> TyCon -> DataCon
 -- The Name should be in the DataName name space; it's the name
 -- of the DataCon itself.
 --
@@ -625,7 +656,7 @@ mkDataConWorkerName data_con wrk_key =
 pcSpecialDataCon :: Name -> [Type] -> TyCon -> RuntimeRepInfo -> DataCon
 pcSpecialDataCon dc_name arg_tys tycon rri
   = pcDataConWithFixity' False dc_name (dataConWorkerUnique (nameUnique dc_name)) rri
-                         [] [] [] arg_tys tycon
+                         [] [] [] (map linear arg_tys) tycon
 
 {-
 ************************************************************************
@@ -651,7 +682,7 @@ constraintKindTyCon = pcTyCon constraintKindTyConName Nothing [] []
 
 liftedTypeKind, typeToTypeKind, constraintKind :: Kind
 liftedTypeKind   = tYPE liftedRepTy
-typeToTypeKind   = liftedTypeKind `mkVisFunTy` liftedTypeKind
+typeToTypeKind   = liftedTypeKind `mkVisFunTyMany` liftedTypeKind
 constraintKind   = mkTyConApp constraintKindTyCon []
 
 {-
@@ -791,7 +822,8 @@ isBuiltInOcc_maybe occ =
       "~"    -> Just eqTyConName
 
       -- function tycon
-      "->"   -> Just funTyConName
+      "FUN"  -> Just funTyConName
+      "->"  -> Just unrestrictedFunTyConName
 
       -- boxed tuple data/tycon
       -- We deliberately exclude Solo (the boxed 1-tuple).
@@ -1149,7 +1181,7 @@ eqSCSelId, heqSCSelId, coercibleSCSelId :: Id
                              rhs klass
                              (mkPrelTyConRepName eqTyConName)
     klass     = mk_class tycon sc_pred sc_sel_id
-    datacon   = pcDataCon eqDataConName tvs [sc_pred] tycon
+    datacon   = pcDataConW eqDataConName tvs [unrestricted sc_pred] tycon
 
     -- Kind: forall k. k -> k -> Constraint
     binders   = mkTemplateTyConBinders [liftedTypeKind] (\[k] -> [k,k])
@@ -1167,7 +1199,7 @@ eqSCSelId, heqSCSelId, coercibleSCSelId :: Id
                              rhs klass
                              (mkPrelTyConRepName heqTyConName)
     klass     = mk_class tycon sc_pred sc_sel_id
-    datacon   = pcDataCon heqDataConName tvs [sc_pred] tycon
+    datacon   = pcDataConW heqDataConName tvs [unrestricted sc_pred] tycon
 
     -- Kind: forall k1 k2. k1 -> k2 -> Constraint
     binders   = mkTemplateTyConBinders [liftedTypeKind, liftedTypeKind] id
@@ -1185,7 +1217,7 @@ eqSCSelId, heqSCSelId, coercibleSCSelId :: Id
                              rhs klass
                              (mkPrelTyConRepName coercibleTyConName)
     klass     = mk_class tycon sc_pred sc_sel_id
-    datacon   = pcDataCon coercibleDataConName tvs [sc_pred] tycon
+    datacon   = pcDataConW coercibleDataConName tvs [unrestricted sc_pred] tycon
 
     -- Kind: forall k. k -> k -> Constraint
     binders   = mkTemplateTyConBinders [liftedTypeKind] (\[k] -> [k,k])
@@ -1203,6 +1235,67 @@ mk_class tycon sc_pred sc_sel_id
 
 
 
+{- *********************************************************************
+*                                                                      *
+                Multiplicity Polymorphism
+*                                                                      *
+********************************************************************* -}
+
+{- Multiplicity polymorphism is implemented very similarly to levity
+ polymorphism. We write in the multiplicity kind and the One and Many
+ types which can appear in user programs. These are defined properly in GHC.Types.
+
+data Multiplicity = One | Many
+-}
+
+multiplicityTy :: Type
+multiplicityTy = mkTyConTy multiplicityTyCon
+
+multiplicityTyCon :: TyCon
+multiplicityTyCon = pcTyCon multiplicityTyConName Nothing []
+                          [oneDataCon, manyDataCon]
+
+oneDataCon, manyDataCon :: DataCon
+oneDataCon = pcDataCon oneDataConName [] [] multiplicityTyCon
+manyDataCon = pcDataCon manyDataConName [] [] multiplicityTyCon
+
+oneDataConTy, manyDataConTy :: Type
+oneDataConTy = mkTyConTy oneDataConTyCon
+manyDataConTy = mkTyConTy manyDataConTyCon
+
+oneDataConTyCon, manyDataConTyCon :: TyCon
+oneDataConTyCon = promoteDataCon oneDataCon
+manyDataConTyCon = promoteDataCon manyDataCon
+
+multMulTyConName :: Name
+multMulTyConName =
+    mkWiredInTyConName UserSyntax gHC_TYPES (fsLit "MultMul") multMulTyConKey multMulTyCon
+
+multMulTyCon :: TyCon
+multMulTyCon = mkFamilyTyCon multMulTyConName binders multiplicityTy Nothing
+                         (BuiltInSynFamTyCon trivialBuiltInFamily)
+                         Nothing
+                         NotInjective
+  where
+    binders = mkTemplateAnonTyConBinders [multiplicityTy, multiplicityTy]
+
+unrestrictedFunTy :: Type
+unrestrictedFunTy = functionWithMultiplicity manyDataConTy
+
+unrestrictedFunTyCon :: TyCon
+unrestrictedFunTyCon = buildSynTyCon unrestrictedFunTyConName [] arrowKind [] unrestrictedFunTy
+  where arrowKind = mkTyConKind binders liftedTypeKind
+        -- See also funTyCon
+        binders = [ Bndr runtimeRep1TyVar (NamedTCB Inferred)
+                  , Bndr runtimeRep2TyVar (NamedTCB Inferred)
+                  ]
+                  ++ mkTemplateAnonTyConBinders [ tYPE runtimeRep1Ty
+                                                , tYPE runtimeRep2Ty
+                                                ]
+
+unrestrictedFunTyConName :: Name
+unrestrictedFunTyConName = mkWiredInTyConName BuiltInSyntax gHC_TYPES (fsLit "->") unrestrictedFunTyConKey unrestrictedFunTyCon
+
 {- *********************************************************************
 *                                                                      *
                 Kinds and RuntimeRep
@@ -1576,7 +1669,7 @@ consDataCon :: DataCon
 consDataCon = pcDataConWithFixity True {- Declared infix -}
                consDataConName
                alpha_tyvar [] alpha_tyvar
-               [alphaTy, mkTyConApp listTyCon alpha_ty] listTyCon
+               (map linear [alphaTy, mkTyConApp listTyCon alpha_ty]) listTyCon
 -- Interesting: polymorphic recursion would help here.
 -- We can't use (mkListTy alphaTy) in the defn of consDataCon, else mkListTy
 -- gets the over-specific type (Type -> Type)

diff --git a/compiler/GHC/Builtin/Types.hs-boot b/compiler/GHC/Builtin/Types.hs-boot
@@ -44,4 +44,13 @@ anyTypeOfKind :: Kind -> Type
 unboxedTupleKind :: [Type] -> Type
 mkPromotedListTy :: Type -> [Type] -> Type
 
+multiplicityTyCon :: TyCon
+multiplicityTy :: Type
+oneDataConTy :: Type
+oneDataConTyCon :: TyCon
+manyDataConTy :: Type
+manyDataConTyCon :: TyCon
+unrestrictedFunTyCon :: TyCon
+multMulTyCon :: TyCon
+
 tupleTyConName :: TupleSort -> Arity -> Name