[GHC] #13201: Type-level naturals aren't instantiate with GHCi debugger

28 Jan 2017

      #13201: Type-level naturals aren't instantiate with GHCi debugger
-------------------------------------+-------------------------------------
           Reporter:  konn           |             Owner:
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.0.2
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 GHCi debugger cannot use the information of specific value type-level
 natural number, even if it is explicitly specified.

 For example, consider the following code:

 {{{#!hs
 {-# LANGUAGE DataKinds, KindSignatures, StandaloneDeriving, TypeOperators
 #-}
 module Main where
 import GHC.TypeLits

 data Foo (n :: Nat) = Foo
 deriving instance KnownNat n => Show (Foo n)

 fooSucc :: Foo n -> Foo (n + 1)
 fooSucc Foo = Foo

 foos :: Foo n -> [Foo (n + 1)]
 foos f = loop 5
   where
     loop 0 = []
     loop n = fooSucc f : loop (n - 1)

 main :: IO ()
 main = print $ foos (Foo :: Foo 5)
 }}}

 Loading it with GHCi Debugger, we cannot `show` the value of `f`, because
 GHCi debugger doesn't know the specific value of `n` (in`Foo n`), even
 though we specify it in `main`!

 {{{#!hs
 ghci> :l tmp.hs
 [1 of 1] Compiling Main             ( tmp.hs, interpreted )
 Ok, modules loaded: Main.

 ghci> :break foos
 Breakpoint 0 activated at tmp.hs:13:10-15

 ghci> :set stop :list
 ghci> main
 Stopped in Main.foos, tmp.hs:13:10-15
 _result :: [Foo (n + 1)] = _
 loop :: (Num t, Eq t) => t -> [Foo (n + 1)] = _
 12  foos :: Foo n -> [Foo (n + 1)]
 13  foos f = loop 5
 14    where

 ghci> :step
 Stopped in Main.foos.loop, tmp.hs:16:14-37
 _result :: [Foo (n + 1)] = _
 f :: Foo n = _
 n :: Integer = 5
 15      loop 0 = []
 16      loop n = fooSucc f : loop (n - 1)
 17

 ghci> :t f
 f :: Foo n

 ghci> f

 <interactive>:8:1: error:
     • No instance for (KnownNat n) arising from a use of ‘print’
     • In a stmt of an interactive GHCi command: print it
 }}}

 Of course, we can inspect the internal representation via `:print` or
 `:force` command, but it is rather impractical when we cannot easily read
 its pretty form from its internal representation .

 I tested this with GHC 7.0.1 and 7.0.2.

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