From bf15057ac7bedc089ed650684d65c427cb599e68 Mon Sep 17 00:00:00 2001
From: M Farkas-Dyck <strake888@gmail.com>
Date: Fri, 17 Aug 2018 23:48:04 -0800
Subject: [PATCH 1/2] solve more inequalities involving exponentiation

---
 src/GHC/TypeLits/Normalise/Unify.hs | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

diff --git a/src/GHC/TypeLits/Normalise/Unify.hs b/src/GHC/TypeLits/Normalise/Unify.hs
index 84d71a0..aa82355 100644
--- a/src/GHC/TypeLits/Normalise/Unify.hs
+++ b/src/GHC/TypeLits/Normalise/Unify.hs
@@ -624,6 +624,7 @@ ineqRules =
   , pow2MonotoneSpecial
   , haveSmaller
   , haveBigger
+  , powMisc
   ]
 
 -- | Transitivity of inequality
@@ -874,3 +875,16 @@ facSymbol n (E s p)
   | Just s' <- facSOP n s
   = Just (mergeSOPMul s' (S [p]))
 facSymbol _ _ = Nothing
+
+powMisc :: IneqRule
+  -- want: a <= b^p
+  -- have: x <= y
+  -- new want: want
+  -- new have: b^x <= b^y
+powMisc want@(_,S [P [E b p]],_) (S [x],S [y],le)
+  | p == y = [(want, (S [P [E b x]], S [P [E b y]], le))]
+  -- want: x <= b^x
+  -- new want: 2 <= b
+powMisc (S [P [x]],S [P [E b (P [y])]],le) have
+  | x == y = [((S [P [I 2]],b,le),have)]
+powMisc _ _ = []

From a089625d3f69215583ac3d0a5a48d9bae840bc22 Mon Sep 17 00:00:00 2001
From: M Farkas-Dyck <strake888@gmail.com>
Date: Sun, 19 Aug 2018 07:08:45 -0800
Subject: [PATCH 2/2] test `powMisc`

---
 tests/Tests.hs | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

diff --git a/tests/Tests.hs b/tests/Tests.hs
index 036416a..39db767 100644
--- a/tests/Tests.hs
+++ b/tests/Tests.hs
@@ -1,5 +1,6 @@
 {-# LANGUAGE CPP                 #-}
 {-# LANGUAGE DataKinds           #-}
+{-# LANGUAGE ConstraintKinds     #-}
 {-# LANGUAGE GADTs               #-}
 {-# LANGUAGE KindSignatures      #-}
 {-# LANGUAGE TypeOperators       #-}
@@ -7,6 +8,8 @@
 {-# LANGUAGE Rank2Types          #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications    #-}
+{-# LANGUAGE StandaloneDeriving  #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}
 
 #if __GLASGOW_HASKELL__ >= 805
 {-# LANGUAGE NoStarIsType #-}
@@ -365,6 +368,17 @@ proxyInEqImplication2
   -> Proxy n
 proxyInEqImplication2 _ _ _ x = x
 
+proxyInEqImplication3 :: forall b n . (2 <= b) :- (n <= b^n)
+proxyInEqImplication3 = Sub Dict
+
+proxyInEqImplication4 :: (a <= b^p, x <= y) :- (b^x <= b^y)
+proxyInEqImplication4 = Sub Dict
+
+data Dict a where Dict :: a => Dict a
+newtype a :- b = Sub (a => Dict b)
+deriving instance Show (Dict a)
+instance Show (a :- b) where show _ = "Sub Dict"
+
 data AtMost n = forall a. (KnownNat a, a <= n) => AtMost (Proxy a)
 
 instance Show (AtMost n) where
@@ -461,6 +475,10 @@ tests = testGroup "ghc-typelits-natnormalise"
     , testCase "1 <= 2^(a+3)" $
       show (proxyInEq7 (Proxy :: Proxy 1) (Proxy :: Proxy 8)) @?=
       "()"
+    , testCase "`2 <= b` implies `x <= b^x`" $
+      show (proxyInEqImplication3) @?= "Sub Dict"
+    , testCase "`x <= y` implies `b^x <= b^y`" $
+      show (proxyInEqImplication4) @?= "Sub Dict"
     ]
   , testGroup "errors"
     [ testCase "x + 2 ~ 3 + x" $ testProxy1 `throws` testProxy1Errors