[GHC] #7259: Eta expansion of products in System FC

[GHC]

#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