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`.

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}
 
 %************************************************************************

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

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
 

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)

compiler/ghc.cabal.in

@@ -383,6 +383,7 @@ Library
         TcInteract
         TcCanonical
         TcSMonad
+        TcTypeNats
         Class
         Coercion
         FamInstEnv

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)))

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

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}
 

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

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}
 
 

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

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

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,

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}
+
+
+

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}
+
+

compiler/typecheck/FamInst.lhs-boot

+\begin{code}
+module FamInst where
+
+data TcBuiltInSynFamily
+\end{code}

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)

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}

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

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 &&