Could not deduce KnownNat n from the context: 4 ~ (1 + n)

[sheaf]

I don't know if this is expected, but I would hope for the plugin to be able to deduce n ~ 3 from 4 ~ (1+n), and thus be able to satisfy a KnownNat n constraint.

For a simple test case, using GHC 8.6, ghc-typelits-knownnat 0.6 and ghc-typelits-natnormalise 0.6.2:

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

{-# LANGUAGE DataKinds, GADTs, TypeOperators #-}

import GHC.TypeNats
  ( Nat, KnownNat, type (+), natVal )
import Numeric.Natural
  ( Natural )

unknown :: ( 4 ~ (1+n) ) => proxy n -> Natural
unknown = natVal

src\knownnattest.hs:12:11: error:
    • Could not deduce (KnownNat n) arising from a use of ‘natVal’
      from the context: 4 ~ (1 + n)
        bound by the type signature for:
                   unknown :: forall (n :: Nat) (proxy :: Nat -> Type).
                              (4 ~ (1 + n)) =>
                              proxy n -> Natural
        at src\knownnattest.hs:11:1-46
      Possible fix:
        add (KnownNat n) to the context of
          the type signature for:
            unknown :: forall (n :: Nat) (proxy :: Nat -> Type).
                       (4 ~ (1 + n)) =>
                       proxy n -> Natural
    • In the expression: natVal
      In an equation for ‘unknown’: unknown = natVal
   |
12 | unknown = natVal
   |           ^^^^^^

[sheaf]

Oops, realised this is a duplicate of #13. Apologies.