Add a type-function for subtraction.

This is used in the definition of `ToNat1` in the `base` library
(module GHC.TypeLits).

2 files changed, 59 insertions, 8 deletions

diff --git a/compiler/prelude/PrelNames.lhs b/compiler/prelude/PrelNames.lhs
index 07730e653d..453f554ef4 100644
--- a/compiler/prelude/PrelNames.lhs
+++ b/compiler/prelude/PrelNames.lhs
@@ -1465,7 +1465,7 @@ rep1TyConKey = mkPreludeTyConUnique 156
 -- Type-level naturals
 typeNatKindConNameKey, typeSymbolKindConNameKey,
   typeNatAddTyFamNameKey, typeNatMulTyFamNameKey, typeNatExpTyFamNameKey,
-  typeNatLeqTyFamNameKey
+  typeNatLeqTyFamNameKey, typeNatSubTyFamNameKey
   :: Unique
 typeNatKindConNameKey     = mkPreludeTyConUnique 160
 typeSymbolKindConNameKey  = mkPreludeTyConUnique 161
@@ -1473,6 +1473,7 @@ typeNatAddTyFamNameKey    = mkPreludeTyConUnique 162
 typeNatMulTyFamNameKey    = mkPreludeTyConUnique 163
 typeNatExpTyFamNameKey    = mkPreludeTyConUnique 164
 typeNatLeqTyFamNameKey    = mkPreludeTyConUnique 165
+typeNatSubTyFamNameKey    = mkPreludeTyConUnique 166
 
 ntTyConKey:: Unique
 ntTyConKey = mkPreludeTyConUnique 174
diff --git a/compiler/typecheck/TcTypeNats.hs b/compiler/typecheck/TcTypeNats.hs
index 2ff083c418..7961df4a7d 100644
--- a/compiler/typecheck/TcTypeNats.hs
+++ b/compiler/typecheck/TcTypeNats.hs
@@ -23,6 +23,7 @@ import PrelNames  ( gHC_TYPELITS
                   , typeNatMulTyFamNameKey
                   , typeNatExpTyFamNameKey
                   , typeNatLeqTyFamNameKey
+                  , typeNatSubTyFamNameKey
                   )
 import FamInst    ( TcBuiltInSynFamily(..) )
 import FastString ( FastString, fsLit )
@@ -39,6 +40,7 @@ typeNatTyCons =
   , typeNatMulTyCon
   , typeNatExpTyCon
   , typeNatLeqTyCon
+  , typeNatSubTyCon
   ]
 
 typeNatAddTyCon :: TyCon
@@ -52,6 +54,17 @@ typeNatAddTyCon = mkTypeNatFunTyCon2 name
   name = mkWiredInTyConName UserSyntax gHC_TYPELITS (fsLit "+")
             typeNatAddTyFamNameKey typeNatAddTyCon
 
+typeNatSubTyCon :: TyCon
+typeNatSubTyCon = mkTypeNatFunTyCon2 name
+  TcBuiltInSynFamily
+    { sfMatchFam      = matchFamSub
+    , sfInteractTop   = interactTopSub
+    , sfInteractInert = interactInertSub
+    }
+  where
+  name = mkWiredInTyConName UserSyntax gHC_TYPELITS (fsLit "-")
+            typeNatSubTyFamNameKey typeNatSubTyCon
+
 typeNatMulTyCon :: TyCon
 typeNatMulTyCon = mkTypeNatFunTyCon2 name
   TcBuiltInSynFamily
@@ -127,22 +140,28 @@ axAddDef
   , axExp1R
   , axLeqRefl
   , 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)
+
+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
@@ -170,6 +189,7 @@ typeNatCoAxiomRules = Map.fromList $ map (\x -> (coaxrName x, x))
   , axExp1R
   , axLeqRefl
   , axLeq0L
+  , axSubDef
   ]
 
 
@@ -181,6 +201,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]
 
@@ -221,7 +244,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,7 +255,8 @@ 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
     }
 
@@ -264,6 +288,15 @@ matchFamAdd [s,t]
         mbY = isNumLitTy t
 matchFamAdd _ = Nothing
 
+matchFamSub :: [Type] -> Maybe (TcCoercion, TcType)
+matchFamSub [s,t]
+  | Just 0 <- mbY = Just (mkTcAxiomRuleCo axSub0R [s] [], s)
+  | Just x <- mbX, Just y <- mbY, Just z <- minus x y =
+    Just (mkTcAxiomRuleCo axSubDef [s,t] [], num z)
+  where mbX = isNumLitTy s
+        mbY = isNumLitTy t
+matchFamSub _ = Nothing
+
 matchFamMul :: [Xi] -> Maybe (TcCoercion, Xi)
 matchFamMul [s,t]
   | Just 0 <- mbX = Just (mkTcAxiomRuleCo axMul0L [t] [], num 0)
@@ -312,6 +345,16 @@ interactTopAdd [s,t] r
   mbZ = isNumLitTy r
 interactTopAdd _ _ = []
 
+interactTopSub :: [Xi] -> Xi -> [Pair Type]
+interactTopSub [s,t] r
+  | Just 0 <- mbZ = [ s === t ]
+  | otherwise     = [ t .+. r === s ]
+  where
+  mbZ = isNumLitTy r
+interactTopSub _ _ = []
+
+
+
 interactTopMul :: [Xi] -> Xi -> [Pair Type]
 interactTopMul [s,t] r
   | Just 1 <- mbZ = [ s === num 1, t === num 1 ]
@@ -355,6 +398,13 @@ interactInertAdd [x1,y1] z1 [x2,y2] z2
   where sameZ = eqType z1 z2
 interactInertAdd _ _ _ _ = []
 
+{- XXX: Should we add some rules here?
+When `interactTopSub` sees `x - y ~ z`, it generates `z + y ~ x`.
+Hopefully, this should interact further and generate all additional
+needed facts that we might need. -}
+interactInertSub :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type]
+interactInertSub _ _ _ _ = []
+
 interactInertMul :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type]
 interactInertMul [x1,y1] z1 [x2,y2] z2
   | sameZ && known (/= 0) x1 && eqType x1 x2 = [ y1 === y2 ]