Re: [GHC] #9858: Typeable instance for datatype and its promoted constructor is the same

19 Jan 2015

      #9858: Typeable instance for datatype and its promoted constructor is the same
-------------------------------------+-------------------------------------
        Reporter:  dreixel           |                   Owner:  dreixel
            Type:  bug               |                  Status:  new
        Priority:  high              |               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):

 Replying to [comment:14 simonpj]:
...
Pedro: how do you suggest we proceed with this?  It seems quite urgent
 if you can use it to write `unsafeCoerce`.
Simon
If I may comment too, I think the ''long-term'' solution for these bugs
 cannot be anything less than including kind information in typereps, at
 least for type constructors of polymorphic kind.

 However that may be too hard to get done in the short term, in which case
 one possibility might be to somehow disallow `PolyKinds`, or possibly
 `Typeable` instances for polykinds, in Safe Haskell.  Note that exploiting
 this doesn't require any explicit extensions mentioning kinds, `Typeable`
 or deriving, this was my last version (works in GHCi 7.8.3):
 {{{
 {-# LANGUAGE TypeFamilies #-}

 import Data.Typeable

 type E = (:~:)

 data family F p a b

 newtype instance F a b (Proxy (Proxy :: * -> *)) = ID (a -> a)
 newtype instance F a b (Proxy (Proxy :: (* -> *) -> *)) = UC (a -> b)

 -- Needed to prevent faulty inlining in GHCi.  Maybe expand further if it
 -- breaks at higher optimization levels.
 munge = id

 ecast :: E p q -> f p -> f q
 ecast Refl = id

 supercast ::
        F a b (Proxy (Proxy :: * -> *))
     -> F a b (Proxy (Proxy :: (* -> *) -> *))
 supercast = case cast e of
     Just e' -> munge ecast e'
   where
     e = Refl
     e :: E (Proxy (Proxy :: * -> *)) (Proxy (Proxy :: * -> *))

 uc :: a -> b
 uc = case supercast (ID id) of UC f -> f
 }}}

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