[GHC] #5277: Clash between RankNTypes and TypeFamilies

[GHC]

#5277: Clash between RankNTypes and TypeFamilies
---------------------------------+------------------------------------------
    Reporter:  stefan            |       Owner:                                              
        Type:  bug               |      Status:  new                                         
    Priority:  normal            |   Component:  Compiler                                    
     Version:  7.0.3             |    Keywords:  rank-n types, type families, type signatures
    Testcase:                    |   Blockedby:                                              
          Os:  Unknown/Multiple  |    Blocking:                                              
Architecture:  Unknown/Multiple  |     Failure:  GHC rejects valid program                   
---------------------------------+------------------------------------------
 [Note: a more specific summary line is in order for this ticket.]

 Consider the following program:

 {{{
 {-# LANGUAGE RankNTypes   #-}
 {-# LANGUAGE TypeFamilies #-}

 type family F a b  ::  *
 data W a b         =   W {unW :: F a b}
 data T a           =   T {unT :: forall b. W a b}

 -- f               ::  T a -> F a b
 f                  =   unW . unT
 }}}

 It type checks fine and querying the inferred type for f interactively
 yields the expected type. However, adding a type signature for f,

 {{{
 f  ::  T a -> F a b
 f  =   unW . unT
 }}}

 results in a typing error:

 {{{
 Couldn't match type `F a b0' with `F a b'
 NB: `F' is a type function, and may not be injective
 Expected type: W a b0 -> F a b
   Actual type: W a b0 -> F a b0
 In the first argument of `(.)', namely `unW'
 In the expression: unW . unT
 }}}

-- 
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/5277>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler