Generate Typeable info at definition sites
[ghc.git] / compiler / typecheck / TcTypeNats.hs
index 2ff083c..e64f43a 100644 (file)
@@ -1,36 +1,51 @@
 module TcTypeNats
   ( typeNatTyCons
   , typeNatCoAxiomRules
-  , TcBuiltInSynFamily(..)
+  , BuiltInSynFamily(..)
+
+  , typeNatAddTyCon
+  , typeNatMulTyCon
+  , typeNatExpTyCon
+  , typeNatLeqTyCon
+  , typeNatSubTyCon
+  , typeNatCmpTyCon
+  , typeSymbolCmpTyCon
   ) where
 
 import Type
 import Pair
-import TcType     ( TcType )
-import TyCon      ( TyCon, SynTyConRhs(..), mkSynTyCon, TyConParent(..)  )
+import TcType     ( TcType, tcEqType )
+import TyCon      ( TyCon, FamTyConFlav(..), mkFamilyTyCon
+                  , Injectivity(..) )
 import Coercion   ( Role(..) )
 import TcRnTypes  ( Xi )
-import TcEvidence ( mkTcAxiomRuleCo, TcCoercion )
-import CoAxiom    ( CoAxiomRule(..) )
+import CoAxiom    ( CoAxiomRule(..), BuiltInSynFamily(..) )
 import Name       ( Name, BuiltInSyntax(..) )
-import TysWiredIn ( typeNatKind, mkWiredInTyConName
+import TysWiredIn ( typeNatKind, typeSymbolKind
+                  , mkWiredInTyConName
                   , promotedBoolTyCon
                   , promotedFalseDataCon, promotedTrueDataCon
+                  , promotedOrderingTyCon
+                  , promotedLTDataCon
+                  , promotedEQDataCon
+                  , promotedGTDataCon
                   )
-import TysPrim    ( tyVarList, mkArrowKinds )
+import TysPrim    ( mkArrowKinds, mkTemplateTyVars )
 import PrelNames  ( gHC_TYPELITS
                   , typeNatAddTyFamNameKey
                   , typeNatMulTyFamNameKey
                   , typeNatExpTyFamNameKey
                   , typeNatLeqTyFamNameKey
+                  , typeNatSubTyFamNameKey
+                  , typeNatCmpTyFamNameKey
+                  , typeSymbolCmpTyFamNameKey
                   )
-import FamInst    ( TcBuiltInSynFamily(..) )
 import FastString ( FastString, fsLit )
 import qualified Data.Map as Map
 import Data.Maybe ( isJust )
 
 {-------------------------------------------------------------------------------
-Built-in type constructors for functions on type-lelve nats
+Built-in type constructors for functions on type-level nats
 -}
 
 typeNatTyCons :: [TyCon]
@@ -39,11 +54,14 @@ typeNatTyCons =
   , typeNatMulTyCon
   , typeNatExpTyCon
   , typeNatLeqTyCon
+  , typeNatSubTyCon
+  , typeNatCmpTyCon
+  , typeSymbolCmpTyCon
   ]
 
 typeNatAddTyCon :: TyCon
 typeNatAddTyCon = mkTypeNatFunTyCon2 name
-  TcBuiltInSynFamily
+  BuiltInSynFamily
     { sfMatchFam      = matchFamAdd
     , sfInteractTop   = interactTopAdd
     , sfInteractInert = interactInertAdd
@@ -52,9 +70,20 @@ typeNatAddTyCon = mkTypeNatFunTyCon2 name
   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
-  TcBuiltInSynFamily
+  BuiltInSynFamily
     { sfMatchFam      = matchFamMul
     , sfInteractTop   = interactTopMul
     , sfInteractInert = interactInertMul
@@ -65,7 +94,7 @@ typeNatMulTyCon = mkTypeNatFunTyCon2 name
 
 typeNatExpTyCon :: TyCon
 typeNatExpTyCon = mkTypeNatFunTyCon2 name
-  TcBuiltInSynFamily
+  BuiltInSynFamily
     { sfMatchFam      = matchFamExp
     , sfInteractTop   = interactTopExp
     , sfInteractInert = interactInertExp
@@ -76,33 +105,75 @@ typeNatExpTyCon = mkTypeNatFunTyCon2 name
 
 typeNatLeqTyCon :: TyCon
 typeNatLeqTyCon =
-  mkSynTyCon name
+  mkFamilyTyCon name
     (mkArrowKinds [ typeNatKind, typeNatKind ] boolKind)
-    (take 2 $ tyVarList typeNatKind)
-    [Nominal,Nominal]
+    (mkTemplateTyVars [ typeNatKind, typeNatKind ])
+    Nothing
     (BuiltInSynFamTyCon ops)
-    NoParentTyCon
+    Nothing
+    NotInjective
 
   where
   name = mkWiredInTyConName UserSyntax gHC_TYPELITS (fsLit "<=?")
                 typeNatLeqTyFamNameKey typeNatLeqTyCon
-  ops = TcBuiltInSynFamily
+  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
+
+  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 -> TcBuiltInSynFamily -> TyCon
+mkTypeNatFunTyCon2 :: Name -> BuiltInSynFamily -> TyCon
 mkTypeNatFunTyCon2 op tcb =
-  mkSynTyCon op
+  mkFamilyTyCon op
     (mkArrowKinds [ typeNatKind, typeNatKind ] typeNatKind)
-    (take 2 $ tyVarList typeNatKind)
-    [Nominal,Nominal]
+    (mkTemplateTyVars [ typeNatKind, typeNatKind ])
+    Nothing
     (BuiltInSynFamTyCon tcb)
-    NoParentTyCon
-
+    Nothing
+    NotInjective
 
 
 
@@ -116,6 +187,8 @@ axAddDef
   , axMulDef
   , axExpDef
   , axLeqDef
+  , axCmpNatDef
+  , axCmpSymbolDef
   , axAdd0L
   , axAdd0R
   , axMul0L
@@ -126,23 +199,50 @@ axAddDef
   , axExp0R
   , axExp1R
   , axLeqRefl
+  , axCmpNatRefl
+  , axCmpSymbolRefl
   , axLeq0L
+  , axSubDef
+  , axSub0R
   :: CoAxiomRule
 
 axAddDef = mkBinAxiom "AddDef" typeNatAddTyCon $
-              \x y -> num (x + y)
+              \x y -> Just $ num (x + y)
 
-axMulDef = mkBinAxiom "MulDef" typeNatMulTyCon $ 
-              \x y -> num (x * y)
+axMulDef = mkBinAxiom "MulDef" typeNatMulTyCon $
+              \x y -> Just $ num (x * y)
 
 axExpDef = mkBinAxiom "ExpDef" typeNatExpTyCon $
-              \x y -> num (x ^ y)
+              \x y -> Just $ num (x ^ y)
 
 axLeqDef = mkBinAxiom "LeqDef" typeNatLeqTyCon $
-              \x y -> bool (x <= y)
+              \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
@@ -151,6 +251,10 @@ 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
@@ -159,6 +263,8 @@ typeNatCoAxiomRules = Map.fromList $ map (\x -> (coaxrName x, x))
   , axMulDef
   , axExpDef
   , axLeqDef
+  , axCmpNatDef
+  , axCmpSymbolDef
   , axAdd0L
   , axAdd0R
   , axMul0L
@@ -169,7 +275,10 @@ typeNatCoAxiomRules = Map.fromList $ map (\x -> (coaxrName x, x))
   , axExp0R
   , axExp1R
   , axLeqRefl
+  , axCmpNatRefl
+  , axCmpSymbolRefl
   , axLeq0L
+  , axSubDef
   ]
 
 
@@ -181,6 +290,9 @@ 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]
 
@@ -190,6 +302,12 @@ 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
 
@@ -211,6 +329,25 @@ isBoolLitTy tc =
          | 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
@@ -221,7 +358,7 @@ known p x = case isNumLitTy x of
 
 -- For the definitional axioms
 mkBinAxiom :: String -> TyCon ->
-              (Integer -> Integer -> Type) -> CoAxiomRule
+              (Integer -> Integer -> Maybe Type) -> CoAxiomRule
 mkBinAxiom str tc f =
   CoAxiomRule
     { coaxrName      = fsLit str
@@ -232,10 +369,13 @@ mkBinAxiom str tc f =
         case (ts,cs) of
           ([s,t],[]) -> do x <- isNumLitTy s
                            y <- isNumLitTy t
-                           return (mkTyConApp tc [s,t] === f x y)
+                           z <- f x y
+                           return (mkTyConApp tc [s,t] === z)
           _ -> Nothing
     }
 
+
+
 mkAxiom1 :: String -> (Type -> Pair Type) -> CoAxiomRule
 mkAxiom1 str f =
   CoAxiomRule
@@ -254,69 +394,139 @@ mkAxiom1 str f =
 Evaluation
 -------------------------------------------------------------------------------}
 
