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.

4 files changed, 56 insertions, 0 deletions

diff --git a/compiler/deSugar/DsBinds.lhs b/compiler/deSugar/DsBinds.lhs
index 7cc58583dd..9753d3ebb4 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 cb4c75cc6e..e2313443aa 100644
--- a/compiler/typecheck/TcEvidence.lhs
+++ b/compiler/typecheck/TcEvidence.lhs
@@ -466,6 +466,9 @@ data EvTerm
                                  -- dictionaries, even though the former have no

                                  -- 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 3e18da52cc..0ac550d10c 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 b0eca45ebf..4da4c9f007 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