I have the following Haskell code which uses ghc-typelits-knownnat-0.5 package as a plugin:

{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators       #-}

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

module Nats where

import Data.Proxy (Proxy (..))
import Data.Typeable (Typeable)
import GHC.TypeLits (KnownNat, type (+))

f :: forall n . (Typeable n, KnownNat n) => Proxy n -> ()
f _ = ()
f _ = f (Proxy :: Proxy (n + 1))

When I try to compile this code I observe the following error message:

    • Could not deduce (Typeable (n + 1)) arising from a use of ‘f’
      from the context: (Typeable n, KnownNat n)
        bound by the type signature for:
                   f :: forall (n :: ghc-prim-0.5.2.0:GHC.Types.Nat).
                        (Typeable n, KnownNat n) =>
                        Proxy n -> ()
        at src/Nats.hs:13:1-57
    • In the expression: f (Proxy :: Proxy (n + 1))
      In an equation for ‘f’: f _ = f (Proxy :: Proxy (n + 1))
   |
15 | f _ = f (Proxy :: Proxy (n + 1))
   |       ^^^^^^^^^^^^^^^^^^^^^^^^^^

This code works for both GHC-8.2.2 and GHC-8.0.2. I found similar ticket with exactly this problem but looks like this is broken again: #10348 (closed) (bug).

Originally reported at Github for ghc-typelits-knownnat package:

• https://github.com/clash-lang/ghc-typelits-knownnat/issues/21

ghc-typelits-knownnat package correctly infers KnownNat (n + 1) constraint so GHC should be able to infer Typeable (n + 1).