id,summary,reporter,owner,description,type,status,priority,milestone,component,version,resolution,keywords,cc,os,architecture,failure,testcase,blockedby,blocking,related,differential
5277,Clash between RankNTypes and TypeFamilies,stefan,,"[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
}}}",bug,closed,normal,,Compiler,7.0.3,invalid,"rank-n types, type families, type signatures",simonpj@… dimitris@… stefan@…,Unknown/Multiple,Unknown/Multiple,GHC rejects valid program,,,,,