Add support for evaluation of type-level natural numbers.

This patch implements some simple evaluation of type-level expressions
featuring natural numbers.  We can evaluate *concrete* expressions that
use the built-in type families (+), (*), (^), and (<=?), declared in
GHC.TypeLits.   We can also do some type inference involving these
functions.  For example, if we encounter a constraint such as `(2 + x) ~ 5`
we can infer that `x` must be 3.  Note, however, this is used only to
resolve unification variables (i.e., as a form of a constraint improvement)
and not to generate new facts.  This is similar to how functional
dependencies work in GHC.

The patch adds a new form of coercion, `AxiomRuleCo`, which makes use
of a new form of axiom called `CoAxiomRule`.  This is the form of evidence
generate when we solve a constraint, such as `(1 + 2) ~ 3`.

The patch also adds support for built-in type-families, by adding a new
form of TyCon rhs: `BuiltInSynFamTyCon`.  such built-in type-family
constructors contain a record with functions that are used by the
constraint solver to simplify and improve constraints involving the
built-in function (see `TcInteract`).  The record in defined in `FamInst`.

The type constructors and rules for evaluating the type-level functions
are in a new module called `TcTypeNats`.

29 files changed, 887 insertions, 27 deletions

diff --git a/compiler/coreSyn/CoreLint.lhs b/compiler/coreSyn/CoreLint.lhs
index ffddd78516..9a9860f0fa 100644
--- a/compiler/coreSyn/CoreLint.lhs
+++ b/compiler/coreSyn/CoreLint.lhs
@@ -54,6 +54,7 @@ import OptCoercion ( checkAxInstCo )
 import Control.Monad
 import MonadUtils
 import Data.Maybe
+import Pair
 \end{code}
 
 Note [GHC Formalism]
@@ -987,6 +988,53 @@ lintCoercion co@(SubCo co')
   = do { (k,s,t,r) <- lintCoercion co'
        ; checkRole co Nominal r
        ; return (k,s,t,Representational) }
+
+
+lintCoercion this@(AxiomRuleCo co ts cs)
+  = do _ks <- mapM lintType ts
+       eqs <- mapM lintCoercion cs
+
+       let tyNum = length ts
+
+       case compare (coaxrTypeArity co) tyNum of
+         EQ -> return ()
+         LT -> err "Too many type arguments"
+                    [ txt "expected" <+> int (coaxrTypeArity co)
+                    , txt "provided" <+> int tyNum ]
+         GT -> err "Not enough type arguments"
+                    [ txt "expected" <+> int (coaxrTypeArity co)
+                          , txt "provided" <+> int tyNum ]
+       checkRoles 0 (coaxrAsmpRoles co) eqs
+
+       case coaxrProves co ts [ Pair l r | (_,l,r,_) <- eqs ] of
+         Nothing -> err "Malformed use of AxiomRuleCo" [ ppr this ]
+         Just (Pair l r) ->
+           do kL <- lintType l
+              kR <- lintType r
+              unless (eqKind kL kR)
+                $ err "Kind error in CoAxiomRule"
+                       [ppr kL <+> txt "/=" <+> ppr kR]
+              return (kL, l, r, coaxrRole co)
+  where
+  txt       = ptext . sLit
+  err m xs  = failWithL $
+                hang (txt m) 2 $ vcat (txt "Rule:" <+> ppr (coaxrName co) : xs)
+
+  checkRoles n (e : es) ((_,_,_,r) : rs)
+    | e == r    = checkRoles (n+1) es rs
+    | otherwise = err "Argument roles mismatch"
+                      [ txt "In argument:" <+> int (n+1)
+                      , txt "Expected:" <+> ppr e
+                      , txt "Found:" <+> ppr r ]
+  checkRoles _ [] []  = return ()
+  checkRoles n [] rs  = err "Too many coercion arguments"
+                          [ txt "Expected:" <+> int n
+                          , txt "Provided:" <+> int (n + length rs) ]
+
+  checkRoles n es []  = err "Not enough coercion arguments"
+                          [ txt "Expected:" <+> int (n + length es)
+                          , txt "Provided:" <+> int n ]
+
 \end{code}
 
 %************************************************************************
diff --git a/compiler/coreSyn/MkExternalCore.lhs b/compiler/coreSyn/MkExternalCore.lhs
index bdb54d80d6..6a6f0551ed 100644
--- a/compiler/coreSyn/MkExternalCore.lhs
+++ b/compiler/coreSyn/MkExternalCore.lhs
@@ -332,6 +332,8 @@ make_co dflags (NthCo d co)          = C.NthCoercion d (make_co dflags co)
 make_co dflags (LRCo lr co)          = C.LRCoercion (make_lr lr) (make_co dflags co)
 make_co dflags (InstCo co ty)        = C.InstCoercion (make_co dflags co) (make_ty dflags ty)
 make_co dflags (SubCo co)            = C.SubCoercion (make_co dflags co)
+make_co _ (AxiomRuleCo {})           = panic "make_co AxiomRuleCo: not yet implemented"
+
 
 make_lr :: LeftOrRight -> C.LeftOrRight
 make_lr CLeft  = C.CLeft
diff --git a/compiler/coreSyn/TrieMap.lhs b/compiler/coreSyn/TrieMap.lhs
index f8ad8da5f4..255ab899d7 100644
--- a/compiler/coreSyn/TrieMap.lhs
+++ b/compiler/coreSyn/TrieMap.lhs
@@ -18,7 +18,8 @@ module TrieMap(
    CoercionMap, 
    MaybeMap, 
    ListMap,
-   TrieMap(..)
+   TrieMap(..),
+   lookupTypeMapTyCon
  ) where
 
 import CoreSyn
@@ -27,10 +28,12 @@ import Literal
 import Name
 import Type
 import TypeRep
+import TyCon(TyCon)
 import Var
 import UniqFM
 import Unique( Unique )
 import FastString(FastString)
+import CoAxiom(CoAxiomRule(coaxrName))
 
 import qualified Data.Map    as Map
 import qualified Data.IntMap as IntMap
@@ -471,7 +474,10 @@ data CoercionMap a
        , km_left   :: CoercionMap a
        , km_right  :: CoercionMap a
        , km_inst   :: CoercionMap (TypeMap a) 
-       , km_sub    :: CoercionMap a }
+       , km_sub    :: CoercionMap a
+       , km_axiom_rule :: Map.Map FastString
+                                  (ListMap TypeMap (ListMap CoercionMap a))
+       }
 
 wrapEmptyKM :: CoercionMap a
 wrapEmptyKM = KM { km_refl = emptyTM, km_tc_app = emptyTM
@@ -479,7 +485,8 @@ wrapEmptyKM = KM { km_refl = emptyTM, km_tc_app = emptyTM
                  , km_var = emptyTM, km_axiom = emptyNameEnv
                  , km_univ = emptyTM, km_sym = emptyTM, km_trans = emptyTM
                  , km_nth = emptyTM, km_left = emptyTM, km_right = emptyTM
-                 , km_inst = emptyTM, km_sub = emptyTM }
+                 , km_inst = emptyTM, km_sub = emptyTM 
+                 , km_axiom_rule = emptyTM }
 
 instance TrieMap CoercionMap where
    type Key CoercionMap = Coercion
@@ -496,7 +503,8 @@ mapC f (KM { km_refl = krefl, km_tc_app = ktc
            , km_var = kvar, km_axiom = kax
            , km_univ   = kuniv  , km_sym = ksym, km_trans = ktrans
            , km_nth = knth, km_left = kml, km_right = kmr
-           , km_inst = kinst, km_sub = ksub })
+           , km_inst = kinst, km_sub = ksub
+           , km_axiom_rule = kaxr })
   = KM { km_refl   = mapTM (mapTM f) krefl
        , km_tc_app = mapTM (mapNameEnv (mapTM f)) ktc
        , km_app    = mapTM (mapTM f) kapp
@@ -510,7 +518,9 @@ mapC f (KM { km_refl = krefl, km_tc_app = ktc
        , km_left   = mapTM f kml
        , km_right  = mapTM f kmr
        , km_inst   = mapTM (mapTM f) kinst
-       , km_sub    = mapTM f ksub }
+       , km_sub    = mapTM f ksub
+       , km_axiom_rule = mapTM (mapTM (mapTM f)) kaxr
+       }
 
 lkC :: CmEnv -> Coercion -> CoercionMap a -> Maybe a
 lkC env co m 
@@ -531,6 +541,11 @@ lkC env co m
     go (LRCo CLeft  c)         = km_left   >.> lkC env c
     go (LRCo CRight c)         = km_right  >.> lkC env c
     go (SubCo c)               = km_sub    >.> lkC env c
+    go (AxiomRuleCo co ts cs)  = km_axiom_rule >.>
+                                    lookupTM (coaxrName co) >=>
+                                    lkList (lkT env) ts >=>
+                                    lkList (lkC env) cs
+
 
 xtC :: CmEnv -> Coercion -> XT a -> CoercionMap a -> CoercionMap a
 xtC env co f EmptyKM = xtC env co f wrapEmptyKM
@@ -549,6 +564,10 @@ xtC env (NthCo n c)             f m = m { km_nth    = km_nth m |> xtInt n |>> xt
 xtC env (LRCo CLeft  c)         f m = m { km_left   = km_left  m |> xtC env c f } 
 xtC env (LRCo CRight c)         f m = m { km_right  = km_right m |> xtC env c f }
 xtC env (SubCo c)               f m = m { km_sub    = km_sub m |> xtC env c f } 
+xtC env (AxiomRuleCo co ts cs)  f m = m { km_axiom_rule = km_axiom_rule m
+                                                        |>  alterTM (coaxrName co)
+                                                        |>> xtList (xtT env) ts
+                                                        |>> xtList (xtC env) cs f}
 
 fdC :: (a -> b -> b) -> CoercionMap a -> b -> b
 fdC _ EmptyKM = \z -> z
@@ -566,6 +585,7 @@ fdC k m = foldTM (foldTM k) (km_refl m)
         . foldTM k          (km_right m)
         . foldTM (foldTM k) (km_inst m)
         . foldTM k          (km_sub m)
+        . foldTM (foldTM (foldTM k)) (km_axiom_rule m)
 
 \end{code}
 
@@ -630,6 +650,15 @@ emptyTypeMap = EmptyTM
 lookupTypeMap :: TypeMap a -> Type -> Maybe a
 lookupTypeMap cm t = lkT emptyCME t cm
 
+-- Returns the type map entries that have keys starting with the given tycon.
+-- This only considers saturated applications (i.e. TyConApp ones).
+lookupTypeMapTyCon :: TypeMap a -> TyCon -> [a]
+lookupTypeMapTyCon EmptyTM _ = []
+lookupTypeMapTyCon TM { tm_tc_app = cs } tc =
+  case lookupUFM cs tc of
+    Nothing -> []
+    Just xs -> foldTM (:) xs []
+
 extendTypeMap :: TypeMap a -> Type -> a -> TypeMap a
 extendTypeMap m t v = xtT emptyCME t (\_ -> Just v) m
 
diff --git a/compiler/deSugar/DsBinds.lhs b/compiler/deSugar/DsBinds.lhs
index 617516bd97..a1f5e77b5f 100644
--- a/compiler/deSugar/DsBinds.lhs
+++ b/compiler/deSugar/DsBinds.lhs
@@ -847,6 +847,11 @@ ds_tc_coercion subst role tc_co
     go r (TcCastCo co1 co2)     = maybeSubCo r $ mkCoCast (go Nominal co1)
                                                           (go Nominal co2)
     go r (TcCoVarCo v)          = maybeSubCo r $ ds_ev_id subst v
+    go _ (TcAxiomRuleCo co ts cs) = AxiomRuleCo co
+                                      (map (Coercion.substTy subst) ts)
+                                      (map (go Nominal) cs)
+
+
 
     ds_co_binds :: TcEvBinds -> CvSubst
     ds_co_binds (EvBinds bs)      = foldl ds_scc subst (sccEvBinds bs)
diff --git a/compiler/ghc.cabal.in b/compiler/ghc.cabal.in
index bfcbb87eb9..553d27d2ba 100644
--- a/compiler/ghc.cabal.in
+++ b/compiler/ghc.cabal.in
@@ -383,6 +383,7 @@ Library
         TcInteract
         TcCanonical
         TcSMonad
+        TcTypeNats
         Class
         Coercion
         FamInstEnv
diff --git a/compiler/ghc.mk b/compiler/ghc.mk
index a7b7294916..66548b67da 100644
--- a/compiler/ghc.mk
+++ b/compiler/ghc.mk
@@ -445,7 +445,8 @@ compiler_stage3_SplitObjs = NO
 # We therefore need to split some of the modules off into a separate
 # DLL. This clump are the modules reachable from DynFlags:
 compiler_stage2_dll0_START_MODULE = DynFlags
-compiler_stage2_dll0_MODULES = Annotations Avail Bag BasicTypes Binary Bitmap BlockId BreakArray BufWrite ByteCodeAsm ByteCodeInstr ByteCodeItbls ByteCodeLink CLabel Class CmdLineParser Cmm CmmCallConv CmmExpr CmmInfo CmmMachOp CmmNode CmmType CmmUtils CoAxiom CodeGen.Platform CodeGen.Platform.ARM CodeGen.Platform.NoRegs CodeGen.Platform.PPC CodeGen.Platform.PPC_Darwin CodeGen.Platform.SPARC CodeGen.Platform.X86 CodeGen.Platform.X86_64 Coercion Config Constants CoreArity CoreFVs CoreSubst CoreSyn CoreTidy CoreUnfold CoreUtils CostCentre DataCon Demand Digraph DriverPhases DynFlags Encoding ErrUtils Exception FamInstEnv FastBool FastFunctions FastMutInt FastString FastTypes Fingerprint FiniteMap ForeignCall Hoopl Hoopl.Dataflow HsBinds HsDecls HsDoc HsExpr HsImpExp HsLit HsPat HsSyn HsTypes HsUtils HscTypes Id IdInfo IfaceSyn IfaceType InstEnv InteractiveEvalTypes Kind ListSetOps Literal Maybes MkCore MkGraph MkId Module MonadUtils Name NameEnv NameSet ObjLink OccName OccurAnal OptCoercion OrdList Outputable PackageConfig Packages Pair Panic Platform PlatformConstants PprCmm PprCmmDecl PprCmmExpr PprCore PrelNames PrelRules Pretty PrimOp RdrName Reg RegClass Rules SMRep Serialized SrcLoc StaticFlags StgCmmArgRep StgCmmClosure StgCmmEnv StgCmmLayout StgCmmMonad StgCmmProf StgCmmTicky StgCmmUtils StgSyn Stream StringBuffer TcEvidence TcType TrieMap TyCon Type TypeRep TysPrim TysWiredIn Unify UniqFM UniqSet UniqSupply Unique Util Var VarEnv VarSet
+
+compiler_stage2_dll0_MODULES =Annotations Avail Bag BasicTypes BinIface Binary Bitmap BlockId BreakArray BufWrite BuildTyCl ByteCodeAsm ByteCodeInstr ByteCodeItbls ByteCodeLink CLabel Class CmdLineParser Cmm CmmCallConv CmmExpr CmmInfo CmmMachOp CmmNode CmmType CmmUtils CoAxiom CodeGen.Platform CodeGen.Platform.ARM CodeGen.Platform.NoRegs CodeGen.Platform.PPC CodeGen.Platform.PPC_Darwin CodeGen.Platform.SPARC CodeGen.Platform.X86 CodeGen.Platform.X86_64 Coercion Config Constants CoreArity CoreFVs CoreLint CoreSubst CoreSyn CoreTidy CoreUnfold CoreUtils CostCentre DataCon Demand Digraph DriverPhases DynFlags Encoding ErrUtils Exception FamInst FamInstEnv FastBool FastFunctions FastMutInt FastString FastTypes Finder Fingerprint FiniteMap ForeignCall Hoopl Hoopl.Dataflow HsBinds HsDecls HsDoc HsExpr HsImpExp HsLit HsPat HsSyn HsTypes HsUtils HscTypes IOEnv Id IdInfo IfaceEnv IfaceSyn IfaceType InstEnv InteractiveEvalTypes Kind ListSetOps Literal LoadIface Maybes MkCore MkGraph MkId Module MonadUtils Name NameEnv NameSet ObjLink OccName OccurAnal OptCoercion OrdList Outputable PackageConfig Packages Pair Panic Platform PlatformConstants PprCmm PprCmmDecl PprCmmExpr PprCore PrelInfo PrelNames PrelRules Pretty PrimOp RdrName Reg RegClass Rules SMRep Serialized SrcLoc StaticFlags StgCmmArgRep StgCmmClosure StgCmmEnv StgCmmLayout StgCmmMonad StgCmmProf StgCmmTicky StgCmmUtils StgSyn Stream StringBuffer TcEvidence TcIface TcMType TcRnMonad TcRnTypes TcType TcTypeNats TrieMap TyCon Type TypeRep TysPrim TysWiredIn Unify UniqFM UniqSet UniqSupply Unique Util Var VarEnv VarSet
 
 compiler_stage2_dll0_HS_OBJS = \
     $(patsubst %,compiler/stage2/build/%.$(dyn_osuf),$(subst .,/,$(compiler_stage2_dll0_MODULES)))
diff --git a/compiler/iface/IfaceSyn.lhs b/compiler/iface/IfaceSyn.lhs
index f6e68e2836..e162cc3a80 100644
--- a/compiler/iface/IfaceSyn.lhs
+++ b/compiler/iface/IfaceSyn.lhs
@@ -1404,6 +1404,10 @@ freeNamesIfCoercion (IfaceInstCo co ty)
   = freeNamesIfCoercion co &&& freeNamesIfType ty
 freeNamesIfCoercion (IfaceSubCo co)
   = freeNamesIfCoercion co
+freeNamesIfCoercion (IfaceAxiomRuleCo _ax tys cos)
+  -- the axiom is just a string, so we don't count it as a name.
+  = fnList freeNamesIfType tys &&&
+    fnList freeNamesIfCoercion cos
 
 freeNamesIfTvBndrs :: [IfaceTvBndr] -> NameSet
 freeNamesIfTvBndrs = fnList freeNamesIfTvBndr
diff --git a/compiler/iface/IfaceType.lhs b/compiler/iface/IfaceType.lhs
index b9d6a445cf..fc05aa5283 100644
--- a/compiler/iface/IfaceType.lhs
+++ b/compiler/iface/IfaceType.lhs
@@ -106,6 +106,7 @@ data IfaceCoercion
   | IfaceLRCo        LeftOrRight IfaceCoercion
   | IfaceInstCo      IfaceCoercion IfaceType
   | IfaceSubCo       IfaceCoercion
+  | IfaceAxiomRuleCo IfLclName [IfaceType] [IfaceCoercion]
 \end{code}
 
 %************************************************************************
@@ -334,6 +335,10 @@ ppr_co ctxt_prec (IfaceInstCo co ty)
   = maybeParen ctxt_prec tYCON_PREC $
     ptext (sLit "Inst") <+> pprParendIfaceCoercion co <+> pprParendIfaceType ty
 
+ppr_co ctxt_prec (IfaceAxiomRuleCo tc tys cos)
+  = maybeParen ctxt_prec tYCON_PREC
+               (sep [ppr tc, nest 4 (sep (map pprParendIfaceType tys ++ map pprParendIfaceCoercion cos))])
+
 ppr_co ctxt_prec co
   = ppr_special_co ctxt_prec doc cos
   where (doc, cos) = case co of
@@ -493,7 +498,12 @@ instance Binary IfaceCoercion where
   put_ bh (IfaceSubCo a) = do
           putByte bh 14
           put_ bh a
-  
+  put_ bh (IfaceAxiomRuleCo a b c) = do
+          putByte bh 15
+          put_ bh a
+          put_ bh b
+          put_ bh c
+
   get bh = do
       tag <- getByte bh
       case tag of
@@ -540,6 +550,10 @@ instance Binary IfaceCoercion where
                    return $ IfaceInstCo a b
            14-> do a <- get bh
                    return $ IfaceSubCo a
+           15-> do a <- get bh
+                   b <- get bh
+                   c <- get bh
+                   return $ IfaceAxiomRuleCo a b c
            _ -> panic ("get IfaceCoercion " ++ show tag)             
 
 \end{code}
@@ -629,5 +643,9 @@ toIfaceCoercion (InstCo co ty)      = IfaceInstCo (toIfaceCoercion co)
                                                   (toIfaceType ty)
 toIfaceCoercion (SubCo co)          = IfaceSubCo (toIfaceCoercion co)
 
+toIfaceCoercion (AxiomRuleCo co ts cs) = IfaceAxiomRuleCo
+                                          (coaxrName co)
+                                          (map toIfaceType ts)
+                                          (map toIfaceCoercion cs)
 \end{code}
 
diff --git a/compiler/iface/MkIface.lhs b/compiler/iface/MkIface.lhs
index 44f99d520e..80b83f197e 100644
--- a/compiler/iface/MkIface.lhs
+++ b/compiler/iface/MkIface.lhs
@@ -1526,6 +1526,9 @@ tyConToIfaceDecl env tycon
     to_ifsyn_rhs (SynonymTyCon ty)
       = IfaceSynonymTyCon (tidyToIfaceType env1 ty)
 
+    to_ifsyn_rhs (BuiltInSynFamTyCon {}) = pprPanic "toIfaceDecl: BuiltInFamTyCon" (ppr tycon)
+
+
     ifaceConDecls (NewTyCon { data_con = con })     = IfNewTyCon  (ifaceConDecl con)
     ifaceConDecls (DataTyCon { data_cons = cons })  = IfDataTyCon (map ifaceConDecl cons)
     ifaceConDecls (DataFamilyTyCon {})              = IfDataFamTyCon
diff --git a/compiler/iface/TcIface.lhs b/compiler/iface/TcIface.lhs
index 2d2e867390..38043c6454 100644
--- a/compiler/iface/TcIface.lhs
+++ b/compiler/iface/TcIface.lhs
@@ -17,6 +17,7 @@ module TcIface (
 
 #include "HsVersions.h"
 
+import TcTypeNats(typeNatCoAxiomRules)
 import IfaceSyn
 import LoadIface
 import IfaceEnv
@@ -67,6 +68,7 @@ import Util
 import FastString
 
 import Control.Monad
+import qualified Data.Map as Map
 \end{code}
 
 This module takes
@@ -1013,9 +1015,19 @@ tcIfaceCo (IfaceInstCo c1 t2)       = InstCo   <$> tcIfaceCo c1
 tcIfaceCo (IfaceNthCo d c)          = NthCo d  <$> tcIfaceCo c
 tcIfaceCo (IfaceLRCo lr c)          = LRCo lr  <$> tcIfaceCo c
 tcIfaceCo (IfaceSubCo c)            = SubCo    <$> tcIfaceCo c
+tcIfaceCo (IfaceAxiomRuleCo ax tys cos) = AxiomRuleCo
+                                            <$> tcIfaceCoAxiomRule ax
+                                            <*> mapM tcIfaceType tys
+                                            <*> mapM tcIfaceCo cos
 
 tcIfaceCoVar :: FastString -> IfL CoVar
 tcIfaceCoVar = tcIfaceLclId
+
+tcIfaceCoAxiomRule :: FastString -> IfL CoAxiomRule
+tcIfaceCoAxiomRule n =
+  case Map.lookup n typeNatCoAxiomRules of
+    Just ax -> return ax
+    _  -> pprPanic "tcIfaceCoAxiomRule" (ppr n)
 \end{code}
 
 
diff --git a/compiler/main/PprTyThing.hs b/compiler/main/PprTyThing.hs
index b95c69902a..98f2c50ae5 100644
--- a/compiler/main/PprTyThing.hs
+++ b/compiler/main/PprTyThing.hs
@@ -184,6 +184,9 @@ pprTyCon pefas ss tyCon
       AbstractClosedSynFamilyTyCon -> closed_family_header <+> ptext (sLit "..")
       SynonymTyCon rhs_ty -> hang (pprTyConHdr pefas tyCon <+> equals) 
                                      2 (ppr rhs_ty)   -- Don't suppress foralls on RHS type!
+      BuiltInSynFamTyCon {} -> pprTyConHdr pefas tyCon <+> dcolon <+> 
+                             pprTypeForUser pefas (GHC.synTyConResKind tyCon)
+
                                                  -- e.g. type T = forall a. a->a
   | Just cls <- GHC.tyConClass_maybe tyCon
   = pprClass pefas ss cls
diff --git a/compiler/prelude/PrelInfo.lhs b/compiler/prelude/PrelInfo.lhs
index bb3e54ada2..4a39977797 100644
--- a/compiler/prelude/PrelInfo.lhs
+++ b/compiler/prelude/PrelInfo.lhs
@@ -42,6 +42,7 @@ import HscTypes
 import Class
 import TyCon
 import Util
+import {-# SOURCE #-} TcTypeNats ( typeNatTyCons )
 
 import Data.Array
 \end{code}
@@ -89,7 +90,8 @@ wiredInThings
 	, map (AnId . primOpId) allThePrimOps
     ]
   where
-    tycon_things = map ATyCon ([funTyCon] ++ primTyCons ++ wiredInTyCons)
+    tycon_things = map ATyCon ([funTyCon] ++ primTyCons ++ wiredInTyCons
+                                    ++ typeNatTyCons)
 \end{code}
 
 We let a lot of "non-standard" values be visible, so that we can make
diff --git a/compiler/prelude/PrelNames.lhs b/compiler/prelude/PrelNames.lhs
index b428f6e375..acac400c04 100644
--- a/compiler/prelude/PrelNames.lhs
+++ b/compiler/prelude/PrelNames.lhs
@@ -295,10 +295,6 @@ basicKnownKeyNames
 
         -- Type-level naturals
         singIClassName,
-        typeNatLeqClassName,
-        typeNatAddTyFamName,
-        typeNatMulTyFamName,
-        typeNatExpTyFamName,
 
         -- Implicit parameters
         ipClassName,
@@ -1144,13 +1140,8 @@ randomGenClassName  = clsQual rANDOM (fsLit "RandomGen") randomGenClassKey
 isStringClassName   = clsQual dATA_STRING (fsLit "IsString") isStringClassKey
 
 -- Type-level naturals
-singIClassName, typeNatLeqClassName,
-  typeNatAddTyFamName, typeNatMulTyFamName, typeNatExpTyFamName :: Name
+singIClassName :: Name
 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
-typeNatExpTyFamName = tcQual  gHC_TYPELITS (fsLit "^")   typeNatExpTyFamNameKey
 
 -- Implicit parameters
 ipClassName :: Name
@@ -1273,9 +1264,8 @@ constructorClassKey = mkPreludeClassUnique 40
 selectorClassKey    = mkPreludeClassUnique 41
 
 -- SingI: see Note [SingI and EvLit] in TcEvidence
-singIClassNameKey, typeNatLeqClassNameKey :: Unique
+singIClassNameKey :: Unique
 singIClassNameKey       = mkPreludeClassUnique 42
-typeNatLeqClassNameKey  = mkPreludeClassUnique 43
 
 ghciIoClassKey :: Unique
 ghciIoClassKey = mkPreludeClassUnique 44
@@ -1477,13 +1467,15 @@ rep1TyConKey = mkPreludeTyConUnique 156
 
 -- Type-level naturals
 typeNatKindConNameKey, typeSymbolKindConNameKey,
-  typeNatAddTyFamNameKey, typeNatMulTyFamNameKey, typeNatExpTyFamNameKey
+  typeNatAddTyFamNameKey, typeNatMulTyFamNameKey, typeNatExpTyFamNameKey,
+  typeNatLeqTyFamNameKey
   :: Unique
 typeNatKindConNameKey     = mkPreludeTyConUnique 160
 typeSymbolKindConNameKey  = mkPreludeTyConUnique 161
 typeNatAddTyFamNameKey    = mkPreludeTyConUnique 162
 typeNatMulTyFamNameKey    = mkPreludeTyConUnique 163
 typeNatExpTyFamNameKey    = mkPreludeTyConUnique 164
+typeNatLeqTyFamNameKey    = mkPreludeTyConUnique 165
 
 -- SIMD vector types (Unique keys)
 floatX4PrimTyConKey, doubleX2PrimTyConKey, int32X4PrimTyConKey,
diff --git a/compiler/prelude/TysWiredIn.lhs b/compiler/prelude/TysWiredIn.lhs
index b563b25cc4..d8c880f1c3 100644
--- a/compiler/prelude/TysWiredIn.lhs
+++ b/compiler/prelude/TysWiredIn.lhs
@@ -14,6 +14,7 @@ module TysWiredIn (
         boolTy, boolTyCon, boolTyCon_RDR, boolTyConName,
         trueDataCon,  trueDataConId,  true_RDR,
         falseDataCon, falseDataConId, false_RDR,
+        promotedBoolTyCon, promotedFalseDataCon, promotedTrueDataCon,
 
         -- * Ordering
         ltDataCon, ltDataConId,
@@ -68,6 +69,8 @@ module TysWiredIn (
         -- * Equality predicates
         eqTyCon_RDR, eqTyCon, eqTyConName, eqBoxDataCon,
 
+        mkWiredInTyConName -- This is used in TcTypeNats to define the
+                           -- built-in functions for evaluation.
     ) where
 
 #include "HsVersions.h"
@@ -782,3 +785,15 @@ mkPArrFakeCon arity  = data_con
 isPArrFakeCon      :: DataCon -> Bool
 isPArrFakeCon dcon  = dcon == parrFakeCon (dataConSourceArity dcon)
 \end{code}
+
+Promoted Booleans
+
+\begin{code}
+promotedBoolTyCon, promotedFalseDataCon, promotedTrueDataCon :: TyCon
+promotedBoolTyCon     = promoteTyCon boolTyCon
+promotedTrueDataCon   = promoteDataCon trueDataCon
+promotedFalseDataCon  = promoteDataCon falseDataCon
+\end{code}
+
+
+
diff --git a/compiler/typecheck/FamInst.lhs b/compiler/typecheck/FamInst.lhs
index 3ca28ef203..b0cc8b2a5a 100644
--- a/compiler/typecheck/FamInst.lhs
+++ b/compiler/typecheck/FamInst.lhs
@@ -13,9 +13,11 @@ module FamInst (
         checkFamInstConsistency, tcExtendLocalFamInstEnv,
 	tcLookupFamInst, 
         tcGetFamInstEnvs,
-        newFamInst
+        newFamInst,
+        TcBuiltInSynFamily(..), trivialBuiltInFamily
     ) where
 
+import Pair(Pair)
 import HscTypes
 import FamInstEnv
 import InstEnv( roughMatchTcs )
@@ -39,6 +41,7 @@ import VarSet
 import Control.Monad
 import Data.Map (Map)
 import qualified Data.Map as Map
+import TcEvidence(TcCoercion)
 
 #include "HsVersions.h"
 \end{code}
@@ -331,3 +334,26 @@ tcGetFamInstEnvs
   = do { eps <- getEps; env <- getGblEnv
        ; return (eps_fam_inst_env eps, tcg_fam_inst_env env) }
 \end{code}
+
+
+Type checking of built-in families
+==================================
+
+\begin{code}
+data TcBuiltInSynFamily = TcBuiltInSynFamily
+  { sfMatchFam      :: [Type] -> Maybe (TcCoercion, TcType)
+  , sfInteractTop   :: [Type] -> Type -> [Pair TcType]
+  , sfInteractInert :: [Type] -> Type ->
+                       [Type] -> Type -> [Pair TcType]
+  }
+
+-- Provides default implementations that do nothing.
+trivialBuiltInFamily :: TcBuiltInSynFamily
+trivialBuiltInFamily = TcBuiltInSynFamily
+  { sfMatchFam      = \_ -> Nothing
+  , sfInteractTop   = \_ _ -> []
+  , sfInteractInert = \_ _ _ _ -> []
+  }
+\end{code}
+
+
diff --git a/compiler/typecheck/FamInst.lhs-boot b/compiler/typecheck/FamInst.lhs-boot
new file mode 100644
index 0000000000..6e4bd1d185
--- /dev/null
+++ b/compiler/typecheck/FamInst.lhs-boot
@@ -0,0 +1,5 @@
+\begin{code}
+module FamInst where
+
+data TcBuiltInSynFamily
+\end{code}
diff --git a/compiler/typecheck/TcEvidence.lhs b/compiler/typecheck/TcEvidence.lhs
index a18dc21438..ffdce640fd 100644
--- a/compiler/typecheck/TcEvidence.lhs
+++ b/compiler/typecheck/TcEvidence.lhs
@@ -22,6 +22,7 @@ module TcEvidence (
   mkTcReflCo, mkTcTyConAppCo, mkTcAppCo, mkTcAppCos, mkTcFunCo,
   mkTcAxInstCo, mkTcUnbranchedAxInstCo, mkTcForAllCo, mkTcForAllCos, 
   mkTcSymCo, mkTcTransCo, mkTcNthCo, mkTcLRCo, mkTcInstCos,
+  mkTcAxiomRuleCo,
   tcCoercionKind, coVarsOfTcCo, isEqVar, mkTcCoVarCo, 
   isTcReflCo, isTcReflCo_maybe, getTcCoVar_maybe,
   liftTcCoSubstWith
@@ -105,6 +106,9 @@ data TcCoercion
   | TcCoVarCo EqVar               -- variable always at role N
   | TcAxiomInstCo (CoAxiom Branched) Int [TcType] -- Int specifies branch number
                                                   -- See [CoAxiom Index] in Coercion.lhs
+  -- This is number of types and coercions are expected to macth to CoAxiomRule
+  -- (i.e., the CoAxiomRules are always fully saturated)
+  | TcAxiomRuleCo CoAxiomRule [TcType] [TcCoercion]
   | TcSymCo TcCoercion
   | TcTransCo TcCoercion TcCoercion
   | TcNthCo Int TcCoercion
@@ -156,6 +160,9 @@ mkTcAxInstCo ax ind tys
     arity = coAxiomArity ax ind
     ax_br = toBranchedAxiom ax
 
+mkTcAxiomRuleCo :: CoAxiomRule -> [TcType] -> [TcCoercion] -> TcCoercion
+mkTcAxiomRuleCo = TcAxiomRuleCo
+
 mkTcUnbranchedAxInstCo :: CoAxiom Unbranched -> [TcType] -> TcCoercion
 mkTcUnbranchedAxInstCo ax tys
   = mkTcAxInstCo ax 0 tys
@@ -231,6 +238,10 @@ tcCoercionKind co = go co
     go (TcTransCo co1 co2)    = Pair (pFst (go co1)) (pSnd (go co2))
     go (TcNthCo d co)         = tyConAppArgN d <$> go co
     go (TcLRCo lr co)         = (pickLR lr . tcSplitAppTy) <$> go co
+    go (TcAxiomRuleCo ax ts cs) =
+       case coaxrProves ax ts (map tcCoercionKind cs) of
+         Just res -> res
+         Nothing -> panic "tcCoercionKind: malformed TcAxiomRuleCo"
 
     -- c.f. Coercion.coercionKind
     go_inst (TcInstCo co ty) tys = go_inst co (ty:tys)
@@ -264,6 +275,8 @@ coVarsOfTcCo tc_co
                                    `minusVarSet` get_bndrs bs
     go (TcLetCo {}) = emptyVarSet    -- Harumph. This does legitimately happen in the call
                                      -- to evVarsOfTerm in the DEBUG check of setEvBind
+    go (TcAxiomRuleCo _ _ cos)   = foldr (unionVarSet . go) emptyVarSet cos
+
 
     -- We expect only coercion bindings, so use evTermCoercion 
     go_bind :: EvBind -> VarSet
@@ -330,6 +343,25 @@ ppr_co p (TcTransCo co1 co2) = maybeParen p FunPrec $
 ppr_co p (TcSymCo co)         = pprPrefixApp p (ptext (sLit "Sym")) [pprParendTcCo co]
 ppr_co p (TcNthCo n co)       = pprPrefixApp p (ptext (sLit "Nth:") <+> int n) [pprParendTcCo co]
 ppr_co p (TcLRCo lr co)       = pprPrefixApp p (ppr lr) [pprParendTcCo co]
+ppr_co p (TcAxiomRuleCo co ts ps) = maybeParen p TopPrec
+                                  $ ppr_tc_axiom_rule_co co ts ps
+
+ppr_tc_axiom_rule_co :: CoAxiomRule -> [TcType] -> [TcCoercion] -> SDoc
+ppr_tc_axiom_rule_co co ts ps = ppr (coaxrName co) <> ppTs ts $$ nest 2 (ppPs ps)
+  where
+  ppTs []   = Outputable.empty
+  ppTs [t]  = ptext (sLit "@") <> ppr_type TopPrec t
+  ppTs ts   = ptext (sLit "@") <>
+                parens (hsep $ punctuate comma $ map pprType ts)
+
+  ppPs []   = Outputable.empty
+  ppPs [p]  = pprParendTcCo p
+  ppPs (p : ps) = ptext (sLit "(") <+> pprTcCo p $$
+                  vcat [ ptext (sLit ",") <+> pprTcCo q | q <- ps ] $$
+                  ptext (sLit ")")
+
+
+
 
 ppr_fun_co :: Prec -> TcCoercion -> SDoc
 ppr_fun_co p co = pprArrowChain p (split co)
diff --git a/compiler/typecheck/TcHsSyn.lhs b/compiler/typecheck/TcHsSyn.lhs
index 8e10303869..363e691348 100644
--- a/compiler/typecheck/TcHsSyn.lhs
+++ b/compiler/typecheck/TcHsSyn.lhs
@@ -1406,4 +1406,8 @@ zonkTcLCoToLCo env co
     go (TcForAllCo tv co)     = ASSERT( isImmutableTyVar tv )
                                 do { co' <- go co; return (mkTcForAllCo tv co') }
     go (TcInstCo co ty)       = do { co' <- go co; ty' <- zonkTcTypeToType env ty; return (TcInstCo co' ty') }
+    go (TcAxiomRuleCo co ts cs) = do { ts' <- zonkTcTypeToTypes env ts
+                                     ; cs' <- mapM go cs
+                                     ; return (TcAxiomRuleCo co ts' cs')
+                                     }
 \end{code}
diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs
index 23d63ba178..9b970c96e6 100644
--- a/compiler/typecheck/TcInteract.lhs
+++ b/compiler/typecheck/TcInteract.lhs
@@ -20,6 +20,7 @@ import VarSet
 import Type
 import Unify
 import FamInstEnv
+import FamInst(TcBuiltInSynFamily(..))
 import InstEnv( lookupInstEnv, instanceDFunId )
 
 import Var
@@ -44,11 +45,12 @@ import Maybes( orElse )
 import Bag
 
 import Control.Monad ( foldM )
+import Data.Maybe(catMaybes)
 
 import VarEnv
 
 import Control.Monad( when, unless )
-import Pair ()
+import Pair (Pair(..))
 import Unique( hasKey )
 import UniqFM
 import FastString ( sLit ) 
@@ -563,6 +565,7 @@ interactWithInertsStage wi
   = do { traceTcS "interactWithInerts" $ text "workitem = " <+> ppr wi
        ; rels <- extractRelevantInerts wi 
        ; traceTcS "relevant inerts are:" $ ppr rels
+       ; builtInInteractions
        ; foldlBagM interact_next (ContinueWith wi) rels }
 
   where interact_next Stop atomic_inert 
@@ -591,6 +594,31 @@ interactWithInertsStage wi
                        -> do { insertInertItemTcS atomic_inert
                              ; return (ContinueWith wi) }
                }
+
+        -- See if we can compute some new derived work for built-ins.
+        builtInInteractions
+          | CFunEqCan { cc_fun = tc, cc_tyargs = args, cc_rhs = xi } <- wi
+          , Just ops <- isBuiltInSynFamTyCon_maybe tc =
+            do is <- getInertsFunEqTyCon tc
+               traceTcS "builtInCandidates: " $ ppr is
+               let interact = sfInteractInert ops args xi
+               impMbs <- sequence
+                 [ do mb <- newDerived (mkTcEqPred lhs rhs)
+                      case mb of
+                        Just x -> return $ Just $ mkNonCanonical d x
+                        Nothing -> return Nothing
+                 | CFunEqCan { cc_tyargs = iargs
+                             , cc_rhs = ixi
+                             , cc_loc = d } <- is
+                 , Pair lhs rhs <- interact iargs ixi
+                 ]
+               let imps = catMaybes impMbs
+               unless (null imps) $ updWorkListTcS (extendWorkListEqs imps)
+          | otherwise = return ()
+
+
+
+
 \end{code}
 
 \begin{code}
@@ -1427,10 +1455,10 @@ doTopReactFunEq _ct fl fun_tc args xi loc
                 succeed_with "Fun/Cache" (evTermCoercion (ctEvTerm ctev)) rhs_ty ;
            _other -> 
 
-    -- Look up in top-level instances
+    -- Look up in top-level instances, or built-in axiom
     do { match_res <- matchFam fun_tc args   -- See Note [MATCHING-SYNONYMS]
        ; case match_res of {
-           Nothing -> return NoTopInt ;
+           Nothing -> try_improve_and_return ;
            Just (co, ty) ->
 
     -- Found a top-level instance
@@ -1441,6 +1469,19 @@ doTopReactFunEq _ct fl fun_tc args xi loc
   where
     fam_ty = mkTyConApp fun_tc args
 
+    try_improve_and_return =
+      do { case isBuiltInSynFamTyCon_maybe fun_tc of
+             Just ops ->
+               do { let eqns = sfInteractTop ops args xi
+                  ; impsMb <- mapM (\(Pair x y) -> newDerived (mkTcEqPred x y))
+                                   eqns
+                  ; let work = map (mkNonCanonical loc) (catMaybes impsMb)
+                  ; unless (null work) (updWorkListTcS (extendWorkListEqs work))
+                  }
+             _ -> return ()
+         ; return NoTopInt
+         }
+
     succeed_with :: String -> TcCoercion -> TcType -> TcS TopInteractResult
     succeed_with str co rhs_ty    -- co :: fun_tc args ~ rhs_ty
       = do { ctevs <- xCtFlavor fl [mkTcEqPred rhs_ty xi] xev
diff --git a/compiler/typecheck/TcRnDriver.lhs b/compiler/typecheck/TcRnDriver.lhs
index d918cba0c9..4818b76259 100644
--- a/compiler/typecheck/TcRnDriver.lhs
+++ b/compiler/typecheck/TcRnDriver.lhs
@@ -784,6 +784,7 @@ checkBootTyCon tc1 tc2
             = eqClosedFamilyAx ax1 ax2
         eqSynRhs (SynonymTyCon t1) (SynonymTyCon t2)
             = eqTypeX env t1 t2
+        eqSynRhs (BuiltInSynFamTyCon _) (BuiltInSynFamTyCon _) = tc1 == tc2
         eqSynRhs _ _ = False
     in
     roles1 == roles2 &&
diff --git a/compiler/typecheck/TcSMonad.lhs b/compiler/typecheck/TcSMonad.lhs
index 5674b47ee2..de16efe9b5 100644
--- a/compiler/typecheck/TcSMonad.lhs
+++ b/compiler/typecheck/TcSMonad.lhs
@@ -72,6 +72,7 @@ module TcSMonad (
     modifyInertTcS,
     insertInertItemTcS, partitionCCanMap, partitionEqMap,
     getRelevantCts, extractRelevantInerts,
+    getInertsFunEqTyCon,
     CCanMap(..), CtTypeMap, CtFamHeadMap, CtPredMap,
     PredMap, FamHeadMap,
     partCtFamHeadMap, lookupFamHead, lookupSolvedDict,
@@ -827,6 +828,18 @@ checkAllSolved
                      || unsolved_dicts || unsolved_funeqs
                      || not (isEmptyBag (inert_insols icans)))) }
 
+
+{- Get inert function equation constraints that have the given tycon
+in their head.  Not that the constraints remain in the inert set.
+We use this to check for derived interactions with built-in type-function
+constructors. -}
+getInertsFunEqTyCon :: TyCon -> TcS [Ct]
+getInertsFunEqTyCon tc =
+  do is <- getTcSInerts
+     let mp = unFamHeadMap $ inert_funeqs $ inert_cans is
+     return $ lookupTypeMapTyCon mp tc
+
+
 extractRelevantInerts :: Ct -> TcS Cts
 -- Returns the constraints from the inert set that are 'relevant' to react with 
 -- this constraint. The monad is left with the 'thinner' inerts. 
@@ -1657,6 +1670,8 @@ matchFam tycon args
         ty = pSnd (tcCoercionKind co)
     in return $ Just (co, ty)
 
+  | Just ops <- isBuiltInSynFamTyCon_maybe tycon = return (sfMatchFam ops args)
+
   | otherwise
   = return Nothing
        
diff --git a/compiler/typecheck/TcTyClsDecls.lhs b/compiler/typecheck/TcTyClsDecls.lhs
index f4e4dabd1b..6a9da43c1b 100644
--- a/compiler/typecheck/TcTyClsDecls.lhs
+++ b/compiler/typecheck/TcTyClsDecls.lhs
@@ -1422,6 +1422,7 @@ checkValidTyCon tc mroles
       SynonymTyCon ty              -> 
         do { check_roles
            ; checkValidType syn_ctxt ty }
+      BuiltInSynFamTyCon _ -> return ()
 
   | otherwise
   = do { unless (isFamilyTyCon tc) $ check_roles -- don't check data families!
diff --git a/compiler/typecheck/TcType.lhs b/compiler/typecheck/TcType.lhs
index fddd1607c3..4ef261ca4a 100644
--- a/compiler/typecheck/TcType.lhs
+++ b/compiler/typecheck/TcType.lhs
@@ -1352,6 +1352,8 @@ orphNamesOfCo (NthCo _ co)          = orphNamesOfCo co
 orphNamesOfCo (LRCo  _ co)          = orphNamesOfCo co
 orphNamesOfCo (InstCo co ty)        = orphNamesOfCo co `unionNameSets` orphNamesOfType ty
 orphNamesOfCo (SubCo co)            = orphNamesOfCo co
+orphNamesOfCo (AxiomRuleCo _ ts cs) = orphNamesOfTypes ts `unionNameSets`
+                                      orphNamesOfCos cs
 
 orphNamesOfCos :: [Coercion] -> NameSet
 orphNamesOfCos = orphNamesOfThings orphNamesOfCo
diff --git a/compiler/typecheck/TcTypeNats.hs b/compiler/typecheck/TcTypeNats.hs
new file mode 100644
index 0000000000..3d3ebb9952
--- /dev/null
+++ b/compiler/typecheck/TcTypeNats.hs
@@ -0,0 +1,467 @@
+module TcTypeNats
+  ( typeNatTyCons
+  , typeNatCoAxiomRules
+  , TcBuiltInSynFamily(..)
+  ) where
+
+import Type
+import Pair
+import TcType     ( TcType )
+import TyCon      ( TyCon, SynTyConRhs(..), mkSynTyCon, TyConParent(..)  )
+import Coercion   ( Role(..) )
+import TcRnTypes  ( Xi )
+import TcEvidence ( mkTcAxiomRuleCo, TcCoercion )
+import CoAxiom    ( CoAxiomRule(..) )
+import Name       ( Name, BuiltInSyntax(..) )
+import TysWiredIn ( typeNatKind, mkWiredInTyConName
+                  , promotedBoolTyCon
+                  , promotedFalseDataCon, promotedTrueDataCon
+                  )
+import TysPrim    ( tyVarList, mkArrowKinds )
+import PrelNames  ( gHC_TYPELITS
+                  , typeNatAddTyFamNameKey
+                  , typeNatMulTyFamNameKey
+                  , typeNatExpTyFamNameKey
+                  , typeNatLeqTyFamNameKey
+                  )
+import FamInst    ( TcBuiltInSynFamily(..) )
+import FastString ( FastString, fsLit )
+import qualified Data.Map as Map
+import Data.Maybe ( isJust )
+
+{-------------------------------------------------------------------------------
+Built-in type constructors for functions on type-lelve nats
+-}
+
+typeNatTyCons :: [TyCon]
+typeNatTyCons =
+  [ typeNatAddTyCon
+  , typeNatMulTyCon
+  , typeNatExpTyCon
+  , typeNatLeqTyCon
+  ]
+
+typeNatAddTyCon :: TyCon
+typeNatAddTyCon = mkTypeNatFunTyCon2 name
+  TcBuiltInSynFamily
+    { sfMatchFam      = matchFamAdd
+    , sfInteractTop   = interactTopAdd
+    , sfInteractInert = interactInertAdd
+    }
+  where
+  name = mkWiredInTyConName UserSyntax gHC_TYPELITS (fsLit "+")
+            typeNatAddTyFamNameKey typeNatAddTyCon
+
+typeNatMulTyCon :: TyCon
+typeNatMulTyCon = mkTypeNatFunTyCon2 name
+  TcBuiltInSynFamily
+    { sfMatchFam      = matchFamMul
+    , sfInteractTop   = interactTopMul
+    , sfInteractInert = interactInertMul
+    }
+  where
+  name = mkWiredInTyConName UserSyntax gHC_TYPELITS (fsLit "*")
+            typeNatMulTyFamNameKey typeNatMulTyCon
+
+typeNatExpTyCon :: TyCon
+typeNatExpTyCon = mkTypeNatFunTyCon2 name
+  TcBuiltInSynFamily
+    { sfMatchFam      = matchFamExp
+    , sfInteractTop   = interactTopExp
+    , sfInteractInert = interactInertExp
+    }
+  where
+  name = mkWiredInTyConName UserSyntax gHC_TYPELITS (fsLit "^")
+                typeNatExpTyFamNameKey typeNatExpTyCon
+
+typeNatLeqTyCon :: TyCon
+typeNatLeqTyCon =
+  mkSynTyCon name
+    (mkArrowKinds [ typeNatKind, typeNatKind ] boolKind)
+    (take 2 $ tyVarList typeNatKind)
+    [Nominal,Nominal]
+    (BuiltInSynFamTyCon ops)
+    NoParentTyCon
+
+  where
+  name = mkWiredInTyConName UserSyntax gHC_TYPELITS (fsLit "<=?")
+                typeNatLeqTyFamNameKey typeNatLeqTyCon
+  ops = TcBuiltInSynFamily
+    { sfMatchFam      = matchFamLeq
+    , sfInteractTop   = interactTopLeq
+    , sfInteractInert = interactInertLeq
+    }
+
+
+-- Make a binary built-in constructor of kind: Nat -> Nat -> Nat
+mkTypeNatFunTyCon2 :: Name -> TcBuiltInSynFamily -> TyCon
+mkTypeNatFunTyCon2 op tcb =
+  mkSynTyCon op
+    (mkArrowKinds [ typeNatKind, typeNatKind ] typeNatKind)
+    (take 2 $ tyVarList typeNatKind)
+    [Nominal,Nominal]
+    (BuiltInSynFamTyCon tcb)
+    NoParentTyCon
+
+
+
+
+{-------------------------------------------------------------------------------
+Built-in rules axioms
+-------------------------------------------------------------------------------}
+
+-- If you add additional rules, please remember to add them to
+-- `typeNatCoAxiomRules` also.
+axAddDef
+  , axMulDef
+  , axExpDef
+  , axLeqDef
+  , axAdd0L
+  , axAdd0R
+  , axMul0L
+  , axMul0R
+  , axMul1L
+  , axMul1R
+  , axExp1L
+  , axExp0R
+  , axExp1R
+  , axLeqRefl
+  , axLeq0L
+  :: CoAxiomRule
+
+axAddDef = mkBinAxiom "AddDef" typeNatAddTyCon $
+              \x y -> num (x + y)
+
+axMulDef = mkBinAxiom "MulDef" typeNatMulTyCon $ 
+              \x y -> num (x * y)
+
+axExpDef = mkBinAxiom "ExpDef" typeNatExpTyCon $
+              \x y -> num (x ^ y)
+
+axLeqDef = mkBinAxiom "LeqDef" typeNatLeqTyCon $
+              \x y -> bool (x <= y)
+
+axAdd0L     = mkAxiom1 "Add0L"    $ \t -> (num 0 .+. t) === t
+axAdd0R     = mkAxiom1 "Add0R"    $ \t -> (t .+. num 0) === t
+axMul0L     = mkAxiom1 "Mul0L"    $ \t -> (num 0 .*. t) === num 0
+axMul0R     = mkAxiom1 "Mul0R"    $ \t -> (t .*. num 0) === num 0
+axMul1L     = mkAxiom1 "Mul1L"    $ \t -> (num 1 .*. t) === t
+axMul1R     = mkAxiom1 "Mul1R"    $ \t -> (t .*. num 1) === t
+axExp1L     = mkAxiom1 "Exp1L"    $ \t -> (num 1 .^. t) === num 1
+axExp0R     = mkAxiom1 "Exp0R"    $ \t -> (t .^. num 0) === num 1
+axExp1R     = mkAxiom1 "Exp1R"    $ \t -> (t .^. num 1) === t
+axLeqRefl   = mkAxiom1 "LeqRefl"  $ \t -> (t <== t) === bool True
+axLeq0L     = mkAxiom1 "Leq0L"    $ \t -> (num 0 <== t) === bool True
+
+typeNatCoAxiomRules :: Map.Map FastString CoAxiomRule
+typeNatCoAxiomRules = Map.fromList $ map (\x -> (coaxrName x, x))
+  [ axAddDef
+  , axMulDef
+  , axExpDef
+  , axLeqDef
+  , axAdd0L
+  , axAdd0R
+  , axMul0L
+  , axMul0R
+  , axMul1L
+  , axMul1R
+  , axExp1L
+  , axExp0R
+  , axExp1R
+  , axLeqRefl
+  , axLeq0L
+  ]
+
+
+
+{-------------------------------------------------------------------------------
+Various utilities for making axioms and types
+-------------------------------------------------------------------------------}
+
+(.+.) :: Type -> Type -> Type
+s .+. t = mkTyConApp typeNatAddTyCon [s,t]
+
+(.*.) :: Type -> Type -> Type
+s .*. t = mkTyConApp typeNatMulTyCon [s,t]
+
+(.^.) :: Type -> Type -> Type
+s .^. t = mkTyConApp typeNatExpTyCon [s,t]
+
+(<==) :: Type -> Type -> Type
+s <== t = mkTyConApp typeNatLeqTyCon [s,t]
+
+(===) :: Type -> Type -> Pair Type
+x === y = Pair x y
+
+num :: Integer -> Type
+num = mkNumLitTy
+
+boolKind :: Kind
+boolKind = mkTyConApp promotedBoolTyCon []
+
+bool :: Bool -> Type
+bool b = if b then mkTyConApp promotedTrueDataCon []
+              else mkTyConApp promotedFalseDataCon []
+
+isBoolLitTy :: Type -> Maybe Bool
+isBoolLitTy tc =
+  do (tc,[]) <- splitTyConApp_maybe tc
+     case () of
+       _ | tc == promotedFalseDataCon -> return False
+         | tc == promotedTrueDataCon  -> return True
+         | otherwise                   -> Nothing
+
+known :: (Integer -> Bool) -> TcType -> Bool
+known p x = case isNumLitTy x of
+              Just a  -> p a
+              Nothing -> False
+
+
+
+
+-- For the definitional axioms
+mkBinAxiom :: String -> TyCon ->
+              (Integer -> Integer -> Type) -> CoAxiomRule
+mkBinAxiom str tc f =
+  CoAxiomRule
+    { coaxrName      = fsLit str
+    , coaxrTypeArity = 2
+    , coaxrAsmpRoles = []
+    , coaxrRole      = Nominal
+    , coaxrProves    = \ts cs ->
+        case (ts,cs) of
+          ([s,t],[]) -> do x <- isNumLitTy s
+                           y <- isNumLitTy t
+                           return (mkTyConApp tc [s,t] === f x y)
+          _ -> Nothing
+    }
+
+mkAxiom1 :: String -> (Type -> Pair Type) -> CoAxiomRule
+mkAxiom1 str f =
+  CoAxiomRule
+    { coaxrName      = fsLit str
+    , coaxrTypeArity = 1
+    , coaxrAsmpRoles = []
+    , coaxrRole      = Nominal
+    , coaxrProves    = \ts cs ->
+        case (ts,cs) of
+          ([s],[]) -> return (f s)
+          _        -> Nothing
+    }
+
+
+{-------------------------------------------------------------------------------
+Evaluation
+-------------------------------------------------------------------------------}
+
+matchFamAdd :: [Type] -> Maybe (TcCoercion, TcType)
+matchFamAdd [s,t]
+  | Just 0 <- mbX = Just (mkTcAxiomRuleCo axAdd0L [t] [], t)
+  | Just 0 <- mbY = Just (mkTcAxiomRuleCo axAdd0R [s] [], s)
+  | Just x <- mbX, Just y <- mbY =
+    Just (mkTcAxiomRuleCo axAddDef [s,t] [], num (x + y))
+  where mbX = isNumLitTy s
+        mbY = isNumLitTy t
+matchFamAdd _ = Nothing
+
+matchFamMul :: [Xi] -> Maybe (TcCoercion, Xi)
+matchFamMul [s,t]
+  | Just 0 <- mbX = Just (mkTcAxiomRuleCo axMul0L [t] [], num 0)
+  | Just 0 <- mbY = Just (mkTcAxiomRuleCo axMul0R [s] [], num 0)
+  | Just 1 <- mbX = Just (mkTcAxiomRuleCo axMul1L [t] [], t)
+  | Just 1 <- mbY = Just (mkTcAxiomRuleCo axMul1R [s] [], s)
+  | Just x <- mbX, Just y <- mbY =
+    Just (mkTcAxiomRuleCo axMulDef [s,t] [], num (x * y))
+  where mbX = isNumLitTy s
+        mbY = isNumLitTy t
+matchFamMul _ = Nothing
+
+matchFamExp :: [Xi] -> Maybe (TcCoercion, Xi)
+matchFamExp [s,t]
+  | Just 0 <- mbY = Just (mkTcAxiomRuleCo axExp0R [s] [], num 1)
+  | Just 1 <- mbX = Just (mkTcAxiomRuleCo axExp1L [t] [], num 1)
+  | Just 1 <- mbY = Just (mkTcAxiomRuleCo axExp1R [s] [], s)
+  | Just x <- mbX, Just y <- mbY =
+    Just (mkTcAxiomRuleCo axExpDef [s,t] [], num (x ^ y))
+  where mbX = isNumLitTy s
+        mbY = isNumLitTy t
+matchFamExp _ = Nothing
+
+matchFamLeq :: [Xi] -> Maybe (TcCoercion, Xi)
+matchFamLeq [s,t]
+  | Just 0 <- mbX = Just (mkTcAxiomRuleCo axLeq0L [t] [], bool True)
+  | Just x <- mbX, Just y <- mbY =
+    Just (mkTcAxiomRuleCo axLeqDef [s,t] [], bool (x <= y))
+  | eqType s t  = Just (mkTcAxiomRuleCo axLeqRefl [s] [], bool True)
+  where mbX = isNumLitTy s
+        mbY = isNumLitTy t
+matchFamLeq _ = Nothing
+
+{-------------------------------------------------------------------------------
+Interact with axioms
+-------------------------------------------------------------------------------}
+
+interactTopAdd :: [Xi] -> Xi -> [Pair Type]
+interactTopAdd [s,t] r
+  | Just 0 <- mbZ = [ s === num 0, t === num 0 ]
+  | Just x <- mbX, Just z <- mbZ, Just y <- minus z x = [t === num y]
+  | Just y <- mbY, Just z <- mbZ, Just x <- minus z y = [s === num x]
+  where
+  mbX = isNumLitTy s
+  mbY = isNumLitTy t
+  mbZ = isNumLitTy r
+interactTopAdd _ _ = []
+
+interactTopMul :: [Xi] -> Xi -> [Pair Type]
+interactTopMul [s,t] r
+  | Just 1 <- mbZ = [ s === num 1, t === num 1 ]
+  | Just x <- mbX, Just z <- mbZ, Just y <- divide z x = [t === num y]
+  | Just y <- mbY, Just z <- mbZ, Just x <- divide z y = [s === num x]
+  where
+  mbX = isNumLitTy s
+  mbY = isNumLitTy t
+  mbZ = isNumLitTy r
+interactTopMul _ _ = []
+
+interactTopExp :: [Xi] -> Xi -> [Pair Type]
+interactTopExp [s,t] r
+  | Just 0 <- mbZ = [ s === num 0 ]
+  | Just x <- mbX, Just z <- mbZ, Just y <- logExact  z x = [t === num y]
+  | Just y <- mbY, Just z <- mbZ, Just x <- rootExact z y = [s === num x]
+  where
+  mbX = isNumLitTy s
+  mbY = isNumLitTy t
+  mbZ = isNumLitTy r
+interactTopExp _ _ = []
+
+interactTopLeq :: [Xi] -> Xi -> [Pair Type]
+interactTopLeq [s,t] r
+  | Just 0 <- mbY, Just True <- mbZ = [ s === num 0 ]
+  where
+  mbY = isNumLitTy t
+  mbZ = isBoolLitTy r
+interactTopLeq _ _ = []
+
+
+
+{-------------------------------------------------------------------------------
+Interacton with inerts
+-------------------------------------------------------------------------------}
+
+interactInertAdd :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type]
+interactInertAdd [x1,y1] z1 [x2,y2] z2
+  | sameZ && eqType x1 x2         = [ y1 === y2 ]
+  | sameZ && eqType y1 y2         = [ x1 === x2 ]
+  where sameZ = eqType z1 z2
+interactInertAdd _ _ _ _ = []
+
+interactInertMul :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type]
+interactInertMul [x1,y1] z1 [x2,y2] z2
+  | sameZ && known (/= 0) x1 && eqType x1 x2 = [ y1 === y2 ]
+  | sameZ && known (/= 0) y1 && eqType y1 y2 = [ x1 === x2 ]
+  where sameZ   = eqType z1 z2
+
+interactInertMul _ _ _ _ = []
+
+interactInertExp :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type]
+interactInertExp [x1,y1] z1 [x2,y2] z2
+  | sameZ && known (> 1) x1 && eqType x1 x2 = [ y1 === y2 ]
+  | sameZ && known (> 0) y1 && eqType y1 y2 = [ x1 === x2 ]
+  where sameZ = eqType z1 z2
+
+interactInertExp _ _ _ _ = []
+
+
+interactInertLeq :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type]
+interactInertLeq [x1,y1] z1 [x2,y2] z2
+  | bothTrue && eqType x1 y2 && eqType y1 x2 = [ x1 === y1 ]
+  | bothTrue && eqType y1 x2                 = [ (x1 <== y2) === bool True ]
+  | bothTrue && eqType y2 x1                 = [ (x2 <== y1) === bool True ]
+  where bothTrue = isJust $ do True <- isBoolLitTy z1
+                               True <- isBoolLitTy z2
+                               return ()
+
+interactInertLeq _ _ _ _ = []
+
+
+
+
+{- -----------------------------------------------------------------------------
+These inverse functions are used for simplifying propositions using
+concrete natural numbers.
+----------------------------------------------------------------------------- -}
+
+-- | Subtract two natural numbers.
+minus :: Integer -> Integer -> Maybe Integer
+minus x y = if x >= y then Just (x - y) else Nothing
+
+-- | Compute the exact logarithm of a natural number.
+-- The logarithm base is the second argument.
+logExact :: Integer -> Integer -> Maybe Integer
+logExact x y = do (z,True) <- genLog x y
+                  return z
+
+
+-- | Divide two natural numbers.
+divide :: Integer -> Integer -> Maybe Integer
+divide _ 0  = Nothing
+divide x y  = case divMod x y of
+                (a,0) -> Just a
+                _     -> Nothing
+
+-- | Compute the exact root of a natural number.
+-- The second argument specifies which root we are computing.
+rootExact :: Integer -> Integer -> Maybe Integer
+rootExact x y = do (z,True) <- genRoot x y
+                   return z
+
+
+
+{- | Compute the the n-th root of a natural number, rounded down to
+the closest natural number.  The boolean indicates if the result
+is exact (i.e., True means no rounding was done, False means rounded down).
+The second argument specifies which root we are computing. -}
+genRoot :: Integer -> Integer -> Maybe (Integer, Bool)
+genRoot _  0    = Nothing
+genRoot x0 1    = Just (x0, True)
+genRoot x0 root = Just (search 0 (x0+1))
+  where
+  search from to = let x = from + div (to - from) 2
+                       a = x ^ root
+                   in case compare a x0 of
+                        EQ              -> (x, True)
+                        LT | x /= from  -> search x to
+                           | otherwise  -> (from, False)
+                        GT | x /= to    -> search from x
+                           | otherwise  -> (from, False)
+
+{- | Compute the logarithm of a number in the given base, rounded down to the
+closest integer.  The boolean indicates if we the result is exact
+(i.e., True means no rounding happened, False means we rounded down).
+The logarithm base is the second argument. -}
+genLog :: Integer -> Integer -> Maybe (Integer, Bool)
+genLog x 0    = if x == 1 then Just (0, True) else Nothing
+genLog _ 1    = Nothing
+genLog 0 _    = Nothing
+genLog x base = Just (exactLoop 0 x)
+  where
+  exactLoop s i
+    | i == 1     = (s,True)
+    | i < base   = (s,False)
+    | otherwise  =
+        let s1 = s + 1
+        in s1 `seq` case divMod i base of
+                      (j,r)
+                        | r == 0    -> exactLoop s1 j
+                        | otherwise -> (underLoop s1 j, False)
+
+  underLoop s i
+    | i < base  = s
+    | otherwise = let s1 = s + 1 in s1 `seq` underLoop s1 (div i base)
+
+
+
+
+
+
+
diff --git a/compiler/typecheck/TcTypeNats.hs-boot b/compiler/typecheck/TcTypeNats.hs-boot
new file mode 100644
index 0000000000..12f3e41b3f
--- /dev/null
+++ b/compiler/typecheck/TcTypeNats.hs-boot
@@ -0,0 +1,5 @@
+module TcTypeNats where
+
+import TyCon (TyCon)
+
+typeNatTyCons :: [TyCon]
diff --git a/compiler/types/CoAxiom.lhs b/compiler/types/CoAxiom.lhs
index ed1a68432b..671e857620 100644
--- a/compiler/types/CoAxiom.lhs
+++ b/compiler/types/CoAxiom.lhs
@@ -26,7 +26,9 @@ module CoAxiom (
        coAxBranchLHS, coAxBranchRHS, coAxBranchSpan, coAxBranchIncomps,
        placeHolderIncomps,
 
-       Role(..), pprFullRole
+       Role(..), pprFullRole,
+
+       CoAxiomRule(..), Eqn
        ) where 
 
 import {-# SOURCE #-} TypeRep ( Type )
@@ -38,6 +40,7 @@ import Unique
 import Var
 import Util
 import Binary
+import Pair
 import BasicTypes
 import Data.Typeable ( Typeable )
 import SrcLoc
@@ -462,4 +465,52 @@ instance Binary Role where
                           3 -> return Phantom
                           _ -> panic ("get Role " ++ show tag)
 
-\end{code}
\ No newline at end of file
+\end{code}
+
+
+Rules for building Evidence
+---------------------------
+
+Conditional axioms.  The genral idea is that a `CoAxiomRule` looks like this:
+
+    forall as. (r1 ~ r2, s1 ~ s2) => t1 ~ t2
+
+My intension is to reuse these for both (~) and (~#).
+The short-term plan is to use this datatype to represent the type-nat axioms.
+In the longer run, it would probably be good to unify this and `CoAxiom`,
+as `CoAxiom` is the special case when there are no assumptions.
+
+\begin{code}
+-- | A more explicit representation for `t1 ~ t2`.
+type Eqn = Pair Type
+
+-- | For now, we work only with nominal equality.
+data CoAxiomRule = CoAxiomRule
+  { coaxrName      :: FastString
+  , coaxrTypeArity :: Int       -- number of type argumentInts
+  , coaxrAsmpRoles :: [Role]    -- roles of parameter equations
+  , coaxrRole      :: Role      -- role of resulting equation
+  , coaxrProves    :: [Type] -> [Eqn] -> Maybe Eqn
+    -- ^ This returns @Nothing@ when we don't like
+    -- the supplied arguments.
+  } deriving Typeable
+
+instance Data.Data CoAxiomRule where
+  -- don't traverse?
+  toConstr _   = abstractConstr "CoAxiomRule"
+  gunfold _ _  = error "gunfold"
+  dataTypeOf _ = mkNoRepType "CoAxiomRule"
+
+instance Uniquable CoAxiomRule where
+  getUnique = getUnique . coaxrName
+
+instance Eq CoAxiomRule where
+  x == y = coaxrName x == coaxrName y
+
+instance Ord CoAxiomRule where
+  compare x y = compare (coaxrName x) (coaxrName y)
+
+instance Outputable CoAxiomRule where
+  ppr = ppr . coaxrName
+\end{code}
+
diff --git a/compiler/types/Coercion.lhs b/compiler/types/Coercion.lhs
index b0da3edd53..8d593c65fb 100644
--- a/compiler/types/Coercion.lhs
+++ b/compiler/types/Coercion.lhs
@@ -35,6 +35,7 @@ module Coercion (
 	mkInstCo, mkAppCo, mkTyConAppCo, mkFunCo,
         mkForAllCo, mkUnsafeCo, mkUnivCo, mkSubCo, mkPhantomCo,
         mkNewTypeCo, maybeSubCo, maybeSubCo2,
+        mkAxiomRuleCo,
 
         -- ** Decomposition
         splitNewTypeRepCo_maybe, instNewTyCon_maybe, 
@@ -180,6 +181,10 @@ data Coercion
   | SymCo Coercion             -- :: e -> e
   | TransCo Coercion Coercion  -- :: e -> e -> e
 
+    -- The number of types and coercions should match exactly the expectations
+    -- of the CoAxiomRule (i.e., the rule is fully saturated).
+  | AxiomRuleCo CoAxiomRule [Type] [Coercion]
+
   -- These are destructors
 
   | NthCo  Int         Coercion     -- Zero-indexed; decomposes (T t0 ... tn)
@@ -529,6 +534,7 @@ tyCoVarsOfCo (NthCo _ co)          = tyCoVarsOfCo co
 tyCoVarsOfCo (LRCo _ co)           = tyCoVarsOfCo co
 tyCoVarsOfCo (InstCo co ty)        = tyCoVarsOfCo co `unionVarSet` tyVarsOfType ty
 tyCoVarsOfCo (SubCo co)            = tyCoVarsOfCo co
+tyCoVarsOfCo (AxiomRuleCo _ ts cs) = tyVarsOfTypes ts `unionVarSet` tyCoVarsOfCos cs
 
 tyCoVarsOfCos :: [Coercion] -> VarSet
 tyCoVarsOfCos cos = foldr (unionVarSet . tyCoVarsOfCo) emptyVarSet cos
@@ -548,6 +554,7 @@ coVarsOfCo (NthCo _ co)          = coVarsOfCo co
 coVarsOfCo (LRCo _ co)           = coVarsOfCo co
 coVarsOfCo (InstCo co _)         = coVarsOfCo co
 coVarsOfCo (SubCo co)            = coVarsOfCo co
+coVarsOfCo (AxiomRuleCo _ _ cos) = coVarsOfCos cos
 
 coVarsOfCos :: [Coercion] -> VarSet
 coVarsOfCos cos = foldr (unionVarSet . coVarsOfCo) emptyVarSet cos
@@ -566,6 +573,8 @@ coercionSize (NthCo _ co)          = 1 + coercionSize co
 coercionSize (LRCo  _ co)          = 1 + coercionSize co
 coercionSize (InstCo co ty)        = 1 + coercionSize co + typeSize ty
 coercionSize (SubCo co)            = 1 + coercionSize co
+coercionSize (AxiomRuleCo _ tys cos) = 1 + sum (map typeSize tys)
+                                         + sum (map coercionSize cos)
 \end{code}
 
 %************************************************************************
@@ -599,6 +608,12 @@ tidyCo env@(_, subst) co
     go (InstCo co ty)         = (InstCo $! go co) $! tidyType env ty
     go (SubCo co)             = SubCo $! go co
 
+    go (AxiomRuleCo ax tys cos) = let tys1 = map (tidyType env) tys
+                                      cos1 = tidyCos env cos
+                                  in tys1 `seqList` cos1 `seqList`
+                                     AxiomRuleCo ax tys1 cos1
+
+
 tidyCos :: TidyEnv -> [Coercion] -> [Coercion]
 tidyCos env = map (tidyCo env)
 \end{code}
@@ -652,6 +667,24 @@ ppr_co p (SymCo co)         = pprPrefixApp p (ptext (sLit "Sym")) [pprParendCo c
 ppr_co p (NthCo n co)       = pprPrefixApp p (ptext (sLit "Nth:") <> int n) [pprParendCo co]
 ppr_co p (LRCo sel co)      = pprPrefixApp p (ppr sel) [pprParendCo co]
 ppr_co p (SubCo co)         = pprPrefixApp p (ptext (sLit "Sub")) [pprParendCo co]
+ppr_co p (AxiomRuleCo co ts cs) = maybeParen p TopPrec $
+                                  ppr_axiom_rule_co co ts cs
+
+ppr_axiom_rule_co :: CoAxiomRule -> [Type] -> [Coercion] -> SDoc
+ppr_axiom_rule_co co ts ps = ppr (coaxrName co) <> ppTs ts $$ nest 2 (ppPs ps)
+  where
+  ppTs []   = Outputable.empty
+  ppTs [t]  = ptext (sLit "@") <> ppr_type TopPrec t
+  ppTs ts   = ptext (sLit "@") <>
+                parens (hsep $ punctuate comma $ map pprType ts)
+
+  ppPs []   = Outputable.empty
+  ppPs [p]  = pprParendCo p
+  ppPs (p : ps) = ptext (sLit "(") <+> pprCo p $$
+                  vcat [ ptext (sLit ",") <+> pprCo q | q <- ps ] $$
+                  ptext (sLit ")")
+
+
 
 ppr_role :: Role -> SDoc
 ppr_role r = underscore <> ppr r
@@ -972,6 +1005,9 @@ mkUnivCo role ty1 ty2
   | ty1 `eqType` ty2 = Refl role ty1
   | otherwise        = UnivCo role ty1 ty2
 
+mkAxiomRuleCo :: CoAxiomRule -> [Type] -> [Coercion] -> Coercion
+mkAxiomRuleCo = AxiomRuleCo
+
 -- input coercion is Nominal
 mkSubCo :: Coercion -> Coercion
 mkSubCo (Refl Nominal ty) = Refl Representational ty
@@ -981,6 +1017,7 @@ mkSubCo (UnivCo Nominal ty1 ty2) = UnivCo Representational ty1 ty2
 mkSubCo co = ASSERT2( coercionRole co == Nominal, ppr co )
              SubCo co
 
+
 -- takes a Nominal coercion and possibly casts it into a Representational one
 maybeSubCo :: Role -> Coercion -> Coercion
 maybeSubCo Nominal          = id
@@ -1211,6 +1248,9 @@ coreEqCoercion2 env (InstCo co1 ty1) (InstCo co2 ty2)
 coreEqCoercion2 env (SubCo co1) (SubCo co2)
   = coreEqCoercion2 env co1 co2
 
+coreEqCoercion2 env (AxiomRuleCo a1 ts1 cs1) (AxiomRuleCo a2 ts2 cs2)
+  = a1 == a2 && all2 (eqTypeX env) ts1 ts2 && all2 (coreEqCoercion2 env) cs1 cs2
+
 coreEqCoercion2 _ _ _ = False
 \end{code}
 
@@ -1357,6 +1397,12 @@ subst_co subst co
     go (LRCo lr co)          = mkLRCo lr (go co)
     go (InstCo co ty)        = mkInstCo (go co) $! go_ty ty
     go (SubCo co)            = mkSubCo (go co)
+    go (AxiomRuleCo co ts cs)  = let ts1 = map go_ty ts
+                                     cs1 = map go cs
+                                 in ts1 `seqList` cs1 `seqList`
+                                    AxiomRuleCo co ts1 cs1
+
+
 
 substCoVar :: CvSubst -> CoVar -> Coercion
 substCoVar (CvSubst in_scope _ cenv) cv
@@ -1655,6 +1701,7 @@ seqCo (NthCo _ co)              = seqCo co
 seqCo (LRCo _ co)               = seqCo co
 seqCo (InstCo co ty)            = seqCo co `seq` seqType ty
 seqCo (SubCo co)                = seqCo co
+seqCo (AxiomRuleCo _ ts cs)     = seqTypes ts `seq` seqCos cs
 
 seqCos :: [Coercion] -> ()
 seqCos []       = ()
@@ -1702,6 +1749,11 @@ coercionKind co = go co
     go (LRCo lr co)          = (pickLR lr . splitAppTy) <$> go co
     go (InstCo aco ty)       = go_app aco [ty]
     go (SubCo co)            = go co
+    go (AxiomRuleCo ax tys cos) =
+      case coaxrProves ax tys (map coercionKind cos) of
+        Just res -> res
+        Nothing  -> panic "coercionKind: Malformed coercion"
+
 
     go_app :: Coercion -> [Type] -> Pair Type
     -- Collect up all the arguments and apply all at once
@@ -1731,6 +1783,7 @@ coercionRole = go
     go (LRCo _ _)           = Nominal
     go (InstCo co _)        = go co
     go (SubCo _)            = Representational
+    go (AxiomRuleCo c _ _)  = coaxrRole c
 \end{code}
 
 Note [Nested InstCos]
diff --git a/compiler/types/OptCoercion.lhs b/compiler/types/OptCoercion.lhs
index 9f965ece26..f63ca38129 100644
--- a/compiler/types/OptCoercion.lhs
+++ b/compiler/types/OptCoercion.lhs
@@ -224,6 +224,16 @@ opt_co' env sym mrole (InstCo co ty)
 
 opt_co' env sym _ (SubCo co) = opt_co env sym (Just Representational) co
 
+-- XXX: We could add another field to CoAxiomRule that
+-- would allow us to do custom simplifications.
+opt_co' env sym mrole (AxiomRuleCo co ts cs) =
+  wrapRole mrole (coaxrRole co) $
+    wrapSym sym $
+    AxiomRuleCo co (map (substTy env) ts)
+                   (zipWith (opt_co env False) (map Just (coaxrAsmpRoles co)) cs)
+
+
+
 -------------
 opt_univ :: CvSubst -> Role -> Type -> Type -> Coercion
 opt_univ env role oty1 oty2
diff --git a/compiler/types/TyCon.lhs b/compiler/types/TyCon.lhs
index 47e64301b0..7c765a76b2 100644
--- a/compiler/types/TyCon.lhs
+++ b/compiler/types/TyCon.lhs
@@ -48,6 +48,7 @@ module TyCon(
         isFamilyTyCon, isOpenFamilyTyCon,
         isSynFamilyTyCon, isDataFamilyTyCon,
         isOpenSynFamilyTyCon, isClosedSynFamilyTyCon_maybe,
+        isBuiltInSynFamTyCon_maybe,
         isUnLiftedTyCon,
         isGadtSyntaxTyCon, isDistinctTyCon, isDistinctAlgRhs,
         isTyConAssoc, tyConAssoc_maybe,
@@ -88,12 +89,14 @@ module TyCon(
 
         -- * Recursion breaking
         RecTcChecker, initRecTc, checkRecTc
+
 ) where
 
 #include "HsVersions.h"
 
 import {-# SOURCE #-} TypeRep ( Kind, Type, PredType )
 import {-# SOURCE #-} DataCon ( DataCon, isVanillaDataCon )
+import {-# SOURCE #-} FamInst ( TcBuiltInSynFamily )
 
 import Var
 import Class
@@ -628,6 +631,8 @@ data SynTyConRhs
    -- | A closed type synonym family declared in an hs-boot file with
    -- type family F a where ..
    | AbstractClosedSynFamilyTyCon
+
+   | BuiltInSynFamTyCon TcBuiltInSynFamily
 \end{code}
 
 Note [Closed type families]
@@ -1207,6 +1212,7 @@ isFamilyTyCon :: TyCon -> Bool
 isFamilyTyCon (SynTyCon {synTcRhs = OpenSynFamilyTyCon })              = True
 isFamilyTyCon (SynTyCon {synTcRhs = ClosedSynFamilyTyCon {} })         = True
 isFamilyTyCon (SynTyCon {synTcRhs = AbstractClosedSynFamilyTyCon {} }) = True
+isFamilyTyCon (SynTyCon {synTcRhs = BuiltInSynFamTyCon {} })           = True
 isFamilyTyCon (AlgTyCon {algTcRhs = DataFamilyTyCon {}})               = True
 isFamilyTyCon _ = False
 
@@ -1222,6 +1228,7 @@ isSynFamilyTyCon :: TyCon -> Bool
 isSynFamilyTyCon (SynTyCon {synTcRhs = OpenSynFamilyTyCon {}})           = True
 isSynFamilyTyCon (SynTyCon {synTcRhs = ClosedSynFamilyTyCon {}})         = True
 isSynFamilyTyCon (SynTyCon {synTcRhs = AbstractClosedSynFamilyTyCon {}}) = True
+isSynFamilyTyCon (SynTyCon {synTcRhs = BuiltInSynFamTyCon {}})           = True
 isSynFamilyTyCon _ = False
 
 isOpenSynFamilyTyCon :: TyCon -> Bool
@@ -1234,6 +1241,11 @@ isClosedSynFamilyTyCon_maybe
   (SynTyCon {synTcRhs = ClosedSynFamilyTyCon ax}) = Just ax
 isClosedSynFamilyTyCon_maybe _ = Nothing
 
+isBuiltInSynFamTyCon_maybe :: TyCon -> Maybe TcBuiltInSynFamily
+isBuiltInSynFamTyCon_maybe
+  SynTyCon {synTcRhs = BuiltInSynFamTyCon ops } = Just ops
+isBuiltInSynFamTyCon_maybe _ = Nothing
+
 -- | Is this a synonym 'TyCon' that can have may have further instances appear?
 isDataFamilyTyCon :: TyCon -> Bool
 isDataFamilyTyCon (AlgTyCon {algTcRhs = DataFamilyTyCon {}}) = True