Add some operations on type-level naturals.
authorIavor S. Diatchki <iavor.diatchki@gmail.com>
Sun, 16 Jan 2011 21:59:43 +0000 (13:59 -0800)
committerIavor S. Diatchki <iavor.diatchki@gmail.com>
Sun, 16 Jan 2011 21:59:43 +0000 (13:59 -0800)
The core of the work happens in module TcTypeNats (a new module).

compiler/deSugar/DsBinds.lhs
compiler/ghc.cabal.in
compiler/hsSyn/HsBinds.lhs
compiler/prelude/PrelNames.lhs
compiler/typecheck/TcHsSyn.lhs
compiler/typecheck/TcInteract.lhs
compiler/typecheck/TcMType.lhs
compiler/typecheck/TcSMonad.lhs
compiler/typecheck/TcTyClsDecls.lhs
compiler/typecheck/TcTypeNats.hs [new file with mode: 0644]

index 815c0d1..0c188a8 100644 (file)
@@ -59,6 +59,7 @@ import FastString
 import Util
 
 import MonadUtils
+import HscTypes (MonadThings)
 \end{code}
 
 %************************************************************************
@@ -217,7 +218,7 @@ dsTcEvBinds (TcEvBinds {}) = panic "dsEvBinds"      -- Zonker has got rid of this
 dsTcEvBinds (EvBinds bs)   = dsEvBinds bs
 
 dsEvBinds :: Bag EvBind -> DsM [DsEvBind]
-dsEvBinds bs = return (map dsEvGroup sccs)
+dsEvBinds bs = mapM dsEvGroup sccs
   where
     sccs :: [SCC EvBind]
     sccs = stronglyConnCompFromEdgedVertices edges
@@ -234,12 +235,14 @@ dsEvBinds bs = return (map dsEvGroup sccs)
     free_vars_of (EvCoercion co)    = varSetElems (tyVarsOfType co)
     free_vars_of (EvDFunApp _ _ vs) = vs
     free_vars_of (EvSuperClass d _) = [d]
+    free_vars_of (EvInteger _)      = []
+    free_vars_of (EvAxiom _ _)      = []
 
-dsEvGroup :: SCC EvBind -> DsEvBind
+dsEvGroup :: MonadThings m => SCC EvBind -> m DsEvBind
 dsEvGroup (AcyclicSCC (EvBind co_var (EvSuperClass dict n)))
   | isCoVar co_var      -- An equality superclass
   = ASSERT( null other_data_cons )
-    CaseEvBind dict (DataAlt data_con) bndrs
+    return (CaseEvBind dict (DataAlt data_con) bndrs)
   where
     (cls, tys) = getClassPredTys (evVarPred dict)
     (data_con:other_data_cons) = tyConDataCons (classTyCon cls)
@@ -252,24 +255,30 @@ dsEvGroup (AcyclicSCC (EvBind co_var (EvSuperClass dict n)))
                         | otherwise = mkWildEvBinder p
     
 dsEvGroup (AcyclicSCC (EvBind v r))
-  = LetEvBind (NonRec v (dsEvTerm r))
+  = do d <- dsEvTerm r
+       return (LetEvBind (NonRec v d))
 
 dsEvGroup (CyclicSCC bs)
-  = LetEvBind (Rec (map ds_pair bs))
+  = do ds <- mapM ds_pair bs
+       return (LetEvBind (Rec ds))
   where
-    ds_pair (EvBind v r) = (v, dsEvTerm r)
-
-dsEvTerm :: EvTerm -> CoreExpr
-dsEvTerm (EvId v)                = Var v
-dsEvTerm (EvCast v co)           = Cast (Var v) co
-dsEvTerm (EvDFunApp df tys vars) = Var df `mkTyApps` tys `mkVarApps` vars
-dsEvTerm (EvCoercion co)         = Type co
+    ds_pair (EvBind v r) = do ev <- dsEvTerm r
+                              return (v, ev)
+
+dsEvTerm :: MonadThings m => EvTerm -> m CoreExpr
+dsEvTerm (EvId v)         = return (Var v)
+dsEvTerm (EvCast v co)    = return (Cast (Var v) co)
+dsEvTerm (EvDFunApp df tys vars) =
+                            return (Var df `mkTyApps` tys `mkVarApps` vars)
+dsEvTerm (EvCoercion co)  = return (Type co)
+dsEvTerm (EvInteger n)    = mkIntegerExpr n
+dsEvTerm (EvAxiom x t)    = return (mkRuntimeErrorApp rUNTIME_ERROR_ID t x)
 dsEvTerm (EvSuperClass d n)
   = ASSERT( isClassPred (classSCTheta cls !! n) )
            -- We can only select *dictionary* superclasses
            -- in terms.  Equality superclasses are dealt with
            -- in dsEvGroup, where they can generate a case expression
-    Var sc_sel_id `mkTyApps` tys `App` Var d
+    return (Var sc_sel_id `mkTyApps` tys `App` Var d)
   where
     sc_sel_id  = classSCSelId cls n    -- Zero-indexed
     (cls, tys) = getClassPredTys (evVarPred d)    
@@ -747,5 +756,6 @@ dsHsWrapper (WpCompose c1 c2) = do { k1 <- dsHsWrapper c1
 dsHsWrapper (WpCast co)       = return (\e -> Cast e co) 
 dsHsWrapper (WpEvLam ev)      = return (\e -> Lam ev e) 
 dsHsWrapper (WpTyLam tv)      = return (\e -> Lam tv e) 
-dsHsWrapper (WpEvApp evtrm)   = return (\e -> App e (dsEvTerm evtrm))
+dsHsWrapper (WpEvApp evtrm)   = do ev <- dsEvTerm evtrm
+                                   return (\e -> App e ev)
 \end{code}
index 0711a93..6457f8b 100644 (file)
@@ -415,6 +415,7 @@ Library
         TcType
         TcUnify
         TcInteract
+        TcTypeNats
         TcCanonical
         TcSMonad
         Class
index 2544515..5cffebc 100644 (file)
@@ -453,6 +453,9 @@ data EvTerm
   | EvSuperClass DictId Int    -- n'th superclass. Used for both equalities and
                                -- dictionaries, even though the former have no
                               -- selector Id.  We count up from _0_ 
+
+  | EvInteger Integer          -- (e.g., evidence for "TypeNat n")
+  | EvAxiom String Type        -- Unused evidence (see Note [EvAxiom])
                               
   deriving( Data, Typeable)
 
@@ -461,6 +464,30 @@ evVarTerm v | isCoVar v = EvCoercion (mkCoVarCoercion v)
             | otherwise = EvId v
 \end{code}
 
+Note [EvAxiom]
+~~~~~~~~~~~~~~
+"EvAxiom description evidence_type"  is "evidence" which should not
+be used/needed at run-time.  Such values are generated when solving
+predicates for built-in "classes" (e.g., the <= operator on
+type-level naturals, see TcTypeNats for more details).
+
+The situation is similar to what happens with equality predicates:
+it would be nice if we could avoid having the evidence at run-time at all.
+
+Unfortunately, the mechanism used to avoid passing runtime evidence for
+equalities (lifting the evidence to the type level and using a dependent
+kind to classify it) is not easy to generalize to other predicates.
+
+One alternative might be to teach GHC core about "irrelevant" arguments,
+so when we emit code we skip such arguments in function definitions and
+applications.  This would allow us to treat all erasable entities in the
+same way (i.e., both types and evidence which is not needed
+at run-time such as the evidence for (a ~ b), (a <= b), or ordinary classes
+with no methods and super-classes).
+
+
+
+
 Note [EvBinds/EvTerm]
 ~~~~~~~~~~~~~~~~~~~~~
 How evidence is created and updated. Bindings for dictionaries, 
@@ -576,6 +603,9 @@ instance Outputable EvTerm where
   ppr (EvCoercion co)    = ppr co
   ppr (EvSuperClass d n) = ptext (sLit "sc") <> parens (ppr (d,n))
   ppr (EvDFunApp df tys ts) = ppr df <+> sep [ char '@' <> ppr tys, ppr ts ]
+  ppr (EvInteger n)      = integer n
+  ppr (EvAxiom x t)      = parens (ptext (sLit ("axiom " ++ x)) <+> 
+                                            ptext (sLit "::") <+> ppr t)
 \end{code}
 
 %************************************************************************
index dee65d1..58a785f 100644 (file)
@@ -211,6 +211,13 @@ basicKnownKeyNames
        -- Other classes
        randomClassName, randomGenClassName, monadPlusClassName,
 
+        -- Type-level naturals
+        typeNatClassName,
+        lessThanEqualClassName,
+        addTyFamName,
+        mulTyFamName,
+        expTyFamName,
+
         -- Annotation type checking
         toAnnotationWrapperName
 
@@ -248,7 +255,8 @@ gHC_PRIM, gHC_TYPES, gHC_UNIT, gHC_ORDERING, gHC_GENERICS,
     gHC_ST, gHC_ARR, gHC_STABLE, gHC_ADDR, gHC_PTR, gHC_ERR, gHC_REAL,
     gHC_FLOAT, gHC_TOP_HANDLER, sYSTEM_IO, dYNAMIC, tYPEABLE, gENERICS,
     dOTNET, rEAD_PREC, lEX, gHC_INT, gHC_WORD, mONAD, mONAD_FIX, aRROW, cONTROL_APPLICATIVE,
-    gHC_DESUGAR, rANDOM, gHC_EXTS, cONTROL_EXCEPTION_BASE :: Module
+    gHC_DESUGAR, rANDOM, gHC_EXTS, cONTROL_EXCEPTION_BASE,
+    gHC_TYPENATS :: Module
 
 gHC_PRIM       = mkPrimModule (fsLit "GHC.Prim")   -- Primitive types and values
 gHC_TYPES       = mkPrimModule (fsLit "GHC.Types")
@@ -303,6 +311,7 @@ gHC_DESUGAR = mkBaseModule (fsLit "GHC.Desugar")
 rANDOM         = mkBaseModule (fsLit "System.Random")
 gHC_EXTS       = mkBaseModule (fsLit "GHC.Exts")
 cONTROL_EXCEPTION_BASE = mkBaseModule (fsLit "Control.Exception.Base")
+gHC_TYPENATS    = mkBaseModule (fsLit "GHC.TypeNats")
 
 mAIN, rOOT_MAIN :: Module
 mAIN           = mkMainModule_ mAIN_NAME
@@ -826,6 +835,15 @@ randomClassName     = clsQual rANDOM (fsLit "Random")    randomClassKey
 randomGenClassName  = clsQual rANDOM (fsLit "RandomGen") randomGenClassKey
 isStringClassName   = clsQual dATA_STRING (fsLit "IsString") isStringClassKey
 
+-- Type-level naturals
+typeNatClassName, lessThanEqualClassName,
+  addTyFamName, mulTyFamName, expTyFamName :: Name
+typeNatClassName    = clsQual gHC_TYPENATS (fsLit "TypeNat") typeNatClassKey
+lessThanEqualClassName = clsQual gHC_TYPENATS (fsLit "<=") lessThanEqualClassKey
+addTyFamName        = tcQual gHC_TYPENATS (fsLit "+")   addTyFamNameKey
+mulTyFamName        = tcQual gHC_TYPENATS (fsLit "*")   mulTyFamNameKey
+expTyFamName        = tcQual gHC_TYPENATS (fsLit "^")   expTyFamNameKey
+
 -- dotnet interop
 objectTyConName :: Name
 objectTyConName            = tcQual   dOTNET (fsLit "Object") objectTyConKey
@@ -924,6 +942,12 @@ applicativeClassKey, foldableClassKey, traversableClassKey :: Unique
 applicativeClassKey    = mkPreludeClassUnique 34
 foldableClassKey       = mkPreludeClassUnique 35
 traversableClassKey    = mkPreludeClassUnique 36
+
+typeNatClassKey, lessThanEqualClassKey :: Unique
+typeNatClassKey         = mkPreludeClassUnique 37
+lessThanEqualClassKey   = mkPreludeClassUnique 38
+
+
 \end{code}
 
 %************************************************************************
@@ -1067,6 +1091,13 @@ opaqueTyConKey                          = mkPreludeTyConUnique 133
 stringTyConKey :: Unique
 stringTyConKey                         = mkPreludeTyConUnique 134
 
+addTyFamNameKey, mulTyFamNameKey, expTyFamNameKey :: Unique
+addTyFamNameKey                         = mkPreludeTyConUnique 135
+mulTyFamNameKey                         = mkPreludeTyConUnique 136
+expTyFamNameKey                         = mkPreludeTyConUnique 137
+
+
+
 ---------------- Template Haskell -------------------
 --     USES TyConUniques 100-129
 -----------------------------------------------------
index 5bc7333..d293d45 100644 (file)
@@ -1027,6 +1027,10 @@ zonkEvTerm env (EvDFunApp df tys tms)
   = do { tys' <- zonkTcTypeToTypes env tys
        ; let tms' = map (zonkEvVarOcc env) tms
        ; return (EvDFunApp (zonkIdOcc env df) tys' tms') }
+zonkEvTerm _env t@(EvInteger _)   = return t
+zonkEvTerm env (EvAxiom x t)
+  = do { t' <- zonkTcTypeToType env t
+       ; return (EvAxiom x t') }
 
 zonkTcEvBinds :: ZonkEnv -> TcEvBinds -> TcM (ZonkEnv, TcEvBinds)
 zonkTcEvBinds env (TcEvBinds var) = do { (env', bs') <- zonkEvBindsVar env var
index 1194b0c..86b5f95 100644 (file)
@@ -22,7 +22,8 @@ import InstEnv
 import Class
 import TyCon
 import Name
-
+import PrelNames (typeNatClassName,lessThanEqualClassName,
+                  addTyFamName, mulTyFamName, expTyFamName)
 import FunDeps
 
 import Control.Monad ( when ) 
@@ -31,6 +32,7 @@ import Coercion
 import Outputable
 
 import TcRnTypes
+import TcTypeNats
 import TcErrors
 import TcSMonad
 import Bag
@@ -516,7 +518,9 @@ thePipeline :: [(String,SimplifierStage)]
 thePipeline = [ ("interact with inert eqs", interactWithInertEqsStage)
               , ("interact with inerts",    interactWithInertsStage)
               , ("spontaneous solve",       spontaneousSolveStage)
-              , ("top-level reactions",     topReactionsStage) ]
+              , ("numeric reactions",       numericReactionsStage)
+              , ("top-level reactions",     topReactionsStage)
+              ]
 \end{code}
 
 *********************************************************************************
@@ -1087,6 +1091,69 @@ doInteractWithInert _fdimprs
 -- Fall-through case for all other situations
 doInteractWithInert _fdimprs _ workItem = noInteraction workItem
 
+
+numericReactionsStage :: SimplifierStage
+numericReactionsStage workItem inert
+  | isNumWork =
+    if isWanted (cc_flavor workItem) then
+        do (val,new) <- solveNumWanted grelevant wrelevant workItem
+           return
+            SR { sr_stop = case val of
+                             Nothing -> Stop
+                             Just v  -> ContinueWith v
+               , sr_new_work = new
+               , sr_inerts = inert
+               }
+    else do (val,ins,new) <- addNumGiven grelevant wrelevant workItem
+            return
+              SR { sr_stop = case val of
+                               Nothing -> Stop
+                               Just v  -> ContinueWith v
+                 , sr_new_work = new
+                 , sr_inerts = foldrBag (flip updInertSet) inert_residual ins
+                 }
+
+  where (grelevant, wrelevant, inert_residual) = getNumInerts inert
+
+        isNumWork = case workItem of
+                      CFunEqCan { cc_fun   = f }  -> isNumFun f
+                      CDictCan  { cc_class = c }  -> isNumClass c
+                      _                           -> False
+
+numericReactionsStage workItem inert = return
+  SR { sr_inerts    = inert
+     , sr_new_work  = emptyBag
+     , sr_stop      = ContinueWith workItem
+     }
+
+-- Extract constraints which may interact with numeric predicates.
+getNumInerts :: InertSet -> (CanonicalCts, CanonicalCts, InertSet)
+getNumInerts i =
+  let (gfuns, wfuns, other_funs) = partitionCCanMap isNumFun (inert_funeqs i)
+      (gcls,  wcls, other_cls)   = partitionCCanMap isNumClass (inert_dicts i)
+  in ( unionWorkLists gfuns gcls
+     , unionWorkLists wfuns wcls
+     , i { inert_funeqs = other_funs, inert_dicts = other_cls }
+     )
+
+
+isNumFun :: TyCon -> Bool
+isNumFun tc = tyConName tc `elem` [ addTyFamName, mulTyFamName, expTyFamName ]
+
+-- Does not include 'TypeNat' (it does not interact with numeric predicates).
+isNumClass :: Class -> Bool
+isNumClass cls  = className cls == lessThanEqualClassName
+
+partitionCCanMap ::
+  Ord a => (a -> Bool) -> CCanMap a -> (CanonicalCts, CanonicalCts, CCanMap a)
+partitionCCanMap p cmap =
+  let (relw,not_relw) = Map.partitionWithKey (\k _ -> p k) (cts_wanted cmap)
+      (relg,not_relg) = Map.partitionWithKey (\k _ -> p k) (cts_givder cmap)
+  in ( unionManyBags (Map.elems relg)
+     , unionManyBags (Map.elems relw)
+     , cmap { cts_wanted = not_relw, cts_givder = not_relg }
+     )
+
 -------------------------
 -- Equational Rewriting 
 rewriteDict  :: (CoVar, TcTyVar, Xi) -> (DictId, CtFlavor, Class, [Xi]) -> TcS CanonicalCt
@@ -1944,6 +2011,11 @@ data LookupInstResult
   | GenInst [WantedEvVar] EvTerm 
 
 matchClassInst :: Class -> [Type] -> WantedLoc -> TcS LookupInstResult
+
+matchClassInst clas [ ty ] _
+  | className clas == typeNatClassName
+  , Just n <- isNumberTy ty = return (GenInst [] (EvInteger n))
+
 matchClassInst clas tys loc
    = do { let pred = mkClassPred clas tys 
         ; mb_result <- matchClass clas tys
index 9921767..2539964 100644 (file)
@@ -89,6 +89,7 @@ import BasicTypes
 import SrcLoc
 import Outputable
 import FastString
+import PrelNames (typeNatClassName, lessThanEqualClassName)
 import Bag
 
 import Control.Monad
@@ -1364,6 +1365,10 @@ checkValidInstHead clas tys
          -- May not contain type family applications
        ; mapM_ checkTyFamFreeness tys
 
+        -- Check that this is not a built-in type
+       ; checkTc (not (isBuiltInClass clas))
+                 (instTypeErr pp_pred builtin_class_msg)
+
        ; mapM_ checkValidMonoType tys
        -- For now, I only allow tau-types (not polytypes) in 
        -- the head of an instance decl.  
@@ -1389,10 +1394,17 @@ checkValidInstHead clas tys
                 text "Only one type can be given in an instance head." $$
                 text "Use -XMultiParamTypeClasses if you want to allow more.")
 
+    builtin_class_msg = parens (
+                text "Built-in classes may not have custom instances.")
+
 instTypeErr :: SDoc -> SDoc -> SDoc
 instTypeErr pp_ty msg
   = sep [ptext (sLit "Illegal instance declaration for") <+> quotes pp_ty, 
         nest 2 msg]
+
+isBuiltInClass :: Class -> Bool
+isBuiltInClass c = name == typeNatClassName || name == lessThanEqualClassName
+  where name = className c
 \end{code}
 
 
index 36c46b3..ac16e09 100644 (file)
@@ -40,6 +40,7 @@ module TcSMonad (
  
     getInstEnvs, getFamInstEnvs,                -- Getting the environments 
     getTopEnv, getGblEnv, getTcEvBinds, getUntouchables,
+    tcsLookupClass, tcsLookupTyCon,
     getTcEvBindsBag, getTcSContext, getTcSTyBinds, getTcSTyBindsMap, getTcSErrors,
     getTcSErrorsBag, FrozenError (..),
     addErrorTcS,
@@ -90,7 +91,8 @@ import FamInstEnv
 import qualified TcRnMonad as TcM
 import qualified TcMType as TcM
 import qualified TcEnv as TcM 
-       ( checkWellStaged, topIdLvl, tcLookupFamInst, tcGetDefaultTys )
+       ( checkWellStaged, topIdLvl, tcLookupFamInst, tcGetDefaultTys
+       , tcLookupClass, tcLookupTyCon )
 import TcType
 import DynFlags
 
@@ -706,6 +708,12 @@ getTopEnv = wrapTcS $ TcM.getTopEnv
 getGblEnv :: TcS TcGblEnv 
 getGblEnv = wrapTcS $ TcM.getGblEnv 
 
+tcsLookupClass :: Name -> TcS Class
+tcsLookupClass name = wrapTcS (TcM.tcLookupClass name)
+
+tcsLookupTyCon :: Name -> TcS TyCon
+tcsLookupTyCon name = wrapTcS (TcM.tcLookupTyCon name)
+
 -- Various smaller utilities [TODO, maybe will be absorbed in the instance matcher]
 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
@@ -904,6 +912,8 @@ isGoodRecEv ev_var wv
         chase_ev assocs trg curr_grav visited (EvDFunApp _ _ ev_deps)
             = do { chase_results <- mapM (chase_ev_var assocs trg (curr_grav+1) visited) ev_deps
                  ; return (comb_chase_res Nothing chase_results) }
+        chase_ev _assocs _trg _curr_grav _visited (EvInteger _) = return Nothing
+        chase_ev _assocs _trg _curr_grav _visited (EvAxiom _ _) = return Nothing
 
         chase_co assocs trg curr_grav visited co 
             = -- Look for all the coercion variables in the coercion 
index a433d69..348052a 100644 (file)
@@ -47,6 +47,7 @@ import DynFlags
 import FastString
 import Unique          ( mkBuiltinUnique )
 import BasicTypes
+import PrelNames        ( addTyFamName, mulTyFamName, expTyFamName )
 
 import Bag
 import Control.Monad
@@ -159,6 +160,10 @@ tcFamInstDecl top_lvl (L loc decl)
        ; checkTc type_families $ badFamInstDecl (tcdLName decl)
        ; checkTc (not is_boot) $ badBootFamInstDeclErr
 
+         -- Check that this in not a built-in name
+       ; when (isBuiltinFamily (tcdName decl))
+              (addErr $ builtinFamilyErr (tcdName decl))
         -- Perform kind and type checking
        ; tc <- tcFamInstDecl1 decl
        ; checkValidTyCon tc    -- Remember to check validity;
@@ -176,6 +181,16 @@ isAssocFamily tycon
           Nothing       -> panic "isAssocFamily: no family?!?"
           Just (fam, _) -> isTyConAssoc fam
 
+isBuiltinFamily :: Name -> Bool
+isBuiltinFamily tc = tc `elem`
+                        [ addTyFamName, mulTyFamName, expTyFamName ]
+
+builtinFamilyErr :: Name -> SDoc
+builtinFamilyErr name
+  = ptext (sLit "Built-in type familiy") <+> quotes (ppr name) <+>
+    ptext (sLit "may not have user-defined instances.")
+
+
 assocInClassErr :: Name -> SDoc
 assocInClassErr name
  = ptext (sLit "Associated type") <+> quotes (ppr name) <+>
diff --git a/compiler/typecheck/TcTypeNats.hs b/compiler/typecheck/TcTypeNats.hs
new file mode 100644 (file)
index 0000000..0033d0c
--- /dev/null
@@ -0,0 +1,409 @@
+{-# LANGUAGE PatternGuards #-}
+module TcTypeNats (solveNumWanted, addNumGiven) where
+
+import TcSMonad   ( TcS, Xi
+                  , newWantedCoVar
+                  , setWantedCoBind, setDictBind, newDictVar
+                  , tcsLookupTyCon, tcsLookupClass
+                  , CanonicalCt (..), CanonicalCts
+                  , traceTcS
+                  )
+import TcCanonical (mkCanonicals)
+import HsBinds    (EvTerm(..))
+import Class      ( Class, className, classTyCon )
+import Type       ( tcView, mkTyConApp, mkNumberTy, isNumberTy
+                  , tcEqType )
+import TypeRep    (Type(..))
+import TyCon      (TyCon, tyConName)
+import Var        (EvVar)
+import Coercion   ( mkUnsafeCoercion )
+import Outputable
+import PrelNames  ( lessThanEqualClassName
+                  , addTyFamName, mulTyFamName, expTyFamName
+                  )
+import Bag        (bagToList, emptyBag, unionBags)
+import Data.Maybe (fromMaybe)
+import Control.Monad (msum, mplus, zipWithM, (<=<))
+
+
+
+data Term = Var Xi | Num Integer (Maybe Xi)
+data Op   = Add | Mul | Exp deriving Eq
+data Prop = EqFun Op Term Term Term
+          | Leq Term Term
+          | Eq Term Term
+
+commutative :: Op -> Bool
+commutative op = op == Add || op == Mul
+
+num :: Integer -> Term
+num n = Num n Nothing
+
+instance Eq Term where
+  Var x   == Var y    = tcEqType x y
+  Num x _ == Num y _  = x == y
+  _       == _        = False
+
+
+--------------------------------------------------------------------------------
+-- Interface with the type checker
+--------------------------------------------------------------------------------
+
+
+-- We keep the original type in numeric constants to preserve type synonyms.
+toTerm :: Xi -> Term
+toTerm xi = case mplus (isNumberTy xi) (isNumberTy =<< tcView xi) of
+              Just n -> Num n (Just xi)
+              _      -> Var xi
+
+fromTerm :: Term -> Xi
+fromTerm (Num n mb) = fromMaybe (mkNumberTy n) mb
+fromTerm (Var xi)   = xi
+
+toProp :: CanonicalCt -> Prop
+toProp (CDictCan { cc_class = c, cc_tyargs = [xi1,xi2] })
+  | className c == lessThanEqualClassName = Leq (toTerm xi1) (toTerm xi2)
+
+toProp (CFunEqCan { cc_fun = tc, cc_tyargs = [xi11,xi12], cc_rhs = xi2 })
+  | tyConName tc == addTyFamName = EqFun Add t1 t2 t3
+  | tyConName tc == mulTyFamName = EqFun Mul t1 t2 t3
+  | tyConName tc == expTyFamName = EqFun Exp t1 t2 t3
+
+    where t1 = toTerm xi11
+          t2 = toTerm xi12
+          t3 = toTerm xi2
+
+toProp p = panic $
+  "[TcTypeNats.toProp] Unexpected CanonicalCt: " ++ showSDoc (ppr p)
+
+
+solveNumWanted :: CanonicalCts -> CanonicalCts -> CanonicalCt ->
+                TcS (Maybe CanonicalCt, CanonicalCts)
+solveNumWanted given wanted prop =
+  do let asmps = map toProp $ bagToList $ unionBags given wanted
+         goal  = toProp prop
+
+     numTrace "solveNumWanted" (vmany asmps <+> text "|-" <+> ppr goal)
+
+     case solve asmps goal of
+
+       Simplified sgs ->
+         do numTrace "Simplified to" (vmany sgs)
+            defineDummy (cc_id prop) =<< fromProp goal
+            evs   <- mapM (newSubGoal <=< fromProp) sgs
+            goals <- mkCanonicals (cc_flavor prop) evs
+            return (Nothing, goals)
+
+       -- XXX: The new wanted might imply some of the existing wanteds...
+       Improved is ->
+         do numTrace "Improved by" (vmany is)
+            evs   <- mapM (newSubGoal <=< fromProp) is
+            goals <- mkCanonicals (cc_flavor prop) evs
+            return (Just prop, goals)
+
+       -- XXX: Report an error
+       Impossible ->
+         do numTrace "Impssoble" empty
+            return (Just prop, emptyBag)
+
+
+addNumGiven :: CanonicalCts -> CanonicalCts -> CanonicalCt ->
+              TcS (Maybe CanonicalCt, CanonicalCts, CanonicalCts)
+addNumGiven given wanted prop =
+  do let asmps = map toProp $ bagToList $ unionBags given wanted
+         goal  = toProp prop
+
+     numTrace "addNumGiven" (vmany asmps <+> text " /\\ " <+> ppr goal)
+     case solve asmps goal of
+
+       Simplified sgs ->
+         do numTrace "Simplified to" (vmany sgs)
+            evs   <- mapM (newFact <=< fromProp) sgs
+            facts <- mkCanonicals (cc_flavor prop) evs
+            return (Nothing, unionBags given wanted, facts)
+
+       Improved is ->
+         do numTrace "Improved by" (vmany is)
+            evs <- mapM (newFact <=< fromProp) is
+            facts <- mkCanonicals (cc_flavor prop) evs
+            return (Just prop, given, unionBags wanted facts)
+
+       -- XXX: report error
+       Impossible ->
+         do numTrace "Impossible" empty
+            return (Just prop, unionBags given wanted, emptyBag)
+
+
+
+data CvtProp  = CvtClass Class [Type]
+              | CvtCo Type Type
+
+fromProp :: Prop -> TcS CvtProp
+fromProp (Leq t1 t2) =
+  do cl <- tcsLookupClass lessThanEqualClassName
+     return (CvtClass cl [ fromTerm t1, fromTerm t2 ])
+
+fromProp (Eq t1 t2) = return $ CvtCo (fromTerm t1) (fromTerm t2)
+
+fromProp (EqFun op t1 t2 t3) =
+  do tc <- tcsLookupTyCon $ case op of
+                              Add -> addTyFamName
+                              Mul -> mulTyFamName
+                              Exp -> expTyFamName
+     return $ CvtCo (mkTyConApp tc [fromTerm t1, fromTerm t2]) (fromTerm t3)
+
+
+newSubGoal :: CvtProp -> TcS EvVar
+newSubGoal (CvtClass c ts) = newDictVar c ts
+newSubGoal (CvtCo t1 t2)   = newWantedCoVar t1 t2
+
+newFact :: CvtProp -> TcS EvVar
+newFact prop =
+  do d <- newSubGoal prop
+     defineDummy d prop
+     return d
+
+
+-- If we decided that we want to generate evidence terms,
+-- here we would set the evidence properly.  For now, we skip this
+-- step because evidence terms are not used for anything, and they
+-- get quite large, at least, if we start with a small set of axioms.
+defineDummy :: EvVar -> CvtProp -> TcS ()
+defineDummy d (CvtClass c ts) =
+  setDictBind d $ EvAxiom "<=" $ mkTyConApp (classTyCon c) ts
+
+defineDummy c (CvtCo t1 t2) =
+  setWantedCoBind c $ mkUnsafeCoercion t1 t2
+
+
+
+
+--------------------------------------------------------------------------------
+-- The Solver
+--------------------------------------------------------------------------------
+
+
+data Result = Impossible            -- We know that the goal cannot be solved.
+            | Simplified [Prop]     -- We reformulated the goal.
+            | Improved   [Prop]     -- We learned some new facts.
+
+solve :: [Prop] -> Prop -> Result
+solve asmps prop =
+  case solveWanted1 prop of
+    Just sgs -> Simplified sgs
+    Nothing ->
+      case msum $ zipWith solveWanted2 asmps (repeat prop) of
+        Just sgs -> Simplified sgs
+        Nothing  ->
+          case improve1 prop of
+            Nothing   -> Impossible
+            Just eqs  ->
+              case zipWithM improve2 asmps (repeat prop) of
+                Nothing   -> Impossible
+                Just eqs1 -> Improved (concat (eqs : eqs1))
+
+
+
+
+improve1 :: Prop -> Maybe [Prop]
+improve1 prop =
+  case prop of
+
+    Leq s t@(Num 0 _)                -> Just [ Eq s t ]
+
+
+    EqFun Add (Num m _) (Num n _) t         -> Just [ Eq (num (m+n)) t ]
+    EqFun Add (Num 0 _) s         t         -> Just [ Eq s t ]
+    EqFun Add (Num m _) s         (Num n _)
+      | m <= n                              -> Just [ Eq (num (n-m)) s ]
+      | otherwise                           -> Nothing
+    EqFun Add r         s         t
+      | r == t                              -> Just [ Eq (num 0) s ]
+      | s == t                              -> Just [ Eq (num 0) r ]
+
+    EqFun Mul (Num m _) (Num n _) t -> Just [ Eq (num (m*n)) t ]
+    EqFun Mul (Num 0 _) _         t -> Just [ Eq (num 0) t ]
+    EqFun Mul (Num 1 _) s         t -> Just [ Eq s t ]
+    EqFun Mul (Num _ _) s         t
+      | s == t                      -> Just [ Eq (num 0) s ]
+
+    EqFun Mul r         s (Num 1 _) -> Just [ Eq (num 1) r, Eq (num 1) s ]
+    EqFun Mul (Num m _) s (Num n _)
+      | Just a <- divide n m        -> Just [ Eq (num a) s ]
+      | otherwise                   -> Nothing
+
+
+    EqFun Exp (Num m _) (Num n _) t -> Just [ Eq (num (m ^ n)) t ]
+
+    EqFun Exp (Num 1 _) _         t -> Just [ Eq (num 1) t ]
+    EqFun Exp (Num _ _) s t
+      | s == t                      -> Nothing
+    EqFun Exp (Num m _) s (Num n _) -> do a <- descreteLog m n
+                                          return [ Eq (num a) s ]
+
+    EqFun Exp _ (Num 0 _) t         -> Just [ Eq (num 1) t ]
+    EqFun Exp r (Num 1 _) t         -> Just [ Eq r t ]
+    EqFun Exp r (Num m _) (Num n _) -> do a <- descreteRoot m n
+                                          return [ Eq (num a) r ]
+
+    _                               -> Just []
+
+improve2 :: Prop -> Prop -> Maybe [ Prop ]
+improve2 asmp prop =
+  case asmp of
+
+    EqFun Add a1 b1 c1 ->
+      case prop of
+        EqFun Add a2 b2 c2
+          | a1 == a2 && b1 == b2  -> Just [ Eq c1 c2 ]
+          | a1 == b2 && b1 == a2  -> Just [ Eq c1 c2 ]
+          | c1 == c2 && a1 == a2  -> Just [ Eq b1 b2 ]
+          | c1 == c2 && a1 == b2  -> Just [ Eq b1 a2 ]
+          | c1 == c2 && b1 == b2  -> Just [ Eq a1 a2 ]
+          | c1 == c2 && b1 == a2  -> Just [ Eq a1 b2 ]
+        _ -> Just []
+
+
+    EqFun Mul a1 b1 c1 ->
+      case prop of
+        EqFun Mul a2 b2 c2
+          | a1 == a2 && b1 == b2  -> Just [ Eq c1 c2 ]
+          | a1 == b2 && b1 == a2  -> Just [ Eq c1 c2 ]
+          | c1 == c2 && b1 == b2, Num m _ <- a1, Num n _ <- a2, m /= n
+                                  -> Just [ Eq (num 0) b1, Eq (num 0) c1 ]
+        _ -> Just []
+
+
+    _ -> Just []
+
+
+solveWanted1 :: Prop -> Maybe [ Prop ]
+solveWanted1 prop =
+  case prop of
+
+    Leq (Num m _) (Num n _) | m <= n      -> Just []
+    Leq (Num 0 _) _                       -> Just []
+    Leq s t                 | s == t      -> Just []
+
+    EqFun Add (Num m _) (Num n _) (Num mn _)  | m + n == mn -> Just []
+    EqFun Add (Num 0 _) s         t           | s == t      -> Just []
+    EqFun Add r         s         t           | r == s      ->
+                                                Just [ EqFun Mul (num 2) r t ]
+
+    EqFun Mul (Num m _) (Num n _) (Num mn _)  | m * n == mn -> Just []
+    EqFun Mul (Num 0 _) _         (Num 0 _)                 -> Just []
+    EqFun Mul (Num 1 _) s         t           | s == t      -> Just []
+    EqFun Mul r         s         t           | r == s      ->
+                                                Just [ EqFun Exp r (num 2) t ]
+
+    -- Simple normalization of commutative operators
+    EqFun op  r@(Var _) s@(Num _ _) t         | commutative op ->
+                                                Just [ EqFun op s r t ]
+
+    EqFun Exp (Num m _) (Num n _) (Num mn _)  | m ^ n == mn -> Just []
+    EqFun Exp (Num 1 _) _         (Num 1 _)                 -> Just []
+    EqFun Exp _         (Num 0 _) (Num 1 _)                 -> Just []
+    EqFun Exp r         (Num 1 _) t           | r == t      -> Just []
+    EqFun Exp r         (Num _ _) t           | r == t      ->
+                                                Just  [Leq r (num 1)]
+
+    _ -> Nothing
+
+
+solveWanted2 :: Prop -> Prop -> Maybe [Prop]
+solveWanted2 asmp prop =
+  case (asmp, prop) of
+
+    (Leq s1 t1, Leq s2 t2)
+      | s1 == s2 && t1 == t2    -> Just []
+
+    (Leq (Num m _) t1, Leq (Num n _) t2)
+      | t1 == t2 && m >= n      -> Just []
+
+    (Leq s1 (Num m _), Leq s2 (Num n _))
+      | s1 == s2 && m <= n      -> Just []
+
+    (EqFun Add r1 s1 t1, Leq r2 t2)
+      | t1 == t2 && r1 == r2    -> Just []
+      | t1 == t2 && s1 == r2    -> Just []
+
+    -- XXX: others, transitivity
+
+    (EqFun op1 r1 s1 t1, EqFun op2 r2 s2 t2)
+      | op1 == op2 && t1 == t2 &&
+      (  r1 == r2 && s1 == s2
+      || commutative op1 && r1 == s2 && s1 == r2
+      )                         -> Just []
+
+    (EqFun Add (Num m _) b c1, EqFun Add (Num n _) d c2)
+      | c1 == c2 -> if m >= n then Just [ EqFun Add (num (m - n)) b d ]
+                              else Just [ EqFun Add (num (n - m)) d b ]
+
+    (EqFun Mul (Num m _) b c1, EqFun Mul (Num n _) d c2)
+      | c1 == c2, Just x <- divide m n -> Just [ EqFun Mul (num x) b d ]
+      | c1 == c2, Just x <- divide n m -> Just [ EqFun Mul (num x) d b ]
+
+    -- hm:  m * b = c |- c + b = d <=> (m + 1) * b = d
+    (EqFun Mul (Num m _) s1 t1, EqFun Add r2 s2 t2)
+      | t1 == r2 && s1 == s2    -> Just [ EqFun Mul (num (m + 1)) s1 t2 ]
+      | t1 == s2 && s1 == r2    -> Just [ EqFun Mul (num (m + 1)) r2 t2 ]
+
+    _                           -> Nothing
+
+
+
+
+--------------------------------------------------------------------------------
+-- Descrete Math
+--------------------------------------------------------------------------------
+
+descreteRoot :: Integer -> Integer -> Maybe Integer
+descreteRoot root num = search 0 num
+  where
+  search from to = let x = from + div (to - from) 2
+                       a = x ^ root
+                   in case compare a num of
+                        EQ              -> Just x
+                        LT | x /= from  -> search x to
+                        GT | x /= to    -> search from x
+                        _               -> Nothing
+
+descreteLog :: Integer -> Integer -> Maybe Integer
+descreteLog _    0   = Just 0
+descreteLog base num | base == num  = Just 1
+descreteLog base num = case divMod num base of
+                         (x,0) -> fmap (1+) (descreteLog base x)
+                         _     -> Nothing
+
+divide :: Integer -> Integer -> Maybe Integer
+divide _ 0  = Nothing
+divide x y  = case divMod x y of
+                (a,0) -> Just a
+                _     -> Nothing
+
+
+--------------------------------------------------------------------------------
+-- Debugging
+--------------------------------------------------------------------------------
+
+numTrace :: String -> SDoc -> TcS ()
+numTrace x y = traceTcS ("[numerics] " ++ x) y
+
+vmany :: Outputable a => [a] -> SDoc
+vmany xs = braces $ hcat $ punctuate comma $ map ppr xs
+
+instance Outputable Term where
+  ppr (Var xi)  = ppr xi
+  ppr (Num n _) = integer n
+
+instance Outputable Prop where
+  ppr (EqFun op t1 t2 t3) = ppr t1 <+> ppr op <+> ppr t2 <+> char '~' <+> ppr t3
+  ppr (Leq t1 t2)         = ppr t1 <+> text "<=" <+> ppr t2
+  ppr (Eq t1 t2)          = ppr t1 <+> char '~'  <+> ppr t2
+
+instance Outputable Op where
+  ppr op  = case op of
+              Add -> char '+'
+              Mul -> char '*'
+              Exp -> char '^'
+