id summary reporter owner description type status priority milestone component version resolution keywords cc os architecture failure testcase blockedby blocking related differential wikipage
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