Commit c3762fa4 authored by Iavor S. Diatchki's avatar Iavor S. Diatchki
Browse files

Update and clean-up the implmenation of GHC.TypeLits

* Replace class `SingI` with two separate classes: `KnownNat` and `KnownSymbol`

* Rename `magicSingId` to `magicDictId`.

* Simplify and clean-up the "magic" implementation.  This version makes
  a lot more sense, at least to me :-)

* Update notes about how it all works:

  Note [KnownNat & KnownSymbol and EvLit] explains the evidence for the
  built-in classes

  Note [magicDictId magic] explains how we coerce singleton values into
  dictionaries.  This is used to turn run-time integers and strings into
  Proxy singletons of unknwon type (using an existential).
parent a83652ed
......@@ -35,7 +35,7 @@ module MkId (
wiredInIds, ghcPrimIds,
unsafeCoerceName, unsafeCoerceId, realWorldPrimId,
voidArgId, nullAddrId, seqId, lazyId, lazyIdKey,
coercionTokenId, magicSingIId,
coercionTokenId, magicDictId,
-- Re-export error Ids
module PrelRules
......@@ -137,7 +137,7 @@ ghcPrimIds
unsafeCoerceId,
nullAddrId,
seqId,
magicSingIId,
magicDictId,
coerceId,
proxyHashId
]
......@@ -1038,14 +1038,14 @@ they can unify with both unlifted and lifted types. Hence we provide
another gun with which to shoot yourself in the foot.
\begin{code}
lazyIdName, unsafeCoerceName, nullAddrName, seqName, realWorldName, coercionTokenName, magicSingIName, coerceName, proxyName :: Name
lazyIdName, unsafeCoerceName, nullAddrName, seqName, realWorldName, coercionTokenName, magicDictName, coerceName, proxyName :: Name
unsafeCoerceName = mkWiredInIdName gHC_PRIM (fsLit "unsafeCoerce#") unsafeCoerceIdKey unsafeCoerceId
nullAddrName = mkWiredInIdName gHC_PRIM (fsLit "nullAddr#") nullAddrIdKey nullAddrId
seqName = mkWiredInIdName gHC_PRIM (fsLit "seq") seqIdKey seqId
realWorldName = mkWiredInIdName gHC_PRIM (fsLit "realWorld#") realWorldPrimIdKey realWorldPrimId
lazyIdName = mkWiredInIdName gHC_MAGIC (fsLit "lazy") lazyIdKey lazyId
coercionTokenName = mkWiredInIdName gHC_PRIM (fsLit "coercionToken#") coercionTokenIdKey coercionTokenId
magicSingIName = mkWiredInIdName gHC_PRIM (fsLit "magicSingI") magicSingIKey magicSingIId
magicDictName = mkWiredInIdName gHC_PRIM (fsLit "magicDict") magicDictKey magicDictId
coerceName = mkWiredInIdName gHC_PRIM (fsLit "coerce") coerceKey coerceId
proxyName = mkWiredInIdName gHC_PRIM (fsLit "proxy#") proxyHashKey proxyHashId
\end{code}
......@@ -1130,8 +1130,8 @@ lazyId = pcMiscPrelId lazyIdName ty info
--------------------------------------------------------------------------------
magicSingIId :: Id -- See Note [magicSingIId magic]
magicSingIId = pcMiscPrelId magicSingIName ty info
magicDictId :: Id -- See Note [magicDictId magic]
magicDictId = pcMiscPrelId magicDictName ty info
where
info = noCafIdInfo `setInlinePragInfo` neverInlinePragma
ty = mkForAllTys [alphaTyVar] alphaTy
......@@ -1245,42 +1245,49 @@ lazyId is defined in GHC.Base, so we don't *have* to inline it. If it
appears un-applied, we'll end up just calling it.
Note [magicSingIId magic]
Note [magicDictId magic]
~~~~~~~~~~~~~~~~~~~~~~~~~
The identifier `magicSIngI` is just a place-holder, which is used to
The identifier `magicDict` is just a place-holder, which is used to
implement a primitve that we cannot define in Haskell but we can write
in Core. It is declared with a place-holder type:
magicSingI :: forall a. a
magicDict :: forall a. a
The intention is that the identifier will be used in a very specific way,
namely we add the following to the library:
to create dictionaries for classes with a single method. Consider a class
like this:
withSingI :: Sing n -> (SingI n => a) -> a
withSingI x = magicSingI x ((\f -> f) :: () -> ())
class C a where
f :: T a
The actual primitive is `withSingI`, and it uses its first argument
(of type `Sing n`) as the evidece/dictionary in the second argument.
This is done by adding a built-in rule to `prelude/PrelRules.hs`
(see `match_magicSingI`), which works as follows:
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:
magicSingI @ (Sing n -> (() -> ()) -> (SingI n -> a) -> a)
x
(\f -> _)
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.
\(f :: (SingI n -> a) -> a) -> f (cast x (newtypeCo n))
Next, we add a built-in Prelude rule (see prelude/PrelRules.hs),
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 `newtypeCo` coercion is extracted from the `SingI` type constructor,
which is available in the instantiation. We are casting `Sing n` into `SingI n`,
which is OK because `SingI` is a class with a single methid,
and thus it is implemented as newtype.
The `co` coercion is the newtype-coercion extracted from the type-class.
The type class is obtain by looking at the type of wrap.
The `(\f -> f)` parameter is there just so that we can avoid
having to make up a new name for the lambda, it is completely
changed by the rewrite.
-------------------------------------------------------------
......
......@@ -10,7 +10,7 @@ data DataConBoxer
mkDataConWorkId :: Name -> DataCon -> Id
mkPrimOpId :: PrimOp -> Id
magicSingIId :: Id
magicDictId :: Id
\end{code}
......@@ -294,7 +294,7 @@ basicKnownKeyNames
randomClassName, randomGenClassName, monadPlusClassName,
-- Type-level naturals
singIClassName,
knownNatClassName, knownSymbolClassName,
-- Implicit parameters
ipClassName,
......@@ -1137,8 +1137,10 @@ randomGenClassName = clsQual rANDOM (fsLit "RandomGen") randomGenClassKey
isStringClassName = clsQual dATA_STRING (fsLit "IsString") isStringClassKey
-- Type-level naturals
singIClassName :: Name
singIClassName = clsQual gHC_TYPELITS (fsLit "SingI") singIClassNameKey
knownNatClassName :: Name
knownNatClassName = clsQual gHC_TYPELITS (fsLit "KnownNat") knownNatClassNameKey
knownSymbolClassName :: Name
knownSymbolClassName = clsQual gHC_TYPELITS (fsLit "KnownSymbol") knownSymbolClassNameKey
-- Implicit parameters
ipClassName :: Name
......@@ -1260,9 +1262,13 @@ datatypeClassKey = mkPreludeClassUnique 39
constructorClassKey = mkPreludeClassUnique 40
selectorClassKey = mkPreludeClassUnique 41
-- SingI: see Note [SingI and EvLit] in TcEvidence
singIClassNameKey :: Unique
singIClassNameKey = mkPreludeClassUnique 42
-- KnownNat: see Note [KnowNat & KnownSymbol and EvLit] in TcEvidence
knownNatClassNameKey :: Unique
knownNatClassNameKey = mkPreludeClassUnique 42
-- KnownSymbol: see Note [KnownNat & KnownSymbol and EvLit] in TcEvidence
knownSymbolClassNameKey :: Unique
knownSymbolClassNameKey = mkPreludeClassUnique 43
ghciIoClassKey :: Unique
ghciIoClassKey = mkPreludeClassUnique 44
......@@ -1713,8 +1719,8 @@ checkDotnetResNameIdKey = mkPreludeMiscIdUnique 154
undefinedKey :: Unique
undefinedKey = mkPreludeMiscIdUnique 155
magicSingIKey :: Unique
magicSingIKey = mkPreludeMiscIdUnique 156
magicDictKey :: Unique
magicDictKey = mkPreludeMiscIdUnique 156
coerceKey :: Unique
coerceKey = mkPreludeMiscIdUnique 157
......
......@@ -20,12 +20,11 @@ module PrelRules ( primOpRules, builtinRules ) where
#include "HsVersions.h"
#include "../includes/MachDeps.h"
import {-# SOURCE #-} MkId ( mkPrimOpId, magicSingIId )
import {-# SOURCE #-} MkId ( mkPrimOpId, magicDictId )
import CoreSyn
import MkCore
import Id
import Var (setVarType)
import Literal
import CoreSubst ( exprIsLiteral_maybe )
import PrimOp ( PrimOp(..), tagToEnumKey )
......@@ -888,8 +887,8 @@ builtinRules
ru_nargs = 2, ru_try = \dflags _ _ -> match_eq_string dflags },
BuiltinRule { ru_name = fsLit "Inline", ru_fn = inlineIdName,
ru_nargs = 2, ru_try = \_ _ _ -> match_inline },
BuiltinRule { ru_name = fsLit "MagicSingI", ru_fn = idName magicSingIId,
ru_nargs = 3, ru_try = \_ _ _ -> match_magicSingI }
BuiltinRule { ru_name = fsLit "MagicDict", ru_fn = idName magicDictId,
ru_nargs = 4, ru_try = \_ _ _ -> match_magicDict }
]
++ builtinIntegerRules
......@@ -1062,18 +1061,19 @@ match_inline (Type _ : e : _)
match_inline _ = Nothing
-- See Note [magicSingIId magic] in `basicTypes/MkId.lhs`
-- See Note [magicDictId magic] in `basicTypes/MkId.lhs`
-- for a description of what is going on here.
match_magicSingI :: [Expr CoreBndr] -> Maybe (Expr CoreBndr)
match_magicSingI (Type t : e : Lam b _ : _)
| ((_ : _ : fu : _),_) <- splitFunTys t
, (sI_type,_) <- splitFunTy fu
, Just (sI_tc,xs) <- splitTyConApp_maybe sI_type
, Just (_,_,co) <- unwrapNewTyCon_maybe sI_tc
= Just $ let f = setVarType b fu
in Lam f $ Var f `App` Cast e (mkSymCo (mkUnbranchedAxInstCo Representational co xs))
match_magicSingI _ = Nothing
match_magicDict :: [Expr CoreBndr] -> Maybe (Expr CoreBndr)
match_magicDict [Type _, 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
-------------------------------------------------
-- Integer rules
......
......@@ -532,8 +532,8 @@ data EvTerm
-- dictionaries, even though the former have no
-- selector Id. We count up from _0_
| EvLit EvLit -- Dictionary for class "SingI" for type lits.
-- Note [SingI and EvLit]
| EvLit EvLit -- Dictionary for KnownNat and KnownLit classes.
-- Note [KnownNat & KnownSymbol and EvLit]
| EvCoercible EvCoercible -- Dictionary for "Coercible a b"
-- Note [Coercible Instances]
......@@ -606,40 +606,57 @@ Conclusion: a new wanted coercion variable should be made mutable.
from super classes will be "given" and hence rigid]
Note [SingI and EvLit]
~~~~~~~~~~~~~~~~~~~~~~
A part of the type-level literals implementation is the class "SingI",
which provides a "smart" constructor for defining singleton values.
Here is the key stuff from GHC.TypeLits
Note [KnownNat & KnownSymbol and EvLit]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
A part of the type-level literals implementation are the classes
"KnownNat" and "KnownLit", which provide a "smart" constructor for
defining singleton values. Here is the key stuff from GHC.TypeLits
class SingI n where
sing :: Sing n
class KnownNat (n :: Nat) where
natSing :: SNat n
data family Sing (n::k)
newtype instance Sing (n :: Nat) = SNat Integer
newtype instance Sing (s :: Symbol) = SSym String
newtype SNat (n :: Nat) = SNat Integer
Conceptually, this class has infinitely many instances:
instance Sing 0 where sing = SNat 0
instance Sing 1 where sing = SNat 1
instance Sing 2 where sing = SNat 2
instance Sing "hello" where sing = SSym "hello"
instance KnownNat 0 where natSing = SNat 0
instance KnownNat 1 where natSing = SNat 1
instance KnownNat 2 where natSing = SNat 2
...
In practice, we solve "SingI" predicates in the type-checker because we can't
have infinately many instances. The evidence (aka "dictionary")
for "SingI (n :: Nat)" is of the form "EvLit (EvNum n)".
In practice, we solve `KnownNat` predicates in the type-checker
(see typecheck/TcInteract.hs) because we can't have infinately many instances.
The evidence (aka "dictionary") for `KnownNat` is of the form `EvLit (EvNum n)`.
We make the following assumptions about dictionaries in GHC:
1. The "dictionary" for classes with a single method---like SingI---is
1. The "dictionary" for classes with a single method---like `KnownNat`---is
a newtype for the type of the method, so using a evidence amounts
to a coercion, and
2. Newtypes use the same representation as their definition types.
So, the evidence for "SingI" is just a value of the representation type,
wrapped in two newtype constructors: one to make it into a "Sing" value,
and another to make it into "SingI" evidence.
So, the evidence for `KnownNat` is just a value of the representation type,
wrapped in two newtype constructors: one to make it into a `SNat` value,
and another to make it into a `KnownNat` dictionary.
Also note that `natSing` and `SNat` are never actually exposed from the
library---they are just an implementation detail. Instead, users see
a more convenient function, defined in terms of `natSing`:
natVal :: KnownNat n => proxy n -> Integer
The reason we don't use this directly in the class is that it is simpler
and more efficient to pass around an integer rather than an entier function,
especialy when the `KnowNat` evidence is packaged up in an existential.
The story for kind `Symbol` is analogous:
* class KnownSymbol
* newypte SSymbol
* Evidence: EvLit (EvStr n)
\begin{code}
......
......@@ -13,19 +13,17 @@ module TcInteract (
#include "HsVersions.h"
import BasicTypes ()
import TcCanonical
import VarSet
import Type
import Unify
import FamInstEnv
import FamInst(TcBuiltInSynFamily(..))
import InstEnv( lookupInstEnv, instanceDFunId )
import Var
import TcType
import PrelNames (singIClassName, ipClassNameKey )
import PrelNames (knownNatClassName, knownSymbolClassName, ipClassNameKey )
import TysWiredIn ( coercibleClass )
import Id( idType )
import Class
......@@ -1734,47 +1732,41 @@ instance Outputable LookupInstResult where
matchClassInst :: InertSet -> Class -> [Type] -> CtLoc -> TcS LookupInstResult
matchClassInst _ clas [ k, ty ] _
| className clas == singIClassName
matchClassInst _ clas [ ty ] _
| className clas == knownNatClassName
, Just n <- isNumLitTy ty = makeDict (EvNum n)
| className clas == singIClassName
| className clas == knownSymbolClassName
, Just s <- isStrLitTy ty = makeDict (EvStr s)
where
{- This adds a coercion that will convert the literal into a dictionary
of the appropriate type. See Note [SingI and EvLit] in TcEvidence.
The coercion happens in 3 steps:
of the appropriate type. See Note [KnownNat & KnownSymbol and EvLit]
in TcEvidence. The coercion happens in 2 steps:
Integer -> SNat n -- representation of literal to singleton
SNat n -> KnownNat n -- singleton to dictionary
evLit -> Sing_k_n -- literal to representation of data family
Sing_k_n -> Sing k n -- representation of data family to data family
Sing k n -> SingI k n -- data family to class dictionary.
The process is mirrored for Symbols:
String -> SSymbol n
SSymbol n -> KnownSymbol n
-}
makeDict evLit =
case unwrapNewTyCon_maybe (classTyCon clas) of
Just (_,dictRep, axDict)
| Just tcSing <- tyConAppTyCon_maybe dictRep ->
do mbInst <- matchOpenFam tcSing [k,ty]
case mbInst of
Just FamInstMatch
{ fim_instance = FamInst { fi_axiom = axDataFam
, fi_flavor = DataFamilyInst tcon
}
, fim_tys = tys
} | Just (_,_,axSing) <- unwrapNewTyCon_maybe tcon ->
-- co1 and co3 are at role R, while co2 is at role N.
-- BUT, when desugaring to Coercions, the roles get fixed.
do let co1 = mkTcSymCo $ mkTcUnbranchedAxInstCo axSing tys
co2 = mkTcSymCo $ mkTcUnbranchedAxInstCo axDataFam tys
co3 = mkTcSymCo $ mkTcUnbranchedAxInstCo axDict [k,ty]
return $ GenInst [] $ EvCast (EvLit evLit) $
mkTcTransCo co1 $ mkTcTransCo co2 co3
_ -> unexpected
_ -> unexpected
unexpected = panicTcS (text "Unexpected evidence for SingI")
Just (_,_, axDict)
| [ meth ] <- classMethods clas
, Just tcRep <- tyConAppTyCon_maybe -- SNat
$ funResultTy -- SNat n
$ dropForAlls -- KnownNat n => SNat n
$ idType meth -- forall n. KnownNat n => SNat n
, Just (_,_,axRep) <- unwrapNewTyCon_maybe tcRep
-> return $
let co1 = mkTcSymCo $ mkTcUnbranchedAxInstCo axRep [ty]
co2 = mkTcSymCo $ mkTcUnbranchedAxInstCo axDict [ty]
in GenInst [] $ EvCast (EvLit evLit) (mkTcTransCo co1 co2)
_ -> panicTcS (text "Unexpected evidence for" <+> ppr (className clas)
$$ vcat (map (ppr . idType) (classMethods clas)))
matchClassInst _ clas [ ty1, ty2 ] _
| clas == coercibleClass = do
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment