Type-level naturals aren't instantiated with GHCi debugger

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:

{-# 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 (inFoo n), even though we specify it in main!

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.

Trac metadata

Trac field	Value
Version	8.0.2
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture