Commit 1bfb9798 authored by Iavor S. Diatchki's avatar Iavor S. Diatchki

Update names to match the implementation in GHC.TypeLits.

parent f0d10e34
......@@ -276,8 +276,7 @@ basicKnownKeyNames
-- Type-level naturals
typeNatKindConName,
typeStringKindConName,
typeNatClassName,
typeStringClassName,
singIClassName,
typeNatLeqClassName,
typeNatAddTyFamName,
typeNatMulTyFamName,
......@@ -1052,14 +1051,12 @@ isStringClassName = clsQual dATA_STRING (fsLit "IsString") isStringClassKey
-- Type-level naturals
typeNatKindConName, typeStringKindConName,
typeNatClassName, typeStringClassName, typeNatLeqClassName,
singIClassName, typeNatLeqClassName,
typeNatAddTyFamName, typeNatMulTyFamName, typeNatExpTyFamName :: Name
typeNatKindConName = tcQual gHC_TYPELITS (fsLit "Nat") typeNatKindConNameKey
typeStringKindConName = tcQual gHC_TYPELITS (fsLit "Symbol")
typeStringKindConNameKey
typeNatClassName = clsQual gHC_TYPELITS (fsLit "NatI") typeNatClassNameKey
typeStringClassName = clsQual gHC_TYPELITS (fsLit "SymbolI")
typeStringClassNameKey
singIClassName = clsQual gHC_TYPELITS (fsLit "SingI") singIClassNameKey
typeNatLeqClassName = clsQual gHC_TYPELITS (fsLit "<=") typeNatLeqClassNameKey
typeNatAddTyFamName = tcQual gHC_TYPELITS (fsLit "+") typeNatAddTyFamNameKey
typeNatMulTyFamName = tcQual gHC_TYPELITS (fsLit "*") typeNatMulTyFamNameKey
......@@ -1179,10 +1176,9 @@ datatypeClassKey = mkPreludeClassUnique 39
constructorClassKey = mkPreludeClassUnique 40
selectorClassKey = mkPreludeClassUnique 41
typeNatClassNameKey, typeStringClassNameKey, typeNatLeqClassNameKey :: Unique
typeNatClassNameKey = mkPreludeClassUnique 42
typeStringClassNameKey = mkPreludeClassUnique 43
typeNatLeqClassNameKey = mkPreludeClassUnique 44
singIClassNameKey, typeNatLeqClassNameKey :: Unique
singIClassNameKey = mkPreludeClassUnique 42
typeNatLeqClassNameKey = mkPreludeClassUnique 43
\end{code}
%************************************************************************
......
......@@ -473,7 +473,7 @@ data EvTerm
| EvKindCast EvVar TcCoercion -- See Note [EvKindCast]
| EvLit EvLit -- The dictionary for class "NatI"
| EvLit EvLit -- Dictionary for class "SingI" for type lits.
-- Note [EvLit]
deriving( Data.Data, Data.Typeable)
......@@ -519,33 +519,39 @@ Conclusion: a new wanted coercion variable should be made mutable.
Note [EvLit]
~~~~~~~~~~~~
A part of the type-level naturals implementation is the class "NatI",
A part of the type-level literals implementation is the class "SingI",
which provides a "smart" constructor for defining singleton values.
newtype TNat (n :: Nat) = TNat Integer
newtype Sing n = Sing (SingRep n)
class NatI n where
tNat :: TNat n
class SingI n where
sing :: Sing n
type family SingRep a
type instance SingRep (a :: Nat) = Integer
type instance SingRep (a :: Symbol) = String
Conceptually, this class has infinitely many instances:
instance NatI 0 where natS = TNat 0
instance NatI 1 where natS = TNat 1
instance NatI 2 where natS = TNat 2
instance Sing 0 where sing = Sing 0
instance Sing 1 where sing = Sing 1
instance Sing 2 where sing = Sing 2
instance Sing "hello" where sing = Sing "hello"
...
In practice, we solve "NatI" predicates in the type-checker because we can't
In practice, we solve "SingI" predicates in the type-checker because we can't
have infinately many instances. The evidence (aka "dictionary")
for "NatI n" is of the form "EvLit (EvNum n)".
for "SingI (n :: Nat)" 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 NatI---is
1. The "dictionary" for classes with a single method---like SingI---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 "NatI" is just an integer wrapped in 2 newtypes:
one to make it into a "TNat" value, and another to make it into "NatI" evidence.
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.
\begin{code}
......
......@@ -26,7 +26,7 @@ import Id
import Var
import TcType
import PrelNames (typeNatClassName, typeStringClassName)
import PrelNames (singIClassName)
import Class
import TyCon
......@@ -1865,11 +1865,11 @@ data LookupInstResult
matchClassInst :: InertSet -> Class -> [Type] -> WantedLoc -> TcS LookupInstResult
matchClassInst _ clas [ ty ] _
| className clas == typeNatClassName
matchClassInst _ clas [ _, ty ] _
| className clas == singIClassName
, Just n <- isNumLitTy ty = return $ GenInst [] $ EvLit $ EvNum n
| className clas == typeStringClassName
| className clas == singIClassName
, Just s <- isStrLitTy ty = return $ GenInst [] $ EvLit $ EvStr s
......
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