#9858: Typeable instances should be kind-aware -------------------------------------+------------------------------------- Reporter: dreixel | Owner: Type: bug | Status: merge Priority: highest | Milestone: 7.10.2 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: | typecheck/should_fail/T9858a, | should_run/T9858b | Blocking: | Differential Revisions: Phab:D652 -------------------------------------+------------------------------------- Comment (by ekmett): Rather than just say it is sad, let's see if we can tackle this issue head on. A while back, Simon, you posed a sketch of an idea of how to remove the superkinding / existing type hacks by adding another very simple level we can quantify over. It could be adapted to address this situation. Consider a type checker where we've removed `*`, `Constraint` and `#` and made a single unified kind `Sort a b` where `a` and `b` are allowed to range over a binary alphabet, lets consider `{T,F}` as that alphabet. [*] Then {{{ * = Sort T T Constraint = Sort T F # = Sort F T }}} and we can talk about the kinds of existing types: {{{ () :: forall a. Sort T a }}} lets `()` work as both a `Constraint` or `*`. {{{ (,) :: forall a. Sort T a -> Sort T a -> Sort T a }}} lets us tuple up anything as long as both are *'s or both are Constraints. Unboxed tuples fit: {{{ (#,#) :: forall a b. Sort a T -> Sort a T -> Sort F T }}} lets unboxed tuples carry `*`'s and `#`'s. and the existing function overloads fit: {{{ (->) :: forall a b. Sort a T -> Sort b T -> Sort T T }}} All of this then works without the typechecker ever internally lying to itself which then solves this issue in a principled way, as the Typeable instance can know the full choice of kind without subversion. This removes all of the hacks where `(->) :: * -> * -> *` but `a -> b` might have `a` and `b` have kinds other than `*`, etc. in the typechecker, and lets us talk about `(->) Int#`, or `(,) (Eq Int)` which are both types we currently can't write: {{{ ghci> :k (->) Int# <interactive>:1:6: Expecting a lifted type, but ‘Int#’ is unlifted In a type in a GHCi command: (->) Int# }}} I already have to work around the lack of the latter by constructing my own product for constraints. {{{ class (p,q) => p & q instance (p,q) => p & q }}} Now I can talk about `(&) (Eq Int) :: Constraint -> Constraint`, but there is no corresponding partial application trick for `(->)`. We've already implemented a related trick in Ermine without appreciable impact, our kinds there are a little different, so the details vary a bit. [*] To prevent weird quantifier abuse, you may want to require each of the arguments of Sort to have different ranges, otherwise `Sort a a` becomes weird. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9858#comment:89 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler