Could not deduce (Typeable (n + 1)) with GHC-8.4.3

[chshersh]

I'm using ghc-typelits-knownnat-0.5. And I have the following code:

{-# 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 _ (_:xs) = f (Proxy :: Proxy (n + 1)) xs

This code produces the following error when compiling with GHC-8.4.3:

    • 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-65
    • In the expression: f (Proxy :: Proxy (n + 1)) xs
      In an equation for ‘f’:
          f _ (_ : xs) = f (Proxy :: Proxy (n + 1)) xs
   |
15 | f _ (_:xs) = f (Proxy :: Proxy (n + 1)) xs
   |              ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

However, it compiles and works completely okay with GHC-8.2.2 and GHC-8.0.2. What should I do to make this code work with latest GHC version?

[christiaanb]

This seems more of a GHC issue than a ghc-typelits-knownnat issue, because for both GHC 8.2 and GHC 8.4 ghc-typelits-knownnat solves the KnownNat (n+1) constraint from the KnownNat n constraint. The difference seems to be that in GHC 8.2 and earlier, GHC used the KnownNat (n+1) constraint solved by ghc-typelits-knownnat to solve the Typeable (n+1) constraint, whereas in GHC 8.4 no longer does this.

[chshersh]

@christiaanb Thanks for quick response! I discovered that there already was similar GHC issue but it's fixed:

• https://ghc.haskell.org/trac/ghc/ticket/10348

Looks like it become broken again... I will open new issue in GHC.

UPDATE: Here is the issue:

• https://ghc.haskell.org/trac/ghc/ticket/15322