Add basic support for number type literals.
authorIavor S. Diatchki <iavor.diatchki@gmail.com>
Sun, 16 Jan 2011 21:56:36 +0000 (13:56 -0800)
committerIavor S. Diatchki <iavor.diatchki@gmail.com>
Sun, 16 Jan 2011 21:56:36 +0000 (13:56 -0800)
We add a new kind, Nat, inhabited by a family of types,
one for each natural number:

0, 1, 2 .. :: Nat

In terms of GHC's sub-kind relation, Nat is only a sub-kind of itself.

The numeric types are empty because there are no primitives of these
types, and the kind "Nat" is not related to *, the kind of types which
can be defined in Haskell programs.

34 files changed:
compiler/codeGen/ClosureInfo.lhs
compiler/codeGen/StgCmmClosure.hs
compiler/coreSyn/CoreLint.lhs
compiler/coreSyn/ExternalCore.lhs
compiler/coreSyn/MkExternalCore.lhs
compiler/coreSyn/PprExternalCore.lhs
compiler/hsSyn/Convert.lhs
compiler/hsSyn/HsTypes.lhs
compiler/iface/BinIface.hs
compiler/iface/IfaceSyn.lhs
compiler/iface/IfaceType.lhs
compiler/iface/TcIface.lhs
compiler/main/DynFlags.hs
compiler/parser/Lexer.x
compiler/parser/Parser.y.pp
compiler/parser/RdrHsSyn.lhs
compiler/prelude/PrelNames.lhs
compiler/rename/RnHsSyn.lhs
compiler/rename/RnTypes.lhs
compiler/typecheck/TcCanonical.lhs
compiler/typecheck/TcErrors.lhs
compiler/typecheck/TcHsType.lhs
compiler/typecheck/TcMType.lhs
compiler/typecheck/TcSimplify.lhs
compiler/typecheck/TcSplice.lhs
compiler/typecheck/TcTyDecls.lhs
compiler/typecheck/TcType.lhs
compiler/typecheck/TcUnify.lhs
compiler/types/Coercion.lhs
compiler/types/FamInstEnv.lhs
compiler/types/OptCoercion.lhs
compiler/types/Type.lhs
compiler/types/TypeRep.lhs
compiler/types/Unify.lhs

index d2c63b3..c4ed016 100644 (file)
@@ -1044,6 +1044,7 @@ getTyDescription ty
       TyConApp tycon _              -> getOccString tycon
       PredTy sty            -> getPredTyDescription sty
       ForAllTy _ ty          -> getTyDescription ty
+      LiteralTy _            -> panic "getTyDecription LiteralTy"
     }
   where
     fun_result (FunTy _ res) = '>' : fun_result res
index d66dda5..09bff0b 100644 (file)
@@ -1079,6 +1079,7 @@ getTyDescription ty
       TyConApp tycon _              -> getOccString tycon
       PredTy sty            -> getPredTyDescription sty
       ForAllTy _ ty          -> getTyDescription ty
+      LiteralTy _            -> panic "getTyDescription LiteralTy"
     }
   where
     fun_result (FunTy _ res) = '>' : fun_result res
index 5cc82a2..86d4a4e 100644 (file)
@@ -661,6 +661,8 @@ lintCoercion' ty@(TyConApp tc tys)
        ; check_co_app ty (tyConKind tc) ss
        ; return (TyConApp tc ss, TyConApp tc ts) }
 
+lintCoercion' ty@(LiteralTy _) = return (ty, ty)
+
 lintCoercion' ty@(PredTy (ClassP cls tys))
   = do { (ss,ts) <- mapAndUnzipM lintCoercion tys
        ; check_co_app ty (tyConKind (classTyCon cls)) ss
@@ -766,6 +768,8 @@ lintType ty@(AppTy t1 t2)
 lintType ty@(FunTy t1 t2)
   = lint_ty_app ty (tyConKind funTyCon) [t1,t2]
 
+lintType ty@(LiteralTy l) = lintTyLit l >> return (typeKind ty)
+
 lintType ty@(TyConApp tc tys)
   | tyConHasKind tc
   = lint_ty_app ty (tyConKind tc) tys
@@ -785,6 +789,18 @@ lintType (PredTy (IParam _ p_ty))
 lintType ty@(PredTy (EqPred {}))
   = failWithL (badEq ty)
 
+
+---
+
+lintTyLit :: TyLit -> LintM ()
+lintTyLit (NumberTyLit n)
+  | n >= 0    = return ()
+  | otherwise = failWithL msg
+    where msg = ptext (sLit "Negative type literal:") <+> integer n
+
+
+
+
 ----------------
 lint_ty_app :: Type -> Kind -> [OutType] -> LintM Kind
 lint_ty_app ty k tys 
index 07a1dfb..5017551 100644 (file)
@@ -56,6 +56,7 @@ data Ty
   | Tcon (Qual Tcon)
   | Tapp Ty Ty
   | Tforall Tbind Ty 
+  | Tliteral TLit
 -- We distinguish primitive coercions
 -- (represented in GHC by wired-in names), because
 -- External Core treats them specially, so we have
@@ -74,6 +75,10 @@ data Kind
   | Kopen
   | Karrow Kind Kind
   | Keq Ty Ty
+  | Knat
+
+data TLit
+  = TLnumber Integer
 
 data Lit 
   = Lint Integer Ty
index cb784e8..e72d492 100644 (file)
@@ -209,6 +209,7 @@ make_ty t = make_ty' t
 -- note calls to make_ty so as to expand types recursively
 make_ty' :: Type -> C.Ty
 make_ty' (TyVarTy tv)           = C.Tvar (make_var_id (tyVarName tv))
+make_ty' (LiteralTy n)           = C.Tliteral (make_tlit n)
 make_ty' (AppTy t1 t2)                  = C.Tapp (make_ty t1) (make_ty t2)
 make_ty' (FunTy t1 t2)                  = make_ty (TyConApp funTyCon [t1,t2])
 make_ty' (ForAllTy tv t)        = C.Tforall (make_tbind tv) (make_ty t)
@@ -228,6 +229,9 @@ make_ty' (TyConApp tc ts)    = make_tyConApp tc ts
 
 make_ty' (PredTy p)    = make_ty (predTypeRep p)
 
+make_tlit :: TyLit -> C.TLit
+make_tlit (NumberTyLit n) = C.TLnumber n
+
 make_tyConApp :: TyCon -> [Type] -> C.Ty
 make_tyConApp tc [t1, t2] | tc == transCoercionTyCon =
   C.TransCoercion (make_ty t1) (make_ty t2)
@@ -257,6 +261,7 @@ make_kind k
   | isLiftedTypeKind k   = C.Klifted
   | isUnliftedTypeKind k = C.Kunlifted
   | isOpenTypeKind k     = C.Kopen
+  | isNatKind k          = C.Knat
 make_kind _ = error "MkExternalCore died: make_kind"
 
 {- Id generation. -}
index 3c4b25e..f7ae7d9 100644 (file)
@@ -82,6 +82,7 @@ pakind, pkind :: Kind -> Doc
 pakind (Klifted) = char '*'
 pakind (Kunlifted) = char '#'
 pakind (Kopen) = char '?'
+pakind (Knat) = text "Nat"
 pakind k = parens (pkind k)
 
 pkind (Karrow k1 k2) = parens (pakind k1 <> text "->" <> pkind k2)
@@ -92,6 +93,7 @@ pkind k = pakind k
 paty, pbty, pty :: Ty -> Doc
 paty (Tvar n) = pname n
 paty (Tcon c) = pqname c
+paty (Tliteral n) = ptlit n
 paty t = parens (pty t)
 
 pbty (Tapp(Tapp(Tcon tc) t1) t2) | tc == tcArrow = parens(fsep [pbty t1, text "->",pty t2])
@@ -114,6 +116,9 @@ pty (InstCoercion t1 t2) =
   sep [text "%inst", paty t1, paty t2]
 pty t = pbty t
 
+ptlit :: TLit -> Doc
+ptlit (TLnumber n) = integer n
+
 pappty :: Ty -> [Ty] -> Doc
 pappty (Tapp t1 t2) ts = pappty t1 (t2:ts)
 pappty t ts = sep (map paty (t:ts))
index dcef02f..b81265e 100644 (file)
@@ -270,6 +270,7 @@ cvt_tyinst_hdr cxt tc tys
     collect (TupleT _)   = return []
     collect ArrowT       = return []
     collect ListT        = return []
+    collect (LiteralT _) = return []
     collect (AppT t1 t2)
       = do { tvs1 <- collect t1
            ; tvs2 <- collect t2
index 38608a4..8f3a9cf 100644 (file)
@@ -168,6 +168,11 @@ data HsType name
        -- interface files smaller), so when printing a HsType we may need to
        -- add parens.  
 
+  | HsNumberTy          Integer         -- Type level number
+      -- Uses a separate constructor from the generics one to avoid confusion.
+      -- In this way we could support both by just modifying the parser to
+      -- avoid the overlap between the two.
+
   | HsNumTy             Integer                -- Generics only
 
   | HsPredTy           (HsPred name)   -- Only used in the type of an instance
@@ -440,6 +445,7 @@ ppr_mono_ty _    (HsKindSig ty kind) = parens (ppr_mono_lty pREC_TOP ty <+> dcol
 ppr_mono_ty _    (HsListTy ty)      = brackets (ppr_mono_lty pREC_TOP ty)
 ppr_mono_ty _    (HsPArrTy ty)      = pabrackets (ppr_mono_lty pREC_TOP ty)
 ppr_mono_ty _    (HsPredTy pred)     = ppr pred
+ppr_mono_ty _    (HsNumberTy n)      = integer n
 ppr_mono_ty _    (HsNumTy n)         = integer n  -- generics only
 ppr_mono_ty _    (HsSpliceTy s _ _)  = pprSplice s
 ppr_mono_ty _    (HsCoreTy ty)       = ppr ty
index b1c97cd..4878983 100644 (file)
@@ -885,6 +885,11 @@ instance Binary IfaceType where
     put_ bh (IfacePredTy aq) = do
            putByte bh 5
            put_ bh aq
+    put_ bh (IfaceLiteralTy n) = do
+           putByte bh 20
+           put_ bh n
+
+
 
        -- Simple compression for common cases of TyConApp
     put_ bh (IfaceTyConApp IfaceIntTc  [])   = putByte bh 6
@@ -900,6 +905,7 @@ instance Binary IfaceType where
     put_ bh (IfaceTyConApp IfaceUnliftedTypeKindTc []) = putByte bh 14
     put_ bh (IfaceTyConApp IfaceUbxTupleKindTc [])     = putByte bh 15
     put_ bh (IfaceTyConApp IfaceArgTypeKindTc [])      = putByte bh 16
+    put_ bh (IfaceTyConApp IfaceNatKindTc [])          = putByte bh 21
     put_ bh (IfaceTyConApp (IfaceAnyTc k) [])         = do { putByte bh 17; put_ bh k }
 
        -- Generic cases
@@ -923,6 +929,8 @@ instance Binary IfaceType where
                      return (IfaceFunTy ag ah)
              5 -> do ap <- get bh
                      return (IfacePredTy ap)
+              20 -> do n <- get bh
+                       return (IfaceLiteralTy n)
 
                -- Now the special cases for TyConApp
              6 -> return (IfaceTyConApp IfaceIntTc [])
@@ -936,11 +944,22 @@ instance Binary IfaceType where
               14 -> return (IfaceTyConApp IfaceUnliftedTypeKindTc [])
               15 -> return (IfaceTyConApp IfaceUbxTupleKindTc [])
               16 -> return (IfaceTyConApp IfaceArgTypeKindTc [])
+              21 -> return (IfaceTyConApp IfaceNatKindTc [])
               17 -> do { k <- get bh; return (IfaceTyConApp (IfaceAnyTc k) []) }
 
              18 -> do { tc <- get bh; tys <- get bh; return (IfaceTyConApp (IfaceTc tc) tys) }
              _  -> do { tc <- get bh; tys <- get bh; return (IfaceTyConApp tc tys) }
 
+instance Binary IfaceTyLit where
+  put_ bh (IfaceNumberTyLit n)  = putByte bh 1 >> put_ bh n
+
+  get bh =
+    do tag <- getByte bh
+       case tag of
+         1 -> do n <- get bh
+                 return (IfaceNumberTyLit n)
+
+
 instance Binary IfaceTyCon where
        -- Int,Char,Bool can't show up here because they can't not be saturated
 
@@ -954,6 +973,7 @@ instance Binary IfaceTyCon where
    put_ bh IfaceUnliftedTypeKindTc = putByte bh 8
    put_ bh IfaceUbxTupleKindTc     = putByte bh 9
    put_ bh IfaceArgTypeKindTc      = putByte bh 10
+   put_ bh IfaceNatKindTc          = putByte bh 14
    put_ bh (IfaceTupTc bx ar) = do { putByte bh 11; put_ bh bx; put_ bh ar }
    put_ bh (IfaceTc ext)      = do { putByte bh 12; put_ bh ext }
    put_ bh (IfaceAnyTc k)     = do { putByte bh 13; put_ bh k }
@@ -971,6 +991,7 @@ instance Binary IfaceTyCon where
           8 -> return IfaceUnliftedTypeKindTc
           9 -> return IfaceUbxTupleKindTc
           10 -> return IfaceArgTypeKindTc
+          14 -> return IfaceNatKindTc
          11 -> do { bx <- get bh; ar <- get bh; return (IfaceTupTc bx ar) }
          12 -> do { ext <- get bh; return (IfaceTc ext) }
          _  -> do { k <- get bh; return (IfaceAnyTc k) }
index c06137c..3c22702 100644 (file)
@@ -788,6 +788,8 @@ freeNamesIfType (IfaceTyConApp tc ts) =
 freeNamesIfType (IfaceForAllTy tv t)  =
    freeNamesIfTvBndr tv &&& freeNamesIfType t
 freeNamesIfType (IfaceFunTy s t)      = freeNamesIfType s &&& freeNamesIfType t
+freeNamesIfType (IfaceLiteralTy _)    = emptyNameSet
+
 
 freeNamesIfTvBndrs :: [IfaceTvBndr] -> NameSet
 freeNamesIfTvBndrs = fnList freeNamesIfTvBndr
index c97e16e..6bc8616 100644 (file)
@@ -10,6 +10,7 @@ module IfaceType (
        IfExtName, IfLclName,
 
         IfaceType(..), IfaceKind, IfacePredType(..), IfaceTyCon(..),
+        IfaceTyLit(..),
        IfaceContext, IfaceBndr(..), IfaceTvBndr, IfaceIdBndr, IfaceCoercion,
        ifaceTyConName,
 
@@ -67,12 +68,16 @@ data IfaceType
   | IfaceTyConApp IfaceTyCon [IfaceType]       -- Not necessarily saturated
                                                -- Includes newtypes, synonyms, tuples
   | IfaceFunTy  IfaceType IfaceType
+  | IfaceLiteralTy IfaceTyLit
 
 data IfacePredType     -- NewTypes are handled as ordinary TyConApps
   = IfaceClassP IfExtName [IfaceType]
   | IfaceIParam (IPName OccName) IfaceType
   | IfaceEqPred IfaceType IfaceType
 
+data IfaceTyLit
+  = IfaceNumberTyLit Integer
+
 type IfaceContext = [IfacePredType]
 
 data IfaceTyCon        -- Abbreviations for common tycons with known names
@@ -84,6 +89,7 @@ data IfaceTyCon       -- Abbreviations for common tycons with known names
                             -- other than 'Any :: *' itself
   | IfaceLiftedTypeKindTc | IfaceOpenTypeKindTc | IfaceUnliftedTypeKindTc
   | IfaceUbxTupleKindTc | IfaceArgTypeKindTc 
+  | IfaceNatKindTc 
 
 ifaceTyConName :: IfaceTyCon -> IfExtName
 ifaceTyConName IfaceIntTc             = intTyConName
@@ -97,6 +103,7 @@ ifaceTyConName IfaceOpenTypeKindTc     = openTypeKindTyConName
 ifaceTyConName IfaceUnliftedTypeKindTc = unliftedTypeKindTyConName
 ifaceTyConName IfaceUbxTupleKindTc     = ubxTupleKindTyConName
 ifaceTyConName IfaceArgTypeKindTc      = argTypeKindTyConName
+ifaceTyConName IfaceNatKindTc          = natKindTyConName
 ifaceTyConName (IfaceTc ext)           = ext
 ifaceTyConName (IfaceAnyTc k)          = pprPanic "ifaceTyConName" (ppr k)
                                         -- Note [The Name of an IfaceAnyTc]
@@ -227,6 +234,8 @@ ppr_ty ctxt_prec ty@(IfaceForAllTy _ _)
   = maybeParen ctxt_prec fUN_PREC (pprIfaceForAllPart tvs theta (pprIfaceType tau))
  where         
     (tvs, theta, tau) = splitIfaceSigmaTy ty
+
+ppr_ty _ (IfaceLiteralTy n) = ppr_tylit n
     
 -------------------
 pprIfaceForAllPart :: [IfaceTvBndr] -> IfaceContext -> SDoc -> SDoc
@@ -253,6 +262,9 @@ ppr_tc :: IfaceTyCon -> SDoc
 ppr_tc tc@(IfaceTc ext_nm) = parenSymOcc (getOccName ext_nm) (ppr tc)
 ppr_tc tc                 = ppr tc
 
+ppr_tylit :: IfaceTyLit -> SDoc
+ppr_tylit (IfaceNumberTyLit n) = integer n
+
 -------------------
 instance Outputable IfacePredType where
        -- Print without parens
@@ -268,6 +280,9 @@ instance Outputable IfaceTyCon where
                             -- so we fake it.  It's only for debug printing!
   ppr other_tc       = ppr (ifaceTyConName other_tc)
 
+instance Outputable IfaceTyLit where
+  ppr = ppr_tylit
+
 -------------------
 pprIfaceContext :: IfaceContext -> SDoc
 -- Prints "(C a, D b) =>", including the arrow
@@ -321,6 +336,7 @@ toIfaceType (ForAllTy tv t) =
   IfaceForAllTy (toIfaceTvBndr tv) (toIfaceType t)
 toIfaceType (PredTy st) =
   IfacePredTy (toIfacePred st)
+toIfaceType (LiteralTy n) = IfaceLiteralTy (toIfaceTyLit n)
 
 ----------------
 -- A little bit of (perhaps optional) trickiness here.  When
@@ -357,6 +373,7 @@ toIfaceWiredInTyCon tc nm
   | nm == openTypeKindTyConName     = IfaceOpenTypeKindTc
   | nm == argTypeKindTyConName      = IfaceArgTypeKindTc
   | nm == ubxTupleKindTyConName     = IfaceUbxTupleKindTc
+  | nm == natKindTyConName          = IfaceNatKindTc
   | otherwise                      = IfaceTc nm
 
 ----------------
@@ -372,6 +389,10 @@ toIfacePred (IParam ip t) =
 toIfacePred (EqPred ty1 ty2) =
   IfaceEqPred (toIfaceType ty1) (toIfaceType ty2)
 
+toIfaceTyLit :: TyLit -> IfaceTyLit
+toIfaceTyLit (NumberTyLit x) = IfaceNumberTyLit x
+
+
 ----------------
 toIfaceContext :: ThetaType -> IfaceContext
 toIfaceContext cs = map toIfacePred cs
index 8dccc72..b5c6495 100644 (file)
@@ -787,6 +787,7 @@ tcIfaceVectInfo mod typeEnv (IfaceVectInfo
 \begin{code}
 tcIfaceType :: IfaceType -> IfL Type
 tcIfaceType (IfaceTyVar n)        = do { tv <- tcIfaceTyVar n; return (TyVarTy tv) }
+tcIfaceType (IfaceLiteralTy l)    = do { l <- tcIfaceTyLit l; return (LiteralTy l) }
 tcIfaceType (IfaceAppTy t1 t2)    = do { t1' <- tcIfaceType t1; t2' <- tcIfaceType t2; return (AppTy t1' t2') }
 tcIfaceType (IfaceFunTy t1 t2)    = do { t1' <- tcIfaceType t1; t2' <- tcIfaceType t2; return (FunTy t1' t2') }
 tcIfaceType (IfaceTyConApp tc ts) = do { tc' <- tcIfaceTyCon tc; ts' <- tcIfaceTypes ts; return (mkTyConApp tc' ts') }
@@ -805,6 +806,15 @@ tcIfacePredType (IfaceEqPred t1 t2)  = do { t1' <- tcIfaceType t1; t2' <- tcIfac
 -----------------------------------------
 tcIfaceCtxt :: IfaceContext -> IfL ThetaType
 tcIfaceCtxt sts = mapM tcIfacePredType sts
+
+
+-----------------------------------------
+tcIfaceTyLit :: IfaceTyLit -> IfL TyLit
+tcIfaceTyLit (IfaceNumberTyLit n) = return (NumberTyLit n)
+
+
+
+
 \end{code}
 
 
@@ -1205,6 +1215,7 @@ tcIfaceTyCon IfaceOpenTypeKindTc     = return openTypeKindTyCon
 tcIfaceTyCon IfaceUnliftedTypeKindTc = return unliftedTypeKindTyCon
 tcIfaceTyCon IfaceArgTypeKindTc      = return argTypeKindTyCon
 tcIfaceTyCon IfaceUbxTupleKindTc     = return ubxTupleKindTyCon
+tcIfaceTyCon IfaceNatKindTc          = return natKindTyCon
 
 -- Even though we are in an interface file, we want to make
 -- sure the instances and RULES of this tycon are loaded 
index 92b98ac..53d9c37 100644 (file)
@@ -365,6 +365,7 @@ data ExtensionFlag
    | Opt_DatatypeContexts
    | Opt_NondecreasingIndentation
    | Opt_RelaxedLayout
+   | Opt_TypeNaturals
    deriving (Eq, Show)
 
 -- | Contains not only a collection of 'DynFlag's but also a plethora of
@@ -1631,7 +1632,8 @@ xFlags = [
   ( "OverlappingInstances",             Opt_OverlappingInstances, nop ),
   ( "UndecidableInstances",             Opt_UndecidableInstances, nop ),
   ( "IncoherentInstances",              Opt_IncoherentInstances, nop ),
-  ( "PackageImports",                   Opt_PackageImports, nop )
+  ( "PackageImports",                   Opt_PackageImports, nop ),
+  ( "TypeNaturals",                     Opt_TypeNaturals, nop)
   ]
 
 defaultFlags :: [DynFlag]
@@ -1681,6 +1683,9 @@ impliedFlags
        -- stuff like " 'a' not in scope ", which is a bit silly
        -- if the compiler has just filled in field 'a' of constructor 'C'
     , (Opt_RecordWildCards,     turnOn, Opt_DisambiguateRecordFields)
+
+    , (Opt_TypeNaturals,        turnOn, Opt_TypeOperators)
+    , (Opt_TypeNaturals,        turnOn, Opt_KindSignatures)
   ]
 
 optLevelFlags :: [([Int], DynFlag)]
index 5e65356..d918fa7 100644 (file)
@@ -53,7 +53,7 @@ module Lexer (
    popContext, pushCurrentContext, setLastToken, setSrcLoc,
    activeContext, nextIsEOF,
    getLexState, popLexState, pushLexState,
-   extension, bangPatEnabled, datatypeContextsEnabled,
+   extension, bangPatEnabled, datatypeContextsEnabled, typeNaturalsEnabled,
    addWarning,
    lexTokenStream
   ) where
@@ -1798,6 +1798,8 @@ relaxedLayoutBit :: Int
 relaxedLayoutBit = 24
 nondecreasingIndentationBit :: Int
 nondecreasingIndentationBit = 25
+typeNaturalsBit :: Int
+typeNaturalsBit = 26
 
 always :: Int -> Bool
 always           _     = True
@@ -1841,6 +1843,8 @@ relaxedLayout :: Int -> Bool
 relaxedLayout flags = testBit flags relaxedLayoutBit
 nondecreasingIndentation :: Int -> Bool
 nondecreasingIndentation flags = testBit flags nondecreasingIndentationBit
+typeNaturalsEnabled :: Int -> Bool
+typeNaturalsEnabled flags = testBit flags typeNaturalsBit
 
 -- PState for parsing options pragmas
 --
@@ -1895,6 +1899,7 @@ mkPState flags buf loc =
                .|. alternativeLayoutRuleBit `setBitIf` xopt Opt_AlternativeLayoutRule flags
                .|. relaxedLayoutBit `setBitIf` xopt Opt_RelaxedLayout flags
                .|. nondecreasingIndentationBit `setBitIf` xopt Opt_NondecreasingIndentation flags
+               .|. typeNaturalsBit `setBitIf` xopt Opt_TypeNaturals flags
       --
       setBitIf :: Int -> Bool -> Int
       b `setBitIf` cond | cond      = bit b
index c71e62d..833fe6c 100644 (file)
@@ -1025,8 +1025,7 @@ atype :: { LHsType RdrName }
        | '$(' exp ')'                  { LL $ mkHsSpliceTy $2 }
        | TH_ID_SPLICE                  { LL $ mkHsSpliceTy $ L1 $ HsVar $ 
                                          mkUnqual varName (getTH_ID_SPLICE $1) }
--- Generics
-        | INTEGER                       { L1 (HsNumTy (getINTEGER $1)) }
+        | INTEGER                       {% mkNumberType (L1 (getINTEGER $1)) }
 
 -- An inst_type is what occurs in the head of an instance decl
 --     e.g.  (Foo a, Gaz b) => Wibble a b
@@ -1082,6 +1081,7 @@ kind      :: { Located Kind }
 akind  :: { Located Kind }
        : '*'                   { L1 liftedTypeKind }
        | '!'                   { L1 unliftedTypeKind }
+       | tycon                 {% checkKindCon $1 }
        | '(' kind ')'          { LL (unLoc $2) }
 
 
index 4df2a29..02adc14 100644 (file)
@@ -38,6 +38,8 @@ module RdrHsSyn (
        checkPred,            -- HsType -> P HsPred
        checkTyVars,          -- [LHsType RdrName] -> P ()
        checkKindSigs,        -- [LTyClDecl RdrName] -> P ()
+    checkKindCon,         -- Located RdrName -> P (Located Kind)
+    mkNumberType,
        checkInstType,        -- HsType -> P HsType
        checkPattern,         -- HsExp -> P HsPat
        bang_RDR,
@@ -53,7 +55,7 @@ module RdrHsSyn (
 
 import HsSyn           -- Lots of it
 import Class            ( FunDep )
-import TypeRep          ( Kind )
+import TypeRep          ( Kind, natKind )
 import RdrName         ( RdrName, isRdrTyVar, isRdrTc, mkUnqual, rdrNameOcc, 
                          isRdrDataCon, isUnqual, getRdrName, setRdrNameSpace )
 import BasicTypes      ( maxPrecedence, Activation(..), RuleMatchInfo,
@@ -129,6 +131,7 @@ extract_lty (L loc ty) acc
       HsPredTy p               -> extract_pred p acc
       HsOpTy ty1 (L loc tv) ty2 -> extract_tv loc tv (extract_lty ty1 (extract_lty ty2 acc))
       HsParTy ty                       -> extract_lty ty acc
+      HsNumberTy {}             -> acc
       HsNumTy {}                -> acc
       HsCoreTy {}               -> acc  -- The type is closed
       HsQuasiQuoteTy {}                -> acc  -- Quasi quotes mention no type variables
@@ -572,6 +575,28 @@ checkKindSigs = mapM_ check
       | otherwise           = 
        parseErrorSDoc l (text "Type declaration in a class must be a kind signature or synonym default:" $$ ppr tydecl)
 
+checkKindCon :: Located RdrName -> P (Located Kind)
+checkKindCon (L l name)
+  | occNameString (rdrNameOcc name) == "Nat" =
+    do type_nats_on <- extension typeNaturalsEnabled
+       if type_nats_on
+         then return (L l natKind)
+         else parseErrorSDoc l
+              (text "Invalid kind" <+> ppr name <+> parens
+                (text "Use -XTypeNaturals to enable type-level naturals"))
+checkKindCon name@(L l _) =
+  parseErrorSDoc l (text "Invalid kind" <+> ppr name)
+
+mkNumberType :: Located Integer -> P (LHsType RdrName)
+mkNumberType (L l n) =
+  do type_nats_on <- extension typeNaturalsEnabled
+     if type_nats_on
+       then return (L l (HsNumberTy n))
+       else parseErrorSDoc l
+              (text "Invalid number type," <+> integer n <> dot <+> parens
+                (text "Use -XTypeNaturals to enable type-level naturals"))
+
+
 checkContext :: LHsType RdrName -> P (LHsContext RdrName)
 checkContext (L l t)
   = check t
index 4d3c446..dee65d1 100644 (file)
@@ -1033,12 +1033,13 @@ coSuperKindTyConKey                    = mkPreludeTyConUnique 86
 
 -- Kind constructors
 liftedTypeKindTyConKey, openTypeKindTyConKey, unliftedTypeKindTyConKey,
-    ubxTupleKindTyConKey, argTypeKindTyConKey :: Unique
+    ubxTupleKindTyConKey, argTypeKindTyConKey, natKindTyConKey :: Unique
 liftedTypeKindTyConKey                  = mkPreludeTyConUnique 87
 openTypeKindTyConKey                    = mkPreludeTyConUnique 88
 unliftedTypeKindTyConKey                = mkPreludeTyConUnique 89
 ubxTupleKindTyConKey                    = mkPreludeTyConUnique 90
 argTypeKindTyConKey                     = mkPreludeTyConUnique 91
+natKindTyConKey                         = mkPreludeTyConUnique 92
 
 -- Coercion constructors
 symCoercionTyConKey, transCoercionTyConKey, leftCoercionTyConKey,
@@ -1332,7 +1333,9 @@ kindKeys = [ liftedTypeKindTyConKey
           , openTypeKindTyConKey
           , unliftedTypeKindTyConKey
           , ubxTupleKindTyConKey 
-          , argTypeKindTyConKey ]
+          , argTypeKindTyConKey
+           , natKindTyConKey
+           ]
 \end{code}
 
 
index 9226cb4..55303ac 100644 (file)
@@ -66,6 +66,7 @@ extractHsTyNames ty
     get (HsParTy ty)           = getl ty
     get (HsBangTy _ ty)        = getl ty
     get (HsRecTy flds)         = extractHsTyNames_s (map cd_fld_type flds)
+    get (HsNumberTy _)         = emptyNameSet
     get (HsNumTy _)            = emptyNameSet
     get (HsTyVar tv)           = unitNameSet tv
     get (HsSpliceTy _ fvs _)   = fvs
index 138ffa2..1ebb4c1 100644 (file)
@@ -139,6 +139,8 @@ rnHsType doc (HsRecTy flds)
   = do { flds' <- rnConDeclFields doc flds
        ; return (HsRecTy flds') }
 
+rnHsType _ (HsNumberTy i) = return (HsNumberTy i)
+
 rnHsType _ (HsNumTy i)
   | i == 1    = return (HsNumTy i)
   | otherwise = addErr err_msg >> return (HsNumTy i)
index 60d1836..10dc200 100644 (file)
@@ -116,6 +116,8 @@ flatten ctxt ty
 flatten _ v@(TyVarTy _)
   = return (v, v, emptyCCan)
 
+flatten _ t@(LiteralTy _) = return (t, t, emptyCCan)
+
 flatten ctxt (AppTy ty1 ty2)
   = do { (xi1,co1,c1) <- flatten ctxt ty1
        ; (xi2,co2,c2) <- flatten ctxt ty2
@@ -814,6 +816,7 @@ expandAway tv t@(TyVarTy tv')
   | otherwise = Just t
 expandAway tv xi
   | not (tv `elemVarSet` tyVarsOfType xi) = Just xi
+expandAway _ t@(LiteralTy _) = Just t -- (To avoid incompleteness warning)
 expandAway tv (AppTy ty1 ty2) 
   = do { ty1' <- expandAway tv ty1
        ; ty2' <- expandAway tv ty2 
index c040473..967b312 100644 (file)
@@ -651,6 +651,7 @@ quickFlattenTy :: TcType -> TcM TcType
 -- See Note [Flattening in error message generation]
 quickFlattenTy ty | Just ty' <- tcView ty = quickFlattenTy ty'
 quickFlattenTy ty@(TyVarTy {})  = return ty
+quickFlattenTy ty@(LiteralTy {})= return ty
 quickFlattenTy ty@(ForAllTy {}) = return ty     -- See
 quickFlattenTy ty@(PredTy {})   = return ty     -- Note [Quick-flatten polytypes]
   -- Don't flatten because of the danger or removing a bound variable
index 43e58be..0523d98 100644 (file)
@@ -365,6 +365,8 @@ kc_hs_type (HsPArrTy ty) = do
     ty' <- kcLiftedType ty
     return (HsPArrTy ty', liftedTypeKind)
 
+kc_hs_type (HsNumberTy n) = return (HsNumberTy n, natKind)
+
 kc_hs_type (HsNumTy n)
    = return (HsNumTy n, liftedTypeKind)
 
@@ -606,6 +608,8 @@ ds_type (HsOpTy ty1 (L span op) ty2) = do
     tau_ty2 <- dsHsType ty2
     setSrcSpan span (ds_var_app op [tau_ty1,tau_ty2])
 
+ds_type (HsNumberTy n) = return (mkNumberTy n)
+
 ds_type (HsNumTy n)
   = ASSERT(n==1) do
     tc <- tcLookupTyCon genUnitTyConName
index 08385fe..9921767 100644 (file)
@@ -699,6 +699,8 @@ zonkType zonk_tc_tyvar ty
     go (PredTy p)        = do p' <- go_pred p
                               return (PredTy p')
 
+    go (LiteralTy n)     = return (LiteralTy n)
+
     go (FunTy arg res)   = do arg' <- go arg
                               res' <- go res
                               return (FunTy arg' res')
@@ -986,6 +988,8 @@ check_type rank ubx_tup ty@(TyConApp tc tys)
     arity_msg   = arityErr "Type synonym" (tyConName tc) tc_arity n_args
     ubx_tup_msg = ubxArgTyErr ty
 
+check_type _ _ (LiteralTy _) = return ()
+
 check_type _ _ ty = pprPanic "check_type" (ppr ty)
 
 ----------------------------------------
@@ -1581,6 +1585,7 @@ fvType (PredTy pred)       = fvPred pred
 fvType (FunTy arg res)     = fvType arg ++ fvType res
 fvType (AppTy fun arg)     = fvType fun ++ fvType arg
 fvType (ForAllTy tyvar ty) = filter (/= tyvar) (fvType ty)
+fvType (LiteralTy _)       = []
 
 fvTypes :: [Type] -> [TyVar]
 fvTypes tys                = concat (map fvType tys)
@@ -1599,6 +1604,7 @@ sizeType (PredTy pred)     = sizePred pred
 sizeType (FunTy arg res)   = sizeType arg + sizeType res + 1
 sizeType (AppTy fun arg)   = sizeType fun + sizeType arg
 sizeType (ForAllTy _ ty)   = sizeType ty
+sizeType (LiteralTy _)     = 1
 
 sizeTypes :: [Type] -> Int
 sizeTypes xs               = sum (map sizeType xs)
index 90048b7..3976849 100644 (file)
@@ -768,6 +768,7 @@ floatEqualities skols can_given wanteds
           | not (isTcTyVar tv)               = unitVarSet tv
           | FlatSkol ty <- tcTyVarDetails tv = tvs_under_fsks ty
           | otherwise                        = unitVarSet tv
+        tvs_under_fsks (LiteralTy _)    = emptyVarSet
         tvs_under_fsks (TyConApp _ tys) = unionVarSets (map tvs_under_fsks tys)
         tvs_under_fsks (PredTy sty)     = predTvs_under_fsks sty
         tvs_under_fsks (FunTy arg res)  = tvs_under_fsks arg `unionVarSet` tvs_under_fsks res
index cb4043e..6c5b941 100644 (file)
@@ -1183,6 +1183,10 @@ reifyType (TyConApp tc tys) = reify_tc_app tc tys   -- Do not expand type synony
 reifyType (AppTy t1 t2)     = do { [r1,r2] <- reifyTypes [t1,t2] ; return (r1 `TH.AppT` r2) }
 reifyType (FunTy t1 t2)     = do { [r1,r2] <- reifyTypes [t1,t2] ; return (TH.ArrowT `TH.AppT` r1 `TH.AppT` r2) }
 reifyType ty@(PredTy {})    = pprPanic "reifyType PredTy" (ppr ty)
+reifyType (LiteralTy n)     = do { l <- reifyTyLit n; return (TH.LiteralT l) }
+
+reifyTyLit :: TypeRep.TyLit -> TcM TH.TyLit
+reifyTyLit (NumberTyLit n) = return (TH.NumberTL n)
 
 reify_for_all :: TypeRep.Type -> TcM TH.Type
 reify_for_all ty
index a9ea11a..6831736 100644 (file)
@@ -357,6 +357,7 @@ tcTyConsOfType ty
      go (PredTy (IParam _ ty))     = go ty
      go (PredTy (ClassP cls tys))  = go_tc (classTyCon cls) tys
      go (ForAllTy _ ty)            = go ty
+     go (LiteralTy _)              = emptyNameEnv
      go _                          = panic "tcTyConsOfType"
 
      go_tc tc tys = extendNameEnv (go_s tys) (tyConName tc) tc
index c68c10f..fd2e378 100644 (file)
@@ -537,6 +537,7 @@ tidyType env@(_, subst) ty
     go (PredTy sty)        = PredTy (tidyPred env sty)
     go (AppTy fun arg)     = (AppTy $! (go fun)) $! (go arg)
     go (FunTy fun arg)     = (FunTy $! (go fun)) $! (go arg)
+    go (LiteralTy n)       = LiteralTy n
     go (ForAllTy tv ty)            = ForAllTy tvp $! (tidyType envp ty)
                              where
                                (envp, tvp) = tidyTyVarBndr env tv
@@ -746,8 +747,13 @@ getDFunTyKey (TyConApp tc _) = getOccName tc
 getDFunTyKey (AppTy fun _)   = getDFunTyKey fun
 getDFunTyKey (FunTy _ _)     = getOccName funTyCon
 getDFunTyKey (ForAllTy _ t)  = getDFunTyKey t
+getDFunTyKey (LiteralTy x)   = getDFunTyLitKey x
 getDFunTyKey ty                     = pprPanic "getDFunTyKey" (pprType ty)
 -- PredTy shouldn't happen
+
+getDFunTyLitKey :: TyLit -> OccName
+getDFunTyLitKey (NumberTyLit n) = mkOccName Name.varName (show n)
+
 \end{code}
 
 
@@ -1176,6 +1182,7 @@ tcTyVarsOfType (TyVarTy tv)           = if isTcTyVar tv then unitVarSet tv
 tcTyVarsOfType (TyConApp _ tys)     = tcTyVarsOfTypes tys
 tcTyVarsOfType (PredTy sty)        = tcTyVarsOfPred sty
 tcTyVarsOfType (FunTy arg res)     = tcTyVarsOfType arg `unionVarSet` tcTyVarsOfType res
+tcTyVarsOfType (LiteralTy _)        = emptyVarSet
 tcTyVarsOfType (AppTy fun arg)     = tcTyVarsOfType fun `unionVarSet` tcTyVarsOfType arg
 tcTyVarsOfType (ForAllTy tyvar ty)  = (tcTyVarsOfType ty `delVarSet` tyvar)
                                       `unionVarSet` tcTyVarsOfTyVar tyvar
@@ -1232,6 +1239,7 @@ exactTyVarsOfType ty
     go ty | Just ty' <- tcView ty = go ty'     -- This is the key line
     go (TyVarTy tv)              = unitVarSet tv
     go (TyConApp _ tys)          = exactTyVarsOfTypes tys
+    go (LiteralTy _)              = emptyVarSet
     go (PredTy ty)               = go_pred ty
     go (FunTy arg res)           = go arg `unionVarSet` go res
     go (AppTy fun arg)           = go fun `unionVarSet` go arg
@@ -1262,6 +1270,7 @@ tyClsNamesOfType (PredTy (EqPred ty1 ty2))  = tyClsNamesOfType ty1 `unionNameSet
 tyClsNamesOfType (FunTy arg res)           = tyClsNamesOfType arg `unionNameSets` tyClsNamesOfType res
 tyClsNamesOfType (AppTy fun arg)           = tyClsNamesOfType fun `unionNameSets` tyClsNamesOfType arg
 tyClsNamesOfType (ForAllTy _ ty)           = tyClsNamesOfType ty
+tyClsNamesOfType (LiteralTy _)              = emptyNameSet
 
 tyClsNamesOfTypes :: [Type] -> NameSet
 tyClsNamesOfTypes tys = foldr (unionNameSets . tyClsNamesOfType) emptyNameSet tys
index f74f1af..55657cd 100644 (file)
@@ -577,6 +577,9 @@ uType_np origin orig_ty1 orig_ty2
         -- Predicates
     go (PredTy p1) (PredTy p2) = uPred origin p1 p2
 
+    go ty1@(LiteralTy m) (LiteralTy n)
+      | m == n  = return (IdCo ty1)
+
         -- Coercion functions: (t1a ~ t1b) => t1c  ~  (t2a ~ t2b) => t2c
     go ty1 ty2 
       | Just (t1a,t1b,t1c) <- splitCoPredTy_maybe ty1, 
@@ -938,6 +941,7 @@ checkTauTvUpdate tv ty
         ok (AppTy fun arg) | Just fun' <- ok fun, Just arg' <- ok arg 
                            = Just (AppTy fun' arg') 
         ok (ForAllTy tv1 ty1) | Just ty1' <- ok ty1 = Just (ForAllTy tv1 ty1') 
+        ok t@(LiteralTy _) = Just t
         -- Fall-through 
         ok _ty = Nothing 
        
@@ -1212,6 +1216,8 @@ kindSimpleKind orig_swapped orig_kind
     go sw (FunTy k1 k2) = do { k1' <- go (not sw) k1
                              ; k2' <- go sw k2
                              ; return (mkArrowKind k1' k2') }
+    go _ k
+      | isNatKind k     = return natKind
     go True k
      | isOpenTypeKind k = return liftedTypeKind
      | isArgTypeKind k  = return liftedTypeKind
index 7ac5f63..015beff 100644 (file)
@@ -153,6 +153,7 @@ isSubOpenTypeKind :: Kind -> Bool
 isSubOpenTypeKind (FunTy k1 k2)    = ASSERT2 ( isKind k1, text "isSubOpenTypeKind" <+> ppr k1 <+> text "::" <+> ppr (typeKind k1) ) 
                                      ASSERT2 ( isKind k2, text "isSubOpenTypeKind" <+> ppr k2 <+> text "::" <+> ppr (typeKind k2) ) 
                                      False
+isSubOpenTypeKind k | isNatKind k  = False
 isSubOpenTypeKind (TyConApp kc []) = ASSERT( isKind (TyConApp kc []) ) True
 isSubOpenTypeKind other            = ASSERT( isKind other ) False
          -- This is a conservative answer
@@ -196,6 +197,7 @@ isSubKindCon kc1 kc2
   | isLiftedTypeKindCon kc1   && isLiftedTypeKindCon kc2   = True
   | isUnliftedTypeKindCon kc1 && isUnliftedTypeKindCon kc2 = True
   | isUbxTupleKindCon kc1     && isUbxTupleKindCon kc2     = True
+  | isNatKindCon kc1                                       = isNatKindCon kc2
   | isOpenTypeKindCon kc2                                  = True 
                            -- we already know kc1 is not a fun, its a TyCon
   | isArgTypeKindCon kc2      && isSubArgTypeKindCon kc1   = True
@@ -735,6 +737,7 @@ typeKind (FunTy _arg res)
     | otherwise               = ASSERT( isSubOpenTypeKind k) liftedTypeKind 
     where
       k = typeKind res
+typeKind (LiteralTy x)        = tyLitKind x
 
 ------------------
 predKind :: PredType -> Kind
@@ -742,6 +745,11 @@ predKind (EqPred {}) = coSuperKind -- A coercion kind!
 predKind (ClassP {}) = liftedTypeKind  -- Class and implicitPredicates are
 predKind (IParam {}) = liftedTypeKind  -- always represented by lifted types
 
+
+-----------------
+tyLitKind :: TyLit -> Kind
+tyLitKind (NumberTyLit _) = natKind
+
 ------------------
 -- | If it is the case that
 --
@@ -773,6 +781,8 @@ coercionKind (FunTy ty1 ty2)
         (s1, s2) = coercionKind ty2 in
     (mkFunTy t1 s1, mkFunTy t2 s2)
 
+coercionKind t@(LiteralTy _)  = (t,t)
+
 coercionKind (ForAllTy tv ty)
   | isCoVar tv
 --     c1 :: s1~s2  c2 :: t1~t2   c3 :: r1~r2
index eed3bf5..0257c89 100644 (file)
@@ -500,6 +500,7 @@ normaliseType env ty
   | Just ty' <- coreView ty = normaliseType env ty' 
 normaliseType env (TyConApp tc tys)
   = normaliseTcApp env tc tys
+normaliseType _env ty@(LiteralTy _) = (IdCo ty, ty)
 normaliseType env (AppTy ty1 ty2)
   = let (coi1,nty1) = normaliseType env ty1
         (coi2,nty2) = normaliseType env ty2
index 0fff7ab..ef19b75 100644 (file)
@@ -130,6 +130,8 @@ opt_co' env sym (TyConApp tc cos)
   | otherwise\r
   = TyConApp tc (map (opt_co env sym) cos)\r
 \r
+opt_co' _ _ co@(LiteralTy _) = co\r
+\r
 --------\r
 opt_co_tc_app :: TvSubst -> Bool -> TyCon -> CoTyConDesc -> [Coercion] -> NormalCo\r
 -- Used for CoercionTyCons only\r
@@ -450,4 +452,6 @@ isIdNormCo ty = go ty
     go (PredTy (IParam _ ty))  = go ty\r
     go (PredTy (ClassP _ tys)) = all go tys\r
     go (PredTy (EqPred t1 t2)) = go t1 && go t2\r
+    go (LiteralTy _)           = True\r
 \end{code}  \r
+\r
index 8ff78fb..ef589e2 100644 (file)
@@ -38,6 +38,8 @@ module Type (
 
         mkForAllTy, mkForAllTys, splitForAllTy_maybe, splitForAllTys, 
        applyTy, applyTys, applyTysD, isForAllTy, dropForAlls,
+
+        mkLiteralTy, mkNumberTyLit, mkNumberTy, isNumberTy,
        
        -- (Newtypes)
        newTyConInstRhs, carefullySplitNewType_maybe,
@@ -65,12 +67,14 @@ module Type (
         -- ** Common Kinds and SuperKinds
         liftedTypeKind, unliftedTypeKind, openTypeKind,
         argTypeKind, ubxTupleKind,
+        natKind,
 
         tySuperKind, coSuperKind, 
 
         -- ** Common Kind type constructors
         liftedTypeKindTyCon, openTypeKindTyCon, unliftedTypeKindTyCon,
         argTypeKindTyCon, ubxTupleKindTyCon,
+        natKindTyCon,
 
        -- * Type free variables
        tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta,
@@ -114,6 +118,7 @@ module Type (
        -- * Pretty-printing
        pprType, pprParendType, pprTypeApp, pprTyThingCategory, pprTyThing, pprForAll,
        pprPred, pprEqPred, pprTheta, pprThetaArrow, pprClassPred, pprKind, pprParendKind,
+        pprTyLit,
        
        pprSourceTyCon
     ) where
@@ -188,6 +193,7 @@ infixr 3 `mkFunTy`  -- Associates to the right
 -- (\# a, b \#)   Yes             No              No              Yes
 -- (  a, b  )   No              Yes             Yes             Yes
 -- [a]          No              Yes             Yes             Yes
+-- 42           Yes             n/a             No              No
 -- @
 
 -- $representation_types
@@ -278,6 +284,7 @@ expandTypeSynonyms ty
     go (FunTy t1 t2)   = FunTy (go t1) (go t2)
     go (ForAllTy tv t) = ForAllTy tv (go t)
     go (PredTy p)      = PredTy (go_pred p)
+    go (LiteralTy x)   = LiteralTy x
 
     go_pred (ClassP c ts)  = ClassP c (map go ts)
     go_pred (IParam ip t)  = IParam ip (go t)
@@ -420,6 +427,26 @@ splitAppTys ty = split ty ty []
 
 
 ---------------------------------------------------------------------
+                      LiteralTy
+                      ~~~~~~~~~
+
+\begin{code}
+mkLiteralTy :: TyLit -> Type
+mkLiteralTy = LiteralTy
+
+mkNumberTyLit :: Integer -> TyLit
+mkNumberTyLit = NumberTyLit
+
+mkNumberTy :: Integer -> Type
+mkNumberTy n = mkLiteralTy (mkNumberTyLit n)
+
+isNumberTy :: Type -> Maybe Integer
+isNumberTy (LiteralTy (NumberTyLit n)) = Just n
+isNumberTy _                           = Nothing
+\end{code}
+
+
+---------------------------------------------------------------------
                                FunTy
                                ~~~~~
 
@@ -834,6 +861,7 @@ tyVarsOfType (TyConApp _ tys) = tyVarsOfTypes tys
 tyVarsOfType (PredTy sty)     = tyVarsOfPred sty
 tyVarsOfType (FunTy arg res)  = tyVarsOfType arg `unionVarSet` tyVarsOfType res
 tyVarsOfType (AppTy fun arg)  = tyVarsOfType fun `unionVarSet` tyVarsOfType arg
+tyVarsOfType (LiteralTy _)    = emptyVarSet
 tyVarsOfType (ForAllTy tv ty) -- The kind of a coercion binder 
                              -- can mention type variables!
   | isTyVar tv               = inner_tvs `delVarSet` tv
@@ -874,6 +902,7 @@ tyFamInsts (FunTy ty1 ty2)      = tyFamInsts ty1 ++ tyFamInsts ty2
 tyFamInsts (AppTy ty1 ty2)      = tyFamInsts ty1 ++ tyFamInsts ty2
 tyFamInsts (ForAllTy _ ty)      = tyFamInsts ty
 tyFamInsts (PredTy pty)         = predFamInsts pty
+tyFamInsts (LiteralTy _)        = []
 
 -- | Finds type family instances occuring in a predicate type after expanding 
 -- synonyms.
@@ -902,6 +931,13 @@ isUnLiftedType :: Type -> Bool
 isUnLiftedType ty | Just ty' <- coreView ty = isUnLiftedType ty'
 isUnLiftedType (ForAllTy _ ty)   = isUnLiftedType ty
 isUnLiftedType (TyConApp tc _)   = isUnLiftedTyCon tc
+isUnLiftedType (LiteralTy _)     = False
+  -- Literal types are not really lifted (they are empty) but this
+  -- probably does not matter a lot.  We return 'False' here because
+  -- the rest of the typechecker assumes that only lifted types can be
+  -- unified with type variables (see the note at the top of this file).
+  -- This is a bit odd.
+
 isUnLiftedType _                 = False
 
 isUnboxedTupleType :: Type -> Bool
@@ -962,6 +998,7 @@ isPrimitiveType :: Type -> Bool
 -- ^ Returns true of types that are opaque to Haskell.
 -- Most of these are unlifted, but now that we interact with .NET, we
 -- may have primtive (foreign-imported) types that are lifted
+isPrimitiveType (LiteralTy _) = True
 isPrimitiveType ty = case splitTyConApp_maybe ty of
                        Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
                                              isPrimTyCon tc
@@ -983,6 +1020,7 @@ seqType (FunTy t1 t2)        = seqType t1 `seq` seqType t2
 seqType (PredTy p)       = seqPred p
 seqType (TyConApp tc tys) = tc `seq` seqTypes tys
 seqType (ForAllTy tv ty)  = tv `seq` seqType ty
+seqType (LiteralTy x)     = seqTyLit x
 
 seqTypes :: [Type] -> ()
 seqTypes []       = ()
@@ -992,6 +1030,9 @@ seqPred :: PredType -> ()
 seqPred (ClassP c tys)   = c `seq` seqTypes tys
 seqPred (IParam n ty)    = n `seq` seqType ty
 seqPred (EqPred ty1 ty2) = seqType ty1 `seq` seqType ty2
+
+seqTyLit :: TyLit -> ()
+seqTyLit (NumberTyLit x) = x `seq` ()
 \end{code}
 
 
@@ -1020,6 +1061,7 @@ coreEqType2 rn_env t1 t2
     eq env (ForAllTy tv1 t1)   (ForAllTy tv2 t2) = eq (rnBndr2 env tv1 tv2) t1 t2
     eq env (AppTy s1 t1)       (AppTy s2 t2)     = eq env s1 s2 && eq env t1 t2
     eq env (FunTy s1 t1)       (FunTy s2 t2)     = eq env s1 s2 && eq env t1 t2
+    eq _   (LiteralTy x)       (LiteralTy y)     = x == y
     eq env (TyConApp tc1 tys1) (TyConApp tc2 tys2) 
        | tc1 == tc2, all2 (eq env) tys1 tys2 = True
                        -- The lengths should be equal because
@@ -1092,6 +1134,9 @@ tcPartOfType t1 (AppTy s2 t2)   = tcPartOfType t1 s2 || tcPartOfType t1 t2
 tcPartOfType t1 (FunTy s2 t2)   = tcPartOfType t1 s2 || tcPartOfType t1 t2
 tcPartOfType t1 (PredTy p2)     = tcPartOfPred t1 p2
 tcPartOfType t1 (TyConApp _ ts) = any (tcPartOfType t1) ts
+tcPartOfType _  (LiteralTy _)   = False
+-- XXX: Is the equation for type literals correct?  What is this function for?
+-- It does not seem to be used...
 
 tcPartOfPred :: Type -> PredType -> Bool
 tcPartOfPred t1 (IParam _ t2)  = tcPartOfType t1 t2
@@ -1127,18 +1172,23 @@ cmpTypeX env (AppTy s1 t1)       (AppTy s2 t2)       = cmpTypeX env s1 s2 `thenC
 cmpTypeX env (FunTy s1 t1)       (FunTy s2 t2)       = cmpTypeX env s1 s2 `thenCmp` cmpTypeX env t1 t2
 cmpTypeX env (PredTy p1)         (PredTy p2)         = cmpPredX env p1 p2
 cmpTypeX env (TyConApp tc1 tys1) (TyConApp tc2 tys2) = (tc1 `compare` tc2) `thenCmp` cmpTypesX env tys1 tys2
+cmpTypeX _ (LiteralTy x) (LiteralTy y)               = compare x y
 
-    -- Deal with the rest: TyVarTy < AppTy < FunTy < TyConApp < ForAllTy < PredTy
+    -- Deal with the rest: TyVarTy < LiteralTy < AppTy < FunTy < TyConApp < ForAllTy < PredTy
 cmpTypeX _ (AppTy _ _)    (TyVarTy _)    = GT
+cmpTypeX _ (AppTy _ _)    (LiteralTy _)  = GT
 
 cmpTypeX _ (FunTy _ _)    (TyVarTy _)    = GT
+cmpTypeX _ (FunTy _ _)    (LiteralTy _)  = GT
 cmpTypeX _ (FunTy _ _)    (AppTy _ _)    = GT
 
 cmpTypeX _ (TyConApp _ _) (TyVarTy _)    = GT
+cmpTypeX _ (TyConApp _ _) (LiteralTy _)  = GT
 cmpTypeX _ (TyConApp _ _) (AppTy _ _)    = GT
 cmpTypeX _ (TyConApp _ _) (FunTy _ _)    = GT
 
 cmpTypeX _ (ForAllTy _ _) (TyVarTy _)    = GT
+cmpTypeX _ (ForAllTy _ _) (LiteralTy _)  = GT
 cmpTypeX _ (ForAllTy _ _) (AppTy _ _)    = GT
 cmpTypeX _ (ForAllTy _ _) (FunTy _ _)    = GT
 cmpTypeX _ (ForAllTy _ _) (TyConApp _ _) = GT
@@ -1474,6 +1524,7 @@ subst_ty subst ty
     go (ForAllTy tv ty)  = case substTyVarBndr subst tv of
                               (subst', tv') ->
                                  ForAllTy tv' $! (subst_ty subst' ty)
+    go (LiteralTy x)     = LiteralTy x
 
 substTyVar :: TvSubst -> TyVar  -> Type
 substTyVar subst@(TvSubst _ _) tv
index 8551409..3dfa8e1 100644 (file)
@@ -13,6 +13,7 @@ module TypeRep (
        TyThing(..), 
        Type(..),
        PredType(..),                   -- to friends
+        TyLit(..),                      -- to friends
        
        Kind, ThetaType,                -- Synonyms
 
@@ -22,22 +23,27 @@ module TypeRep (
        pprType, pprParendType, pprTypeApp,
        pprTyThing, pprTyThingCategory, 
        pprPred, pprEqPred, pprTheta, pprForAll, pprThetaArrow, pprClassPred,
+        pprTyLit,
 
        -- Kinds
        liftedTypeKind, unliftedTypeKind, openTypeKind,
         argTypeKind, ubxTupleKind,
+        natKind,
        isLiftedTypeKindCon, isLiftedTypeKind,
+        isNatKindCon, isNatKind,
        mkArrowKind, mkArrowKinds, isCoercionKind,
        coVarPred,
 
         -- Kind constructors...
         liftedTypeKindTyCon, openTypeKindTyCon, unliftedTypeKindTyCon,
         argTypeKindTyCon, ubxTupleKindTyCon,
+        natKindTyCon,
 
         -- And their names
         unliftedTypeKindTyConName, openTypeKindTyConName,
         ubxTupleKindTyConName, argTypeKindTyConName,
         liftedTypeKindTyConName,
+        natKindTyConName,
 
         -- Super Kinds
        tySuperKind, coSuperKind,
@@ -159,8 +165,19 @@ data Type
                        -- of a 'FunTy' (unlike the 'PredType' constructors 'ClassP' or 'IParam')
                        
                        -- See Note [PredTy], and Note [Equality predicates]
+
+  | LiteralTy TyLit     -- Type literals are simillar to type constructors.
+
   deriving (Data, Typeable)
 
+
+-- NOTE:  Other parts of the code assume that type literals do not contain
+-- other types or type variables.
+data TyLit
+  = NumberTyLit Integer
+  deriving (Eq, Ord, Data, Typeable)
+
+
 -- | The key type representing kinds in the compiler.
 -- Invariant: a kind is always in one of these forms:
 --
@@ -290,11 +307,11 @@ We define a few wired-in type constructors here to avoid module knots
 -- | See "Type#kind_subtyping" for details of the distinction between the 'Kind' 'TyCon's
 funTyCon, tySuperKindTyCon, coSuperKindTyCon, liftedTypeKindTyCon,
       openTypeKindTyCon, unliftedTypeKindTyCon,
-      ubxTupleKindTyCon, argTypeKindTyCon
+      ubxTupleKindTyCon, argTypeKindTyCon, natKindTyCon
    :: TyCon
 funTyConName, tySuperKindTyConName, coSuperKindTyConName, liftedTypeKindTyConName,
       openTypeKindTyConName, unliftedTypeKindTyConName,
-      ubxTupleKindTyConName, argTypeKindTyConName
+      ubxTupleKindTyConName, argTypeKindTyConName, natKindTyConName
    :: Name
 
 funTyCon = mkFunTyCon funTyConName (mkArrowKinds [argTypeKind, openTypeKind] liftedTypeKind)
@@ -315,6 +332,7 @@ openTypeKindTyCon     = mkKindTyCon openTypeKindTyConName     tySuperKind
 unliftedTypeKindTyCon = mkKindTyCon unliftedTypeKindTyConName tySuperKind
 ubxTupleKindTyCon     = mkKindTyCon ubxTupleKindTyConName     tySuperKind
 argTypeKindTyCon      = mkKindTyCon argTypeKindTyConName      tySuperKind
+natKindTyCon          = mkKindTyCon natKindTyConName          tySuperKind
 
 --------------------------
 -- ... and now their names
@@ -327,6 +345,7 @@ unliftedTypeKindTyConName = mkPrimTyConName (fsLit "#") unliftedTypeKindTyConKey
 ubxTupleKindTyConName     = mkPrimTyConName (fsLit "(#)") ubxTupleKindTyConKey ubxTupleKindTyCon
 argTypeKindTyConName      = mkPrimTyConName (fsLit "??") argTypeKindTyConKey argTypeKindTyCon
 funTyConName              = mkPrimTyConName (fsLit "(->)") funTyConKey funTyCon
+natKindTyConName          = mkPrimTyConName (fsLit "Nat") natKindTyConKey natKindTyCon
 
 mkPrimTyConName :: FastString -> Unique -> TyCon -> Name
 mkPrimTyConName occ key tycon = mkWiredInName gHC_PRIM (mkTcOccFS occ) 
@@ -343,13 +362,15 @@ kindTyConType :: TyCon -> Type
 kindTyConType kind = TyConApp kind []
 
 -- | See "Type#kind_subtyping" for details of the distinction between these 'Kind's
-liftedTypeKind, unliftedTypeKind, openTypeKind, argTypeKind, ubxTupleKind :: Kind
+liftedTypeKind, unliftedTypeKind, openTypeKind, argTypeKind, ubxTupleKind,
+  natKind :: Kind
 
 liftedTypeKind   = kindTyConType liftedTypeKindTyCon
 unliftedTypeKind = kindTyConType unliftedTypeKindTyCon
 openTypeKind     = kindTyConType openTypeKindTyCon
 argTypeKind      = kindTyConType argTypeKindTyCon
 ubxTupleKind    = kindTyConType ubxTupleKindTyCon
+natKind          = kindTyConType natKindTyCon
 
 -- | Given two kinds @k1@ and @k2@, creates the 'Kind' @k1 -> k2@
 mkArrowKind :: Kind -> Kind -> Kind
@@ -377,10 +398,17 @@ isCoSuperKind _                = False
 isLiftedTypeKindCon :: TyCon -> Bool
 isLiftedTypeKindCon tc    = tc `hasKey` liftedTypeKindTyConKey
 
+isNatKindCon :: TyCon -> Bool
+isNatKindCon tc           =  tc `hasKey` natKindTyConKey
+
 isLiftedTypeKind :: Kind -> Bool
 isLiftedTypeKind (TyConApp tc []) = isLiftedTypeKindCon tc
 isLiftedTypeKind _                = False
 
+isNatKind :: Kind -> Bool
+isNatKind (TyConApp tc [])        = isNatKindCon tc
+isNatKind _                       = False
+
 isCoercionKind :: Kind -> Bool
 -- All coercions are of form (ty1 ~ ty2)
 -- This function is here rather than in Coercion, 
@@ -430,6 +458,9 @@ pprTypeApp :: NamedThing a => a -> [Type] -> SDoc
 -- Print infix if the tycon/class looks like an operator
 pprTypeApp tc tys = ppr_type_app TopPrec (getName tc) tys
 
+pprTyLit :: TyLit -> SDoc
+pprTyLit = ppr_tylit TopPrec
+
 ------------------
 pprPred :: PredType -> SDoc
 pprPred (ClassP cls tys) = pprClassPred cls tys
@@ -474,6 +505,9 @@ instance Outputable Type where
 instance Outputable PredType where
     ppr = pprPred
 
+instance Outputable TyLit where
+   ppr = pprTyLit
+
 instance Outputable name => OutputableBndr (IPName name) where
     pprBndr _ n = ppr n        -- Simple for now
 
@@ -509,6 +543,12 @@ ppr_type p (FunTy ty1 ty2)
     is_pred (PredTy {}) = True
     is_pred _           = False
 
+ppr_type p (LiteralTy x) = ppr_tylit p x
+
+
+ppr_tylit :: Prec -> TyLit -> SDoc
+ppr_tylit _ (NumberTyLit n) = integer n
+
 ppr_forall_type :: Prec -> Type -> SDoc
 ppr_forall_type p ty
   = maybeParen p FunPrec $
@@ -541,6 +581,7 @@ ppr_tc_app _ tc [ty]
   | tc `hasKey` openTypeKindTyConKey     = ptext (sLit "(?)")
   | tc `hasKey` ubxTupleKindTyConKey     = ptext (sLit "(#)")
   | tc `hasKey` argTypeKindTyConKey      = ptext (sLit "??")
+  | tc `hasKey` natKindTyConKey          = ptext (sLit "Nat")
 
 ppr_tc_app p tc tys
   | isTupleTyCon tc && tyConArity tc == length tys
index 2f2cfb8..16bed45 100644 (file)
@@ -193,6 +193,8 @@ match menv subst (AppTy ty1a ty1b) ty2
        -- 'repSplit' used because the tcView stuff is done above
   = do { subst' <- match menv subst ty1a ty2a
        ; match menv subst' ty1b ty2b }
+match _menv subst (LiteralTy x) (LiteralTy y)
+  | x == y = Just subst
 
 match _ _ _ _
   = Nothing
@@ -361,6 +363,11 @@ dataConCannotMatch tys con
        | Just (f1, a1) <- repSplitAppTy_maybe ty1
        = cant_match f1 f2 || cant_match a1 a2
 
+    -- We don't add equations for FunTy, TyConApp on data/newtypes etc.
+    -- because these types have different kinds then type literal,
+    -- and so should not be compared against literals.
+    cant_match (LiteralTy x) (LiteralTy y) = x /= y
+
     cant_match _ _ = False      -- Safe!
 
 -- Things we could add;
@@ -458,6 +465,9 @@ unify subst ty1 (AppTy ty2a ty2b)
   = do { subst' <- unify subst ty1a ty2a
         ; unify subst' ty1b ty2b }
 
+unify subst (LiteralTy x) (LiteralTy y)
+  | x == y  = return subst
+
 unify _ ty1 ty2 = failWith (misMatch ty1 ty2)
        -- ForAlls??