#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