#7259: Eta expansion of products in System FC ---------------------------------+------------------------------------------ Reporter: simonpj | Owner: simonpj Type: bug | Status: new Priority: normal | Milestone: 7.8.1 Component: Compiler | Version: 7.6.1 Keywords: | Os: Unknown/Multiple Architecture: Unknown/Multiple | Failure: None/Unknown Difficulty: Unknown | Testcase: Blockedby: | Blocking: Related: | ---------------------------------+------------------------------------------ Comment(by simonpj): Just by way of concrete example, here's the smallest example Edward wants to do: {{{ {-# LANGUAGE PolyKinds, DataKinds, GADTs #-} import Prelude hiding (id, (.)) class Category (k :: x -> x -> *) where id :: k a a (.) :: k b c -> k a b -> k a c data P :: (x -> x -> *) -> (y -> y -> *) -> (x,y) -> (x,y) -> * where P :: m a b -> n c d -> P m n '(a,c) '(b,d) instance (Category m, Category n) => Category (P m n) where -- id = P id id P lf rf . P lg rg = P (lf . lg) (rf . rg) }}} The addition of id there causes it to fail to typecheck, because refining the kind to `(x,y)` doesn't let it know all types have the form `'(a,b)`. It can't because `Any` still exists as a distinguishable member of every kind, so such a refinement would (currently) be unsound. When we try to build indexed monad transformers we wind up wanting to take product over their indices. Similar issues arise when trying to compute with collages of profunctors and other nifty theoretical toys that have proven quite useful in the `lens` package. -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/7259#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler