Cannot solve KnownNat n from (KnownNat M, KnownNat (n+M))

[sheaf]

Similar to @kozross's example in #13, but without any equality constraints whatsoever:

{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}

{-# LANGUAGE TypeFamilies, TypeOperators, FlexibleContexts #-}

module T59 where

import GHC.TypeNats
import Data.Proxy

type family F (n :: Nat) :: Nat where

bar :: (KnownNat (F m), KnownNat (n + F m)) => Proxy n -> Proxy m -> Natural
bar n _m = natVal n

* Could not deduce `KnownNat n' arising from a use of `natVal'
      from the context: (KnownNat (F m), KnownNat (n + F m))

Obviously the constraint solving problem is:

• [G] KnownNat (F m)
• [G] KnownNat (n + F m)
• [W] KnownNat n

Same happens with a nullary type family, e.g.:

type family M :: Nat

bar :: (KnownNat M, KnownNat (n + M)) => Proxy n -> Natural
bar n = natVal n

I determined that this was the cause of the failure in clash-lang/ghc-typelits-natnormalise#86 (the type family was Length in that example).