Use type-substituted [G]iven KnownNats

This means that:

> (KnownNat n, n ~ (m+1)) ~ KnownNat m

However, this does need the `ghc-typlits-natnormalise` plugin,
as this pluging creates the following contraints:

> (KnownNat n, n ~ (m+1), KnownNat m ~ KnownNat (n-1), 1 <= n)

And only `ghc-typelits-natnormalise` knows that `n ~ m + 1`
implies `1 <= n`.

This partially solves #13, as it still doesn't find the fixpoint
of all possible substitutions. This will be in a follow-up
patch.

src/GHC/TypeLits/KnownNat/Solver.hs

@@ -121,9 +121,10 @@ import TcRnTypes  (Ct, TcPlugin(..), TcPluginResult (..), ctEvidence, ctEvLoc,
                    ctEvPred, ctEvTerm, ctLoc, ctLocSpan, isWanted,
                    mkNonCanonical, setCtLoc, setCtLocSpan)
 import TcTypeNats (typeNatAddTyCon, typeNatSubTyCon)
-import Type       (PredTree (ClassPred), PredType, classifyPredType, dropForAlls,
-                   funResultTy, mkNumLitTy, mkStrLitTy, mkTyConApp, piResultTys,
-                   splitFunTys, splitTyConApp_maybe, tyConAppTyCon_maybe)
+import Type
+  (EqRel (NomEq), PredTree (ClassPred,EqPred), PredType, classifyPredType,
+   dropForAlls, funResultTy, mkNumLitTy, mkStrLitTy, mkTyConApp, piResultTys,
+   splitFunTys, splitTyConApp_maybe, tyConAppTyCon_maybe)
 import TyCon      (tyConName)
 import TyCoRep    (Type (..), TyLit (..))
 import Var        (DFunId)
@@ -371,17 +372,29 @@ constraintToEvTerm defs givens (ct,cls,op) = do
     -- the two are a constant offset apart.
     offset :: Type -> TcPluginM (Maybe (EvTerm,[Ct]))
     offset want = runMaybeT $ do
-      let unKn ty' = case classifyPredType ty' of
+      let -- Get the knownnat contraints
+          unKn ty' = case classifyPredType ty' of
                        ClassPred cls' [ty'']
                          | className cls' == knownNatClassName
                          -> Just ty''
                        _ -> Nothing
+          -- Get the rewrites
+          unEq ty' = case classifyPredType ty' of
+                       EqPred NomEq ty1 ty2 -> Just (ty1,ty2)
+                       _ -> Nothing
+          rewrites = mapMaybe (unEq . unCType . fst) givens
+          -- Rewrite
+          rewriteTy tyK (ty1,ty2) | CType ty1 == CType tyK = Just ty2
+                                  | CType ty2 == CType tyK = Just ty1
+                                  | otherwise              = Nothing
           -- Get only the [G]iven KnownNat constraints
           knowns   = mapMaybe (unKn . unCType . fst) givens
+          -- Get all the rewritten KNs
+          knownsR  = catMaybes $ concatMap (\t -> map (rewriteTy t) rewrites) knowns
           -- pair up the sum-of-products KnownNat constraints
           -- with the original Nat operation
           subWant  = mkTyConApp typeNatSubTyCon . (:[want])
-          exploded = map (normaliseNat . subWant &&& id) knowns
+          exploded = map (normaliseNat . subWant &&& id) (knowns ++ knownsR)
           -- interesting cases for us are those where
           -- wanted and given only differ by a constant
           examineDiff (S [P [I n]]) entire = Just (entire,I n)

tests/Main.hs

@@ -143,6 +143,9 @@ test22 _ _ = natVal (Proxy :: Proxy (y*x*y))
 test23 :: SNat addrSize -> SNat ((addrSize + 1) - (addrSize - 1))
 test23 SNat = SNat
 
+test24 :: (KnownNat n, n ~ (m+1)) => proxy m -> Integer
+test24 = natVal
+
 tests :: TestTree
 tests = testGroup "ghc-typelits-natnormalise"
   [ testGroup "Basic functionality"
@@ -228,6 +231,10 @@ tests = testGroup "ghc-typelits-natnormalise"
     , testCase "SNat ((addrSize + 1) - (addrSize - 1)) = SNat 2" $
       show (test23 (SNat @ 8)) @?=
       "2"
+    , testCase "(KnownNat n, n ~ m + 1) ~ KnownNat m" $
+      show (test24 (Proxy @4)) @?=
+      "4"
+
     ],
     testGroup "QuickCheck"
     [ testProperty "addT = (+)" $ (\a b -> (a >= 0 && b >= 0) ==> (addT a b === a + b)),