Commit 4715b871 authored by Iavor S. Diatchki's avatar Iavor S. Diatchki

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.
parent 8c3bc838
......@@ -65,6 +65,7 @@ import FastString
import Util
import MonadUtils
import Data.Word(Word)
......@@ -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
......@@ -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)
......@@ -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.
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 _) = []
......@@ -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
......@@ -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
......@@ -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)
* *
......@@ -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
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