#11473: Levity polymorphism checks are inadequate -------------------------------------+------------------------------------- Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: highest | Milestone: 8.0.1 Component: Compiler | Version: 7.10.3 Resolution: | Keywords: | LevityPolymorphism, TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by rwbarton): It seems to me the most logical place to put these levity polymorphism checks is in the typing rules for abstraction and application. After all `\(a :: t) -> ...` is really different beasts at runtime depending on whether `t :: * = TYPE L`, or `t :: TYPE UW32`, or `t :: TYPE UW64` etc. We should insist that the rep (the `r` such that `t :: TYPE r`) of `t` be known when type-checking the lambda, and resolve the overloading to `\_L`, or `\_UW32`, or `\_UW64`. In short, treat `\` as ad-hoc polymorphic. Similar comments apply to application. `f x` is really an overloaded `f $_r x`, where the typing rule for `$_r` is {{{ s :: RuntimeRep a :: TYPE r b :: TYPE s f :: a -> b x :: a ------------------------------------------------------------------ f $_r x :: b }}} And this makes sense because later to actually compile an application, we will absolutely need to know the rep of the type of `x`. Then I don't think we need any special rules about the kind of `->`, which can become rep-polymorphic in both arguments. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11473#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler