Repository : ssh://darcs.haskell.org//srv/darcs/ghc On branch : master
http://hackage.haskell.org/trac/ghc/changeset/1bfb97985881bc080956156d40c84a7d888787d1 >--------------------------------------------------------------- commit 1bfb97985881bc080956156d40c84a7d888787d1 Author: Iavor S. Diatchki <[email protected]> Date: Sun Apr 8 19:38:45 2012 -0700 Update names to match the implementation in GHC.TypeLits. >--------------------------------------------------------------- compiler/prelude/PrelNames.lhs | 16 ++++++---------- compiler/typecheck/TcEvidence.lhs | 32 +++++++++++++++++++------------- compiler/typecheck/TcInteract.lhs | 8 ++++---- 3 files changed, 29 insertions(+), 27 deletions(-) diff --git a/compiler/prelude/PrelNames.lhs b/compiler/prelude/PrelNames.lhs index 35806a1..9b47edb 100644 --- a/compiler/prelude/PrelNames.lhs +++ b/compiler/prelude/PrelNames.lhs @@ -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} %************************************************************************ diff --git a/compiler/typecheck/TcEvidence.lhs b/compiler/typecheck/TcEvidence.lhs index 571643c..8ec0a57 100644 --- a/compiler/typecheck/TcEvidence.lhs +++ b/compiler/typecheck/TcEvidence.lhs @@ -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} diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs index 01dcda8..cc9fc06 100644 --- a/compiler/typecheck/TcInteract.lhs +++ b/compiler/typecheck/TcInteract.lhs @@ -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 _______________________________________________ Cvs-ghc mailing list [email protected] http://www.haskell.org/mailman/listinfo/cvs-ghc
