Repository : ssh://darcs.haskell.org//srv/darcs/ghc On branch : type-nats
http://hackage.haskell.org/trac/ghc/changeset/4715b87194db20df0812b4596998a10ca0110c27 >--------------------------------------------------------------- commit 4715b87194db20df0812b4596998a10ca0110c27 Author: Iavor S. Diatchki <[email protected]> Date: Thu Dec 29 19:25:10 2011 -0800 Add the built-in instances for class NatI. Note 1: For the moment, we provide instances only for numbers that fit in a Word. The reason is a quite mundane: to generate evidence for arbitrary integers we need to generate integer literals. In the core syntax this is a monadic operation but the function that generates the core for evidence is pure. It would not be hard to monadify it but requires changes to a bunch of other functions so I thought it is better left for a separate change. Note 2: The evidence that we generate for a NatI is just a word. Technically, we should be generate a word with two coercions: one to turn it into a NatS and another to turn that into a NatI. Operationally, these do not do anything, but it would be better to fix this. I didn't do it yet because I need to look up how to make these coercions. >--------------------------------------------------------------- compiler/deSugar/DsBinds.lhs | 9 +++++++++ compiler/typecheck/TcEvidence.lhs | 37 +++++++++++++++++++++++++++++++++++++ compiler/typecheck/TcHsSyn.lhs | 1 + compiler/typecheck/TcInteract.lhs | 9 +++++++++ 4 files changed, 56 insertions(+), 0 deletions(-) diff --git a/compiler/deSugar/DsBinds.lhs b/compiler/deSugar/DsBinds.lhs index 7cc5858..9753d3e 100644 --- a/compiler/deSugar/DsBinds.lhs +++ b/compiler/deSugar/DsBinds.lhs @@ -65,6 +65,7 @@ import FastString import Util import MonadUtils +import Data.Word(Word) \end{code} %************************************************************************ @@ -707,6 +708,14 @@ dsEvTerm (EvSuperClass d n) sc_sel_id = classSCSelId cls n -- Zero-indexed (cls, tys) = getClassPredTys (evVarPred d) +-- It would be better to make an Integer expression here, but this would +-- require quite a bit of the surrounding code to be monadified. +-- In the intereset of simplicity (and keeping changes incremental) we +-- leave this for a later day. +dsEvTerm (EvInteger n) + | n > fromIntegral (maxBound :: Word) = panic "dsEvTerm: Integer too big!" + | otherwise = mkWordExprWord (fromInteger n) + --------------------------------------- dsTcCoercion :: TcCoercion -> (Coercion -> CoreExpr) -> CoreExpr -- This is the crucial function that moves diff --git a/compiler/typecheck/TcEvidence.lhs b/compiler/typecheck/TcEvidence.lhs index cb4c75c..e231344 100644 --- a/compiler/typecheck/TcEvidence.lhs +++ b/compiler/typecheck/TcEvidence.lhs @@ -467,6 +467,9 @@ data EvTerm -- selector Id. We count up from _0_ | EvKindCast EvVar TcCoercion -- See Note [EvKindCast] + | EvInteger Integer -- The dictionary for class "NatI" + -- Note [EvInteger] + deriving( Data.Data, Data.Typeable) \end{code} @@ -503,6 +506,38 @@ Conclusion: a new wanted coercion variable should be made mutable. from super classes will be "given" and hence rigid] +Note [EvInteger] +~~~~~~~~~~~~~~~~ +A part of the type-level naturals implementation is the class "NatI", +which provides a "smart" constructor for defining singleton values. + +newtype NatS (n :: Nat) = NatS Integer + +class NatI n where + natS :: NatS n + +Conceptually, this class has infinitely many instances: + +instance NatI 0 where natS = NatS 0 +instance NatI 1 where natS = NatS 1 +instance NatI 2 where natS = NatS 2 +... + +In practice, we solve "NatI" predicates in the type-checker because we can't +have infinately many instances. The evidence (aka "dictionary") +for "NatI n" is of the form "EvInteger n". + +We make the following assumptions about dictionaries in GHC: + 1. The "dictionary" for classes with a single method---like NatI---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 "NatS" value, and another to make it into "NatI" evidence. + + + \begin{code} mkEvCast :: EvVar -> TcCoercion -> EvTerm mkEvCast ev lco @@ -531,6 +566,7 @@ evVarsOfTerm (EvSuperClass v _) = [v] evVarsOfTerm (EvCast v co) = v : varSetElems (coVarsOfTcCo co) evVarsOfTerm (EvTupleMk evs) = evs evVarsOfTerm (EvKindCast v co) = v : varSetElems (coVarsOfTcCo co) +evVarsOfTerm (EvInteger _) = [] \end{code} @@ -590,5 +626,6 @@ instance Outputable EvTerm where ppr (EvTupleMk vs) = ptext (sLit "tupmk") <+> ppr vs ppr (EvSuperClass d n) = ptext (sLit "sc") <> parens (ppr (d,n)) ppr (EvDFunApp df tys ts) = ppr df <+> sep [ char '@' <> ppr tys, ppr ts ] + ppr (EvInteger n) = integer n \end{code} diff --git a/compiler/typecheck/TcHsSyn.lhs b/compiler/typecheck/TcHsSyn.lhs index 3e18da5..0ac550d 100644 --- a/compiler/typecheck/TcHsSyn.lhs +++ b/compiler/typecheck/TcHsSyn.lhs @@ -1112,6 +1112,7 @@ zonkEvTerm env (EvKindCast v co) = ASSERT( isId v) zonkEvTerm env (EvTupleSel v n) = return (EvTupleSel (zonkIdOcc env v) n) zonkEvTerm env (EvTupleMk vs) = return (EvTupleMk (map (zonkIdOcc env) vs)) +zonkEvTerm _ (EvInteger n) = return (EvInteger n) zonkEvTerm env (EvSuperClass d n) = return (EvSuperClass (zonkIdOcc env d) n) zonkEvTerm env (EvDFunApp df tys tms) = do { tys' <- zonkTcTypeToTypes env tys diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs index b0eca45..4da4c9f 100644 --- a/compiler/typecheck/TcInteract.lhs +++ b/compiler/typecheck/TcInteract.lhs @@ -26,6 +26,7 @@ import Var import VarEnv ( ) -- unitVarEnv, mkInScopeSet import TcType +import PrelNames (typeNatClassName) import Class import TyCon @@ -56,6 +57,7 @@ import Pair ( pSnd ) import UniqFM import FastString ( sLit ) import DynFlags +import Data.Word(Word) \end{code} ********************************************************************** * * @@ -1770,6 +1772,13 @@ data LookupInstResult | GenInst [WantedEvVar] EvTerm matchClassInst :: InertSet -> Class -> [Type] -> WantedLoc -> TcS LookupInstResult + +matchClassInst _ clas [ ty ] _ + | className clas == typeNatClassName + , Just n <- isNumberTy ty + , n <= fromIntegral (maxBound :: Word) = return (GenInst [] (EvInteger n)) + + matchClassInst inerts clas tys loc = do { let pred = mkClassPred clas tys ; mb_result <- matchClass clas tys _______________________________________________ Cvs-ghc mailing list [email protected] http://www.haskell.org/mailman/listinfo/cvs-ghc
