From 27abfd0023589cb6ee3363512d160df2d1016275 Mon Sep 17 00:00:00 2001 From: Sebastian Graf Date: Sun, 3 Nov 2019 19:42:52 +0000 Subject: Implement the UnliftedDatatypes extension GHC Proposal: 0265-unlifted-datatypes.rst Discussion: https://github.com/ghc-proposals/ghc-proposals/pull/265 Issues: https://gitlab.haskell.org/ghc/ghc/-/issues/19523 Implementation Details: Note [Implementation of UnliftedDatatypes] This patch introduces the `UnliftedDatatypes` extension. When this extension is enabled, GHC relaxes the restrictions around what result kinds are allowed in data declarations. This allows data types for which an unlifted or levity-polymorphic result kind is inferred. The most significant changes are in `GHC.Tc.TyCl`, where `Note [Implementation of UnliftedDatatypes]` describes the details of the implementation. Fixes #19523. --- compiler/GHC/Builtin/Types.hs | 7 +- compiler/GHC/Core/Lint.hs | 1 + compiler/GHC/Core/TyCon.hs | 2 +- compiler/GHC/Core/Type.hs | 213 +++++++++++++-------- compiler/GHC/CoreToStg.hs | 19 +- compiler/GHC/Driver/Session.hs | 5 + compiler/GHC/Stg/Lint.hs | 8 +- compiler/GHC/Stg/Syntax.hs | 2 +- compiler/GHC/StgToCmm/Env.hs | 11 +- compiler/GHC/Tc/Gen/HsType.hs | 107 +++++++---- compiler/GHC/Tc/TyCl.hs | 89 +++++++-- compiler/GHC/Tc/TyCl/Instance.hs | 15 +- compiler/GHC/Tc/Utils/TcMType.hs | 7 + docs/users_guide/9.2.1-notes.rst | 19 ++ docs/users_guide/exts/primitives.rst | 98 +++++++++- .../ghc-boot-th/GHC/LanguageExtensions/Type.hs | 1 + libraries/ghc-prim/GHC/Types.hs | 3 +- testsuite/tests/driver/T4437.hs | 1 + testsuite/tests/unlifted-datatypes/Makefile | 3 + .../unlifted-datatypes/should_compile/Makefile | 3 + .../should_compile/UnlDataFams.hs | 49 +++++ .../should_compile/UnlDataMonoSigs.hs | 22 +++ .../should_compile/UnlDataPolySigs.hs | 31 +++ .../should_compile/UnlDataUsersGuide.hs | 38 ++++ .../tests/unlifted-datatypes/should_compile/all.T | 4 + .../tests/unlifted-datatypes/should_fail/Makefile | 3 + .../should_fail/UnlDataInvalidResKind1.hs | 9 + .../should_fail/UnlDataInvalidResKind1.stderr | 4 + .../should_fail/UnlDataInvalidResKind2.hs | 22 +++ .../should_fail/UnlDataNullaryPoly.hs | 10 + .../should_fail/UnlDataNullaryPoly.stderr | 7 + .../tests/unlifted-datatypes/should_fail/all.T | 2 + .../tests/unlifted-datatypes/should_run/Makefile | 3 + .../unlifted-datatypes/should_run/UnlData1.hs | 34 ++++ .../unlifted-datatypes/should_run/UnlData1.stdout | 4 + .../unlifted-datatypes/should_run/UnlGadt1.hs | 20 ++ .../unlifted-datatypes/should_run/UnlGadt1.stderr | 3 + .../unlifted-datatypes/should_run/UnlGadt1.stdout | 1 + .../tests/unlifted-datatypes/should_run/all.T | 2 + 39 files changed, 719 insertions(+), 163 deletions(-) create mode 100644 testsuite/tests/unlifted-datatypes/Makefile create mode 100644 testsuite/tests/unlifted-datatypes/should_compile/Makefile create mode 100644 testsuite/tests/unlifted-datatypes/should_compile/UnlDataFams.hs create mode 100644 testsuite/tests/unlifted-datatypes/should_compile/UnlDataMonoSigs.hs create mode 100644 testsuite/tests/unlifted-datatypes/should_compile/UnlDataPolySigs.hs create mode 100644 testsuite/tests/unlifted-datatypes/should_compile/UnlDataUsersGuide.hs create mode 100644 testsuite/tests/unlifted-datatypes/should_compile/all.T create mode 100644 testsuite/tests/unlifted-datatypes/should_fail/Makefile create mode 100644 testsuite/tests/unlifted-datatypes/should_fail/UnlDataInvalidResKind1.hs create mode 100644 testsuite/tests/unlifted-datatypes/should_fail/UnlDataInvalidResKind1.stderr create mode 100644 testsuite/tests/unlifted-datatypes/should_fail/UnlDataInvalidResKind2.hs create mode 100644 testsuite/tests/unlifted-datatypes/should_fail/UnlDataNullaryPoly.hs create mode 100644 testsuite/tests/unlifted-datatypes/should_fail/UnlDataNullaryPoly.stderr create mode 100644 testsuite/tests/unlifted-datatypes/should_fail/all.T create mode 100644 testsuite/tests/unlifted-datatypes/should_run/Makefile create mode 100644 testsuite/tests/unlifted-datatypes/should_run/UnlData1.hs create mode 100644 testsuite/tests/unlifted-datatypes/should_run/UnlData1.stdout create mode 100644 testsuite/tests/unlifted-datatypes/should_run/UnlGadt1.hs create mode 100644 testsuite/tests/unlifted-datatypes/should_run/UnlGadt1.stderr create mode 100644 testsuite/tests/unlifted-datatypes/should_run/UnlGadt1.stdout create mode 100644 testsuite/tests/unlifted-datatypes/should_run/all.T diff --git a/compiler/GHC/Builtin/Types.hs b/compiler/GHC/Builtin/Types.hs index 3b928c801f..321b20e877 100644 --- a/compiler/GHC/Builtin/Types.hs +++ b/compiler/GHC/Builtin/Types.hs @@ -1485,22 +1485,25 @@ runtimeRepTy = mkTyConTy runtimeRepTyCon -- Type synonyms; see Note [TYPE and RuntimeRep] in GHC.Builtin.Types.Prim -- and Note [Prefer Type over TYPE 'LiftedRep] in GHC.Core.TyCo.Rep. --- type Type = TYPE ('BoxedRep 'Lifted) --- type LiftedRep = 'BoxedRep 'Lifted +-- +-- @type Type = TYPE ('BoxedRep 'Lifted)@ liftedTypeKindTyCon :: TyCon liftedTypeKindTyCon = buildSynTyCon liftedTypeKindTyConName [] liftedTypeKind [] rhs where rhs = TyCoRep.TyConApp tYPETyCon [mkTyConApp liftedRepTyCon []] +-- | @type UnliftedType = TYPE ('BoxedRep 'Unlifted)@ unliftedTypeKindTyCon :: TyCon unliftedTypeKindTyCon = buildSynTyCon unliftedTypeKindTyConName [] liftedTypeKind [] rhs where rhs = TyCoRep.TyConApp tYPETyCon [mkTyConApp unliftedRepTyCon []] +-- | @type LiftedRep = 'BoxedRep 'Lifted@ liftedRepTyCon :: TyCon liftedRepTyCon = buildSynTyCon liftedRepTyConName [] runtimeRepTy [] liftedRepTy +-- | @type UnliftedRep = 'BoxedRep 'Unlifted@ unliftedRepTyCon :: TyCon unliftedRepTyCon = buildSynTyCon unliftedRepTyConName [] runtimeRepTy [] unliftedRepTy diff --git a/compiler/GHC/Core/Lint.hs b/compiler/GHC/Core/Lint.hs index 40de306802..89914e967f 100644 --- a/compiler/GHC/Core/Lint.hs +++ b/compiler/GHC/Core/Lint.hs @@ -635,6 +635,7 @@ lintLetBind top_lvl rec_flag binder rhs rhs_ty ; checkL ( isJoinId binder || not (isUnliftedType binder_ty) || (isNonRec rec_flag && exprOkForSpeculation rhs) + || isDataConWorkId binder || isDataConWrapId binder -- until #17521 is fixed || exprIsTickedString rhs) (badBndrTyMsg binder (text "unlifted")) diff --git a/compiler/GHC/Core/TyCon.hs b/compiler/GHC/Core/TyCon.hs index 4b517027da..87b7336a76 100644 --- a/compiler/GHC/Core/TyCon.hs +++ b/compiler/GHC/Core/TyCon.hs @@ -1480,7 +1480,7 @@ data PrimRep | FloatRep | DoubleRep | VecRep Int PrimElemRep -- ^ A vector - deriving( Show ) + deriving( Eq, Show ) data PrimElemRep = Int8ElemRep diff --git a/compiler/GHC/Core/Type.hs b/compiler/GHC/Core/Type.hs index b0aa10c4cd..5ed621d404 100644 --- a/compiler/GHC/Core/Type.hs +++ b/compiler/GHC/Core/Type.hs @@ -120,10 +120,10 @@ module GHC.Core.Type ( -- *** Levity and boxity isLiftedType_maybe, - isLiftedTypeKind, isUnliftedTypeKind, pickyIsLiftedTypeKind, - isLiftedRuntimeRep, isUnliftedRuntimeRep, + isLiftedTypeKind, isUnliftedTypeKind, isBoxedTypeKind, pickyIsLiftedTypeKind, + isLiftedRuntimeRep, isUnliftedRuntimeRep, isBoxedRuntimeRep, isLiftedLevity, isUnliftedLevity, - isUnliftedType, mightBeUnliftedType, isUnboxedTupleType, isUnboxedSumType, + isUnliftedType, isBoxedType, mightBeUnliftedType, isUnboxedTupleType, isUnboxedSumType, isAlgType, isDataFamilyAppType, isPrimitiveType, isStrictType, isLevityTy, isLevityVar, @@ -146,10 +146,10 @@ module GHC.Core.Type ( -- ** Finding the kind of a type typeKind, tcTypeKind, isTypeLevPoly, resultIsLevPoly, tcIsLiftedTypeKind, tcIsConstraintKind, tcReturnsConstraintKind, - tcIsRuntimeTypeKind, + tcIsBoxedTypeKind, tcIsRuntimeTypeKind, -- ** Common Kind - liftedTypeKind, + liftedTypeKind, unliftedTypeKind, -- * Type free variables tyCoFVsOfType, tyCoFVsBndr, tyCoFVsVarBndr, tyCoFVsVarBndrs, @@ -294,26 +294,29 @@ import Control.Monad ( guard ) -- $type_classification -- #type_classification# -- --- Types are one of: +-- Types are any, but at least one, of: -- --- [Unboxed] Iff its representation is other than a pointer --- Unboxed types are also unlifted. +-- [Boxed] Iff its representation is a pointer to an object on the +-- GC'd heap. Operationally, heap objects can be entered as +-- a means of evaluation. -- --- [Lifted] Iff it has bottom as an element. --- Closures always have lifted types: i.e. any --- let-bound identifier in Core must have a lifted --- type. Operationally, a lifted object is one that --- can be entered. +-- [Lifted] Iff it has bottom as an element: An instance of a +-- lifted type might diverge when evaluated. +-- GHC Haskell's unboxed types are unlifted. +-- An unboxed, but lifted type is not very useful. +-- (Example: A byte-represented type, where evaluating 0xff +-- computes the 12345678th collatz number modulo 0xff.) -- Only lifted types may be unified with a type variable. -- -- [Algebraic] Iff it is a type with one or more constructors, whether -- declared with @data@ or @newtype@. -- An algebraic type is one that can be deconstructed --- with a case expression. This is /not/ the same as --- lifted types, because we also include unboxed --- tuples in this classification. +-- with a case expression. There are algebraic types that +-- are not lifted types, like unlifted data types or +-- unboxed tuples. -- -- [Data] Iff it is a type declared with @data@, or a boxed tuple. +-- There are also /unlifted/ data types. -- -- [Primitive] Iff it is a built-in type that can't be expressed in Haskell. -- @@ -473,8 +476,8 @@ coreFullView ty@(TyConApp tc _) coreFullView ty = ty {-# INLINE coreFullView #-} -{- Note [Inlining coreView] in GHC.Core.Type -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +{- Note [Inlining coreView] +~~~~~~~~~~~~~~~~~~~~~~~~~~~ It is very common to have a function f :: Type -> ... @@ -585,6 +588,18 @@ expandTypeSynonyms ty -- order of a coercion) go_cobndr subst = substForAllCoBndrUsing False (go_co subst) subst +-- | An INLINE helper for function such as 'kindRep_maybe' below. +-- +-- @isTyConKeyApp_maybe key ty@ returns @Just tys@ iff +-- the type @ty = T tys@, where T's unique = key +isTyConKeyApp_maybe :: Unique -> Type -> Maybe [Type] +isTyConKeyApp_maybe key ty + | TyConApp tc args <- coreFullView ty + , tc `hasKey` key + = Just args + | otherwise + = Nothing +{-# INLINE isTyConKeyApp_maybe #-} -- | Extract the RuntimeRep classifier of a type from its kind. For example, -- @kindRep * = LiftedRep@; Panics if this is not possible. @@ -600,9 +615,18 @@ kindRep k = case kindRep_maybe k of -- Treats * and Constraint as the same kindRep_maybe :: HasDebugCallStack => Kind -> Maybe Type kindRep_maybe kind - | TyConApp tc [arg] <- coreFullView kind - , tc `hasKey` tYPETyConKey = Just arg - | otherwise = Nothing + | Just [arg] <- isTyConKeyApp_maybe tYPETyConKey kind = Just arg + | otherwise = Nothing + +-- | Returns True if the kind classifies types which are allocated on +-- the GC'd heap and False otherwise. Note that this returns False for +-- levity-polymorphic kinds, which may be specialized to a kind that +-- classifies AddrRep or even unboxed kinds. +isBoxedTypeKind :: Kind -> Bool +isBoxedTypeKind kind + = case kindRep_maybe kind of + Just rep -> isBoxedRuntimeRep rep + Nothing -> False -- | This version considers Constraint to be the same as *. Returns True -- if the argument is equivalent to Type/Constraint and False otherwise. @@ -636,54 +660,49 @@ pickyIsLiftedTypeKind kind , tc `hasKey` liftedTypeKindTyConKey = True | otherwise = False +-- | Returns True if the kind classifies unlifted types (like 'Int#') and False +-- otherwise. Note that this returns False for levity-polymorphic kinds, which +-- may be specialized to a kind that classifies unlifted types. +isUnliftedTypeKind :: Kind -> Bool +isUnliftedTypeKind kind + = case kindRep_maybe kind of + Just rep -> isUnliftedRuntimeRep rep + Nothing -> False + +-- | See 'isBoxedRuntimeRep_maybe'. +isBoxedRuntimeRep :: Type -> Bool +isBoxedRuntimeRep rep = isJust (isBoxedRuntimeRep_maybe rep) + +-- | `isBoxedRuntimeRep_maybe (rep :: RuntimeRep)` returns `Just lev` if `rep` +-- expands to `Boxed lev` and returns `Nothing` otherwise. +-- +-- Types with this runtime rep are represented by pointers on the GC'd heap. +isBoxedRuntimeRep_maybe :: Type -> Maybe Type +isBoxedRuntimeRep_maybe rep + | Just [lev] <- isTyConKeyApp_maybe boxedRepDataConKey rep + = Just lev + | otherwise + = Nothing + isLiftedRuntimeRep :: Type -> Bool -- isLiftedRuntimeRep is true of LiftedRep :: RuntimeRep -- False of type variables (a :: RuntimeRep) -- and of other reps e.g. (IntRep :: RuntimeRep) isLiftedRuntimeRep rep - | Just rep' <- coreView rep - = isLiftedRuntimeRep rep' - | TyConApp rr_tc [rr_arg] <- rep - , rr_tc `hasKey` boxedRepDataConKey - = isLiftedLevity rr_arg + | Just [lev] <- isTyConKeyApp_maybe boxedRepDataConKey rep + = isLiftedLevity lev | otherwise = False -isLiftedLevity :: Type -> Bool -isLiftedLevity lev - | Just lev' <- coreView lev = isLiftedLevity lev' - | TyConApp lev_tc lev_args <- lev - , lev_tc `hasKey` liftedDataConKey - = ASSERT( null lev_args ) True - | otherwise = False - -isUnliftedLevity :: Type -> Bool -isUnliftedLevity lev - | Just lev' <- coreView lev = isUnliftedLevity lev' - | TyConApp lev_tc lev_args <- lev - , lev_tc `hasKey` unliftedDataConKey - = ASSERT( null lev_args ) True - | otherwise = False - --- | Returns True if the kind classifies unlifted types and False otherwise. --- Note that this returns False for levity-polymorphic kinds, which may --- be specialized to a kind that classifies unlifted types. -isUnliftedTypeKind :: Kind -> Bool -isUnliftedTypeKind kind - = case kindRep_maybe kind of - Just rep -> isUnliftedRuntimeRep rep - Nothing -> False - isUnliftedRuntimeRep :: Type -> Bool +-- PRECONDITION: The type has kind RuntimeRep -- True of definitely-unlifted RuntimeReps -- False of (LiftedRep :: RuntimeRep) -- and of variables (a :: RuntimeRep) isUnliftedRuntimeRep rep - | Just rep' <- coreView rep -- NB: args might be non-empty - -- e.g. TupleRep [r1, .., rn] - = isUnliftedRuntimeRep rep' -isUnliftedRuntimeRep (TyConApp rr_tc args) - | isPromotedDataCon rr_tc = + | TyConApp rr_tc args <- coreFullView rep -- NB: args might be non-empty + -- e.g. TupleRep [r1, .., rn] + , isPromotedDataCon rr_tc = -- NB: args might be non-empty e.g. TupleRep [r1, .., rn] if (rr_tc `hasKey` boxedRepDataConKey) then case args of @@ -696,21 +715,28 @@ isUnliftedRuntimeRep (TyConApp rr_tc args) -- hence the isPromotedDataCon rr_tc isUnliftedRuntimeRep _ = False --- | Is this the type 'RuntimeRep'? -isRuntimeRepTy :: Type -> Bool -isRuntimeRepTy ty - | Just ty' <- coreView ty = isRuntimeRepTy ty' - | TyConApp tc args <- ty - , tc `hasKey` runtimeRepTyConKey = ASSERT( null args ) True - | otherwise = False +-- | An INLINE helper for function such as 'isLiftedRuntimeRep' below. +isNullaryTyConKeyApp :: Unique -> Type -> Bool +isNullaryTyConKeyApp key ty + | Just args <- isTyConKeyApp_maybe key ty + = ASSERT( null args ) True + | otherwise + = False +{-# INLINE isNullaryTyConKeyApp #-} + +isLiftedLevity :: Type -> Bool +isLiftedLevity = isNullaryTyConKeyApp liftedDataConKey + +isUnliftedLevity :: Type -> Bool +isUnliftedLevity = isNullaryTyConKeyApp unliftedDataConKey -- | Is this the type 'Levity'? isLevityTy :: Type -> Bool -isLevityTy lev - | Just lev' <- coreView lev = isLevityTy lev' - | TyConApp tc args <- coreFullView lev - , tc `hasKey` levityTyConKey = ASSERT( null args ) True - | otherwise = False +isLevityTy = isNullaryTyConKeyApp levityTyConKey + +-- | Is this the type 'RuntimeRep'? +isRuntimeRepTy :: Type -> Bool +isRuntimeRepTy = isNullaryTyConKeyApp runtimeRepTyConKey -- | Is a tyvar of type 'RuntimeRep'? isRuntimeRepVar :: TyVar -> Bool @@ -722,9 +748,7 @@ isLevityVar = isLevityTy . tyVarKind -- | Is this the type 'Multiplicity'? isMultiplicityTy :: Type -> Bool -isMultiplicityTy ty - | TyConApp tc [] <- coreFullView ty = tc `hasKey` multiplicityTyConKey - | otherwise = False +isMultiplicityTy = isNullaryTyConKeyApp multiplicityTyConKey -- | Is a tyvar of type 'Multiplicity'? isMultiplicityVar :: TyVar -> Bool @@ -2219,6 +2243,13 @@ mightBeUnliftedType ty Just is_lifted -> not is_lifted Nothing -> True +-- | See "Type#type_classification" for what a boxed type is. +-- Panics on levity polymorphic types; See 'mightBeUnliftedType' for +-- a more approximate predicate that behaves better in the presence of +-- levity polymorphism. +isBoxedType :: Type -> Bool +isBoxedType ty = isBoxedRuntimeRep (getRuntimeRep ty) + -- | Is this a type of kind RuntimeRep? (e.g. LiftedRep) isRuntimeRepKindedTy :: Type -> Bool isRuntimeRepKindedTy = isRuntimeRepTy . typeKind @@ -2799,28 +2830,40 @@ tcIsConstraintKind ty | otherwise = False --- | Is this kind equivalent to @*@? +-- | Like 'kindRep_maybe', but considers 'Constraint' to be distinct +-- from 'Type'. For a version that treats them as the same type, see +-- 'kindRep_maybe'. +tcKindRep_maybe :: HasDebugCallStack => Kind -> Maybe Type +tcKindRep_maybe kind + | Just (tc, [arg]) <- tcSplitTyConApp_maybe kind -- Note: tcSplit here + , tc `hasKey` tYPETyConKey = Just arg + | otherwise = Nothing + +-- | Is this kind equivalent to 'Type'? -- --- This considers 'Constraint' to be distinct from @*@. For a version that +-- This considers 'Constraint' to be distinct from 'Type'. For a version that -- treats them as the same type, see 'isLiftedTypeKind'. tcIsLiftedTypeKind :: Kind -> Bool -tcIsLiftedTypeKind ty - | Just (tc, [arg]) <- tcSplitTyConApp_maybe ty -- Note: tcSplit here - , tc `hasKey` tYPETyConKey - = isLiftedRuntimeRep arg - | otherwise - = False +tcIsLiftedTypeKind kind + = case tcKindRep_maybe kind of + Just rep -> isLiftedRuntimeRep rep + Nothing -> False + +-- | Is this kind equivalent to @TYPE (BoxedRep l)@ for some @l :: Levity@? +-- +-- This considers 'Constraint' to be distinct from 'Type'. For a version that +-- treats them as the same type, see 'isLiftedTypeKind'. +tcIsBoxedTypeKind :: Kind -> Bool +tcIsBoxedTypeKind kind + = case tcKindRep_maybe kind of + Just rep -> isBoxedRuntimeRep rep + Nothing -> False -- | Is this kind equivalent to @TYPE r@ (for some unknown r)? -- -- This considers 'Constraint' to be distinct from @*@. tcIsRuntimeTypeKind :: Kind -> Bool -tcIsRuntimeTypeKind ty - | Just (tc, _) <- tcSplitTyConApp_maybe ty -- Note: tcSplit here - , tc `hasKey` tYPETyConKey - = True - | otherwise - = False +tcIsRuntimeTypeKind kind = isJust (tcKindRep_maybe kind) tcReturnsConstraintKind :: Kind -> Bool -- True <=> the Kind ultimately returns a Constraint diff --git a/compiler/GHC/CoreToStg.hs b/compiler/GHC/CoreToStg.hs index 1bcf5bdfe9..bfe9a6c89b 100644 --- a/compiler/GHC/CoreToStg.hs +++ b/compiler/GHC/CoreToStg.hs @@ -484,15 +484,16 @@ mkStgAltType bndr alts | otherwise = case prim_reps of - [LiftedRep] -> case tyConAppTyCon_maybe (unwrapType bndr_ty) of - Just tc - | isAbstractTyCon tc -> look_for_better_tycon - | isAlgTyCon tc -> AlgAlt tc - | otherwise -> ASSERT2( _is_poly_alt_tycon tc, ppr tc ) - PolyAlt - Nothing -> PolyAlt - [unlifted] -> PrimAlt unlifted - not_unary -> MultiValAlt (length not_unary) + [rep] | isGcPtrRep rep -> + case tyConAppTyCon_maybe (unwrapType bndr_ty) of + Just tc + | isAbstractTyCon tc -> look_for_better_tycon + | isAlgTyCon tc -> AlgAlt tc + | otherwise -> ASSERT2( _is_poly_alt_tycon tc, ppr tc ) + PolyAlt + Nothing -> PolyAlt + [non_gcd] -> PrimAlt non_gcd + not_unary -> MultiValAlt (length not_unary) where bndr_ty = idType bndr prim_reps = typePrimRep bndr_ty diff --git a/compiler/GHC/Driver/Session.hs b/compiler/GHC/Driver/Session.hs index 8b7ddd321d..000063eb82 100644 --- a/compiler/GHC/Driver/Session.hs +++ b/compiler/GHC/Driver/Session.hs @@ -3566,6 +3566,7 @@ xFlagsDeps = [ flagSpec "UndecidableInstances" LangExt.UndecidableInstances, flagSpec "UndecidableSuperClasses" LangExt.UndecidableSuperClasses, flagSpec "UnicodeSyntax" LangExt.UnicodeSyntax, + flagSpec "UnliftedDatatypes" LangExt.UnliftedDatatypes, flagSpec "UnliftedFFITypes" LangExt.UnliftedFFITypes, flagSpec "UnliftedNewtypes" LangExt.UnliftedNewtypes, flagSpec "ViewPatterns" LangExt.ViewPatterns @@ -3749,6 +3750,10 @@ impliedXFlags , (LangExt.TemplateHaskell, turnOn, LangExt.TemplateHaskellQuotes) , (LangExt.Strict, turnOn, LangExt.StrictData) + + -- The extensions needed to declare an H98 unlifted data type + , (LangExt.UnliftedDatatypes, turnOn, LangExt.DataKinds) + , (LangExt.UnliftedDatatypes, turnOn, LangExt.StandaloneKindSignatures) ] -- Note [When is StarIsType enabled] diff --git a/compiler/GHC/Stg/Lint.hs b/compiler/GHC/Stg/Lint.hs index bf52840f5c..1e12e9bab9 100644 --- a/compiler/GHC/Stg/Lint.hs +++ b/compiler/GHC/Stg/Lint.hs @@ -45,7 +45,7 @@ import GHC.Driver.Session import GHC.Data.Bag ( Bag, emptyBag, isEmptyBag, snocBag, bagToList ) import GHC.Types.Basic ( TopLevelFlag(..), isTopLevel ) import GHC.Types.CostCentre ( isCurrentCCS ) -import GHC.Types.Id ( Id, idType, isJoinId, idName ) +import GHC.Types.Id import GHC.Types.Var.Set import GHC.Core.DataCon import GHC.Core ( AltCon(..) ) @@ -134,8 +134,10 @@ lint_binds_help top_lvl (binder, rhs) lintStgRhs rhs opts <- getStgPprOpts -- Check binder doesn't have unlifted type or it's a join point - checkL (isJoinId binder || not (isUnliftedType (idType binder))) - (mkUnliftedTyMsg opts binder rhs) + checkL ( isJoinId binder + || not (isUnliftedType (idType binder)) + || isDataConWorkId binder || isDataConWrapId binder) -- until #17521 is fixed + (mkUnliftedTyMsg opts binder rhs) -- | Top-level bindings can't inherit the cost centre stack from their -- (static) allocation site. diff --git a/compiler/GHC/Stg/Syntax.hs b/compiler/GHC/Stg/Syntax.hs index 185433100a..53e4b07c69 100644 --- a/compiler/GHC/Stg/Syntax.hs +++ b/compiler/GHC/Stg/Syntax.hs @@ -531,7 +531,7 @@ type GenStgAlt pass GenStgExpr pass) -- ...right-hand side. data AltType - = PolyAlt -- Polymorphic (a lifted type variable) + = PolyAlt -- Polymorphic (a boxed type variable, lifted or unlifted) | MultiValAlt Int -- Multi value of this arity (unboxed tuple or sum) -- the arity could indeed be 1 for unary unboxed tuple -- or enum-like unboxed sums diff --git a/compiler/GHC/StgToCmm/Env.hs b/compiler/GHC/StgToCmm/Env.hs index 3ad42fd19d..ebfff0185f 100644 --- a/compiler/GHC/StgToCmm/Env.hs +++ b/compiler/GHC/StgToCmm/Env.hs @@ -136,12 +136,15 @@ getCgIdInfo id let name = idName id ; if isExternalName name then let ext_lbl - | isUnliftedType (idType id) = + | isBoxedType (idType id) + = mkClosureLabel name $ idCafInfo id + | isUnliftedType (idType id) -- An unlifted external Id must refer to a top-level -- string literal. See Note [Bytes label] in "GHC.Cmm.CLabel". - ASSERT( idType id `eqType` addrPrimTy ) - mkBytesLabel name - | otherwise = mkClosureLabel name $ idCafInfo id + = ASSERT( idType id `eqType` addrPrimTy ) + mkBytesLabel name + | otherwise + = pprPanic "GHC.StgToCmm.Env: label not found" (ppr id <+> dcolon <+> ppr (idType id)) in return $ litIdInfo platform id (mkLFImported id) (CmmLabel ext_lbl) else diff --git a/compiler/GHC/Tc/Gen/HsType.hs b/compiler/GHC/Tc/Gen/HsType.hs index cc82f30dbc..61b66f3919 100644 --- a/compiler/GHC/Tc/Gen/HsType.hs +++ b/compiler/GHC/Tc/Gen/HsType.hs @@ -2908,9 +2908,9 @@ data ContextKind = TheKind Kind -- ^ a specific kind ----------------------- newExpectedKind :: ContextKind -> TcM Kind -newExpectedKind (TheKind k) = return k -newExpectedKind AnyKind = newMetaKindVar -newExpectedKind OpenKind = newOpenTypeKind +newExpectedKind (TheKind k) = return k +newExpectedKind AnyKind = newMetaKindVar +newExpectedKind OpenKind = newOpenTypeKind ----------------------- expectedKindInCtxt :: UserTypeCtxt -> ContextKind @@ -3579,6 +3579,22 @@ data DataSort | DataInstanceSort NewOrData | DataFamilySort +-- | Local helper type used in 'checkDataKindSig'. +-- +-- Superficially similar to 'ContextKind', but it lacks 'AnyKind' +-- and 'AnyBoxedKind', and instead of @'TheKind' liftedTypeKind@ +-- provides 'LiftedKind', which is much simpler to match on and +-- handle in 'isAllowedDataResKind'. +data AllowedDataResKind + = AnyTYPEKind + | AnyBoxedKind + | LiftedKind + +isAllowedDataResKind :: AllowedDataResKind -> Kind -> Bool +isAllowedDataResKind AnyTYPEKind kind = tcIsRuntimeTypeKind kind +isAllowedDataResKind AnyBoxedKind kind = tcIsBoxedTypeKind kind +isAllowedDataResKind LiftedKind kind = tcIsLiftedTypeKind kind + -- | Checks that the return kind in a data declaration's kind signature is -- permissible. There are three cases: -- @@ -3603,7 +3619,7 @@ checkDataKindSig :: DataSort -> Kind -- any arguments in the kind are stripped checkDataKindSig data_sort kind = do { dflags <- getDynFlags ; traceTc "checkDataKindSig" (ppr kind) - ; checkTc (is_TYPE_or_Type dflags || is_kind_var) + ; checkTc (tYPE_ok dflags || is_kind_var) (err_msg dflags) } where res_kind = snd (tcSplitPiTys kind) @@ -3626,6 +3642,13 @@ checkDataKindSig data_sort kind DataInstanceSort new_or_data -> new_or_data == NewType DataFamilySort -> False + is_datatype :: Bool + is_datatype = + case data_sort of + DataDeclSort DataType -> True + DataInstanceSort DataType -> True + _ -> False + is_data_family :: Bool is_data_family = case data_sort of @@ -3633,27 +3656,30 @@ checkDataKindSig data_sort kind DataInstanceSort{} -> False DataFamilySort -> True + allowed_kind :: DynFlags -> AllowedDataResKind + allowed_kind dflags + | is_newtype && xopt LangExt.UnliftedNewtypes dflags + -- With UnliftedNewtypes, we allow kinds other than Type, but they + -- must still be of the form `TYPE r` since we don't want to accept + -- Constraint or Nat. + -- See Note [Implementation of UnliftedNewtypes] in GHC.Tc.TyCl. + = AnyTYPEKind + | is_data_family + -- If this is a `data family` declaration, we don't need to check if + -- UnliftedNewtypes is enabled, since data family declarations can + -- have return kind `TYPE r` unconditionally (#16827). + = AnyTYPEKind + | is_datatype && xopt LangExt.UnliftedDatatypes dflags + -- With UnliftedDatatypes, we allow kinds other than Type, but they + -- must still be of the form `TYPE (BoxedRep l)`, so that we don't + -- accept result kinds like `TYPE IntRep`. + -- See Note [Implementation of UnliftedDatatypes] in GHC.Tc.TyCl. + = AnyBoxedKind + | otherwise + = LiftedKind + tYPE_ok :: DynFlags -> Bool - tYPE_ok dflags = - (is_newtype && xopt LangExt.UnliftedNewtypes dflags) - -- With UnliftedNewtypes, we allow kinds other than Type, but they - -- must still be of the form `TYPE r` since we don't want to accept - -- Constraint or Nat. - -- See Note [Implementation of UnliftedNewtypes] in GHC.Tc.TyCl. - || is_data_family - -- If this is a `data family` declaration, we don't need to check if - -- UnliftedNewtypes is enabled, since data family declarations can - -- have return kind `TYPE r` unconditionally (#16827). - - is_TYPE :: Bool - is_TYPE = tcIsRuntimeTypeKind res_kind - - is_Type :: Bool - is_Type = tcIsLiftedTypeKind res_kind - - is_TYPE_or_Type :: DynFlags -> Bool - is_TYPE_or_Type dflags | tYPE_ok dflags = is_TYPE - | otherwise = is_Type + tYPE_ok dflags = isAllowedDataResKind (allowed_kind dflags) res_kind -- In the particular case of a data family, permit a return kind of the -- form `:: k` (where `k` is a bare kind variable). @@ -3661,17 +3687,32 @@ checkDataKindSig data_sort kind is_kind_var | is_data_family = isJust (tcGetCastedTyVar_maybe res_kind) | otherwise = False + pp_allowed_kind dflags = + case allowed_kind dflags of + AnyTYPEKind -> ppr tYPETyCon + AnyBoxedKind -> ppr boxedRepDataConTyCon + LiftedKind -> ppr liftedTypeKind + err_msg :: DynFlags -> SDoc err_msg dflags = - sep [ (sep [ pp_dec <+> - text "has non-" <> - (if tYPE_ok dflags then text "TYPE" else ppr liftedTypeKind) - , (if is_data_family then text "and non-variable" else empty) <+> - text "return kind" <+> quotes (ppr res_kind) ]) - , if not (tYPE_ok dflags) && is_TYPE && is_newtype && - not (xopt LangExt.UnliftedNewtypes dflags) - then text "Perhaps you intended to use UnliftedNewtypes" - else empty ] + sep [ sep [ pp_dec <+> + text "has non-" <> + pp_allowed_kind dflags + , (if is_data_family then text "and non-variable" else empty) <+> + text "return kind" <+> quotes (ppr kind) ] + , ext_hint dflags ] + + ext_hint dflags + | tcIsRuntimeTypeKind kind + , is_newtype + , not (xopt LangExt.UnliftedNewtypes dflags) + = text "Perhaps you intended to use UnliftedNewtypes" + | tcIsBoxedTypeKind kind + , is_datatype + , not (xopt LangExt.UnliftedDatatypes dflags) + = text "Perhaps you intended to use UnliftedDatatypes" + | otherwise + = empty -- | Checks that the result kind of a class is exactly `Constraint`, rejecting -- type synonyms and type families that reduce to `Constraint`. See #16826. diff --git a/compiler/GHC/Tc/TyCl.hs b/compiler/GHC/Tc/TyCl.hs index e1da82d3bb..ec8c2bb66e 100644 --- a/compiler/GHC/Tc/TyCl.hs +++ b/compiler/GHC/Tc/TyCl.hs @@ -945,7 +945,7 @@ Each forall'd type variable in a type or kind is one of * Specified: the argument can be inferred at call sites, but may be instantiated with visible type/kind application - * Inferred: the must be inferred at call sites; it + * Inferred: the argument must be inferred at call sites; it is unavailable for use with visible type/kind application. Why have Inferred at all? Because we just can't make user-facing @@ -1115,7 +1115,7 @@ We do kind inference as follows: All this is very similar at the level of terms: see GHC.Tc.Gen.Bind Note [Quantified variables in partial type signatures] - But there some tricky corners: Note [Tricky scoping in generaliseTcTyCon] + But there are some tricky corners: Note [Tricky scoping in generaliseTcTyCon] * Step 4. Extend the type environment with a TcTyCon for S and T, now with their utterly-final polymorphic kinds (needed for recursive @@ -1345,7 +1345,7 @@ getInitialKind strategy ; tc <- kcDeclHeader strategy name flav ktvs $ case m_sig of Just ksig -> TheKind <$> tcLHsKindSig ctxt ksig - Nothing -> return $ dataDeclDefaultResultKind new_or_data + Nothing -> return $ dataDeclDefaultResultKind strategy new_or_data ; return [tc] } getInitialKind InitialKindInfer (FamDecl { tcdFam = decl }) @@ -1454,14 +1454,18 @@ have before standalone kind signatures: -} -- See Note [Data declaration default result kind] -dataDeclDefaultResultKind :: NewOrData -> ContextKind -dataDeclDefaultResultKind NewType = OpenKind - -- See Note [Implementation of UnliftedNewtypes], point . -dataDeclDefaultResultKind DataType = TheKind liftedTypeKind +dataDeclDefaultResultKind :: InitialKindStrategy -> NewOrData -> ContextKind +dataDeclDefaultResultKind strategy new_or_data + | NewType <- new_or_data + = OpenKind -- See Note [Implementation of UnliftedNewtypes], point . + | DataType <- new_or_data + , InitialKindCheck (SAKS _) <- strategy + = OpenKind -- See Note [Implementation of UnliftedDatatypes] + | otherwise + = TheKind liftedTypeKind {- Note [Data declaration default result kind] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - When the user has not written an inline result kind annotation on a data declaration, we assume it to be 'Type'. That is, the following declarations D1 and D2 are considered equivalent: @@ -1478,14 +1482,25 @@ accept D4: data D4 :: Type -> Type where MkD4 :: ... -> D4 param -However, there's a twist: for newtypes, we must relax -the assumed result kind to (TYPE r): +However, there are two twists: + + * For unlifted newtypes, we must relax the assumed result kind to (TYPE r): + + newtype D5 where + MkD5 :: Int# -> D5 + + See Note [Implementation of UnliftedNewtypes], STEP 1 and it's sub-note + . + + * For unlifted datatypes, we must relax the assumed result kind to + (TYPE (BoxedRep l)) in the presence of a SAKS: - newtype D5 where - MkD5 :: Int# -> D5 + type D6 :: Type -> TYPE (BoxedRep Unlifted) + data D6 a = MkD6 a + + Otherwise, it would be impossible to declare unlifted data types in H98 + syntax (which doesn't allow specification of a result kind). -See Note [Implementation of UnliftedNewtypes], STEP 1 and it's sub-note -. -} --------------------------------- @@ -2252,6 +2267,52 @@ the validity checker), that will not happen. But I cannot think of a non-contriv example that will notice this lack of inference, so it seems better to improve error messages than be able to infer this instantiation. +Note [Implementation of UnliftedDatatypes] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Expected behavior of UnliftedDatatypes: + +* Proposal: https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0265-unlifted-datatypes.rst +* Discussion: https://github.com/ghc-proposals/ghc-proposals/pull/265 + +The implementation heavily leans on Note [Implementation of UnliftedNewtypes]. + +In the frontend, the following tweaks have been made in the typechecker: + +* STEP 1: In the inferInitialKinds phase, newExpectedKind gives data type + constructors a result kind of `TYPE r` with a fresh unification variable + `r :: RuntimeRep` when there is a SAKS. (Same as for UnliftedNewtypes.) + Not needed with a CUSK, because it can't specify result kinds. + If there's a GADTSyntax result kind signature, we keep on using that kind. + + Similarly, for data instances without a kind signature, we use + `TYPE r` as the result kind, to support the following code: + + data family F a :: UnliftedType + data instance F Int = TInt + + The ommission of a kind signature for `F` should not mean a result kind + of `Type` (and thus a kind error) here. + +* STEP 2: No change to kcTyClDecl. + +* STEP 3: In GHC.Tc.Gen.HsType.checkDataKindSig, we make sure that the result + kind of the data declaration is actually `Type` or `TYPE (BoxedRep l)`, + for some `l`. If UnliftedDatatypes is not activated, we emit an error with a + suggestion in the latter case. + + Why not start out with `TYPE (BoxedRep l)` in the first place? Because then + we get worse kind error messages in e.g. saks_fail010: + + - Couldn't match expected kind: TYPE ('GHC.Types.BoxedRep t0) + - with actual kind: * -> * + + Expected a type, but found something with kind ‘* -> *’ + In the data type declaration for ‘T’ + + It seems `TYPE r` already has appropriate pretty-printing support. + +The changes to Core, STG and Cmm are of rather cosmetic nature. +The IRs are already well-equipped to handle unlifted types, and unlifted +datatypes are just a new sub-class thereof. -} tcTyClDecl :: RolesInfo -> LTyClDecl GhcRn -> TcM (TyCon, [DerivInfo]) diff --git a/compiler/GHC/Tc/TyCl/Instance.hs b/compiler/GHC/Tc/TyCl/Instance.hs index 657e1bffe7..8bfb5370bb 100644 --- a/compiler/GHC/Tc/TyCl/Instance.hs +++ b/compiler/GHC/Tc/TyCl/Instance.hs @@ -727,7 +727,7 @@ tcDataFamInstDecl mb_clsinfo tv_skol_env ; traceTc "tcDataFamInstDecl" $ vcat [ text "Fam tycon:" <+> ppr fam_tc , text "Pats:" <+> ppr pats - , text "visiblities:" <+> ppr (tcbVisibilities fam_tc pats) + , text "visibilities:" <+> ppr (tcbVisibilities fam_tc pats) , text "all_pats:" <+> ppr all_pats , text "ty_binders" <+> ppr ty_binders , text "fam_tc_binders:" <+> ppr (tyConBinders fam_tc) @@ -940,12 +940,15 @@ tcDataFamInstHeader mb_clsinfo fam_tc outer_bndrs fixity fam_name = tyConName fam_tc data_ctxt = DataKindCtxt fam_name - -- See Note [Implementation of UnliftedNewtypes] in GHC.Tc.TyCl, wrinkle (2). + -- See Note [Implementation of UnliftedNewtypes] in GHC.Tc.TyCl, families (2), + -- and Note [Implementation of UnliftedDatatypes]. tc_kind_sig Nothing - = do { unlifted_newtypes <- xoptM LangExt.UnliftedNewtypes - ; if unlifted_newtypes && new_or_data == NewType - then newOpenTypeKind - else pure liftedTypeKind + = do { unlifted_newtypes <- xoptM LangExt.UnliftedNewtypes + ; unlifted_datatypes <- xoptM LangExt.UnliftedDatatypes + ; case new_or_data of + NewType | unlifted_newtypes -> newOpenTypeKind + DataType | unlifted_datatypes -> newOpenTypeKind + _ -> pure liftedTypeKind } -- See Note [Result kind signature for a data family instance] diff --git a/compiler/GHC/Tc/Utils/TcMType.hs b/compiler/GHC/Tc/Utils/TcMType.hs index a3cda06cac..b6f5065997 100644 --- a/compiler/GHC/Tc/Utils/TcMType.hs +++ b/compiler/GHC/Tc/Utils/TcMType.hs @@ -23,6 +23,7 @@ module GHC.Tc.Utils.TcMType ( newFlexiTyVarTy, -- Kind -> TcM TcType newFlexiTyVarTys, -- Int -> Kind -> TcM [TcType] newOpenFlexiTyVar, newOpenFlexiTyVarTy, newOpenTypeKind, + newOpenBoxedTypeKind, newMetaKindVar, newMetaKindVars, newMetaTyVarTyAtLevel, newAnonMetaTyVar, cloneMetaTyVar, newCycleBreakerTyVar, @@ -1075,6 +1076,12 @@ newOpenFlexiTyVar = do { kind <- newOpenTypeKind ; newFlexiTyVar kind } +newOpenBoxedTypeKind :: TcM TcKind +newOpenBoxedTypeKind + = do { lev <- newFlexiTyVarTy (mkTyConTy levityTyCon) + ; let rr = mkTyConApp boxedRepDataConTyCon [lev] + ; return (tYPE rr) } + newMetaTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar]) -- Instantiate with META type variables -- Note that this works for a sequence of kind, type, and coercion variables diff --git a/docs/users_guide/9.2.1-notes.rst b/docs/users_guide/9.2.1-notes.rst index de4a983001..b0f80e93c3 100644 --- a/docs/users_guide/9.2.1-notes.rst +++ b/docs/users_guide/9.2.1-notes.rst @@ -13,6 +13,7 @@ Language `__ (Serrano et al, ICFP 2020). More information here: :ref:`impredicative-polymorphism`. This replaces the old (undefined, flaky) behaviour of the :extension:`ImpredicativeTypes` extension. + * The first stage of the `Pointer Rep Proposal`_ has been implemented. All boxed types, both lifted and unlifted, now have representation kinds of the shape ``BoxedRep r``. Code that references ``LiftedRep`` and ``UnliftedRep`` @@ -20,6 +21,24 @@ Language .. _Pointer Rep Proposal: https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0203-pointer-rep.rst +* :extension:`UnliftedDatatypes`: The `Unlifted Datatypes Proposal`_ has been + implemented. That means GHC Haskell now offers a way to define algebraic + data types with strict semantics like in OCaml or Idris! The distinction to + ordinary lifted data types is made in the kind system: Unlifted data types + live in kind ``TYPE (BoxedRep Unlifted)``. :extension:`UnliftedDatatypes` + allows giving data declarations such result kinds, such as in the following + example with the help of :extension:`StandaloneKindSignatures`: :: + + type IntSet :: UnliftedType -- type UnliftedType = TYPE (BoxedRep Unlifted) + data IntSet = Branch IntSet !Int IntSet | Leaf + + See :extension:`UnliftedDatatypes` for what other declarations are + possible. Slight caveat: Most functions in ``base`` (including ``$``) + are not levity-polymorphic (yet) and hence won't work with unlifted + data types. + +.. _Unlifted Datatypes Proposal: https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0265-unlifted-datatypes.rst + * Kind inference for data/newtype instance declarations is slightly more restrictive than before. See the user manual :ref:`kind-inference-data-family-instances`. This is a breaking change, albeit a fairly obscure one that corrects a specification bug. diff --git a/docs/users_guide/exts/primitives.rst b/docs/users_guide/exts/primitives.rst index 9e82852391..80041dd6ad 100644 --- a/docs/users_guide/exts/primitives.rst +++ b/docs/users_guide/exts/primitives.rst @@ -70,16 +70,16 @@ Unboxed type kinds ------------------ Because unboxed types are represented without the use of pointers, we -cannot store them in a polymorphic datatype. +cannot store them in a polymorphic data type. For example, the ``Just`` node of ``Just 42#`` would have to be different from the ``Just`` node of ``Just 42``; the former stores an integer directly, while the latter stores a pointer. GHC currently does not support this variety of ``Just`` -nodes (nor for any other datatype). Accordingly, the *kind* of an unboxed +nodes (nor for any other data type). Accordingly, the *kind* of an unboxed type is different from the kind of a boxed type. The Haskell Report describes that ``*`` (spelled ``Type`` and imported from -``Data.Kind`` in the GHC dialect of Haskell) is the kind of ordinary datatypes, +``Data.Kind`` in the GHC dialect of Haskell) is the kind of ordinary data types, such as ``Int``. Furthermore, type constructors can have kinds with arrows; for example, ``Maybe`` has kind ``Type -> Type``. Unboxed types have a kind that specifies their runtime representation. For example, the type ``Int#`` has kind @@ -308,7 +308,7 @@ Unlifted Newtypes GHC implements an :extension:`UnliftedNewtypes` extension as specified in `this GHC proposal `_. :extension:`UnliftedNewtypes` relaxes the restrictions around what types can appear inside -of a `newtype`. For example, the type :: +of a ``newtype``. For example, the type :: newtype A = MkA Int# @@ -368,3 +368,93 @@ This extension impacts the determination of whether or not a newtype has a Complete User-Specified Kind Signature (CUSK). The exact impact is specified `the section on CUSKs <#complete-kind-signatures>`__. +Unlifted Datatypes +------------------ + +.. extension:: UnliftedDatatypes + :shortdesc: Enable unlifted data types. + + :implies: :extension:`DataKinds`, :extension:`StandaloneKindSignatures` + :since: 9.2.1 + + Enable the declaration of data types with unlifted or levity-polymorphic + result kind. + +GHC implements the :extension:`UnliftedDatatypes` extension as specified in +`this GHC proposal `_. +:extension:`UnliftedDatatypes` relaxes the restrictions around what result kinds +are allowed in data declarations. For example, the type :: + + data UList a :: UnliftedType where + UCons :: a -> UList a -> UList a + UNil :: UList a + +defines a list type that lives in kind ``UnliftedType`` +(e.g., ``TYPE (BoxedRep Unlifted)``). As such, each occurrence of a term of that +type is assumed to be evaluated (and the compiler makes sure that is indeed the +case). In other words: Unlifted data types behave like data types in strict +languages such as OCaml or Idris. However unlike :extension:`StrictData`, +this extension will not change whether the fields of a (perhaps unlifted) +data type are strict or lazy. For example, ``UCons`` is lazy in its first +argument as its field has kind ``Type``. + +The fact that unlifted types are always evaluated allows GHC to elide +evaluatedness checks at runtime. See the Motivation section of the proposal +for how this can improve performance for some programs. + +The above data declaration in GADT syntax correctly suggests that unlifted +data types are compatible with the full GADT feature set. Somewhat conversely, +you can also declare unlifted data types in Haskell98 syntax, which requires you +to specify the result kind via :extension:`StandaloneKindSignatures`: :: + + type UList :: Type -> UnliftedType + data UList a = UCons a (UList a) | UNil + +You may even declare levity-polymorphic data types: :: + + type PEither :: Type -> Type -> TYPE (BoxedRep l) + data PEither l r = PLeft l | PRight r + + f :: PEither @Unlifted Int Bool -> Bool + f (PRight b) = b + f _ = False + +While ``f`` above could reasonably be levity-polymorphic (as it evaluates its +argument either way), GHC currently disallows the more general type +``PEither @l Int Bool -> Bool``. This is a consequence of the +`levity-polymorphic binder restriction <#levity-polymorphic-restrictions>`__, + +Due to `ticket 19487 `, it's +currently not possible to declare levity-polymorphic data types with nullary +data constructors. There's a workaround, though: :: + + type T :: TYPE (BoxedRep l) + data T where + MkT :: forall l. (() :: Constraint) => T @l + +The use of ``=>`` makes the type of ``MkT`` lifted. +If you want a zero-runtime-cost alternative, use ``MkT :: Proxy# () -> T @l`` +instead and bear with the additional ``proxy#`` argument at construction sites. + +This extension also relaxes some of the restrictions around data family +instances. In particular, :extension:`UnliftedDatatypes` permits a +``data instance`` to be given a return kind that unifies with +``TYPE (BoxedRep l)``, not just ``Type``. For example, the following ``data +instance`` declarations would be permitted: :: + + data family F a :: UnliftedType + data instance F Int = FInt + + data family G a :: TYPE (BoxedRep l) + data instance G Int = GInt Int -- defaults to Type + data instance G Bool :: UnliftedType where + GBool :: Bool -> G Bool + data instance G Char :: Type where + GChar :: Char -> G Char + data instance G Double :: forall l. TYPE (BoxedRep l) where + GDouble :: Int -> G @l Double + +It is worth noting that :extension:`UnliftedDatatypes` is *not* required to give +the data families themselves return kinds involving ``TYPE``, such as the +``G`` example above. The extension is only required for ``data instance`` +declarations, such as ``FInt`` and ``GBool`` above. diff --git a/libraries/ghc-boot-th/GHC/LanguageExtensions/Type.hs b/libraries/ghc-boot-th/GHC/LanguageExtensions/Type.hs index b75977c74c..8dc2b67a36 100644 --- a/libraries/ghc-boot-th/GHC/LanguageExtensions/Type.hs +++ b/libraries/ghc-boot-th/GHC/LanguageExtensions/Type.hs @@ -51,6 +51,7 @@ data Extension | UnboxedTuples | UnboxedSums | UnliftedNewtypes + | UnliftedDatatypes | BangPatterns | TypeFamilies | TypeFamilyDependencies diff --git a/libraries/ghc-prim/GHC/Types.hs b/libraries/ghc-prim/GHC/Types.hs index 59edeec8af..7ce559739f 100644 --- a/libraries/ghc-prim/GHC/Types.hs +++ b/libraries/ghc-prim/GHC/Types.hs @@ -96,7 +96,8 @@ type UnliftedRep = 'BoxedRep 'Unlifted -- | The kind of types with lifted values. For example @Int :: Type@. type Type = TYPE LiftedRep --- | The kind of types with unlifted values. For example @Int# :: UnliftedType@. +-- | The kind of boxed, unlifted values, for example @Array#@ or a user-defined +-- unlifted data type, using @-XUnliftedDataTypes@. type UnliftedType = TYPE UnliftedRep data Multiplicity = Many | One diff --git a/testsuite/tests/driver/T4437.hs b/testsuite/tests/driver/T4437.hs index cbcbefc573..d55dae5484 100644 --- a/testsuite/tests/driver/T4437.hs +++ b/testsuite/tests/driver/T4437.hs @@ -43,6 +43,7 @@ expectedGhcOnlyExtensions = , "FieldSelectors" , "OverloadedRecordDot" , "OverloadedRecordUpdate" + , "UnliftedDatatypes" ] expectedCabalOnlyExtensions :: [String] diff --git a/testsuite/tests/unlifted-datatypes/Makefile b/testsuite/tests/unlifted-datatypes/Makefile new file mode 100644 index 0000000000..9a36a1c5fe --- /dev/null +++ b/testsuite/tests/unlifted-datatypes/Makefile @@ -0,0 +1,3 @@ +TOP=../.. +include $(TOP)/mk/boilerplate.mk +include $(TOP)/mk/test.mk diff --git a/testsuite/tests/unlifted-datatypes/should_compile/Makefile b/testsuite/tests/unlifted-datatypes/should_compile/Makefile new file mode 100644 index 0000000000..9a36a1c5fe --- /dev/null +++ b/testsuite/tests/unlifted-datatypes/should_compile/Makefile @@ -0,0 +1,3 @@ +TOP=../.. +include $(TOP)/mk/boilerplate.mk +include $(TOP)/mk/test.mk diff --git a/testsuite/tests/unlifted-datatypes/should_compile/UnlDataFams.hs b/testsuite/tests/unlifted-datatypes/should_compile/UnlDataFams.hs new file mode 100644 index 0000000000..443deadc1a --- /dev/null +++ b/testsuite/tests/unlifted-datatypes/should_compile/UnlDataFams.hs @@ -0,0 +1,49 @@ +{-# LANGUAGE UnliftedDatatypes #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE RankNTypes #-} + +module UnlDataFams where + +import GHC.Exts +import GHC.Types + +data family F a :: UnliftedType + +data instance F Int = TInt + +data family G a :: TYPE (BoxedRep l) + +data instance G Int = GInt +data instance G Bool :: UnliftedType where + GBool :: G Bool +data instance G Char :: Type where + GChar :: G Char + +data family H :: Type -> UnliftedType +data instance H Int = HInt Int + +type Interpret :: Bool -> Levity +type family Interpret b where + Interpret True = Lifted + Interpret False = Unlifted + +type A :: TYPE (BoxedRep (Interpret b)) +data A = MkA Int + +a :: A @True +a = MkA 42 + +-- type Interpret :: Bool -> RuntimeRep +-- type family Interpret b where +-- Interpret True = BoxedRep Lifted +-- Interpret False = BoxedRep Unlifted +-- +-- type A :: TYPE (Interpret b) +-- data A = MkA Int +-- +-- data B :: TYPE (Interpret b) where +-- MkB :: Int -> B @b diff --git a/testsuite/tests/unlifted-datatypes/should_compile/UnlDataMonoSigs.hs b/testsuite/tests/unlifted-datatypes/should_compile/UnlDataMonoSigs.hs new file mode 100644 index 0000000000..cef48e31e0 --- /dev/null +++ b/testsuite/tests/unlifted-datatypes/should_compile/UnlDataMonoSigs.hs @@ -0,0 +1,22 @@ +{-# LANGUAGE UnliftedDatatypes #-} +{-# LANGUAGE GADTSyntax #-} +{-# LANGUAGE KindSignatures #-} + +module UnlDataMonoSigs where + +import GHC.Exts +import GHC.Types + +data T1 a :: UnliftedType where + MkT1 :: T1 a + +type T2 :: Type -> UnliftedType +data T2 a = T2 + +type T3 :: Type -> UnliftedType +data T3 a where + MkT3 :: T3 a + +type T4 :: Type -> UnliftedType +data T4 a :: UnliftedType where + MkT4 :: T4 a diff --git a/testsuite/tests/unlifted-datatypes/should_compile/UnlDataPolySigs.hs b/testsuite/tests/unlifted-datatypes/should_compile/UnlDataPolySigs.hs new file mode 100644 index 0000000000..6e998155bf --- /dev/null +++ b/testsuite/tests/unlifted-datatypes/should_compile/UnlDataPolySigs.hs @@ -0,0 +1,31 @@ +{-# LANGUAGE UnliftedDatatypes #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TypeApplications #-} + +module UnlDataPolySigs where + +import GHC.Exts +import GHC.Types + +data U1 a :: TYPE (BoxedRep l) where + MkU1 :: Int -> U1 a -- (MkU1 :: forall {k} (a :: k). Int -> U1 @{k} @'Lifted a) + +type U2 :: Type -> TYPE (BoxedRep l) +data U2 a = MkU2 Int -- (MkU2 :: forall (l :: Levity) a. Int -> U2 @l a) + +type U3 :: Type -> TYPE (BoxedRep l) +data U3 a where + MkU3 :: Int -> U3 a -- (MkU3 :: forall a. Int -> U3 @'Lifted a) + +type U4 :: Type -> TYPE (BoxedRep l) +data U4 a :: TYPE (BoxedRep l) where + MkU4 :: Int -> U4 a -- (MkU4 :: forall a. Int -> U4 @'Lifted a) + +data U5 a :: forall l. TYPE (BoxedRep l) where + MkU5 :: Int -> U5 a -- (MkU5 :: forall {k} (a :: k). Int -> U5 @{k} @'Lifted a) + +data U6 a :: forall l. TYPE (BoxedRep l) where + MkU6 :: Int -> U6 a @l -- (MkU6 :: forall {k} (a :: k) (l :: Levity). Int -> U6 @{k} a @l) diff --git a/testsuite/tests/unlifted-datatypes/should_compile/UnlDataUsersGuide.hs b/testsuite/tests/unlifted-datatypes/should_compile/UnlDataUsersGuide.hs new file mode 100644 index 0000000000..9023093ee8 --- /dev/null +++ b/testsuite/tests/unlifted-datatypes/should_compile/UnlDataUsersGuide.hs @@ -0,0 +1,38 @@ +{-# LANGUAGE UnliftedDatatypes #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE MagicHash #-} +{-# LANGUAGE ConstraintKinds #-} + +module UnlDataUsersGuide where + +import GHC.Exts +import GHC.Types + +data UList a :: UnliftedType where + UCons :: a -> UList a -> UList a + UNil :: UList a + +type UList2 :: Type -> UnliftedType +data UList2 a = UCons2 a (UList2 a) | UNil2 + +type PEither :: Type -> Type -> TYPE (BoxedRep l) +data PEither l r = PLeft l | PRight r + +f :: PEither @Unlifted Int Bool -> Bool +f (PRight b) = b +f _ = False + +type T :: TYPE (BoxedRep l) +data T where + MkT :: forall l. (() :: Constraint) => T @l + MkT2 :: Proxy# () -> T @l + +t1 :: T @Lifted +t1 = MkT + +t2 :: T @Lifted +t2 = MkT2 proxy# diff --git a/testsuite/tests/unlifted-datatypes/should_compile/all.T b/testsuite/tests/unlifted-datatypes/should_compile/all.T new file mode 100644 index 0000000000..d8c3eeb457 --- /dev/null +++ b/testsuite/tests/unlifted-datatypes/should_compile/all.T @@ -0,0 +1,4 @@ +test('UnlDataMonoSigs', normal, compile, ['']) +test('UnlDataPolySigs', normal, compile, ['']) +test('UnlDataFams', normal, compile, ['']) +test('UnlDataUsersGuide', normal, compile, ['']) diff --git a/testsuite/tests/unlifted-datatypes/should_fail/Makefile b/testsuite/tests/unlifted-datatypes/should_fail/Makefile new file mode 100644 index 0000000000..9a36a1c5fe --- /dev/null +++ b/testsuite/tests/unlifted-datatypes/should_fail/Makefile @@ -0,0 +1,3 @@ +TOP=../.. +include $(TOP)/mk/boilerplate.mk +include $(TOP)/mk/test.mk diff --git a/testsuite/tests/unlifted-datatypes/should_fail/UnlDataInvalidResKind1.hs b/testsuite/tests/unlifted-datatypes/should_fail/UnlDataInvalidResKind1.hs new file mode 100644 index 0000000000..18dcd1a216 --- /dev/null +++ b/testsuite/tests/unlifted-datatypes/should_fail/UnlDataInvalidResKind1.hs @@ -0,0 +1,9 @@ +{-# LANGUAGE UnliftedDatatypes #-} + +module UnlDataInvalidResKind1 where + +import GHC.Exts +import GHC.Types + +type T :: Type -> TYPE IntRep +data T a = MkT Int diff --git a/testsuite/tests/unlifted-datatypes/should_fail/UnlDataInvalidResKind1.stderr b/testsuite/tests/unlifted-datatypes/should_fail/UnlDataInvalidResKind1.stderr new file mode 100644 index 0000000000..e61b6b4b18 --- /dev/null +++ b/testsuite/tests/unlifted-datatypes/should_fail/UnlDataInvalidResKind1.stderr @@ -0,0 +1,4 @@ + +UnlDataInvalidResKind1.hs:9:1: error: + • Data type has non-'BoxedRep return kind ‘TYPE 'IntRep’ + • In the data declaration for ‘T’ diff --git a/testsuite/tests/unlifted-datatypes/should_fail/UnlDataInvalidResKind2.hs b/testsuite/tests/unlifted-datatypes/should_fail/UnlDataInvalidResKind2.hs new file mode 100644 index 0000000000..427e41bf0c --- /dev/null +++ b/testsuite/tests/unlifted-datatypes/should_fail/UnlDataInvalidResKind2.hs @@ -0,0 +1,22 @@ +{-# LANGUAGE UnliftedDatatypes #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeFamilyDependencies #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE RankNTypes #-} + +module UnlDataInvalidResKind2 where + +import GHC.Exts +import GHC.Types + +type Interpret :: Bool -> RuntimeRep +type family Interpret b = r | r -> b where + Interpret True = BoxedRep Lifted + Interpret False = BoxedRep Unlifted + +-- Not allowed, although well-typed after type fam reduction +type A :: TYPE (Interpret b) +data A = MkA Int diff --git a/testsuite/tests/unlifted-datatypes/should_fail/UnlDataNullaryPoly.hs b/testsuite/tests/unlifted-datatypes/should_fail/UnlDataNullaryPoly.hs new file mode 100644 index 0000000000..1b59bdf24f --- /dev/null +++ b/testsuite/tests/unlifted-datatypes/should_fail/UnlDataNullaryPoly.hs @@ -0,0 +1,10 @@ +{-# LANGUAGE UnliftedDatatypes #-} +{-# LANGUAGE PolyKinds #-} + +module UnlDataNullaryPoly where + +import GHC.Exts +import GHC.Types + +type T :: TYPE (BoxedRep l) +data T = MkT -- Not OK, we get (MkT :: forall l. T @l :: TYPE (BoxedRep l)) which is ill-kinded. diff --git a/testsuite/tests/unlifted-datatypes/should_fail/UnlDataNullaryPoly.stderr b/testsuite/tests/unlifted-datatypes/should_fail/UnlDataNullaryPoly.stderr new file mode 100644 index 0000000000..7c9b856677 --- /dev/null +++ b/testsuite/tests/unlifted-datatypes/should_fail/UnlDataNullaryPoly.stderr @@ -0,0 +1,7 @@ + +UnlDataNullaryPoly.hs:10:10: error: + • Quantified type's kind mentions quantified type variable + type: ‘forall (l :: Levity). T’ + where the body of the forall has this kind: ‘TYPE ('BoxedRep l)’ + • In the definition of data constructor ‘MkT’ + In the data type declaration for ‘T’ diff --git a/testsuite/tests/unlifted-datatypes/should_fail/all.T b/testsuite/tests/unlifted-datatypes/should_fail/all.T new file mode 100644 index 0000000000..f8e8c7c833 --- /dev/null +++ b/testsuite/tests/unlifted-datatypes/should_fail/all.T @@ -0,0 +1,2 @@ +test('UnlDataNullaryPoly', normal, compile_fail, ['']) +test('UnlDataInvalidResKind1', normal, compile_fail, ['']) diff --git a/testsuite/tests/unlifted-datatypes/should_run/Makefile b/testsuite/tests/unlifted-datatypes/should_run/Makefile new file mode 100644 index 0000000000..9a36a1c5fe --- /dev/null +++ b/testsuite/tests/unlifted-datatypes/should_run/Makefile @@ -0,0 +1,3 @@ +TOP=../.. +include $(TOP)/mk/boilerplate.mk +include $(TOP)/mk/test.mk diff --git a/testsuite/tests/unlifted-datatypes/should_run/UnlData1.hs b/testsuite/tests/unlifted-datatypes/should_run/UnlData1.hs new file mode 100644 index 0000000000..19266ea71e --- /dev/null +++ b/testsuite/tests/unlifted-datatypes/should_run/UnlData1.hs @@ -0,0 +1,34 @@ +{-# LANGUAGE UnliftedDatatypes #-} + +import GHC.Exts +import GHC.Types + +type SList :: Type -> UnliftedType +data SList a = Cons a (SList a) | Nil + +-- Sadly no IsList (SList a) or Show a => Show (SList a), +-- because type classes require lifted rep +sfromList :: [a] -> SList a +sfromList [] = Nil +sfromList (x:xs) = Cons x (sfromList xs) +stoList :: SList a -> [a] +stoList (Cons x xs) = x:stoList xs +stoList Nil = [] + +sfromList2 :: [a] -> SList a +sfromList2 xs = foldl (\acc x xs -> acc (Cons x xs)) (\x -> x) xs Nil + +sfromList3 :: [a] -> SList a +sfromList3 xs = foldr (\x acc xs -> Cons x (acc xs)) (\x -> x) xs Nil + +sreverse :: SList a -> SList a +sreverse = go Nil + where + go acc Nil = acc + go acc (Cons x xs) = go (Cons x acc) xs + +main = do + print (stoList (sreverse (Cons 1 (Cons 2 (Cons 3 Nil))))) + print (stoList (sreverse (sfromList [2,3,4]))) + print (stoList (sreverse (sfromList2 [3,4,5]))) + print (stoList (sreverse (sfromList3 [4,5,6]))) diff --git a/testsuite/tests/unlifted-datatypes/should_run/UnlData1.stdout b/testsuite/tests/unlifted-datatypes/should_run/UnlData1.stdout new file mode 100644 index 0000000000..0b1c480e31 --- /dev/null +++ b/testsuite/tests/unlifted-datatypes/should_run/UnlData1.stdout @@ -0,0 +1,4 @@ +[3,2,1] +[4,3,2] +[5,4,3] +[6,5,4] diff --git a/testsuite/tests/unlifted-datatypes/should_run/UnlGadt1.hs b/testsuite/tests/unlifted-datatypes/should_run/UnlGadt1.hs new file mode 100644 index 0000000000..ed19c3236f --- /dev/null +++ b/testsuite/tests/unlifted-datatypes/should_run/UnlGadt1.hs @@ -0,0 +1,20 @@ +{-# LANGUAGE UnliftedDatatypes #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} + +import GHC.Exts +import GHC.Types + +data T a :: UnliftedType where + TInt :: T Int + +f :: T a -> Int +f _ = 0 + +g :: T a -> T a +g TInt = TInt +{-# NOINLINE g #-} + +main = do + case g TInt of TInt -> putStrLn "should see this" + print (f (error "boom")) -- crashes! diff --git a/testsuite/tests/unlifted-datatypes/should_run/UnlGadt1.stderr b/testsuite/tests/unlifted-datatypes/should_run/UnlGadt1.stderr new file mode 100644 index 0000000000..158e2a12ba --- /dev/null +++ b/testsuite/tests/unlifted-datatypes/should_run/UnlGadt1.stderr @@ -0,0 +1,3 @@ +UnlGadt1: boom +CallStack (from HasCallStack): + error, called at UnlGadt1.hs:19:13 in main:Main diff --git a/testsuite/tests/unlifted-datatypes/should_run/UnlGadt1.stdout b/testsuite/tests/unlifted-datatypes/should_run/UnlGadt1.stdout new file mode 100644 index 0000000000..b31e365734 --- /dev/null +++ b/testsuite/tests/unlifted-datatypes/should_run/UnlGadt1.stdout @@ -0,0 +1 @@ +should see this diff --git a/testsuite/tests/unlifted-datatypes/should_run/all.T b/testsuite/tests/unlifted-datatypes/should_run/all.T new file mode 100644 index 0000000000..87b69c89bf --- /dev/null +++ b/testsuite/tests/unlifted-datatypes/should_run/all.T @@ -0,0 +1,2 @@ +test('UnlData1', normal, compile_and_run, ['']) +test('UnlGadt1', exit_code(1), compile_and_run, ['']) -- cgit v1.2.1