Re: [GHC] #9858: Typeable instances should be kind-aware

28 Jan 2015

      #9858: Typeable instances should be kind-aware
-------------------------------------+-------------------------------------
        Reporter:  dreixel           |                   Owner:  dreixel
            Type:  bug               |                  Status:  new
        Priority:  highest           |               Milestone:  7.10.1
       Component:  Compiler          |                 Version:  7.9
      Resolution:                    |                Keywords:
Operating System:  Unknown/Multiple  |            Architecture:
 Type of failure:  None/Unknown      |  Unknown/Multiple
      Blocked By:                    |               Test Case:
 Related Tickets:                    |                Blocking:
                                     |  Differential Revisions:
-------------------------------------+-------------------------------------

Comment (by oerjan):

 I see in the wiki page that the idea of putting kind arguments in TypeReps
 is hitting severe type system problems.  I had another idea, which I
 didn't bother to bring up before since [comment:19 goldfire]'s idea looked
 much prettier.  And now that I tried actually writing up a proof of
 concept, it looks even more monstrous :/

 But anyway, here it is, sort of working, but with some obvious drawbacks:

 {{{
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE ScopedTypeVariables #-}

 import Data.Proxy

 newtype TTypeRep a = TT String deriving Show
 newtype KKindRep a = KK String deriving Show

 class Kindable' (a :: k -> *) where
     kindRep :: KKindRep a

 class Kindable' (Proxy :: k -> *) => Typeable' (a :: k) where
     typeRep :: TTypeRep a

 instance Kindable' (Proxy :: * -> *) where
     kindRep = KK "*"

 instance (Kindable' (Proxy :: k1 -> *), Kindable' (Proxy :: k2 -> *)) =>
 Kindable' (Proxy :: (k1 -> k2) -> *) where
     kindRep = KK $ '(' : k1 ++ " -> " ++ k2 ++ ")"
       where
         KK k1 = kindRep :: KKindRep (Proxy :: k1 -> *)
         KK k2 = kindRep :: KKindRep (Proxy :: k2 -> *)

 instance Kindable' (Proxy :: k -> *) => Typeable' (Proxy :: k -> *) where
     typeRep = TT $ "Proxy :: " ++ k
       where
         KK k = kindRep :: KKindRep (Proxy :: (k -> *) -> *)

 main = do
     print (kindRep :: KKindRep (Proxy :: (* -> * -> *) -> *))
     print (typeRep :: TTypeRep (Proxy :: (* -> * -> *) -> *))
     print (kindRep :: KKindRep (Proxy :: ((* -> *) -> *) -> *))
     print (typeRep :: TTypeRep (Proxy :: ((* -> *) -> *) -> *))

 }}}

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9858#comment:33
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler