`KnownNat` does not imply `Typeable` any more when used with plugin
I have the following Haskell code which uses ghctypelitsknownnat0.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 :: ghcprim0.5.2.0:GHC.Types.Nat).
(Typeable n, KnownNat n) =>
Proxy n > ()
at src/Nats.hs:13:157
• 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 GHC8.2.2 and GHC8.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 ghctypelitsknownnat
package:
ghctypelitsknownnat
package correctly infers KnownNat (n + 1)
constraint so GHC should be able to infer Typeable (n + 1)
.
Trac metadata
Trac field  Value 

Version  8.4.3 
Type  Bug 
TypeOfFailure  OtherFailure 
Priority  normal 
Resolution  Unresolved 
Component  Compiler 
Test case  
Differential revisions  
BlockedBy  
Related  
Blocking  
CC  
Operating system  
Architecture 
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information