-matchFamAdd :: [Type] -> Maybe (TcCoercion, TcType)
+matchFamAdd :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
 matchFamAdd [s,t]
-  | Just 0 <- mbX = Just (mkTcAxiomRuleCo axAdd0L [t] [], t)
-  | Just 0 <- mbY = Just (mkTcAxiomRuleCo axAdd0R [s] [], s)
+  | Just 0 <- mbX = Just (axAdd0L, [t], t)
+  | Just 0 <- mbY = Just (axAdd0R, [s], s)
   | Just x <- mbX, Just y <- mbY =
-    Just (mkTcAxiomRuleCo axAddDef [s,t] [], num (x + y))
+    Just (axAddDef, [s,t], num (x + y))
   where mbX = isNumLitTy s
         mbY = isNumLitTy t
 matchFamAdd _ = Nothing
 
-matchFamMul :: [Xi] -> Maybe (TcCoercion, Xi)
+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 (mkTcAxiomRuleCo axMul0L [t] [], num 0)
-  | Just 0 <- mbY = Just (mkTcAxiomRuleCo axMul0R [s] [], num 0)
-  | Just 1 <- mbX = Just (mkTcAxiomRuleCo axMul1L [t] [], t)
-  | Just 1 <- mbY = Just (mkTcAxiomRuleCo axMul1R [s] [], s)
+  | Just 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 (mkTcAxiomRuleCo axMulDef [s,t] [], num (x * y))
+    Just (axMulDef, [s,t], num (x * y))
   where mbX = isNumLitTy s
         mbY = isNumLitTy t
 matchFamMul _ = Nothing
 
-matchFamExp :: [Xi] -> Maybe (TcCoercion, Xi)
+matchFamExp :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
 matchFamExp [s,t]
-  | Just 0 <- mbY = Just (mkTcAxiomRuleCo axExp0R [s] [], num 1)
-  | Just 1 <- mbX = Just (mkTcAxiomRuleCo axExp1L [t] [], num 1)
-  | Just 1 <- mbY = Just (mkTcAxiomRuleCo axExp1R [s] [], s)
+  | Just 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 (mkTcAxiomRuleCo axExpDef [s,t] [], num (x ^ y))
+    Just (axExpDef, [s,t], num (x ^ y))
   where mbX = isNumLitTy s
         mbY = isNumLitTy t
 matchFamExp _ = Nothing
 
-matchFamLeq :: [Xi] -> Maybe (TcCoercion, Xi)
+matchFamLeq :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
 matchFamLeq [s,t]
-  | Just 0 <- mbX = Just (mkTcAxiomRuleCo axLeq0L [t] [], bool True)
+  | Just 0 <- mbX = Just (axLeq0L, [t], bool True)
   | Just x <- mbX, Just y <- mbY =
-    Just (mkTcAxiomRuleCo axLeqDef [s,t] [], bool (x <= y))
-  | eqType s t  = Just (mkTcAxiomRuleCo axLeqRefl [s] [], bool True)
+    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 ]
-  | Just x <- mbX, Just z <- mbZ, Just y <- minus z x = [t === num y]
-  | Just y <- mbY, Just z <- mbZ, Just x <- minus z y = [s === num x]
+  | 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 _ _ = []
 
+{-
+Note [Weakened interaction rule for subtraction]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+A simpler interaction here might be:
+
+  `s - t ~ r` --> `t + r ~ s`
+
+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:
+
+    0 - 5 ~ r --> 5 + r ~ 0 --> (5 = 0, r = 0)
+
+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:
+
+f :: Proxy (If (5 <=? 0) (0 - 5) (5 - 0)) -> Proxy 5
+f = id
+
+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.
+
+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 _ _ = []
+
+
+
+
+
 interactTopMul :: [Xi] -> Xi -> [Pair Type]
 interactTopMul [s,t] r
-  | Just 1 <- mbZ = [ s === num 1, t === num 1 ]
-  | Just x <- mbX, Just z <- mbZ, Just y <- divide z x = [t === num y]
-  | Just y <- mbY, Just z <- mbZ, Just x <- divide z y = [s === num x]
+  | 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
@@ -325,9 +535,9 @@ interactTopMul _ _ = []
 
 interactTopExp :: [Xi] -> Xi -> [Pair Type]
 interactTopExp [s,t] r
-  | Just 0 <- mbZ = [ s === num 0 ]
-  | Just x <- mbX, Just z <- mbZ, Just y <- logExact  z x = [t === num y]
-  | Just y <- mbY, Just z <- mbZ, Just x <- rootExact z y = [s === num x]
+  | 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
@@ -336,12 +546,23 @@ interactTopExp _ _ = []
 
 interactTopLeq :: [Xi] -> Xi -> [Pair Type]
 interactTopLeq [s,t] r
-  | Just 0 <- mbY, Just True <- mbZ = [ s === num 0 ]
+  | Just 0 <- mbY, Just True <- mbZ = [ s === num 0 ]                     -- (s <= 0) => (s ~ 0)
   where
   mbY = isNumLitTy t
   mbZ = isBoolLitTy r
 interactTopLeq _ _ = []
 
+interactTopCmpNat :: [Xi] -> Xi -> [Pair Type]
+interactTopCmpNat [s,t] r
+  | Just EQ <- isOrderingLitTy r = [ s === t ]
+interactTopCmpNat _ _ = []
+
+interactTopCmpSymbol :: [Xi] -> Xi -> [Pair Type]
+interactTopCmpSymbol [s,t] r
+  | Just EQ <- isOrderingLitTy r = [ s === t ]
+interactTopCmpSymbol _ _ = []
+
+
 
 
 {-------------------------------------------------------------------------------
@@ -350,33 +571,40 @@ Interaction with inerts
 
 interactInertAdd :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type]
 interactInertAdd [x1,y1] z1 [x2,y2] z2
-  | sameZ && eqType x1 x2         = [ y1 === y2 ]
-  | sameZ && eqType y1 y2         = [ x1 === x2 ]
-  where sameZ = eqType z1 z2
+  | sameZ && tcEqType x1 x2         = [ y1 === y2 ]
+  | sameZ && tcEqType y1 y2         = [ x1 === x2 ]
+  where sameZ = tcEqType z1 z2
 interactInertAdd _ _ _ _ = []
 
+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 _ _ _ _ = []
+
 interactInertMul :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type]
 interactInertMul [x1,y1] z1 [x2,y2] z2
-  | sameZ && known (/= 0) x1 && eqType x1 x2 = [ y1 === y2 ]
-  | sameZ && known (/= 0) y1 && eqType y1 y2 = [ x1 === x2 ]
-  where sameZ   = eqType z1 z2
+  | sameZ && known (/= 0) x1 && tcEqType x1 x2 = [ y1 === y2 ]
+  | sameZ && known (/= 0) y1 && tcEqType y1 y2 = [ x1 === x2 ]
+  where sameZ   = tcEqType z1 z2
 
 interactInertMul _ _ _ _ = []
 
 interactInertExp :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type]
 interactInertExp [x1,y1] z1 [x2,y2] z2
-  | sameZ && known (> 1) x1 && eqType x1 x2 = [ y1 === y2 ]
-  | sameZ && known (> 0) y1 && eqType y1 y2 = [ x1 === x2 ]
-  where sameZ = eqType z1 z2
+  | sameZ && known (> 1) x1 && tcEqType x1 x2 = [ y1 === y2 ]
+  | sameZ && known (> 0) y1 && tcEqType y1 y2 = [ x1 === x2 ]
+  where sameZ = tcEqType z1 z2
 
 interactInertExp _ _ _ _ = []
 
 
 interactInertLeq :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type]
 interactInertLeq [x1,y1] z1 [x2,y2] z2
-  | bothTrue && eqType x1 y2 && eqType y1 x2 = [ x1 === y1 ]
-  | bothTrue && eqType y1 x2                 = [ (x1 <== y2) === bool True ]
-  | bothTrue && eqType y2 x1                 = [ (x2 <== y1) === bool True ]
+  | 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 ()
@@ -386,6 +614,10 @@ interactInertLeq _ _ _ _ = []
 
 
 
+
+
+
+
 {- -----------------------------------------------------------------------------
 These inverse functions are used for simplifying propositions using
 concrete natural numbers.