[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):

 To put a finer point on the concern I raised in comment:11:

 Consider this example,
 {{{#!hs
 data TypeRep (a :: k)

 pattern Fun :: forall k k' (a :: k) (b :: k').
                a -> b -> TypeRep (a -> b)

 -- As seen in "A reflection on types"
 data Dynamic where
     Dyn :: TypeRep a -> a -> Dynamic

 dynApply :: Dynamic -> Dynamic -> Maybe Dynamic
 dynApply (Dyn rf f) (Dyn rx x) = do
     Fun arg res <- pure rx
     Just HRefl <- eqTypeRep arg rx

     -- We now know that the argument types match up but what about the
     -- result type?
     --
     -- In order to package up the result (f x) into a `Dyn` we must
     -- know that the its type is of kind *. However, we don't know
     -- this since TypeRep's index is poly-kinded.
     --
     -- Consequently we really need to do this, which requires typeRepKind,
     Just HRefl <- eqTypeRep (typeRepKind res) (typeRep @Type)

     pure $ Dyn res (f x)


 -- Consider this example...
 f :: Int -> Int#
 f (I# n#) = n#

 df :: Dynamic
 df = Dyn f

 -- Here is an example of a use of Dynamic that would expose the issue in
 dynApply
 uhOh :: Maybe Dynamic
 uhOh = dynApply df (Dynamic (42::Int))
 }}}

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