Generate Typeable info at definition sites
[ghc.git] / compiler / typecheck / TcTypeNats.hs
index baf3c02..e64f43a 100644 (file)
-{-# LANGUAGE PatternGuards #-}
-module TcTypeNats (solveNumWanted, addNumGiven) where
-
-import TcSMonad   ( TcS, Xi
-                  , newWantedCoVar
-                  , setWantedCoBind, setDictBind, newDictVar
-                  , tcsLookupTyCon, tcsLookupClass
-                  , CanonicalCt (..), CanonicalCts
-                  , traceTcS
+module TcTypeNats
+  ( typeNatTyCons
+  , typeNatCoAxiomRules
+  , BuiltInSynFamily(..)
+
+  , typeNatAddTyCon
+  , typeNatMulTyCon
+  , typeNatExpTyCon
+  , typeNatLeqTyCon
+  , typeNatSubTyCon
+  , typeNatCmpTyCon
+  , typeSymbolCmpTyCon
+  ) where
+
+import Type
+import Pair
+import TcType     ( TcType, tcEqType )
+import TyCon      ( TyCon, FamTyConFlav(..), mkFamilyTyCon
+                  , Injectivity(..) )
+import Coercion   ( Role(..) )
+import TcRnTypes  ( Xi )
+import CoAxiom    ( CoAxiomRule(..), BuiltInSynFamily(..) )
+import Name       ( Name, BuiltInSyntax(..) )
+import TysWiredIn ( typeNatKind, typeSymbolKind
+                  , mkWiredInTyConName
+                  , promotedBoolTyCon
+                  , promotedFalseDataCon, promotedTrueDataCon
+                  , promotedOrderingTyCon
+                  , promotedLTDataCon
+                  , promotedEQDataCon
+                  , promotedGTDataCon
                   )
-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 TysPrim    ( mkArrowKinds, mkTemplateTyVars )
+import PrelNames  ( gHC_TYPELITS
+                  , typeNatAddTyFamNameKey
+                  , typeNatMulTyFamNameKey
+                  , typeNatExpTyFamNameKey
+                  , typeNatLeqTyFamNameKey
+                  , typeNatSubTyFamNameKey
+                  , typeNatCmpTyFamNameKey
+                  , typeSymbolCmpTyFamNameKey
                   )
-import Bag        (bagToList, emptyBag, unionBags)
-import Data.Maybe (fromMaybe)
-import Data.List  (nub, partition)
-import Control.Monad (msum, mplus, zipWithM, (<=<), guard)
-
-
-
-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
-
-associative :: Op -> Bool
-associative 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
+import FastString ( FastString, fsLit )
+import qualified Data.Map as Map
+import Data.Maybe ( isJust )
+
+{-------------------------------------------------------------------------------
+Built-in type constructors for functions on type-level nats
+-}
+
+typeNatTyCons :: [TyCon]
+typeNatTyCons =
+  [ typeNatAddTyCon
+  , typeNatMulTyCon
+  , typeNatExpTyCon
+  , typeNatLeqTyCon
+  , typeNatSubTyCon
+  , typeNatCmpTyCon
+  , typeSymbolCmpTyCon
+  ]
+
+typeNatAddTyCon :: TyCon
+typeNatAddTyCon = mkTypeNatFunTyCon2 name
+  BuiltInSynFamily
+    { sfMatchFam      = matchFamAdd
+    , sfInteractTop   = interactTopAdd
+    , sfInteractInert = interactInertAdd
+    }
+  where
+  name = mkWiredInTyConName UserSyntax gHC_TYPELITS (fsLit "+")
+            typeNatAddTyFamNameKey typeNatAddTyCon
+
+typeNatSubTyCon :: TyCon
+typeNatSubTyCon = mkTypeNatFunTyCon2 name
+  BuiltInSynFamily
+    { sfMatchFam      = matchFamSub
+    , sfInteractTop   = interactTopSub
+    , sfInteractInert = interactInertSub
+    }
+  where
+  name = mkWiredInTyConName UserSyntax gHC_TYPELITS (fsLit "-")
+            typeNatSubTyFamNameKey typeNatSubTyCon
+
+typeNatMulTyCon :: TyCon
+typeNatMulTyCon = mkTypeNatFunTyCon2 name
+  BuiltInSynFamily
+    { sfMatchFam      = matchFamMul
+    , sfInteractTop   = interactTopMul
+    , sfInteractInert = interactInertMul
+    }
+  where
+  name = mkWiredInTyConName UserSyntax gHC_TYPELITS (fsLit "*")
+            typeNatMulTyFamNameKey typeNatMulTyCon
+
+typeNatExpTyCon :: TyCon
+typeNatExpTyCon = mkTypeNatFunTyCon2 name
+  BuiltInSynFamily
+    { sfMatchFam      = matchFamExp
+    , sfInteractTop   = interactTopExp
+    , sfInteractInert = interactInertExp
+    }
+  where
+  name = mkWiredInTyConName UserSyntax gHC_TYPELITS (fsLit "^")
+                typeNatExpTyFamNameKey typeNatExpTyCon
+
+typeNatLeqTyCon :: TyCon
+typeNatLeqTyCon =
+  mkFamilyTyCon name
+    (mkArrowKinds [ typeNatKind, typeNatKind ] boolKind)
+    (mkTemplateTyVars [ typeNatKind, typeNatKind ])
+    Nothing
+    (BuiltInSynFamTyCon ops)
+    Nothing
+    NotInjective
 
-    where t1 = toTerm xi11
-          t2 = toTerm xi12
-          t3 = toTerm xi2
+  where
+  name = mkWiredInTyConName UserSyntax gHC_TYPELITS (fsLit "<=?")
+                typeNatLeqTyFamNameKey typeNatLeqTyCon
+  ops = BuiltInSynFamily
+    { sfMatchFam      = matchFamLeq
+    , sfInteractTop   = interactTopLeq
+    , sfInteractInert = interactInertLeq
+    }
+
+typeNatCmpTyCon :: TyCon
+typeNatCmpTyCon =
+  mkFamilyTyCon name
+    (mkArrowKinds [ typeNatKind, typeNatKind ] orderingKind)
+    (mkTemplateTyVars [ typeNatKind, typeNatKind ])
+    Nothing
+    (BuiltInSynFamTyCon ops)
+    Nothing
+    NotInjective
 
-toProp p = panic $
-  "[TcTypeNats.toProp] Unexpected CanonicalCt: " ++ showSDoc (ppr p)
+  where
+  name = mkWiredInTyConName UserSyntax gHC_TYPELITS (fsLit "CmpNat")
+                typeNatCmpTyFamNameKey typeNatCmpTyCon
+  ops = BuiltInSynFamily
+    { sfMatchFam      = matchFamCmpNat
+    , sfInteractTop   = interactTopCmpNat
+    , sfInteractInert = \_ _ _ _ -> []
+    }
+
+typeSymbolCmpTyCon :: TyCon
+typeSymbolCmpTyCon =
+  mkFamilyTyCon name
+    (mkArrowKinds [ typeSymbolKind, typeSymbolKind ] orderingKind)
+    (mkTemplateTyVars [ typeSymbolKind, typeSymbolKind ])
+    Nothing
+    (BuiltInSynFamTyCon ops)
+    Nothing
+    NotInjective
 
+  where
+  name = mkWiredInTyConName UserSyntax gHC_TYPELITS (fsLit "CmpSymbol")
+                typeSymbolCmpTyFamNameKey typeSymbolCmpTyCon
+  ops = BuiltInSynFamily
+    { sfMatchFam      = matchFamCmpSymbol
+    , sfInteractTop   = interactTopCmpSymbol
+    , sfInteractInert = \_ _ _ _ -> []
+    }
+
+
+
+
+
+-- Make a binary built-in constructor of kind: Nat -> Nat -> Nat
+mkTypeNatFunTyCon2 :: Name -> BuiltInSynFamily -> TyCon
+mkTypeNatFunTyCon2 op tcb =
+  mkFamilyTyCon op
+    (mkArrowKinds [ typeNatKind, typeNatKind ] typeNatKind)
+    (mkTemplateTyVars [ typeNatKind, typeNatKind ])
+    Nothing
+    (BuiltInSynFamTyCon tcb)
+    Nothing
+    NotInjective
+
+
+
+{-------------------------------------------------------------------------------
+Built-in rules axioms
+-------------------------------------------------------------------------------}
+
+-- If you add additional rules, please remember to add them to
+-- `typeNatCoAxiomRules` also.
+axAddDef
+  , axMulDef
+  , axExpDef
+  , axLeqDef
+  , axCmpNatDef
+  , axCmpSymbolDef
+  , axAdd0L
+  , axAdd0R
+  , axMul0L
+  , axMul0R
+  , axMul1L
+  , axMul1R
+  , axExp1L
+  , axExp0R
+  , axExp1R
+  , axLeqRefl
+  , axCmpNatRefl
+  , axCmpSymbolRefl
+  , axLeq0L
+  , axSubDef
+  , axSub0R
+  :: CoAxiomRule
+
+axAddDef = mkBinAxiom "AddDef" typeNatAddTyCon $
+              \x y -> Just $ num (x + y)
+
+axMulDef = mkBinAxiom "MulDef" typeNatMulTyCon $
+              \x y -> Just $ num (x * y)
+
+axExpDef = mkBinAxiom "ExpDef" typeNatExpTyCon $
+              \x y -> Just $ num (x ^ y)
+
+axLeqDef = mkBinAxiom "LeqDef" typeNatLeqTyCon $
+              \x y -> Just $ bool (x <= y)
+
+axCmpNatDef   = mkBinAxiom "CmpNatDef" typeNatCmpTyCon
+              $ \x y -> Just $ ordering (compare x y)
+
+axCmpSymbolDef =
+  CoAxiomRule
+    { coaxrName      = fsLit "CmpSymbolDef"
+    , coaxrTypeArity = 2
+    , coaxrAsmpRoles = []
+    , coaxrRole      = Nominal
+    , coaxrProves    = \ts cs ->
+        case (ts,cs) of
+          ([s,t],[]) ->
+            do x <- isStrLitTy s
+               y <- isStrLitTy t
+               return (mkTyConApp typeSymbolCmpTyCon [s,t] ===
+                      ordering (compare x y))
+          _ -> Nothing
+    }
+
+axSubDef = mkBinAxiom "SubDef" typeNatSubTyCon $
+              \x y -> fmap num (minus x y)
+
+axAdd0L     = mkAxiom1 "Add0L"    $ \t -> (num 0 .+. t) === t
+axAdd0R     = mkAxiom1 "Add0R"    $ \t -> (t .+. num 0) === t
+axSub0R     = mkAxiom1 "Sub0R"    $ \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
+axCmpNatRefl    = mkAxiom1 "CmpNatRefl"
+                $ \t -> (cmpNat t t) === ordering EQ
+axCmpSymbolRefl = mkAxiom1 "CmpSymbolRefl"
+                $ \t -> (cmpSymbol t t) === ordering EQ
+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
+  , axCmpNatDef
+  , axCmpSymbolDef
+  , axAdd0L
+  , axAdd0R
+  , axMul0L
+  , axMul0R
+  , axMul1L
+  , axMul1R
+  , axExp1L
+  , axExp0R
+  , axExp1R
+  , axLeqRefl
+  , axCmpNatRefl
+  , axCmpSymbolRefl
+  , axLeq0L
+  , axSubDef
+  ]
+
+
+
+{-------------------------------------------------------------------------------
+Various utilities for making axioms and types
+-------------------------------------------------------------------------------}
+
+(.+.) :: Type -> Type -> Type
+s .+. t = mkTyConApp typeNatAddTyCon [s,t]
+
+(.-.) :: Type -> Type -> Type
+s .-. t = mkTyConApp typeNatSubTyCon [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]
+
+cmpNat :: Type -> Type -> Type
+cmpNat s t = mkTyConApp typeNatCmpTyCon [s,t]
+
+cmpSymbol :: Type -> Type -> Type
+cmpSymbol s t = mkTyConApp typeSymbolCmpTyCon [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
+
+orderingKind :: Kind
+orderingKind = mkTyConApp promotedOrderingTyCon []
+
+ordering :: Ordering -> Type
+ordering o =
+  case o of
+    LT -> mkTyConApp promotedLTDataCon []
+    EQ -> mkTyConApp promotedEQDataCon []
+    GT -> mkTyConApp promotedGTDataCon []
+
+isOrderingLitTy :: Type -> Maybe Ordering
+isOrderingLitTy tc =
+  do (tc1,[]) <- splitTyConApp_maybe tc
+     case () of
+       _ | tc1 == promotedLTDataCon -> return LT
+         | tc1 == promotedEQDataCon -> return EQ
+         | tc1 == promotedGTDataCon -> return GT
+         | 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 -> Maybe 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
+                           z <- f x y
+                           return (mkTyConApp tc [s,t] === z)
+          _ -> 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 (CoAxiomRule, [Type], Type)
+matchFamAdd [s,t]
+  | Just 0 <- mbX = Just (axAdd0L, [t], t)
+  | Just 0 <- mbY = Just (axAdd0R, [s], s)
+  | Just x <- mbX, Just y <- mbY =
+    Just (axAddDef, [s,t], num (x + y))
+  where mbX = isNumLitTy s
+        mbY = isNumLitTy t
+matchFamAdd _ = Nothing
+
+matchFamSub :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
+matchFamSub [s,t]
+  | Just 0 <- mbY = Just (axSub0R, [s], s)
+  | Just x <- mbX, Just y <- mbY, Just z <- minus x y =
+    Just (axSubDef, [s,t], num z)
+  where mbX = isNumLitTy s
+        mbY = isNumLitTy t
+matchFamSub _ = Nothing
+
+matchFamMul :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
+matchFamMul [s,t]
+  | Just 0 <- mbX = Just (axMul0L, [t], num 0)
+  | Just 0 <- mbY = Just (axMul0R, [s], num 0)
+  | Just 1 <- mbX = Just (axMul1L, [t], t)
+  | Just 1 <- mbY = Just (axMul1R, [s], s)
+  | Just x <- mbX, Just y <- mbY =
+    Just (axMulDef, [s,t], num (x * y))
+  where mbX = isNumLitTy s
+        mbY = isNumLitTy t
+matchFamMul _ = Nothing
+
+matchFamExp :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
+matchFamExp [s,t]
+  | Just 0 <- mbY = Just (axExp0R, [s], num 1)
+  | Just 1 <- mbX = Just (axExp1L, [t], num 1)
+  | Just 1 <- mbY = Just (axExp1R, [s], s)
+  | Just x <- mbX, Just y <- mbY =
+    Just (axExpDef, [s,t], num (x ^ y))
+  where mbX = isNumLitTy s
+        mbY = isNumLitTy t
+matchFamExp _ = Nothing
+
+matchFamLeq :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
+matchFamLeq [s,t]
+  | Just 0 <- mbX = Just (axLeq0L, [t], bool True)
+  | Just x <- mbX, Just y <- mbY =
+    Just (axLeqDef, [s,t], bool (x <= y))
+  | tcEqType s t  = Just (axLeqRefl, [s], bool True)
+  where mbX = isNumLitTy s
+        mbY = isNumLitTy t
+matchFamLeq _ = Nothing
+
+matchFamCmpNat :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
+matchFamCmpNat [s,t]
+  | Just x <- mbX, Just y <- mbY =
+    Just (axCmpNatDef, [s,t], ordering (compare x y))
+  | tcEqType s t = Just (axCmpNatRefl, [s], ordering EQ)
+  where mbX = isNumLitTy s
+        mbY = isNumLitTy t
+matchFamCmpNat _ = Nothing
+
+matchFamCmpSymbol :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
+matchFamCmpSymbol [s,t]
+  | Just x <- mbX, Just y <- mbY =
+    Just (axCmpSymbolDef, [s,t], ordering (compare x y))
+  | tcEqType s t = Just (axCmpSymbolRefl, [s], ordering EQ)
+  where mbX = isStrLitTy s
+        mbY = isStrLitTy t
+matchFamCmpSymbol _ = Nothing
+
+
+{-------------------------------------------------------------------------------
+Interact with axioms
+-------------------------------------------------------------------------------}
+
+interactTopAdd :: [Xi] -> Xi -> [Pair Type]
+interactTopAdd [s,t] r
+  | Just 0 <- mbZ = [ s === num 0, t === num 0 ]                          -- (s + t ~ 0) => (s ~ 0, t ~ 0)
+  | Just x <- mbX, Just z <- mbZ, Just y <- minus z x = [t === num y]     -- (5 + t ~ 8) => (t ~ 3)
+  | Just y <- mbY, Just z <- mbZ, Just x <- minus z y = [s === num x]     -- (s + 5 ~ 8) => (s ~ 3)
+  where
+  mbX = isNumLitTy s
+  mbY = isNumLitTy t
+  mbZ = isNumLitTy r
+interactTopAdd _ _ = []
 
-solveNumWanted :: CanonicalCts -> CanonicalCts -> CanonicalCt ->
-                TcS (Maybe CanonicalCt, CanonicalCts)
-solveNumWanted given wanted prop =
-  do let asmps = map toProp $ bagToList $ unionBags given wanted
-         goal  = toProp prop
+{-
+Note [Weakened interaction rule for subtraction]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-     numTrace "solveNumWanted" (vmany asmps <+> text "|-" <+> ppr goal)
+A simpler interaction here might be:
 
-     case solve asmps goal of
+  `s - t ~ r` --> `t + r ~ s`
 
-       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)
+This would enable us to reuse all the code for addition.
+Unfortunately, this works a little too well at the moment.
+Consider the following example:
 
-       -- 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)
+    0 - 5 ~ r --> 5 + r ~ 0 --> (5 = 0, r = 0)
 
-       -- XXX: Report an error
-       Impossible ->
-         do numTrace "Impssoble" empty
-            return (Just prop, emptyBag)
+This (correctly) spots that the constraint cannot be solved.
 
+However, this may be a problem if the constraint did not
+need to be solved in the first place!  Consider the following example:
 
-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
+f :: Proxy (If (5 <=? 0) (0 - 5) (5 - 0)) -> Proxy 5
+f = id
 
-     numTrace "addNumGiven" (vmany asmps <+> text " /\\ " <+> ppr goal)
-     case solve asmps goal of
+Currently, GHC is strict while evaluating functions, so this does not
+work, because even though the `If` should evaluate to `5 - 0`, we
+also evaluate the "then" branch which generates the constraint `0 - 5 ~ r`,
+which fails.
 
-       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)
+So, for the time being, we only add an improvement when the RHS is a constant,
+which happens to work OK for the moment, although clearly we need to do
+something more general.
+-}
+interactTopSub :: [Xi] -> Xi -> [Pair Type]
+interactTopSub [s,t] r
+  | Just z <- mbZ = [ s === (num z .+. t) ]         -- (s - t ~ 5) => (5 + t ~ s)
+  where
+  mbZ = isNumLitTy r
+interactTopSub _ _ = []
 
-       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
+interactTopMul :: [Xi] -> Xi -> [Pair Type]
+interactTopMul [s,t] r
+  | Just 1 <- mbZ = [ s === num 1, t === num 1 ]                        -- (s * t ~ 1)  => (s ~ 1, t ~ 1)
+  | Just x <- mbX, Just z <- mbZ, Just y <- divide z x = [t === num y]  -- (3 * t ~ 15) => (t ~ 5)
+  | Just y <- mbY, Just z <- mbZ, Just x <- divide z y = [s === num x]  -- (s * 3 ~ 15) => (s ~ 5)
+  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 ]                                       -- (s ^ t ~ 0) => (s ~ 0)
+  | Just x <- mbX, Just z <- mbZ, Just y <- logExact  z x = [t === num y] -- (2 ^ t ~ 8) => (t ~ 3)
+  | Just y <- mbY, Just z <- mbZ, Just x <- rootExact z y = [s === num x] -- (s ^ 2 ~ 9) => (s ~ 3)
+  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 ]                     -- (s <= 0) => (s ~ 0)
+  where
+  mbY = isNumLitTy t
+  mbZ = isBoolLitTy r
+interactTopLeq _ _ = []
 
-fromProp :: Prop -> TcS CvtProp
-fromProp (Leq t1 t2) =
-  do cl <- tcsLookupClass lessThanEqualClassName
-     return (CvtClass cl [ fromTerm t1, fromTerm t2 ])
+interactTopCmpNat :: [Xi] -> Xi -> [Pair Type]
+interactTopCmpNat [s,t] r
+  | Just EQ <- isOrderingLitTy r = [ s === t ]
+interactTopCmpNat _ _ = []
 
-fromProp (Eq t1 t2) = return $ CvtCo (fromTerm t1) (fromTerm t2)
+interactTopCmpSymbol :: [Xi] -> Xi -> [Pair Type]
+interactTopCmpSymbol [s,t] r
+  | Just EQ <- isOrderingLitTy r = [ s === t ]
+interactTopCmpSymbol _ _ = []
 
-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
+{-------------------------------------------------------------------------------
+Interaction with inerts
+-------------------------------------------------------------------------------}
 
+interactInertAdd :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type]
+interactInertAdd [x1,y1] z1 [x2,y2] z2
+  | sameZ && tcEqType x1 x2         = [ y1 === y2 ]
+  | sameZ && tcEqType y1 y2         = [ x1 === x2 ]
+  where sameZ = tcEqType z1 z2
+interactInertAdd _ _ _ _ = []
 
--- 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
+interactInertSub :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type]
+interactInertSub [x1,y1] z1 [x2,y2] z2
+  | sameZ && tcEqType x1 x2         = [ y1 === y2 ]
+  | sameZ && tcEqType y1 y2         = [ x1 === x2 ]
+  where sameZ = tcEqType z1 z2
+interactInertSub _ _ _ _ = []
 
-defineDummy c (CvtCo t1 t2) =
-  setWantedCoBind c $ mkUnsafeCoercion t1 t2
-
-
-
-
---------------------------------------------------------------------------------
--- The Solver
---------------------------------------------------------------------------------
+interactInertMul :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type]
+interactInertMul [x1,y1] z1 [x2,y2] z2
+  | sameZ && known (/= 0) x1 && tcEqType x1 x2 = [ y1 === y2 ]
+  | sameZ && known (/= 0) y1 && tcEqType y1 y2 = [ x1 === x2 ]
+  where sameZ   = tcEqType z1 z2
 
+interactInertMul _ _ _ _ = []
 
-data Result = Impossible            -- We know that the goal cannot be solved.
-            | Simplified [Prop]     -- We reformulated the goal.
-            | Improved   [Prop]     -- We learned some new facts.
+interactInertExp :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type]
+interactInertExp [x1,y1] z1 [x2,y2] z2
+  | sameZ && known (> 1) x1 && tcEqType x1 x2 = [ y1 === y2 ]
+  | sameZ && known (> 0) y1 && tcEqType y1 y2 = [ x1 === x2 ]
+  where sameZ = tcEqType z1 z2
 
-solve :: [Prop] -> Prop -> Result
-solve asmps (Leq a b) =
-  let ps = propsToOrd asmps
-  in case isLeq ps a b of
-       True  -> Simplified []
-       False ->
-         case improveLeq ps a b of
-           Nothing -> Impossible
-           Just ps -> Improved ps
-
-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))
+interactInertExp _ _ _ _ = []
 
 
+interactInertLeq :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type]
+interactInertLeq [x1,y1] z1 [x2,y2] z2
+  | bothTrue && tcEqType x1 y2 && tcEqType y1 x2 = [ x1 === y1 ]
+  | bothTrue && tcEqType y1 x2                 = [ (x1 <== y2) === bool True ]
+  | bothTrue && tcEqType y2 x1                 = [ (x2 <== y1) === bool True ]
+  where bothTrue = isJust $ do True <- isBoolLitTy z1
+                               True <- isBoolLitTy z2
+                               return ()
 
+interactInertLeq _ _ _ _ = []
 
-improve1 :: Prop -> Maybe [Prop]
-improve1 prop =
-  case prop of
 
-    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
-
-    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
-
-    (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
-
-
---------------------------------------------------------------------------------
--- Reasoning about ordering.
---------------------------------------------------------------------------------
-
--- This function assumes that the assumptions are acyclic.
-isLeq :: [(Term, Term)] -> Term -> Term -> Bool
-isLeq _ (Num 0 _) _         = True
-isLeq _ (Num m _) (Num n _) = m <= n
-isLeq _ a b | a == b        = True
-isLeq ps (Num m _) a        = or [ isLeq ps b a  | (Num x _, b) <- ps, m <= x ]
-isLeq ps a (Num m _)        = or [ isLeq ps a b  | (b, Num x _) <- ps, x <= m ]
-isLeq ps a b                = or [ isLeq ps c b  | (a',c)       <- ps, a == a' ]
-
-isGt :: [(Term, Term)] -> Term -> Term -> Bool
-isGt _ (Num m _) (Num n _)  = m > n
-isGt ps (Num m _) a         = (m > 0) && isLeq ps a (num (m - 1))
-isGt ps a (Num m _)         = isLeq ps (num (m + 1)) a
-isGt _ _ _                  = False
-
-improveLeq :: [(Term,Term)] -> Term -> Term -> Maybe [Prop]
-improveLeq ps a b | isLeq ps b a  = Just [Eq a b]
-                  | isGt ps a b   = Nothing
-                  | otherwise     = Just []
-
--- Ordering constraints derived from numeric predicates.
--- We do not consider equlities because they should be substituted away.
-propsToOrd :: [Prop] -> [(Term,Term)]
-propsToOrd props = loop (step [] unconditional)
-  where
-  loop ps = let new = filter (`notElem` ps) (step ps conditional)
-            in if null new then ps else loop (new ++ ps)
-
-  step ps = nub . concatMap (toOrd ps)
-
-  isConditional (EqFun op _ _ _)  = op == Mul || op == Exp
-  isConditional _                 = False
-
-  (conditional,unconditional)     = partition isConditional props
-
-  toOrd _ (Leq a b) = [(a,b)]
-  toOrd _ (Eq _ _)  = []      -- Would lead to a cycle, should be subst. away
-  toOrd ps (EqFun op a b c) =
-    case op of
-      Add               -> [(a,c),(b,c)]
-
-      Mul               -> (guard (isLeq ps (num 1) a) >> return (b,c)) ++
-                           (guard (isLeq ps (num 1) b) >> return (a,c))
-      Exp
-        | Num 0 _ <- a  -> [(c, num 1)]
-        | a == c        -> [(a, num 1)]
-        | otherwise     -> (guard (isLeq ps (num 2) a) >> return (b,c)) ++
-                           (guard (isLeq ps (num 1) b) >> return (a,c))
-
---------------------------------------------------------------------------------
--- Associativity
---------------------------------------------------------------------------------
-
--- We try to compute new equalities by moving parens to the right:
--- if (a + b) + c = d then a + (b + c) = d
---
--- This desugars to:
---   a + b = p, p + c = q, b + c = r  => a + r = q
---
--- Note that this fires only if we have a name, r, for the right-paren sum,
--- or if we can compute it.
--- a + 2 = p, p + 3 = q => a + 5 = q
---
--- So, when we add a new fact it could match any of the 3 positions
--- in the RHS of this rule.
-
-impAssoc :: [Prop] -> Prop -> [Prop]
-impAssoc ps (EqFun op x y z) | associative op = concatMap imps asmps
-  where
-  asmps         = [ (a,b,c) | EqFun op' a b c <- ps, op == op' ]
-  imps (a,b,c)
-    -- new in position 2
-    | c == x    = [ EqFun op a by z | by <- y_plus b ]
+{- -----------------------------------------------------------------------------
+These inverse functions are used for simplifying propositions using
+concrete natural numbers.
+----------------------------------------------------------------------------- -}
 
-    -- new in position 1
-    | a == z    = [ EqFun op x yb c | yb <- y_plus b ]
+-- | Subtract two natural numbers.
+minus :: Integer -> Integer -> Maybe Integer
+minus x y = if x >= y then Just (x - y) else Nothing
 
-    -- new in position 3
-    | otherwise = [ EqFun op a z e | (c',d,e) <- asmps,
-                                              c == c' && sameSum b d x y ]
-                  ++
-                  [ EqFun op d z c | (d,e,a') <- asmps,
-                                              a == a' && sameSum e b x y ]
+-- | 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
 
-  sameSum a b a' b' = (a == a' && b == b') || (a == b' && b == a')
 
-  y_plus (Num m _) | Num n _ <- y = doOp m n
-  y_plus b                        = [ w | (u,v,w) <- asmps, sameSum y b u v ]
+-- | 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
 
-  doOp m n          = case op of
-                        Add -> [ num (m + n) ]
-                        Mul -> [ num (m * n) ]
-                        _   -> []
+-- | 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
 
-impAssoc _ _ = []
 
---------------------------------------------------------------------------------
--- Descrete Math
---------------------------------------------------------------------------------
 
-descreteRoot :: Integer -> Integer -> Maybe Integer
-descreteRoot root num = search 0 num
+{- | 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 num of
-                        EQ              -> Just x
+                   in case compare a x0 of
+                        EQ              -> (x, True)
                         LT | x /= from  -> search x to
+                           | otherwise  -> (from, False)
                         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
+                           | 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)
 
---------------------------------------------------------------------------------
--- 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 '^'