#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