`KnownNat` does not imply `Typeable` any more when used with plugin
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:
ghc-typelits-knownnat
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 |