Derive KnownNat a ~ KnownNat (((a - b) + c) + (b - c)))

[martijnbastiaan]

'normaliseNatEverywhere' would use 'everywhereM' to walk types and
simplify nats anywhere in it. Because 'everywhereM' doesn't
differentiate between type constructors 'normaliseNat' understands
(i.e., -, +, *, ^) it would also run it on every subexpression.
'normaliseNat' would then yield spurious results it wouldn't have,
if only it had seen the bigger picture..

[christiaanb]

LGTM

I think we should file the following as a new issue:

type family F (a :: Nat) (b :: Nat) :: Nat

proxyEq5
  :: forall a b
   . KnownNat (F (a * 3) b * 3)
  => Proxy a
  -> Proxy b
  -> Proxy (3 * F (3 * a) b)
proxyEq5 = theProxy
 where
  theProxy
    :: forall a b
     . KnownNat (F (2 * a + a) b + (2 * F (a + 2 * a) b))
    => Proxy a
    -> Proxy b
    -> Proxy (3 * F (3 * a) b)
  theProxy _ _ = Proxy

as it might be related to http://hackage.haskell.org/package/ghc-tcplugins-extra-0.4/docs/GHC-TcPluginM-Extra.html#v:flattenGivens

Not urgent though

[christiaanb]

Filed as #47