#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
_______________________________________________
Glasgow-haskell-bugs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
