[GHC] #15322: `KnownNat` does not imply `Typeable` any more when used with plugin

29 Jun 2018

      #15322: `KnownNat` does not imply `Typeable` any more when used with plugin
-------------------------------------+-------------------------------------
           Reporter:  chshersh       |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:  8.6.1
          Component:  Compiler       |           Version:  8.4.3
           Keywords:                 |  Operating System:  Unknown/Multiple
  typeable,knownnat                  |
       Architecture:                 |   Type of failure:  GHC rejects
  Unknown/Multiple                   |  valid program
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:  #10348
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 I have the following Haskell code which uses `ghc-typelits-knownnat-0.5`
 package as a plugin:

 {{{#!hs
 {-# 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
 (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)`.

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15322
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler