diff options
25 files changed, 437 insertions, 135 deletions
diff --git a/compiler/GHC/Builtin/Names.hs b/compiler/GHC/Builtin/Names.hs index 84210fb236..a85b61ca04 100644 --- a/compiler/GHC/Builtin/Names.hs +++ b/compiler/GHC/Builtin/Names.hs @@ -225,6 +225,7 @@ basicKnownKeyNames ioTyConName, ioDataConName, runMainIOName, runRWName, + withDictName, -- Type representation types trModuleTyConName, trModuleDataConName, @@ -545,7 +546,7 @@ pRELUDE :: Module pRELUDE = mkBaseModule_ pRELUDE_NAME gHC_PRIM, gHC_PRIM_PANIC, gHC_PRIM_EXCEPTION, - gHC_TYPES, gHC_GENERICS, gHC_MAGIC, + gHC_TYPES, gHC_GENERICS, gHC_MAGIC, gHC_MAGIC_DICT, gHC_CLASSES, gHC_PRIMOPWRAPPERS, gHC_BASE, gHC_ENUM, gHC_GHCI, gHC_GHCI_HELPERS, gHC_CSTRING, gHC_SHOW, gHC_READ, gHC_NUM, gHC_MAYBE, @@ -567,6 +568,7 @@ gHC_PRIM_PANIC = mkPrimModule (fsLit "GHC.Prim.Panic") gHC_PRIM_EXCEPTION = mkPrimModule (fsLit "GHC.Prim.Exception") gHC_TYPES = mkPrimModule (fsLit "GHC.Types") gHC_MAGIC = mkPrimModule (fsLit "GHC.Magic") +gHC_MAGIC_DICT = mkPrimModule (fsLit "GHC.Magic.Dict") gHC_CSTRING = mkPrimModule (fsLit "GHC.CString") gHC_CLASSES = mkPrimModule (fsLit "GHC.Classes") gHC_PRIMOPWRAPPERS = mkPrimModule (fsLit "GHC.PrimopWrappers") @@ -959,9 +961,10 @@ and it's convenient to write them all down in one place. wildCardName :: Name wildCardName = mkSystemVarName wildCardKey (fsLit "wild") -runMainIOName, runRWName :: Name +runMainIOName, runRWName, withDictName :: Name runMainIOName = varQual gHC_TOP_HANDLER (fsLit "runMainIO") runMainKey runRWName = varQual gHC_MAGIC (fsLit "runRW#") runRWKey +withDictName = varQual gHC_MAGIC_DICT (fsLit "withDict") withDictKey orderingTyConName, ordLTDataConName, ordEQDataConName, ordGTDataConName :: Name orderingTyConName = tcQual gHC_TYPES (fsLit "Ordering") orderingTyConKey @@ -2394,8 +2397,8 @@ rationalToFloatIdKey, rationalToDoubleIdKey :: Unique rationalToFloatIdKey = mkPreludeMiscIdUnique 130 rationalToDoubleIdKey = mkPreludeMiscIdUnique 131 -magicDictKey :: Unique -magicDictKey = mkPreludeMiscIdUnique 156 +withDictKey :: Unique +withDictKey = mkPreludeMiscIdUnique 156 coerceKey :: Unique coerceKey = mkPreludeMiscIdUnique 157 diff --git a/compiler/GHC/Builtin/primops.txt.pp b/compiler/GHC/Builtin/primops.txt.pp index a00f3f8215..d4f56cadfa 100644 --- a/compiler/GHC/Builtin/primops.txt.pp +++ b/compiler/GHC/Builtin/primops.txt.pp @@ -3288,13 +3288,6 @@ pseudoop "void#" } with deprecated_msg = { Use an unboxed unit tuple instead } -pseudoop "magicDict" - a - { {\tt magicDict} is a special-purpose placeholder value. - It is used internally by modules such as {\tt GHC.TypeNats} to cast a typeclass - dictionary with a single method. It is eliminated by a rule during compilation. - For the details, see Note [magicDictId magic] in GHC. } - primtype Proxy# a { The type constructor {\tt Proxy#} is used to bear witness to some type variable. It's used when you want to pass around proxy values diff --git a/compiler/GHC/Core/Opt/ConstantFold.hs b/compiler/GHC/Core/Opt/ConstantFold.hs index 88439edcc6..33ceebe70a 100644 --- a/compiler/GHC/Core/Opt/ConstantFold.hs +++ b/compiler/GHC/Core/Opt/ConstantFold.hs @@ -37,7 +37,7 @@ import GHC.Prelude import GHC.Driver.Ppr -import {-# SOURCE #-} GHC.Types.Id.Make ( mkPrimOpId, magicDictId, voidPrimId ) +import {-# SOURCE #-} GHC.Types.Id.Make ( mkPrimOpId, voidPrimId ) import GHC.Core import GHC.Core.Make @@ -49,11 +49,11 @@ import GHC.Builtin.Types import GHC.Builtin.Types.Prim import GHC.Core.TyCon ( tyConDataCons_maybe, isAlgTyCon, isEnumerationTyCon - , isNewTyCon, unwrapNewTyCon_maybe, tyConDataCons + , isNewTyCon, tyConDataCons , tyConFamilySize ) import GHC.Core.DataCon ( dataConTagZ, dataConTyCon, dataConWrapId, dataConWorkId ) import GHC.Core.Utils ( eqExpr, cheapEqExpr, exprIsHNF, exprType - , stripTicksTop, stripTicksTopT, mkTicks, stripTicksE ) + , stripTicksTop, stripTicksTopT, mkTicks ) import GHC.Core.Multiplicity import GHC.Core.FVs import GHC.Core.Type @@ -70,7 +70,6 @@ import GHC.Types.Basic import GHC.Platform import GHC.Utils.Misc import GHC.Utils.Panic -import GHC.Core.Coercion (mkUnbranchedAxInstCo,mkSymCo,Role(..)) import Control.Applicative ( Alternative(..) ) @@ -1739,8 +1738,6 @@ builtinRules ru_nargs = 1, ru_try = match_cstring_length }, BuiltinRule { ru_name = fsLit "Inline", ru_fn = inlineIdName, ru_nargs = 2, ru_try = \_ _ _ -> match_inline }, - BuiltinRule { ru_name = fsLit "MagicDict", ru_fn = idName magicDictId, - ru_nargs = 4, ru_try = \_ _ _ -> match_magicDict }, mkBasicRule unsafeEqualityProofName 3 unsafeEqualityProofRule, @@ -2239,21 +2236,6 @@ match_inline (Type _ : e : _) match_inline _ = Nothing ---------------------------------------------------- --- See Note [magicDictId magic] in "GHC.Types.Id.Make" --- for a description of what is going on here. -match_magicDict :: [Expr CoreBndr] -> Maybe (Expr CoreBndr) -match_magicDict [Type _, (stripTicksE (const True) -> (Var wrap `App` Type a `App` Type _ `App` f)), x, y ] - | Just (_, fieldTy, _) <- splitFunTy_maybe $ dropForAlls $ idType wrap - , Just (_, dictTy, _) <- splitFunTy_maybe fieldTy - , Just dictTc <- tyConAppTyCon_maybe dictTy - , Just (_,_,co) <- unwrapNewTyCon_maybe dictTc - = Just - $ f `App` Cast x (mkSymCo (mkUnbranchedAxInstCo Representational co [a] [])) - `App` y - -match_magicDict _ = Nothing - -------------------------------------------------------- -- Note [Constant folding through nested expressions] -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/compiler/GHC/HsToCore/Expr.hs b/compiler/GHC/HsToCore/Expr.hs index 37d72fa213..565132aed3 100644 --- a/compiler/GHC/HsToCore/Expr.hs +++ b/compiler/GHC/HsToCore/Expr.hs @@ -44,8 +44,9 @@ import GHC.Tc.Utils.TcType import GHC.Tc.Types.Evidence import GHC.Tc.Utils.Monad import GHC.Core.Type +import GHC.Core.TyCo.Rep import GHC.Core.Multiplicity -import GHC.Core.Coercion( Coercion ) +import GHC.Core.Coercion( instNewTyCon_maybe, mkSymCo ) import GHC.Core import GHC.Core.Utils import GHC.Core.Make @@ -1169,10 +1170,11 @@ dsHsWrapped orig_hs_expr go_l wrap (L _ hs_e) = go wrap hs_e go_head wrap var - = do { let wrapped_e = wrap (Var var) - wrapped_ty = exprType wrapped_e + | var `hasKey` withDictKey + = ds_withDict wrapped_ty - ; checkLevPolyFunction (ppr orig_hs_expr) var wrapped_ty + | otherwise + = do { checkLevPolyFunction (ppr orig_hs_expr) var wrapped_ty -- See Note [Checking for levity-polymorphic functions] -- Pass orig_hs_expr, so that the user can see entire -- expression with -fprint-typechecker-elaboration @@ -1181,7 +1183,164 @@ dsHsWrapped orig_hs_expr ; warnAboutIdentities dflags var wrapped_ty ; return wrapped_e } + where + wrapped_e = wrap (Var var) + wrapped_ty = exprType wrapped_e + +-- See Note [withDict] +ds_withDict :: Type -> DsM CoreExpr +ds_withDict wrapped_ty + -- Check that withDict is of the type `st -> (dt => r) -> r`. + | Just (Anon VisArg (Scaled mult1 st), rest) <- splitPiTy_maybe wrapped_ty + , Just (Anon VisArg (Scaled mult2 dt_to_r), _r1) <- splitPiTy_maybe rest + , Just (Anon InvisArg (Scaled _ dt), _r2) <- splitPiTy_maybe dt_to_r + -- Check that dt is a class constraint `C t_1 ... t_n`, where + -- `dict_tc = C` and `dict_args = t_1 ... t_n`. + , Just (dict_tc, dict_args) <- splitTyConApp_maybe dt + -- Check that C is a class of the form + -- `class C a_1 ... a_n where op :: meth_ty`, where + -- `meth_tvs = a_1 ... a_n` and `co` is a newtype coercion between + -- `C` and `meth_ty`. + , Just (inst_meth_ty, co) <- instNewTyCon_maybe dict_tc dict_args + -- Check that `st` is equal to `meth_ty[t_i/a_i]`. + , st `eqType` inst_meth_ty + = let sv = mkScaledTemplateLocal 1 $ mkScaled mult1 st + k = mkScaledTemplateLocal 2 $ mkScaled mult2 dt_to_r in + pure $ mkLams [sv, k] $ Var k `App` Cast (Var sv) (mkSymCo co) + + | otherwise + = errDsCoreExpr $ hang (text "Invalid instantiation of" <+> + quotes (ppr withDictName) <+> text "at type:") + 4 (ppr wrapped_ty) + +{- +Note [withDict] +~~~~~~~~~~~~~~~ +The identifier `withDict` is just a place-holder, which is used to +implement a primitive that we cannot define in Haskell but we can write +in Core. It is declared with a place-holder type: + + withDict :: forall {rr :: RuntimeRep} st dt (r :: TYPE rr). st -> (dt => r) -> r + +The intention is that the identifier will be used in a very specific way, +to create dictionaries for classes with a single method. Consider a class +like this: + + class C a where + f :: T a + +We can use `withDict`, in conjunction with a special case in the desugarer, to +cast values of type `T a` into dictionaries for `C a`. To do this, we can +define a function like this in the library: + + withT :: T a -> (C a => b) -> b + withT t k = withDict @(T a) @(C a) t k + +Here: + +* The `dt` in `withDict` (short for "dictionary type") is instantiated to + `C a`. + +* The `st` in `withDict` (short for "singleton type") is instantiated to + `T a`. The definition of `T` itself is irrelevant, only that `C a` is a class + with a single method of type `T a`. + +* The `r` in `withDict` is instantiated to `b`. + +There is a special case in dsHsWrapped.go_head which will replace the RHS +of this definition with an appropriate definition in Core. The special case +rewrites applications of `withDict` as follows: + + withDict @{rr} @mtype @(C t_1 ... t_n) @r +----> + \(sv :: mtype) (k :: C t_1 ... t_n => r) -> k (sv |> sym (co t_1 ... t_n)) + +Where: + +* The `C t_1 ... t_n` argument to withDict is a class constraint. + +* C must be defined as: + + class C a_1 ... a_n where + op :: meth_type + + That is, C must be a class with exactly one method and no superclasses. + +* The `mtype` argument to withDict must be equal to `meth_type[t_i/a_i]`, + which is instantied type of C's method. +* `co` is a newtype coercion that, when applied to `t_1 ... t_n`, coerces from + `C t_1 ... t_n` to `mtype`. This coercion is guaranteed to exist by virtue of + the fact that C is a class with exactly one method and no superclasses, so it + is treated like a newtype when compiled to Core. + +These requirements are implemented in the guards in ds_withDict's definition. + +Some further observations about `withDict`: + +* Every use of `withDict` must be instantiated at a /particular/ class C. + It's a bit like levity polymorphism: we don't allow class-polymorphic + calls of `withDict`. We check this in the desugarer -- and then we + can immediately replace this invocation of `withDict` with appropriate + class-specific Core code. + +* The `dt` in the type of withDict must be explicitly instantiated with + visible type application, as invoking `withDict` would be ambiguous + otherwise. + +* For examples of how `withDict` is used in the `base` library, see `withSNat` + in GHC.TypeNats, as well as `withSChar` and `withSSymbol` n GHC.TypeLits. + +* The `r` is levity polymorphic to support things like `withTypeable` in + `Data.Typeable.Internal`. + +* As an alternative to `withDict`, one could define functions like `withT` + above in terms of `unsafeCoerce`. This is more error-prone, however. + +* In order to define things like `reifySymbol` below: + + reifySymbol :: forall r. String -> (forall (n :: Symbol). KnownSymbol n => r) -> r + + `withDict` needs to be instantiated with `Any`, like so: + + reifySymbol n k = withDict @String @(KnownSymbol Any) @r n (k @Any) + + The use of `Any` is explained in Note [NOINLINE someNatVal] in + base:GHC.TypeNats. + +* The only valid way to apply `withDict` is as described above. Applying + `withDict` in any other way will result in a non-recoverable error during + desugaring. In other words, GHC will never execute the `withDict` function + in compiled code. + + In theory, this means that we don't need to define a binding for `withDict` + in GHC.Magic.Dict. In practice, we define a binding anyway, for two reasons: + + - To give it Haddocks, and + - To define the type of `withDict`, which GHC can find in + GHC.Magic.Dict.hi. + + Because we define a binding for `withDict`, we have to provide a right-hand + side for its definition. We somewhat arbitrarily choose: + + withDict = panicError "Non rewritten withDict"# + + This should never be reachable anyway, but just in case ds_withDict fails + to rewrite away `withDict`, this ensures that the program won't get very far. + +* One could conceivably implement this special case for `withDict` as a + constant-folding rule instead of during desugaring. We choose not to do so + for the following reasons: + + - Having a constant-folding rule would require that `withDict`'s definition + be wired in to the compiler so as to prevent `withDict` from inlining too + early. Implementing the special case in the desugarer, on the other hand, + only requires that `withDict` be known-key. + + - If the constant-folding rule were to fail, we want to throw a compile-time + error, which is trickier to do with the way that GHC.Core.Opt.ConstantFold + is set up. +-} -- | Takes a (pretty-printed) expression, a function, and its -- instantiated type. If the function is a hasNoBinding op, and the diff --git a/compiler/GHC/Types/Id/Make.hs b/compiler/GHC/Types/Id/Make.hs index 1fcdabc977..106f0f3ca9 100644 --- a/compiler/GHC/Types/Id/Make.hs +++ b/compiler/GHC/Types/Id/Make.hs @@ -30,7 +30,7 @@ module GHC.Types.Id.Make ( realWorldPrimId, voidPrimId, voidArgId, nullAddrId, seqId, lazyId, lazyIdKey, - coercionTokenId, magicDictId, coerceId, + coercionTokenId, coerceId, proxyHashId, noinlineId, noinlineIdName, coerceName, leftSectionName, rightSectionName, @@ -173,7 +173,6 @@ ghcPrimIds , voidPrimId , nullAddrId , seqId - , magicDictId , coerceId , proxyHashId , leftSectionId @@ -1429,14 +1428,13 @@ failure when trying.) nullAddrName, seqName, realWorldName, voidPrimIdName, coercionTokenName, - magicDictName, coerceName, proxyName, + coerceName, proxyName, leftSectionName, rightSectionName :: Name nullAddrName = mkWiredInIdName gHC_PRIM (fsLit "nullAddr#") nullAddrIdKey nullAddrId seqName = mkWiredInIdName gHC_PRIM (fsLit "seq") seqIdKey seqId realWorldName = mkWiredInIdName gHC_PRIM (fsLit "realWorld#") realWorldPrimIdKey realWorldPrimId voidPrimIdName = mkWiredInIdName gHC_PRIM (fsLit "void#") voidPrimIdKey voidPrimId coercionTokenName = mkWiredInIdName gHC_PRIM (fsLit "coercionToken#") coercionTokenIdKey coercionTokenId -magicDictName = mkWiredInIdName gHC_PRIM (fsLit "magicDict") magicDictKey magicDictId coerceName = mkWiredInIdName gHC_PRIM (fsLit "coerce") coerceKey coerceId proxyName = mkWiredInIdName gHC_PRIM (fsLit "proxy#") proxyHashKey proxyHashId leftSectionName = mkWiredInIdName gHC_PRIM (fsLit "leftSection") leftSectionKey leftSectionId @@ -1598,14 +1596,6 @@ rightSectionId = pcMiscPrelId rightSectionName ty info body = mkLams [f,ymult,xmult] $ mkVarApps (Var f) [xmult,ymult] -------------------------------------------------------------------------------- -magicDictId :: Id -- See Note [magicDictId magic] -magicDictId = pcMiscPrelId magicDictName ty info - where - info = noCafIdInfo `setInlinePragInfo` neverInlinePragma - `setNeverLevPoly` ty - ty = mkSpecForAllTys [alphaTyVar] alphaTy - --------------------------------------------------------------------------------- coerceId :: Id coerceId = pcMiscPrelId coerceName ty info @@ -1801,54 +1791,6 @@ OneShotInfo] in GHC.Core.Tidy. Also see https://gitlab.haskell.org/ghc/ghc/wikis/one-shot. -Note [magicDictId magic] -~~~~~~~~~~~~~~~~~~~~~~~~~ -The identifier `magicDict` is just a place-holder, which is used to -implement a primitive that we cannot define in Haskell but we can write -in Core. It is declared with a place-holder type: - - magicDict :: forall a. a - -The intention is that the identifier will be used in a very specific way, -to create dictionaries for classes with a single method. Consider a class -like this: - - class C a where - f :: T a - -We are going to use `magicDict`, in conjunction with a built-in Prelude -rule, to cast values of type `T a` into dictionaries for `C a`. To do -this, we define a function like this in the library: - - data WrapC a b = WrapC (C a => Proxy a -> b) - - withT :: (C a => Proxy a -> b) - -> T a -> Proxy a -> b - withT f x y = magicDict (WrapC f) x y - -The purpose of `WrapC` is to avoid having `f` instantiated. -Also, it avoids impredicativity, because `magicDict`'s type -cannot be instantiated with a forall. The field of `WrapC` contains -a `Proxy` parameter which is used to link the type of the constraint, -`C a`, with the type of the `Wrap` value being made. - -Next, we add a built-in Prelude rule (see GHC.Core.Opt.ConstantFold), -which will replace the RHS of this definition with the appropriate -definition in Core. The rewrite rule works as follows: - - magicDict @t (wrap @a @b f) x y -----> - f (x `cast` co a) y - -The `co` coercion is the newtype-coercion extracted from the type-class. -The type class is obtained by looking at the type of wrap. - -In the constant folding rule it's very import to make sure to strip all ticks -from the expression as if there's an occurence of -magicDict we *must* convert it for correctness. See #19667 for where this went -wrong in GHCi. - - ------------------------------------------------------------- @realWorld#@ used to be a magic literal, \tr{void#}. If things get nasty as-is, change it back to a literal (@Literal@). diff --git a/compiler/GHC/Types/Id/Make.hs-boot b/compiler/GHC/Types/Id/Make.hs-boot index 40be201e61..6a3f5c44be 100644 --- a/compiler/GHC/Types/Id/Make.hs-boot +++ b/compiler/GHC/Types/Id/Make.hs-boot @@ -12,5 +12,3 @@ mkDictSelId :: Name -> Class -> Id mkPrimOpId :: PrimOp -> Id voidPrimId :: Id - -magicDictId :: Id diff --git a/docs/users_guide/9.4.1-notes.rst b/docs/users_guide/9.4.1-notes.rst new file mode 100644 index 0000000000..8d92d57eec --- /dev/null +++ b/docs/users_guide/9.4.1-notes.rst @@ -0,0 +1,23 @@ +.. _release-9-4-1: + +Version 9.4.1 +============== + +``base`` library +~~~~~~~~~~~~~~~~ + +- ``GHC.Exts.magicDict`` has been renamed to ``withDict`` and given a more + specific type: :: + + withDict :: forall {rr :: RuntimeRep} st dt (r :: TYPE rr). st -> (dt => r) -> r + + Unlike ``magicDict``, ``withDict`` can be used without defining an + intermediate data type. For example, the ``withTypeable`` function from the + ``Data.Typeable`` module can now be defined as: :: + + withTypeable :: forall k (a :: k) rep (r :: TYPE rep). () + => TypeRep a -> (Typeable a => r) -> r + withTypeable rep k = withDict @(TypeRep a) @(Typeable a) rep k + + Note that the explicit type applications are required, as the call to + ``withDict`` would be ambiguous otherwise. diff --git a/docs/users_guide/release-notes.rst b/docs/users_guide/release-notes.rst index 92d4277a67..8b1313d8fe 100644 --- a/docs/users_guide/release-notes.rst +++ b/docs/users_guide/release-notes.rst @@ -6,3 +6,4 @@ Release notes 9.0.1-notes 9.2.1-notes + 9.4.1-notes diff --git a/libraries/base/Data/Typeable/Internal.hs b/libraries/base/Data/Typeable/Internal.hs index 39974b4052..962f5b82c1 100644 --- a/libraries/base/Data/Typeable/Internal.hs +++ b/libraries/base/Data/Typeable/Internal.hs @@ -495,12 +495,7 @@ splitApp (TrTyCon{trTyCon = con, trKindVars = kinds}) -- | Use a 'TypeRep' as 'Typeable' evidence. withTypeable :: forall k (a :: k) rep (r :: TYPE rep). () => TypeRep a -> (Typeable a => r) -> r -withTypeable rep k = unsafeCoerce k' rep - where k' :: Gift a r - k' = Gift k - --- | A helper to satisfy the type checker in 'withTypeable'. -newtype Gift a (r :: TYPE rep) = Gift (Typeable a => r) +withTypeable rep k = withDict @(TypeRep a) @(Typeable a) rep k -- | Pattern match on a type constructor pattern Con :: forall k (a :: k). () diff --git a/libraries/base/GHC/Base.hs b/libraries/base/GHC/Base.hs index 205fee906b..29e7ec85af 100644 --- a/libraries/base/GHC/Base.hs +++ b/libraries/base/GHC/Base.hs @@ -100,6 +100,7 @@ module GHC.Base module GHC.Classes, module GHC.CString, module GHC.Magic, + module GHC.Magic.Dict, module GHC.Types, module GHC.Prim, -- Re-export GHC.Prim and [boot] GHC.Err, module GHC.Prim.Ext, -- to avoid lots of people having to @@ -112,6 +113,7 @@ import GHC.Types import GHC.Classes import GHC.CString import GHC.Magic +import GHC.Magic.Dict import GHC.Prim import GHC.Prim.Ext import GHC.Err diff --git a/libraries/base/GHC/Exts.hs b/libraries/base/GHC/Exts.hs index 0e3cd14407..69b05068cc 100755 --- a/libraries/base/GHC/Exts.hs +++ b/libraries/base/GHC/Exts.hs @@ -76,6 +76,9 @@ module GHC.Exts -- * Running 'RealWorld' state thread runRW#, + -- * Casting class dictionaries with single methods + withDict, + -- * Safe coercions -- -- | These are available from the /Trustworthy/ module "Data.Coerce" as well diff --git a/libraries/base/GHC/TypeLits.hs b/libraries/base/GHC/TypeLits.hs index 2dcc28b223..0eb5f1e2fc 100644 --- a/libraries/base/GHC/TypeLits.hs +++ b/libraries/base/GHC/TypeLits.hs @@ -11,6 +11,7 @@ {-# LANGUAGE NoImplicitPrelude #-} {-# LANGUAGE MagicHash #-} {-# LANGUAGE PolyKinds #-} +{-# LANGUAGE TypeApplications #-} {-| GHC's @DataKinds@ language extension lifts data constructors, natural @@ -58,13 +59,13 @@ module GHC.TypeLits ) where -import GHC.Base(Eq(..), Ord(..), Ordering(..), String, otherwise) +import GHC.Base(Eq(..), Ord(..), Ordering(..), String, otherwise, withDict) import GHC.Types(Symbol, Char) import GHC.Num(Integer, fromInteger) import GHC.Show(Show(..)) import GHC.Read(Read(..)) import GHC.Real(toInteger) -import GHC.Prim(magicDict, Proxy#) +import GHC.Prim(Proxy#) import Data.Maybe(Maybe(..)) import Data.Proxy (Proxy(..)) import Data.Type.Equality((:~:)(Refl)) @@ -306,18 +307,16 @@ cmpChar x y = case compare (charVal x) (charVal y) of newtype SSymbol (s :: Symbol) = SSymbol String -data WrapS a b = WrapS (KnownSymbol a => Proxy a -> b) - --- See Note [magicDictId magic] in "basicType/MkId.hs" -withSSymbol :: (KnownSymbol a => Proxy a -> b) +-- See Note [withDict] in "GHC.HsToCore.Expr" in GHC +withSSymbol :: forall a b. + (KnownSymbol a => Proxy a -> b) -> SSymbol a -> Proxy a -> b -withSSymbol f x y = magicDict (WrapS f) x y +withSSymbol f x y = withDict @(SSymbol a) @(KnownSymbol a) x f y newtype SChar (s :: Char) = SChar Char -data WrapC a b = WrapC (KnownChar a => Proxy a -> b) - --- See Note [q] in "basicType/MkId.hs" -withSChar :: (KnownChar a => Proxy a -> b) +-- See Note [withDict] in "GHC.HsToCore.Expr" in GHC +withSChar :: forall a b. + (KnownChar a => Proxy a -> b) -> SChar a -> Proxy a -> b -withSChar f x y = magicDict (WrapC f) x y +withSChar f x y = withDict @(SChar a) @(KnownChar a) x f y diff --git a/libraries/base/GHC/TypeNats.hs b/libraries/base/GHC/TypeNats.hs index f9733d55a3..fd7c847112 100644 --- a/libraries/base/GHC/TypeNats.hs +++ b/libraries/base/GHC/TypeNats.hs @@ -12,6 +12,7 @@ {-# LANGUAGE NoImplicitPrelude #-} {-# LANGUAGE MagicHash #-} {-# LANGUAGE PolyKinds #-} +{-# LANGUAGE TypeApplications #-} {-| This module is an internal GHC module. It declares the constants used in the implementation of type-level natural numbers. The programmer interface @@ -38,12 +39,12 @@ module GHC.TypeNats ) where -import GHC.Base(Eq(..), Ord(..), otherwise) +import GHC.Base(Eq(..), Ord(..), otherwise, withDict) import GHC.Types import GHC.Num.Natural(Natural) import GHC.Show(Show(..)) import GHC.Read(Read(..)) -import GHC.Prim(magicDict, Proxy#) +import GHC.Prim(Proxy#) import Data.Maybe(Maybe(..)) import Data.Proxy (Proxy(..)) import Data.Type.Equality((:~:)(Refl)) @@ -121,7 +122,7 @@ After inlining and simplification, this ends up looking something like this: where type T = Any Nat `KnownNat` is the constructor for dictionaries for the class `KnownNat`. -See Note [magicDictId magic] in "basicType/MkId.hs" for details on how +See Note [withDict] in "GHC.HsToCore.Expr" for details on how we actually construct the dictionary. Note that using `Any Nat` is not really correct, as multilple calls to @@ -240,9 +241,8 @@ cmpNat x y = case compare (natVal x) (natVal y) of newtype SNat (n :: Nat) = SNat Natural -data WrapN a b = WrapN (KnownNat a => Proxy a -> b) - --- See Note [magicDictId magic] in "basicType/MkId.hs" -withSNat :: (KnownNat a => Proxy a -> b) +-- See Note [withDict] in "GHC.HsToCore.Expr" in GHC +withSNat :: forall a b. + (KnownNat a => Proxy a -> b) -> SNat a -> Proxy a -> b -withSNat f x y = magicDict (WrapN f) x y +withSNat f x y = withDict @(SNat a) @(KnownNat a) x f y diff --git a/libraries/ghc-prim/GHC/Magic/Dict.hs b/libraries/ghc-prim/GHC/Magic/Dict.hs new file mode 100644 index 0000000000..12861db568 --- /dev/null +++ b/libraries/ghc-prim/GHC/Magic/Dict.hs @@ -0,0 +1,44 @@ +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ImpredicativeTypes #-} +{-# LANGUAGE MagicHash #-} +{-# LANGUAGE NoImplicitPrelude #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE Unsafe #-} + +----------------------------------------------------------------------------- +-- | +-- Module : GHC.Magic.Dict +-- Copyright : (c) The University of Glasgow 2009 +-- License : see libraries/ghc-prim/LICENSE +-- +-- Maintainer : cvs-ghc@haskell.org +-- Stability : internal +-- Portability : non-portable (GHC Extensions) +-- +-- Defines the 'withDict' function. For more information, see +-- @Note [withDict]@ in "GHC.HsToCore.Expr" in GHC. +-- The definition of 'withDict' is located in a separate module from +-- "GHC.Magic" because 'withDict' is @Unsafe@ (it threatens type class +-- coherence) while "GHC.Magic" is @Trustworthy@. +-- +-- Use "GHC.Exts" from the @base@ package instead of importing this +-- module directly. +-- +----------------------------------------------------------------------------- + +module GHC.Magic.Dict (withDict) where + +import GHC.Prim.Panic (panicError) +import GHC.Types (RuntimeRep, TYPE) + +-- | @'withDict' d f@ provides a way to call a type-class–overloaded function +-- @f@ by applying it to the supplied dictionary @d@. +-- +-- 'withDict' can only be used if the type class has a single method with no +-- superclasses. For more (important) details on how this works, see +-- @Note [withDict]@ in "GHC.HsToCore.Expr" in GHC. +withDict :: forall {rr :: RuntimeRep} st dt (r :: TYPE rr). st -> (dt => r) -> r +{-# NOINLINE withDict #-} +withDict = panicError "Non-rewritten withDict"# diff --git a/libraries/ghc-prim/changelog.md b/libraries/ghc-prim/changelog.md index 6c7723068f..1ce61e2e61 100644 --- a/libraries/ghc-prim/changelog.md +++ b/libraries/ghc-prim/changelog.md @@ -1,3 +1,25 @@ +## next (edit as necessary) + +- `magicDict` has been renamed to `withDict` and is now defined in + `GHC.Magic.Dict` instead of `GHC.Prim`. `withDict` now has the type: + + ``` + withDict :: forall {rr :: RuntimeRep} st dt (r :: TYPE rr). st -> (dt => r) -> r + ``` + + Unlike `magicDict`, `withDict` can be used without defining an + intermediate data type. For example, the `withTypeable` function from the + `Data.Typeable` module can now be defined as: + + ``` + withTypeable :: forall k (a :: k) rep (r :: TYPE rep). () + => TypeRep a -> (Typeable a => r) -> r + withTypeable rep k = withDict @(TypeRep a) @(Typeable a) rep k + ``` + + Note that the explicit type applications are required, as the call to + `withDict` would be ambiguous otherwise. + ## 0.8.0 (edit as necessary) - Change array access primops to use type with size maxing the element size: @@ -23,7 +45,7 @@ - Add known-key `cstringLength#` to `GHC.CString`. This is just the C function `strlen`, but a built-in rewrite rule allows GHC to compute the result at compile time when the argument is known. - + - In order to support unicode better the following functions in `GHC.CString` gained UTF8 counterparts: @@ -47,7 +69,7 @@ atomicCasAddrAddr# :: Addr# -> Addr# -> Addr# -> State# s -> (# State# s, Addr# #) atomicCasWordAddr# :: Addr# -> Word# -> Word# -> State# s -> (# State# s, Word# #) -- Add an explicit fixity for `(~)` and `(~~)`: +- Add an explicit fixity for `(~)` and `(~~)`: infix 4 ~, ~~ diff --git a/libraries/ghc-prim/ghc-prim.cabal b/libraries/ghc-prim/ghc-prim.cabal index 05fd60f09a..61840021c1 100644 --- a/libraries/ghc-prim/ghc-prim.cabal +++ b/libraries/ghc-prim/ghc-prim.cabal @@ -45,6 +45,7 @@ Library GHC.Debug GHC.IntWord64 GHC.Magic + GHC.Magic.Dict GHC.Prim.Ext GHC.Prim.Panic GHC.Prim.Exception diff --git a/testsuite/tests/ghci/scripts/T19667Ghci.hs b/testsuite/tests/ghci/scripts/T19667Ghci.hs index 21e484bee9..c3ffa71be8 100644 --- a/testsuite/tests/ghci/scripts/T19667Ghci.hs +++ b/testsuite/tests/ghci/scripts/T19667Ghci.hs @@ -6,7 +6,7 @@ module Main (main) where import Data.Proxy (Proxy(..)) -import GHC.Exts (magicDict) +import GHC.Exts (withDict) import GHC.TypeLits (Symbol) import GHC.Exts @@ -18,12 +18,10 @@ class KnownSymbol (n :: Symbol) where symbolVal :: forall n proxy . KnownSymbol n => proxy n -> String symbolVal _ = case symbolSing :: SSymbol n of SSymbol x -> x -data WrapS a b = WrapS (KnownSymbol a => Proxy a -> b) - -- See Note [NOINLINE someNatVal] in GHC.TypeNats {-# NOINLINE reifySymbol #-} reifySymbol :: forall r. String -> (forall (n :: Symbol). KnownSymbol n => Proxy n -> r) -> r -reifySymbol n k = magicDict (WrapS k) (SSymbol n) (Proxy @(Any @Symbol)) +reifySymbol n k = withDict @(SSymbol Any) @(KnownSymbol Any) (SSymbol n) (k @Any) (Proxy @(Any @Symbol)) main :: IO () main = print $ reifySymbol "Hello World" symbolVal diff --git a/testsuite/tests/pmcheck/should_compile/T18478.hs b/testsuite/tests/pmcheck/should_compile/T18478.hs index 6739388d99..6c0fbd9828 100644 --- a/testsuite/tests/pmcheck/should_compile/T18478.hs +++ b/testsuite/tests/pmcheck/should_compile/T18478.hs @@ -99,7 +99,7 @@ import Data.Type.Coercion import GHC.TypeLits (ErrorMessage(..), TypeError) import Data.Typeable import GHC.Generics -import GHC.Exts +import GHC.Exts hiding (withDict) import Data.Kind data T = diff --git a/testsuite/tests/typecheck/should_fail/T16646Fail.hs b/testsuite/tests/typecheck/should_fail/T16646Fail.hs new file mode 100644 index 0000000000..73ded574b7 --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/T16646Fail.hs @@ -0,0 +1,28 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FunctionalDependencies #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +module T16646Fail where + +import Data.Kind +import Data.Proxy +import GHC.Exts + +f :: forall {rr :: RuntimeRep} st dt (r :: TYPE rr). st -> (dt => r) -> r +f = withDict @st @dt + +class Show a => C a where + m :: Maybe a + +g :: forall a r. Maybe a -> (C a => r) -> r +g = withDict @(Maybe a) @(C a) + +class Reifies s a | s -> a where + reflect :: proxy s -> a + +reify :: forall a r. a -> (forall (s :: Type). Reifies s a => Proxy s -> r) -> r +reify a k = withDict @_ @(Reifies (Any @Type) a) (const a) (k @Any) Proxy diff --git a/testsuite/tests/typecheck/should_fail/T16646Fail.stderr b/testsuite/tests/typecheck/should_fail/T16646Fail.stderr new file mode 100644 index 0000000000..3873a096d9 --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/T16646Fail.stderr @@ -0,0 +1,11 @@ + +T16646Fail.hs:16:5: error: + Invalid instantiation of ‘withDict’ at type: st -> (dt => r) -> r + +T16646Fail.hs:22:5: error: + Invalid instantiation of ‘withDict’ at type: + Maybe a -> (C a => r) -> r + +T16646Fail.hs:28:13: error: + Invalid instantiation of ‘withDict’ at type: + (Any -> a) -> (Reifies Any a => Proxy Any -> r) -> Proxy Any -> r diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T index 7891e4543c..65f80a1e13 100644 --- a/testsuite/tests/typecheck/should_fail/all.T +++ b/testsuite/tests/typecheck/should_fail/all.T @@ -527,6 +527,7 @@ test('T16456', normal, compile_fail, ['-fprint-explicit-foralls']) test('T16627', normal, compile_fail, ['']) test('T502', normal, compile_fail, ['']) test('T16517', normal, compile_fail, ['']) +test('T16646Fail', normal, compile_fail, ['']) test('T15883', normal, compile_fail, ['']) test('T15883b', normal, compile_fail, ['']) test('T15883c', normal, compile_fail, ['']) diff --git a/testsuite/tests/typecheck/should_run/T16646.hs b/testsuite/tests/typecheck/should_run/T16646.hs new file mode 100644 index 0000000000..6af86e96a4 --- /dev/null +++ b/testsuite/tests/typecheck/should_run/T16646.hs @@ -0,0 +1,91 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FunctionalDependencies #-} +{-# LANGUAGE ImpredicativeTypes #-} +{-# LANGUAGE TypeFamilies #-} +module Main where + +import Data.Kind (Type) +import Data.Proxy (Proxy(..)) +import GHC.Exts (Any, withDict) +import GHC.TypeLits +import Type.Reflection (TypeRep, typeRep, withTypeable) + +----- +-- reflection +----- + +class Reifies s a | s -> a where + reflect :: proxy s -> a + +instance KnownNat n => Reifies n Integer where + reflect = natVal + +reify :: forall a r. a -> (forall (s :: Type). Reifies s a => Proxy s -> r) -> r +{-# NOINLINE reify #-} -- See Note [NOINLINE someNatVal] in GHC.TypeNats +reify a k = withDict @(forall (proxy :: Type -> Type). proxy Any -> a) + @(Reifies (Any @Type) a) + (const a) (k @Any) Proxy + +class Given a where + given :: a + +withGift :: forall a b. + (Given a => Proxy a -> b) + -> a -> Proxy a -> b +withGift f x y = withDict @a @(Given a) x f y + +give :: forall a r. a -> (Given a => r) -> r +give a k = withGift (\_ -> k) a Proxy + +foo :: Given Int => Bool -> Int +foo True = 42 +foo False = given + +----- +-- singletons +----- + +type family Sing :: k -> Type +data SBool :: Bool -> Type where + SFalse :: SBool False + STrue :: SBool True +deriving instance Show (SBool z) +type instance Sing @Bool = SBool + +class SingI a where + sing :: Sing a + +data SingInstance (a :: k) where + SingInstance :: SingI a => SingInstance a + +singInstance :: forall k (a :: k). Sing a -> SingInstance a +singInstance s = with_sing_i SingInstance + where + with_sing_i :: (SingI a => SingInstance a) -> SingInstance a + with_sing_i si = withDict @(Sing a) @(SingI a) s si + +withSingI :: Sing n -> (SingI n => r) -> r +withSingI sn r = + case singInstance sn of + SingInstance -> r + +----- + +main :: IO () +main = do + -- Type.Reflection + let f :: forall a. TypeRep a -> IO () + f tr = withTypeable tr $ print $ typeRep @a + in f $ typeRep @Int + + -- GHC.TypeLits + print $ someCharVal 'a' + print $ someNatVal 42 + print $ someSymbolVal "Hello World" + + -- reflection + print $ reify 6 (\p -> reflect p + reflect p) + print $ give (23 :: Int) foo True + + -- singletons + print $ withSingI SFalse (sing @False) diff --git a/testsuite/tests/typecheck/should_run/T16646.stdout b/testsuite/tests/typecheck/should_run/T16646.stdout new file mode 100644 index 0000000000..9d2fdaadf5 --- /dev/null +++ b/testsuite/tests/typecheck/should_run/T16646.stdout @@ -0,0 +1,7 @@ +Int +'a' +Just 42 +"Hello World" +12 +42 +SFalse diff --git a/testsuite/tests/typecheck/should_run/T19667.hs b/testsuite/tests/typecheck/should_run/T19667.hs index 21e484bee9..c3ffa71be8 100644 --- a/testsuite/tests/typecheck/should_run/T19667.hs +++ b/testsuite/tests/typecheck/should_run/T19667.hs @@ -6,7 +6,7 @@ module Main (main) where import Data.Proxy (Proxy(..)) -import GHC.Exts (magicDict) +import GHC.Exts (withDict) import GHC.TypeLits (Symbol) import GHC.Exts @@ -18,12 +18,10 @@ class KnownSymbol (n :: Symbol) where symbolVal :: forall n proxy . KnownSymbol n => proxy n -> String symbolVal _ = case symbolSing :: SSymbol n of SSymbol x -> x -data WrapS a b = WrapS (KnownSymbol a => Proxy a -> b) - -- See Note [NOINLINE someNatVal] in GHC.TypeNats {-# NOINLINE reifySymbol #-} reifySymbol :: forall r. String -> (forall (n :: Symbol). KnownSymbol n => Proxy n -> r) -> r -reifySymbol n k = magicDict (WrapS k) (SSymbol n) (Proxy @(Any @Symbol)) +reifySymbol n k = withDict @(SSymbol Any) @(KnownSymbol Any) (SSymbol n) (k @Any) (Proxy @(Any @Symbol)) main :: IO () main = print $ reifySymbol "Hello World" symbolVal diff --git a/testsuite/tests/typecheck/should_run/all.T b/testsuite/tests/typecheck/should_run/all.T index efc9fcb374..a34fb61747 100755 --- a/testsuite/tests/typecheck/should_run/all.T +++ b/testsuite/tests/typecheck/should_run/all.T @@ -76,6 +76,7 @@ test('IPRun', normal, compile_and_run, ['']) test('IPLocation', normal, compile_and_run, ['']) test('T10845', normal, compile_and_run, ['']) test('T10846', normal, compile_and_run, ['']) +test('T16646', normal, compile_and_run, ['']) # Support files for T1735 are in directory T1735_Help/ test('T1735', normal, multimod_compile_and_run, ['T1735','']) |