[GHC] #8778: Typeable TypeNats

[GHC]

#8778: Typeable TypeNats
--------------------------------------------+------------------------------
        Reporter:  dmcclean                 |            Owner:
            Type:  feature request          |           Status:  new
        Priority:  normal                   |        Milestone:  ⊥
       Component:  Compiler (Type checker)  |          Version:
      Resolution:                           |         Keywords:
Operating System:  Unknown/Multiple         |     Architecture:
 Type of failure:  None/Unknown             |  Unknown/Multiple
       Test Case:                           |       Difficulty:  Unknown
        Blocking:                           |       Blocked By:
                                            |  Related Tickets:  4385
--------------------------------------------+------------------------------

Comment (by dmcclean):

 Sorry about that, thoughtpolice, I was thinking the field was for where I
 saw it.

 Example (also attached, but here for discussion):

 {{{
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE AutoDeriveTypeable #-}

 module Test8778 where

 import GHC.TypeLits
 import Data.Dynamic

 data Phantom (n :: Nat) = Phantom

 desirable = toDyn (Phantom :: Phantom 3)
 }}}

 Results in:

 {{{
     No instance for (Typeable 3) arising from a use of `toDyn'
     In the expression: toDyn (Phantom :: Phantom 3)
     In an equation for `desirable':
         desirable = toDyn (Phantom :: Phantom 3)
 Failed, modules loaded: none.
 }}}

 This is unfortunate because it means that you can't use Data.Dynamic with
 any types that have phantom Nat parameters. Up a couple of levels in the
 abstraction hierarchy, this makes it difficult to build a user interface
 that works well with displaying signals and taking input of arbitrary
 dimensional types (lengths, velocities, currents, and the like).

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8778#comment:4>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler