[GHC] #12670: Representation polymorphism validity check is too strict

[GHC]

#12670: Representation polymorphism validity check is too strict
-------------------------------------+-------------------------------------
        Reporter:  bgamari           |                Owner:
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:  8.2.1
       Component:  Compiler (Type    |              Version:  8.0.1
  checker)                           |
      Resolution:                    |             Keywords:  typeable
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by bgamari):

 > Are you stuck on this?

 To an extent, yes I was. The problem is that I cannot really use the
 `TRFun` that we introduced if I define it as,
 {{{#!hs
 data TypeRep (a :: k) where
     TRFun :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep) (arg :: TYPE r1)
 (res :: TYPE r2).
              TypeRep arg -> TypeRep res -> TypeRep (arg -> res)
     ...
 }}}

 due to the overly strict representational polymorphism checks described in
 this ticket.

 I thought would workaround would be to even further narrow the types
 represented by `TypeRep`. Namely, we only represent arrow types where both
 `arg` and `res` are of kind `Type`,
 {{{#!hs
 data TypeRep (a :: k) where
     TRFun :: forall arg res. TypeRep arg -> TypeRep res -> TypeRep (arg ->
 res)
     ...
 }}}

 However, this leads to trouble when implementing serialization,
 {{{#!hs
 putTypeRep :: TypeRep a -> Put
 putTypeRep (TRCon a b c)   = putWord8 0 >> ...
 putTypeRep (TRApp a b c)   = putWord8 1 >> ...
 putTypeRep (TRFun arg res) = putWord8 2 >> putTypeRep arg >> putTypeRep
 res
 ...

 getSomeTypeRep :: Get SomeTypeRep
 getSomeTypeRep = do
     tag <- getWord8
     case tag of
       0 -> ...
       1 -> ...
       2 -> do arg <- getSomeTypeRep
               res <- getSomeTypeRep
               {- uh oh! We don't know the kinds of arg and res -}
               return (TRFun arg res)
 }}}

 The trouble here is that, since we have dropped `typeRepKind`, we have no
 way of verifying during deserialization that `arg` and `res` indeed have
 kind `Type`.

 However, it sounds like `wip/T12819` should unstick me; if I'm not
 mistaken none of this should be problematic assuming we are able to
 represent arrows with arbitrary argument and result kinds.

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